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
> Loading theory "Pure"
> *** Uninitialized theory data "Isar/attributes"
> *** At command "lemma" (line 18 of
I wonder how you even got that far. Did you change anything in the Pure
sources (and startup scripts)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and