[isabelle-dev] status (AFP)
makarius at sketis.net
Thu Oct 4 12:12:27 CEST 2012
On Thu, 4 Oct 2012, Gerwin Klein wrote:
> This is now done, AFP_big has been retired, and afp_build updated
Great. I have removed one more letter in AFP/c9d12d55c3a6.
BTW, my afp_build was more like an example. Feel free to reshape the
standard build process in the way you see fit as AFP administrator.
There is not much functionality left in the script anyway: it just strings
together $AFP_BUILD_OPTIONS with "-d '$AFP' -g AFP" and passes on to
regular isabelle build.
Florian also has an older attempt at some "testafp" tool in the
AFP repository, which should be obsolete now.
> I've removed all occurrences of FLYSPEC_SKIP_PROOFS in isatest and
> afptest, but I'm not sure if it is used in Mira anywhere. It should be
> fail safe, but should be cleaned up.
Independently of the AFP configuration, Mira is still in bad shape (for
1-2 weeks already). E.g. see
The "### Missing Isabelle component: ..." warnings indicate that the local
copy of the standard components are outdated. I still wonder why
/home/isabelle/contrib cannot be used directly in the Mira setup.
More information about the isabelle-dev