[isabelle-dev] Problem in AFP

[Tobias Nipkow]

Yes, it was a problem with the new map update syntac priorities. Thanks for 
pointing it out, I have updates the sources now.

Tobias

On 23/03/2023 18:08, Makarius wrote:
> On 23/03/2023 18:02, Florian Haftmann wrote:
>> 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?
> 
> My change from 16-Jan-2023 is not relevant here.
> 
> I would say the problem is due to recent changes in the Map syntax, which have 
> not been pushed through the "slow" sessions yet.
> 
> 
>      Makarius
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4638 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230326/4fda3a55/attachment.bin>