Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2008 - Can't rebuild Simpl any longer

Email Gateway (Aug 18 2022 at 12:00):

From: George Karabotsos <g_karab@encs.concordia.ca>
Hello,

I have just installed Isabelle2008 with Poly/ML 5.1 - downloading Simpl
(http://afp.sourceforge.net/entries/Simpl.shtml) and trying to rebuild
it gives me the following error:

(30)@kalamata/home/karabot/dev/Isabelle/Simpl > isatool usedir -b HOL simpl
Building simpl ...
simpl FAILED
(see also
/home/karabot/isabelle/heaps/Isabelle2008/polyml-5.1_x86-linux/log/simpl)

"?\<Gamma>\<turnstile> \<langle>?c,Fault ?f\<rangle> \<Rightarrow>

Fault ?f"

Ignoring duplicate introduction (intro)

"?\<Gamma>\<turnstile> \<langle>?c,Stuck\<rangle> \<Rightarrow> Stuck"

Ignoring duplicate introduction (intro)

"?\<Gamma>\<turnstile> \<langle>?c,Abrupt

?s\<rangle> \<Rightarrow> Abrupt ?s"

*** Duplicate fact "Semantic.exec_Call_body"
*** At command "done" (line 428 of
"/home/karabot/dev/Isabelle/Simpl/Semantic.thy").
Exception- TOPLEVEL_ERROR raised
*** exception Fail raised: ML error

Here's some additional information on my system:

uname -a
Linux kalamata 2.6.25.4 #2 SMP Thu May 15 18:20:32 EDT 2008 i686
Intel(R) Pentium(R) D CPU 3.40GHz GenuineIntel GNU/Linux

TIA,

George

Email Gateway (Aug 18 2022 at 12:00):

From: Makarius <makarius@sketis.net>
This is because the official AFP is still for Isabelle2007. At the moment
you should get along with the development version of AFP, until it has
been repackaged for Isabelle2008.

Makarius

Email Gateway (Aug 18 2022 at 12:00):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
Hi George,

sorry it took a while, but the AFP is now updated (see separate announcement).

If you download the current version of Simpl, it should now build normally
with Isabelle2008.

Cheers,
Gerwin

George Karabotsos wrote:

Last updated: May 03 2024 at 12:27 UTC