[isabelle-dev] Building nightly snapshots

[Christian Urban]

Dear Makarius,

On Thursday, August 23, 2012 at 15:23:49 (+0100), Makarius wrote:
 > On Wed, 22 Aug 2012, Christian Urban wrote:
 > 
 > > I am used to building the nightly snapshots, which in the olden days was 
 > > conveniently done by the build script. Well, times change. ;o)
 > 
 > Just yesterday I've starting thinking if these snapshots still have any 
 > purpose.  Since Admin/components is missing, it is relatively hard to 
 > recover a running system from that tar.gz blob.  It is now so much easier 
 > bootstrap directly from the repository (as explained at the end of 
 > README_REPOSITORY).

I am happy to follow new ways (actually that is what I am
trying to do right now; it just does not work and documentation
is still too scant for self-help). 

In the past I found I had no problem *ever* with bootstraping from 
the nightly snapshot. Therefore it was my preferred way of being 
close to the leading development edge. For me bootstrapping 
included four easy steps: 

  (1) copying etc/settings, etc/components and contrib/* from the 
      current working snapshot
 
  (2) running ./build -m HOL-Nominal HOL 

  (3) get a drink, and
 
  (4) install the new snapshot with ./bin/isabelle install -p /usr/local/bin 

This never failed me and only needed adjustment if components
needed to be upgraded. If that can be improved, I am more than
in favour of it. But see below. :o(

BTW, the above had the additional benefit that I could easily 
switch back and forth between snapshots as they lived
in independent directories (already build).

 > Hard to tell without knowing the interval of changeset ids to look at the 
 > differences.  Downloading todays snapshot (which is Isabelle_23-Aug-2012 
 > 4cd4ef1ef4a4), it seems to work.

OK, enough whining about the good olden days. Here is what
currently happens: It definitely does not work for me. Here 
are pointers if they makes any difference. I am trying to do

  ./bin/isabelle build -v -s -c HOL-Nominal

in order to get up and running (not sure whether this is the
received way). I get

14_Aug: 7476665f3e0f   (works)
20_Aug: 56ec76f769c0   ("RAW" exception)
22_Aug: 3db108d14239   ("RAW" exception)
23_Aug: 4cd4ef1ef4a4   ("RAW" exception)

Following your recommendation I also tried the repository at the 
"moment": 

23_Aug: 1c8c15c30356 ("RAW" exception)

That is the precise output for the latter after cloning
the repository:

$ ./bin/isabelle version
unidentified repository version
$ ./bin/isabelle build -v -s -c HOL-Nominal
Started at Thu 23 Aug 2012 20:45:25 BST (polyml-5.4.1_x86-darwin on Christians-MacBook-Air.local)
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86-darwin"
ML_HOME="/usr/local/src/polyml"
ML_SYSTEM="polyml-5.4.1"
ML_OPTIONS="-H 1000"

Duplicate session "RAW" (file "/usr/local/src/isabelle/src/Pure/ROOT")
Finished at Thu 23 Aug 2012 20:45:27 BST
0:00:02 elapsed time, 0:00:03 cpu time

> There might be also some local configuration that pretends that you have 
> certain source directories more than once, say both via some ROOTS file 
> and as Isabelle components.

I also have the feeling that the problem is more subtle than it
first appears and that somewhere is something that confuses
the building process. Could it be that the -c does not clean as
much as it should? Is there a way to get more diagnostics
than -v provides? I never touched any ROOTS file. I am
just starting with looking at ROOT. ;o) 

Any idea? More information needed?

Christian