Email Gateway (Aug 22 2022 at 20:12): Email Gateway (Aug 22 2022 at 20:12):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to clarify certain aspects related to the coding style best
suited for Isabelle2019. The question combines both my concerns about the
changes associated with the new release and, also, some of my previous
concerns. Unfortunately, I was not able to find an explicit Isabelle coding
style guide - please accept my apologies for asking this question if a
document that answers it already exists somewhere.
Should โฆ S โ ๐; T โ ๐; ฯ S; ฯ T โง โน ฯ (S โฉ T) be preferred over S โ ๐
โน T โ ๐ โน ฯ S โน ฯ T โน ฯ (S โฉ T)?
Should ['a set, ('a set โ bool), 'a set] โ bool be preferred over 'a set
โ ('a set โ bool) โ 'a set โ bool?
Should lemma โนโฆ S โ ๐; T โ ๐; ฯ S; ฯ T โง โน ฯ (S โฉ T)โบ be preferred
over lemma "โฆ S โ ๐; T โ ๐; ฯ S; ฯ T โง โน ฯ (S โฉ T)"?
Should definition closed_ow :: โน['a set, ('a set โ bool), 'a set] โ
boolโบ be preferred over definition closed_ow :: "['a set, ('a set โ bool),
'a set] โ bool"?
In general, when should I use double quotation marks over cartouches if
both options are available?
The reference manual states that 'hence' and 'thus' are, effectively,
legacy features. Nevertheless, they are used consistently throughout the
Isabelle sources and there does not seem to be too much effort devoted to
their elimination. Somehow, I always preferred my code to be as concise as
possible and I find it difficult to understand why the readability is
sacrificed when using, for example, 'thus' instead of 'then show'.
Therefore, my question is whether there is a good chance that 'hence' and
'thus' will become obsolete in the future releases.
I would like to understand if it is recommended to use locale structures
for the definition of algebraic structures and abstract spaces. Somehow, I
always found it easier and more natural to state all definitional elements
as explicit locale parameters (also, the main HOL library does not use
structures). Nevertheless, this feature was introduced for a good reason
and there are certain libraries that rely on it (e.g. HOL-Algebra). I would
like to make sure that it is not considered to be bad style not to use it
for the development of new theories/libraries about algebraic structures or
abstract spaces (of course, provided, that these theories/libraries are not
meant to extend one of the existing libraries that already uses structures).
Thank you
Email Gateway (Aug 22 2022 at 20:12):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to make one minor remark with regard to the statement "I was
not able to find an explicit Isabelle coding style guide" in my original
post. Actually, this should say "I was not able to find an explicit
official Isabelle 2019 coding style guide". Of course, I am aware of the
website https://proofcraft.org/blog/isabelle-style.html.
Thank you
Email Gateway (Aug 22 2022 at 20:12):From: Lawrence Paulson <lp15@cam.ac.uk>
I strongly prefer the bracketed style. The linear style is not very legible, especially when there is nesting.
But there are different points of view, and the bracket-style print mode is hard to access. To enable it, insert the line
JEDIT_PRINT_MODE=brackets
in your settings file.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:12):From: "lammich@in.tum.de" <lammich@in.tum.de>
I agree with Larry about brackets, but acknowledge that's personal preference.
I know many people who prefer linear mode.
BTW the print mode is also accessible in jedits option menu, use plugins
isabelle general options and look for the print mode field.
Peter
Email Gateway (Aug 22 2022 at 20:13):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Ooh, a style bike-shed discussion :-)
I also strongly prefer the bracket style (for lemmas and theorems), because linear style becomes very hard to read for larger goals, but I use the linear (=> only) style for types, mostly because people are familiar with that from programming languages and types tend to not go over more than a line or two.
I use quotes for definitions, not cartouches, mostly because Iโm used to it and it is fast to type, and I use cartouches for text and ML code, because Iโm more likely to need to use quotes inside these.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 20:13):From: "lammich@in.tum.de" <lammich@in.tum.de>
About typing speed: I usually adjust completion delay to 0, then the
completions for abbreviations like cartouche when typing ", or symbols pops up
immediately. However, to get semantic completions that come from pide then one
has to wait and press ctrl-b.
Anyway, I find it more annoying to wait the default 0.5 seconds for any non
ascii symbol, than not to have semantic completions without pressing a
shortcut.
Peter
Email Gateway (Aug 22 2022 at 20:13):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Following are some of my personal style decisions.
- Should
โฆ S โ ๐; T โ ๐; ฯ S; ฯ T โง โน ฯ (S โฉ T)be preferred
overS โ ๐ โน T โ ๐ โน ฯ S โน ฯ T โน ฯ (S โฉ T)?
I avoid both of these at the top level of a formula. Instead, I use Isar
constructs: assumes and shows for lemma statements and if for the
introduction rules in inductive definitions.
- In general, when should I use double quotation marks over
cartouches if both options are available?
The default setting for PDF generation is to drop quotation marks but
preserve cartouches. Therefore, I use cartouches in precisely those
places where the bracketing they add may be necessary to understand the
code. In particular, I use quotation marks for propositions after things
like lemma and have, but I use cartouches around field types in
datatype declarations and locale arguments after interpretation.
Regarding my use of cartouches, consider something like the following:
datatype expr = App โนexpr โ exprโบ โนexprโบ | โฆ
Dropping the cartouches would result in expr โ expr expr, which would
look like there was only one field with this illegal type.
All the best,
Wolfgang
Last updated: Apr 20 2024 at 04:19 UTC