[isabelle-dev] Building nightly snapshots

[Makarius]

On Thu, 23 Aug 2012, Christian Urban wrote:

>  (1) copying etc/settings, etc/components and contrib/* from the
>      current working snapshot

Wait, this sounds suspicious.  What is "the current working snapshot"? The 
etc stuff in ISABELLE_HOME needs to match the version, so you should not 
copy anything from one to another.

You probably suffer from a mismatch related to Isabelle/9032f4bdf205, 
where I rearranged etc/components a little, and added ROOTS.

With "isabelle components -l" you should get an overview of available 
components like this:

Available components:
   /home/makarius/isabelle/repos
   /home/makarius/isabelle/repos/src/Tools/Code
   /home/makarius/isabelle/repos/src/Tools/jEdit
   /home/makarius/isabelle/repos/src/Tools/WWW_Find
   /home/makarius/isabelle/repos/src/HOL/Mirabelle
   /home/makarius/isabelle/repos/src/HOL/Mutabelle
   /home/makarius/isabelle/repos/src/HOL/Library/Sum_of_Squares
   /home/makarius/isabelle/repos/src/HOL/Tools/ATP
   /home/makarius/isabelle/repos/src/HOL/Tools/Predicate_Compile
   /home/makarius/isabelle/repos/src/HOL/Tools/SMT
   /home/makarius/isabelle/repos/src/HOL/TPTP
   /home/makarius/isabelle/repos/Admin
   /home/makarius/.isabelle
   /home/makarius/.isabelle/contrib/cvc3-2.4.1
   /home/makarius/.isabelle/contrib/e-1.5
   /home/makarius/.isabelle/contrib/jdk-7u6
   /home/makarius/.isabelle/contrib/jedit_build-20120813
   /home/makarius/.isabelle/contrib/kodkodi-1.2.16
   /home/makarius/.isabelle/contrib/scala-2.9.2
   /home/makarius/.isabelle/contrib/spass-3.8ds
   /home/makarius/.isabelle/contrib/z3-4.0
   /home/makarius/isabelle/afp-devel

Make sure that you don't have duplicates, and don't have the object-logic 
source directories as components, as was done in the past.


> $ ./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"

You can shorten your time for drinks with leading-edge Poly/ML 5.5.0-pre 
from the SVN, e.g. 1569.  It is very good at managing the heap, although I 
can't say how it works out on weak hardware ike the MacBook Air.

In any case, David Matthews is interested on any kind of feedback in these 
weeks before his next release.


 	Makarius