Alex Mobius (Oct 20 2026 at 15:02): Alex Mobius (Oct 20 2026 at 15:02):Hello,
I have written a couple of times here about this bug, which I believe I have a fix for now. Essentially, raising the default sort lf a class context (like HOLCF class bifinite does, raising it from type to cpo) leads to the class context failing to import theorem definitions from superclasses, leaving instead locale versions that refer to locale fixes (e.g. po.below instead of global below :: 'a::po => 'a => bool). The fix is relatively straightforward - when assembling the class context, cast the 'a type variable in the definitions to the right sort. This is sound, because subclasses necessarily have higher sort for that variable than superclasses. The small patch and the reproduction suite are attached, checked against the newest RC3. I would really appreciate if someone could take a look.
class-base-sort-repro.tar.gz
class-base-sort-syntax.patch
Kevin Kappelmann (Oct 20 2026 at 18:08):Hi Alex, it seems like the file you are trying to patch is authored by Florian Haftmann, TU Munich. Have you tried to contact him directly? Typically patching something such fundamental requires having a discussion with the responsible author of the affected modules.
Alex Mobius (Oct 24 2026 at 07:35):Thank you for the advice, Kevin! Will do. Unfortunately it doesn't seem like you can easily get on isabelle-dev mailing list... Seems like that'd be a good place to find the current maintainer
Kevin Kappelmann (Oct 24 2026 at 09:00):why do you think that? i thought everyone can sign up.
anyway: you shouldn't post there (that one is mostly for the isabelle development version). You are asking for something that is already in stable releases. I think directly contacting Florian Haftmann with a brief email is your best bet.
Kevin Kappelmann (Oct 24 2026 at 09:00):Note that only very very few (and typically busy) people know the locale and classes infrastructure so it is hard to get things changed.
Alex Mobius (Oct 24 2026 at 09:40):Ah well, it just 403's when you try to sign up for the newsletter. I got the impression it's hard to change yeah... That is the biggest downside of Isabelle so far
Kevin Kappelmann (Oct 24 2026 at 10:28):Oh, I see. The server error you can report on the users list if you are subscribed there?
I also see Florian on Tuesday by chance. If you send him an email, I can also ask him if what he's currently up to and able to look into it.
Alex Mobius (Oct 24 2026 at 15:27):Thank you very much, but no need - he already replied and said that he will have time to look at it on Thursday. Again much obliged for your advice!
Last updated: Oct 25 2026 at 18:46 UTC