Email Gateway (Aug 22 2022 at 10:02): Email Gateway (Aug 22 2022 at 10:02):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
As promised, part 2 of the Isabelle style guide:
http://proofcraft.org/blog/isabelle-style-part2.html
Feedback for the first part was great, keep it coming!
Enjoy,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:02):From: Lars Noschinski <noschinl@in.tum.de>
For the context section, maybe mention bundles? You may need to open a
context with the individualized setup multiple times.
-- Lars
Email Gateway (Aug 22 2022 at 10:02):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Excellent point. Have updated the text.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:02):From: Makarius <makarius@sketis.net>
"Isabelle supports literal proofs": you probably mean "literate proofs".
This should give most people an idea about the point of it, although the
official slogan talks about "proof documents".
You could also add a note that the SideKick plugin of Isabelle/jEdit
helps getting an overview of a text that is nicely structured with
chapter, section, subsection etc.
CamelCaseNames for datatype constructors: around 2006/2007 this was
discontinued as canonical form in Isabelle/Pure/ML and replaced by
Camel_Case_Names with_proper_underscore. Both the old and new forms are
widely used, though, since renaming constructors in ML is always a bit
dangerous (but not in HOL).
About bad "definition f" and "This will reserve the name f and make it
unusable for variables". Having a constant called "f" in the global
context is certainly bad, but there should always be a way to produce a
free variable of that name, by using explicit "fixes", "for" or "!!f.
..." in closed propositions. Isar has been designed like that from the
very start, although surprisingly many people don't know that --
especially when building tools that ignore the concepts of
eigen-contexts of statements.
"typed as \open and \close in jEdit": This should be Isabelle/jEdit,
since jEdit does not know anything about it. The canonical shortcut in
the Prover IDE works via ASCII backquote, although that is sometimes
hard to find on strange keyboards (e.g. German Macintosh). At some
point, the canonical key for cartouches might become " (double-quote),
when terms are accepted in that form as well.
Makarius
Email Gateway (Aug 22 2022 at 10:03):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 31.05.2015, at 07:00, Makarius <makarius@sketis.net> wrote:
On Sat, 30 May 2015, Gerwin Klein wrote:
As promised, part 2 of the Isabelle style guide:
http://proofcraft.org/blog/isabelle-style-part2.html
Feedback for the first part was great, keep it coming!
- "Isabelle supports literal proofs": you probably mean "literate proofs”.
Thanks for catching that. This is indeed precisely what I meant to say. Already updated.
You could also add a note that the SideKick plugin of Isabelle/jEdit
helps getting an overview of a text that is nicely structured with
chapter, section, subsection etc.
Good idea.
- CamelCaseNames for datatype constructors: around 2006/2007 this was
discontinued as canonical form in Isabelle/Pure/ML and replaced by
Camel_Case_Names with_proper_underscore. Both the old and new forms are
widely used, though, since renaming constructors in ML is always a bit
dangerous (but not in HOL).
I still like the pre 2006 style, but I should mention both, yes.
- About bad "definition f" and "This will reserve the name f and make it
unusable for variables". Having a constant called "f" in the global
context is certainly bad, but there should always be a way to produce a
free variable of that name, by using explicit "fixes", "for" or "!!f.
..." in closed propositions. Isar has been designed like that from the
very start, although surprisingly many people don't know that --
especially when building tools that ignore the concepts of
eigen-contexts of statements.
I guess I should clarify that more, yes. There are certainly plenty of options to still use the name f as a parameter or variable, but you usually need to do something, and I’ve often seen people confused by it, esp when it’s only in a PDF without syntax highlighting.
- "typed as \open and \close in jEdit": This should be Isabelle/jEdit,
since jEdit does not know anything about it. The canonical shortcut in
the Prover IDE works via ASCII backquote, although that is sometimes
hard to find on strange keyboards (e.g. German Macintosh).
I managed to miss that. Way nicer to type! Will add.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 27 2024 at 01:05 UTC