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

The settings were

  ML_SYSTEM=polyml-5.3.0
  ML_HOME=/home/gbuday/usr/polyml/bin/bin
  ML_OPTIONS=-H 200
  ML_PLATFORM=x86-linux

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

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

Best Wishes

- Gergely





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