Re: [isabelle] (no subject)



On Mon, 27 Nov 2006, Priya Gopalan wrote:

> I am compiling Isabelle using a flavour of ML called alice. While 
> loading the ROOT.ML file (src/Pure/ROOT.ML) at the alice ML shell-level, 
> it interprets most of it fine, and gets stuck at the point when the 
> following is invoked:
> 
> use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;

Building Isabelle requires an incremental compiler, where new code can be 
processed at runtime.  Both sml/nj and Poly/ML support this, but many more 
recent ML implementations don't -- I am unsure about Alice ML.

Basically Pure is a plain static compile until the very end, where 
theories "Pure" and "CPure" are loaded.  You should still be able to get 
past this point, but the real trouble will start when object-logics are 
bootstrapped.  (It might be better to try FOL first before attempting 
HOL.)


> Loading theory "Pure"
> *** Uninitialized theory data "Isar/attributes"
> *** At command "lemma" (line 18 of
> "~/Priya/Work/IsabelleTest/Isabelle2005/src/Pure/Pure.thy")

I wonder how you even got that far.  Did you change anything in the Pure 
sources (and startup scripts)?


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.