[isabelle] building HOL

Hi there,

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
      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?

The settings were


  ISABELLE_USEDIR_OPTIONS=-M 1 -p 1 -v true -V outline=/proof,/ML

And this was a

Red Hat Enterprise Linux AS release 4 (Nahant Update 3)

With sml/nj I got

Building HOL ...
Expected to find ML heap file
(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
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?

Best Wishes

- Gergely

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