[isabelle-dev] Problem in AFP

[Makarius]

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