[isabelle-dev] AFP broken

[Makarius]

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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161019/43ee53e0/attachment.sig>