On 19/10/16 20:23, Florian Haftmann wrote: >> isabelle: ae7c11573922 tip >> afp: 1bffa6708aea tip >> *** [line 5 of >> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/lib/WordDecl.thy"] >> error: command "theory" expected, >> *** but identifier was found: >> *** header
I have also noticed that, running around with manual "isabelle build"
processes in the traditional way.
Such incidents of total-existence failure of AFP session structure
happen about two times per year. We are used to that.
The situation can be easily improved: the AFP submission system merely
needs to check for "Legacy feature" warnings, and tell the authors to
eliminate them beforehand.
Legacy features usually have one or two release cycles, before the
feature is removed. It seems that few people care about that themselves,
so they need to be informed explicitly.
Another possible improvement for AFP checks:
isabelle check_sources '$AFP_BASE'
This is available in Isabelle/Scala module Check_Sources.
Makarius
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
