[isabelle-dev] Problem in AFP

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Mar 23 18:02:40 CET 2023


isabelle: d5060a919b3f tip
afp: c3a4497b0f9d tip

$ isabelle build ConcurrentGC
> Running ConcurrentGC ...
> ConcurrentGC FAILED (see also "isabelle build_log -H Error ConcurrentGC")
 > […]
> *** Inner syntax error (line 116 of "$AFP/ConcurrentGC/Global_Invariants_Lemmas.thy")
> *** at "↦ obj ) ⦈ ) ) = mut_m.tso_store_refs m s"
> *** Failed to parse prop
> *** At command "lemma" (line 106 of "$AFP/ConcurrentGC/Global_Invariants_Lemmas.thy")

$ hg log -l 1 thys/ConcurrentGC
> Änderung:        13340:ab90e6e586ca
> Vorgänger:       13338:3090aa3b36a4
> Nutzer:          wenzelm
> Datum:           Mon Jan 16 13:40:54 2023 +0100
> Zusammenfassung: isabelle update -u cite

Any clue what went wrong here?

	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 13043 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230323/c9942195/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230323/c9942195/attachment.sig>


More information about the isabelle-dev mailing list