Re: [isabelle] building HOL



On Tue, 10 Nov 2009, Gergely Buday wrote:

I've tried to build Pure and HOL with

./build HOL

but got the following with the new Poly/ML 5.3:

val share_common_data = fn : unit -> unit
Error- in 'ML-Systems/polyml.ML', line 56.
Type error in function application.
  Function: PolyML.Compiler.CPErrorMessageProc :
     (
     {hard: bool, context: pretty option, message: pretty, location: location}
     -> unit) -> Compiler.compilerParameters
  Argument: (put o message) : string * bool * int -> unit
  Reason:
     Can't unify
     {hard: bool, context: pretty option, message: pretty, location: location}
     to string * bool * int (Different number of fields)
Found near
 [
    PolyML.Compiler.CPOutStream put,
    PolyML.Compiler.CPLineNo (fn () => ... ...),
    PolyML.Compiler.CPErrorMessageProc (put o message),
    PolyML.Compiler.CPNameSpace name_space
    ]

What can I do to make it compile? Should I contact the Poly/ML list about this?

Poly/ML 5.3 has just been released, and I am still in the process of fine-tuning the setup for the *next* Isabelle release (which will come in a few weeks).

Normally, we never backport the ML system compatibility layer to older Isabelle versions, since there is hardly a real reasons other than having always the "lastest" things around. While Poly/ML 5.3 introduces many important improvements, Isabelle2009 does not make use of any of them, and Poly/ML 5.2.1 is rock-solid.

Isabelle2009 + Poly/ML 5.2.1 should work out of the box, if you download everything from our site. There is also a precompiled Isabelle/HOL image for that Poly/ML compilation.


With sml/nj I got

Building HOL ...
Expected to find ML heap file
/home/gbuday/src/Isabelle/Isabelle2009/heaps/smlnj-110_x86-linux/HOL.x86-linux
HOL FAILED
(see also /home/gbuday/src/Isabelle/Isabelle2009/heaps/smlnj-110_x86-linux/log/HOL)

*** <instream>:337.7-337.49 Warning: type vars not generalized because of
***    value restriction are instantiated to dummy types (X1,X2,...)
*** <instream>:350.34-350.78 Error: value type in structure doesn't
match signature spec
***     name: trans_tac
***   spec:   simpset -> thm option -> tactic
***   actual: ?.X1 -> thm option -> tactic
*** At command "use" (line 1521 of
"/home/gbuday/src/Isabelle/Isabelle2009/src/HOL/Int.thy").
Error in ROOT.ML

*** exception Fail raised: ML error

make: *** [/home/gbuday/src/Isabelle/Isabelle2009/heaps/smlnj-110_x86-linux/HOL]
Error 1
Finished at Tue Nov 10 17:01:43 EET 2009
0:03:46 elapsed time, 0:03:39 cpu time, factor 0.96

Do you see from this what the problem is?

Normally, the official Isabelle releases should work with SML/NJ as well. Either we failed to get it right for Isabelle2009, or there have been recent changes in SML/NJ that make it fail now.

Unless you have some special needs to use SML/NJ, it is not really worth investing more time here: it has become very slow due to the large heap size of main HOL. Apart from that it can only use 1 CPU core.


	Makarius





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