[isabelle-dev] status (AFP)

[Makarius]

On Thu, 4 Oct 2012, Gerwin Klein wrote:

> This is now done, AFP_big has been retired, and afp_build updated 
> accordingly.

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 
http://isabelle.in.tum.de/reports/Isabelle/report/3b4b73890515487a97a26dc8f4c56370

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.


 	Makarius