Isaac Freund (Jul 20 2022 at 18:27): Isaac Freund (Jul 20 2022 at 18:27):Is there a standard/recommended style guide for Isabelle documented anywhere? From what code I've seen 2 space indentation seems to be the norm...
Isaac Freund (Jul 20 2022 at 18:28):Even better would be a tool to automatically format Isabelle code
Mathias Fleury (Jul 20 2022 at 18:36):jedit auto-indents code (C-i to reindent a selected part IIRC).
Mathias Fleury (Jul 20 2022 at 18:37):There are parts of the automatic indentation I really don't like (mostly related to inductive predicates and labels), but the default works mostly well.
Manuel Eberl (Jul 20 2022 at 18:44):See the following:
https://isabelle.systems/conventions/
https://proofcraft.org/blog/isabelle-style.html
Neither of these are official in any way though. The AFP also has some style guidelines, although most of them are more concerned with robustness than style:
https://www.isa-afp.org/submission/
Isaac Freund (Jul 20 2022 at 18:53):Thanks to both of you, that jedit key bind seems pretty useful and those documents even more so :)
Manuel Eberl (Jul 20 2022 at 20:36):There's also a few more general tips here: https://isabelle.systems/cookbook/
Wolfgang Jeltsch (Jul 20 2022 at 22:01):Isaac Freund said:
Even better would be a tool to automatically format Isabelle code
I’m very happy that at least there is no such tool integrated into the Isabelle IDE. About two Isabelle versions ago, I had to switch off the auto-indenter, because it made decisions that were apparently ridiculous, so that I found myself spending a considerable amount of effort to manually correct indentation.
Autoformatters would be cool if their authors would have only sensible ideas regarding what a good style is. Sadly, it seems that the authors of autoformatters often have strange ideas regarding that. Maybe for the most part their ideas are reasonable, but one bad idea can be enough to spoil the whole idea of autoformatting. In addition, there might be situation where making exceptions to the rule is reasonable. Because of all that, I think the author should retain the final say regarding code formatting.
Mathias Fleury (Jul 21 2022 at 05:00):I am slightly curious: what did you dislike that much? The one I dislike, but this is more or less the only instance:
inductive rtranclp :: ‹('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool› for r :: ‹'a ⇒ 'a ⇒ bool› where
base:
‹rtranclp r a a› |
step:
‹rtranclp r a c›
if
‹r a b›
Last updated: Apr 19 2024 at 16:20 UTC