Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Problem in AFP


view this post on Zulip Email Gateway (Mar 23 2023 at 17:03):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature

view this post on Zulip Email Gateway (Mar 23 2023 at 17:09):

From: Makarius <makarius@sketis.net>
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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Mar 26 2023 at 17:03):

From: Tobias Nipkow <nipkow@in.tum.de>
Yes, it was a problem with the new map update syntac priorities. Thanks for
pointing it out, I have updates the sources now.

Tobias

smime.p7s

view this post on Zulip Email Gateway (Mar 26 2023 at 18:55):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Excellent, thanks.

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature


Last updated: Mar 04 2024 at 10:08 UTC