Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Simpl in AFP release for 2011-1 does not build

view this post on Zulip Email Gateway (Aug 19 2022 at 08:42):

From: Lars Noschinski <noschinl@in.tum.de>
Hi,

to test the autocorres tool[1], which is not yet available for Isabelle
2012, I downloaded the Isabelle 2011-1 release and the latest AFP
release for 2011-1 (afp-2011-11-27.tar.gz).

However, building the Simpl image from this release fails: First, due to
missing recdef (which is easily solved by importing the Old_Recdef
theory), then due to some missing constant:

*** Theory loader: failed to load "Simpl" (unresolved "VcgEx", "XVcgEx",
"VcgExSP", "ClosureEx", "ComposeEx", "ProcParEx", "Quicksort",
"UserGuide", "SyntaxTest", "VcgExTotal", "ProcParExSP")
*** Unknown constant: "Complete_Lattice.SUPR" (line 134 of
"/home/lars/opt/afp-2011-11-27/Simpl/hoare.ML")
*** At command "use" (line 36 of
"/home/lars/opt/afp-2011-11-27/Simpl/Vcg.thy")
Exception- TOPLEVEL_ERROR raised
*** ML error

make: ***
[/home/lars/.isabelle/Isabelle2011-1/heaps/polyml-5.4.0_x86-linux/Simpl]
Fehler 1

So it seems this AFP release is not the right one for 2011-1, but this
holds also for afp-2011-04-01.tar.gz -- so is there anywhere an AFP
release, which works with Isabelle 2011-1 out-of-the-box?

[1] http://ssrg.nicta.com.au/projects/TS/autocorres/

-- Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 08:42):

From: Lars Noschinski <noschinl@in.tum.de>
I now looked at the AFP repository. The version there tagged with
Isabelle2011-1 is a lot newer (despite dating from 2011-10-10) then
afp-2011-11-27.tar.gz, which is refered to on [1] as the release for
Isabelle 2011-1. More importantly, it works.

Can we fix the AFP webpage to point to a correct version of the AFP for
2011-1?

[1] http://sourceforge.net/projects/afp/files/afp-Isabelle2011-1/

view this post on Zulip Email Gateway (Aug 19 2022 at 08:43):

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

thanks for spotting that. Looks like something went wrong in my AFP release update back then.

Will take care of it.

Cheers,
Gerwin

view this post on Zulip Email Gateway (Aug 19 2022 at 08:44):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
Fixed.

I had embarrassingly just forgotten to update the SF download system, so it was still pointing to the Isabelle2011 version in Isabelle2011-1

The direct link on http://afp.sourceforge.net/entries/Simpl.shtml has been working, which was the main thing I had tested.

The link on the download system should now work as well. Sorry for the confusion.

Cheers,
Gerwin

Last updated: Apr 19 2024 at 01:05 UTC