Email Gateway (Aug 22 2022 at 20:03): Email Gateway (Aug 22 2022 at 20:03):From: Dominique Unruh <unruh@ut.ee>
Hello,
in a diamond shaped theory structure I get "exception Match raised (line
338 of "Isar/code.ML")".
This is in Code.merge_specs, so it seems to be a problem with merging
the code generation specifications.
I have attached a minimal example, the error is in AB.thy (I can provide
the original theory where it happened, too, if needed.)
I am using Isabelle2019, session HOL.
Best wishes,
Dominique.
A.thy
AB.thy
B.thy
Bot.thy
Email Gateway (Aug 22 2022 at 20:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Domininique,
thanks for reporting this.
This is indeed a serious, so far unnoted omission in the merge algorithm
for code data, which will disappear in the next Isabelle release.
In the meantime, you can linearize your theory graph: only theory A
imports theory Bot directly.
Hope this helps,
Florian
signature.asc
Last updated: Apr 26 2024 at 12:28 UTC