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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
