Email Gateway (Aug 18 2022 at 14:16): Email Gateway (Aug 18 2022 at 14:16):From: Gergely Buday <gbuday@gmail.com>
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
Email Gateway (Aug 18 2022 at 14:16):From: Makarius <makarius@sketis.net>
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.96Do 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
Last updated: Apr 26 2024 at 20:16 UTC