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



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





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