Excellent, thanks.
FlorianAm 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 ConcurrentGCRunning 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 citeAny 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-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
OpenPGP_0xA707172232CFA4E9.asc
Description: OpenPGP public key
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
