Email Gateway (Aug 17 2022 at 14:49): Email Gateway (Aug 17 2022 at 14:49):From: Steven Obua <obua@in.tum.de>
I am wondering, did you address the signaling issue David Matthews
talked about? If not, then this could be an explanation why you run out
of memory too soon (because garbage collection does not kick in when it
should).
Steven
Email Gateway (Aug 17 2022 at 14:49):From: Martin Klebermaß <martin@klebermass.de>
Hello,
i think i have got polyml running on my IntelMac now.
So i can now continue getting Isabelle running.
Trying to compile the pure logics i get the some errors (attached at
the end).
There seem to be some problems with the CPure Theory. As i can see in
the changelog file, there have been some changes in the CPure Theory.
Any ideas how to solve the problem?
Thanks
Martin
Errormessage i got by compiling the Pure Logics:
Started at Do Jun 29 17:50:50 CEST 2006 (polyml-4.2.0_unknown-
platform on martin-klebermas-computer.local)
Building Pure ...
Pure FAILED
(see also /usr/local/Isabelle_29-Jun-2006/heaps/polyml-4.2.0_unknown-
platform/log/Pure)
lemma conjunction_imp:
(PROP ?A && PROP ?B ==> PROP ?C) == ([| PROP ?A; PROP ?B |] ==> PROP ?C)
val it = () : unit
structure Pure : sig val thy : Theory.theory end
val it = () : unit
Loading theory "CPure"
*** Bind
*** Theory data method Pure/simpset.extend failed
*** At command "theory" (line 7 of "/usr/local/Isabelle_29-Jun-2006/
src/Pure/CPure.thy").
Exception- TOPLEVEL_ERROR raised
make[1]: *** [/usr/local/Isabelle_29-Jun-2006/heaps/
polyml-4.2.0_unknown-platform/Pure] Error 3
make: *** [Pure] Error 2
Finished at Do Jun 29 17:56:06 CEST 2006
0:05:16 elapsed time, 0:05:14 cpu time
Email Gateway (Aug 17 2022 at 14:49):From: Martin Klebermaß <martin@klebermass.de>
Seems to be you are right.
The problems came from polyml.
I have now set up Isabelle SML-NJ on my IntelMac and it is working now.
If anyone need help setting up Isabelle with SML-NJ on IntelMac , he
can ask me.
Martin
Last updated: May 03 2024 at 08:18 UTC