[isabelle-dev] Problem in AFP

[Florian Haftmann]

Excellent, thanks.

	Florian

Am 26.03.23 um 19:03 schrieb 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
> 
> _______________________________________________
> 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: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 13043 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230326/f235ded3/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/20230326/f235ded3/attachment.sig>