Email Gateway (Aug 22 2022 at 14:24): Email Gateway (Aug 22 2022 at 14:24):From: Makarius <makarius@sketis.net>
This looks strange, but it might be just the mailer messing up the
indentation. I am including my own experiment in Scratch.thy, which
looks fine to me.
(This is Isabelle2016-1-RC2 with clean defaults.)
Makarius
Scratch.thy
Email Gateway (Aug 22 2022 at 14:25):From: Makarius <makarius@sketis.net>
There are actually two different effects seen in both 2. and 3.:
(a) inner syntax vs. outer syntax
(b) indendation of 'where'
Inner syntax is not taken into account in indentation right now: it is
far to complex and PIDE markup for its structure is mostly missing. To
clarify the non-observance of inner syntax further, I have made two
small changes in
https://bitbucket.org/isabelle_project/isabelle-release/commits/b87697eec2acb383b204d4874c9d8f9c25823fc1?w=1#chg-src/Tools/jEdit/src/text_structure.scala
The 'where' keyword is different. It belongs to a new category of "quasi
commands"; other examples are 'imports', 'fixes', 'assumes', 'shows',
'obtains'. These keywords are indented like a secondary command that is
nested inside the main command. This explains the 4 instead of 2 spaces
here:
definition foo
where
"foo x = x"
Here is definition with more clauses. It shows how everything fits
nicely together:
fun bar :: "nat ⇒ nat"
where
"bar 0 = 0"
| "bar (Suc n) = n"
This indentation of 'imports', 'where', '|' is a change of what I have
considered canonical indentation over many years. But there was no
particular reason for the former format. The reason for the new one is
more uniformity: fewer rules and special cases are required to specify
how indentation works.
Makarius
Email Gateway (Aug 22 2022 at 14:25):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
When I wrote my e-mail 1.5 weeks ago, I really got the indentation as shown in the quote
above (with show starting in the first column). When I tried today again, I was not able
to reproduce this behaviour. I get the same indentation as you got. Strange.
Andreas
Email Gateway (Aug 22 2022 at 14:25):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
- The keyword "where" in definitions is indented according to the
indentation of the type when the type spans several lines. For example,definition foo :: "this_is_a_very ⇒
(long_type,
where_it_makes_sense_to_use ⇒ several_lines) type_constructor"
where
"foo = undefined"Here, "where" is indented on space too far (three instead of two),
because the last line of the type is indented by one (which I find
desireable, because it emphasizes that the return type of the function
goes on).What is the point of aligning minor keywords like "where" with the
previous line of inner syntax? IMO "where" belongs to the outer syntax
of "definition" and should therefore ignore any alignment of inner syntax.Of course, I can manually delete the space before "where", but whenever
I hit <RET> again on that line, it will insert it again. :-(
- Reformatting destroys all semantic indentation of inner syntax. For
example, in the example of 2., when I mark the whole definition and
press C-C C-i, I getdefinition foo :: "this_is_a_very ⇒
(long_type,
where_it_makes_sense_to_use ⇒ several_lines) type_constructor,"
where
"foo = undefined"This seems wrong for two reasons: First, it has destroyed the formatting
of the type. Second, the specification equation is now indented by 4
spaces. Why should we indent specifications by 4 spaces? The position of
the "where" (on the line of the type vs. on a new line) should not
affect the indentation, but apparently it does. Is there a good reason
for this?There are actually two different effects seen in both 2. and 3.:
(a) inner syntax vs. outer syntax
(b) indendation of 'where'Inner syntax is not taken into account in indentation right now: it is
far to complex and PIDE markup for its structure is mostly missing. To
clarify the non-observance of inner syntax further, I have made two
small changes in
https://bitbucket.org/isabelle_project/isabelle-release/commits/b87697eec2acb383b204d4874c9d8f9c25823fc1?w=1#chg-src/Tools/jEdit/src/text_structure.scalaI haven't tried this changes yet and I cannot tell from a quick look at the sources what
they do. I hope that outer syntax now ignores the indentation of inner syntax (which was
not the case in Isabelle2016-1-RC2).
The 'where' keyword is different. It belongs to a new category of "quasi
commands"; other examples are 'imports', 'fixes', 'assumes', 'shows',
'obtains'. These keywords are indented like a secondary command that is
nested inside the main command. This explains the 4 instead of 2 spaces
here:definition foo
where
"foo x = x"Here is definition with more clauses. It shows how everything fits
nicely together:fun bar :: "nat ⇒ nat"
where
"bar 0 = 0"
| "bar (Suc n) = n"This indentation of 'imports', 'where', '|' is a change of what I have
considered canonical indentation over many years. But there was no
particular reason for the former format. The reason for the new one is
more uniformity: fewer rules and special cases are required to specify
how indentation works.
Indeed, one could argue forever whether
fun bar :: "nat => nat" where
"bar 0 = 0"
| "bar (Suc n) = n"
or
fun bar :: "nat => nat" where
"bar 0 = 0"
| "bar (Suc n) = n"
is better. I prefer the former because it saves to spaces of indentation, so I can stick
two more characters onto a line. But that's not a strong argument.
What I found confusing was that the level of indentation depends on whether "where" is on
a line of its own or not. In Isabelle2016-1-RC2, I get the following indentation behaviour:
definition bar :: "nat ⇒ nat" where
"bar = id"
definition bar :: "nat ⇒ nat"
where
"bar = id"
This does not make sense to me and I find it quite annoying. Especially if the right
hand side spans several lines. Then, when I change the type, say because I have to add
another parameter, and put the "where" quasi-command on a new line, I have to adjust the
indentation of the whole right hand side. For me, it's OK if we indent definitions by 4
spaces, but it's not OK if the indentation depends on whether the "where" is on the same
line or not.
By the way, the same applies to "obtain" inside Isar proofs. Here's such a silly example
of an indentation produced by C-c C-i:
notepad begin
obtain n :: nat where "n = n"
and "n = n" sorry
obtain n :: nat
where "n = n"
and "n = n" sorry
I hope that your changeset above addresses these inconsistencies.
Best,
Andreas
Email Gateway (Aug 22 2022 at 14:25):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
A follow-up on this issue. I've now observed a similarly wrong indentation with context
blocks:
context<RET>assumes "True"<RET>and "True"<RET>begin
yields
context
assumes "True"
and "True"
begin
rather than
context
assumes "True"
and "True"
begin
This is on a freshly installed Isabelle2016-1-RC2 in an empty theory. If necessary, I can
also try to shoot a short video of my screen.
Andreas
Email Gateway (Aug 22 2022 at 14:37):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
While testing (and working with) Isabelle2016-1-RC2, I've used the new automatic
indentation a lot (I have enabled the options "Indent Newline" and "Indent Script").
Overall, my feeling is that at the moment I have to do about as much manual editing of the
indentation as before. Therefore. I'd like to share the issues I ran into. Apologies in
advance for this lengthy post. I hope that it stirs some discussion about what is good
indentation and helps to improve the auto-indentation (ideally before the next release).
lemma<RET>assumes "True"<RET>and "True"<RET>shows "True"<RET>
Here is what the automatic indentation produces in the editor, which is clearly not what I
want and would have expected. So I have to go over it again and adjust the indentation.
This requires more typing than without automatic indentation.
lemma
assumes "True"
and "True"
shows "True"
definition foo :: "this_is_a_very ⇒
(long_type,
where_it_makes_sense_to_use ⇒ several_lines) type_constructor"
where
"foo = undefined"
Here, "where" is indented on space too far (three instead of two), because the last line
of the type is indented by one (which I find desireable, because it emphasizes that the
return type of the function goes on).
What is the point of aligning minor keywords like "where" with the previous line of inner
syntax? IMO "where" belongs to the outer syntax of "definition" and should therefore
ignore any alignment of inner syntax.
Of course, I can manually delete the space before "where", but whenever I hit <RET> again
on that line, it will insert it again. :-(
definition foo :: "this_is_a_very ⇒
(long_type,
where_it_makes_sense_to_use ⇒ several_lines) type_constructor,"
where
"foo = undefined"
This seems wrong for two reasons: First, it has destroyed the formatting of the type.
Second, the specification equation is now indented by 4 spaces. Why should we indent
specifications by 4 spaces? The position of the "where" (on the line of the type vs. on a
new line) should not affect the indentation, but apparently it does. Is there a good
reason for this?
apply immediately before done should not be indented. For example, auto-indentation
produces the following, but this just looks silly.
have "statement"
apply(rule a)
apply(rule b)
apply(rule rule_with_many_premises)
apply(auto simp add: ...)
done
The rule in the third apply produces many subgoals, all of which are solved in one go with
auto. IMO there is little reason to indent this single like like that. I'd prefer to have
something like
have "statement"
apply(rule a)
apply(rule b)
apply(rule rule_with_many_premises)
apply(auto simp add: ...)
done
because it is clear that auto is supposed to solve all goals that are there. (I use such
apply scripts a lot when I develop proof and my definitions are still unstable.
Ultimately, I will go over this proof to polish it and probably collapse everything into a
one-line proof. But I do so only when I know that I am not going to change my definitions
again, which may take several weeks or months. Before that, there is no point in
compressing such proof steps because I would have to manually reconstruct the apply script
again when the definition changes and the proof breaks to see how I can fix it. For this
intermediate period of time, I'd prefer to avoid these silly indentations.)
Refinement proof steps (using/including) break the indentation of apply scripts when
they are used in the middle of the proof script. When I develop my proofs, I frequenly
have scripts that look like the following:
have "statement"
apply(rule rule_with_several_premises)
apply(simp)
using some_fact apply(clarsimp simp add: ...)
apply simp
including lifting_syntax
apply transfer_prover_start
Unfortunately, this does not go well with the "Indent Script" option. This option pulls
the "using some_fact" to the indentation level of the first apply (4 spaces here). But
this is completely pointless, because the proof method clarsimp will only insert it into
the current subgoal. Even worse, when I manually indent the "using ..." line as it is
shown in the example, all the subsequent apply's will be indented relative to the start of
using. Can I somehow avoid this?
Side remark 1: I know that there is the new apply(use some_fact in
\<open>clarsimp\<close>) syntax, but this is too cumbersome to type when I am just
exploring a proof. In the final, polished version, all of this will probably be deleted
again. And it is much easier to just enter "using some_fact " before the "apply clarsimp"
than to navigate the cursor to the start of the clarsimp and enter "use some_fact
\<open>", then to navigate to the end of the line, move the cursor left by one character
and then enter "\<close".
Side remark 2: I don't use "subgoal using some_fact by(clarsimp simp add: ...)" because
subgoal transfers all goal parameters into fixed variables of the context. Often, these
parameters are tuples, which clarsimp then cannot split into their components any more, so
the proof would fail.
Andreas
Email Gateway (Aug 22 2022 at 14:46):From: Makarius <makarius@sketis.net>
I have refined that in
https://bitbucket.org/isabelle_project/isabelle-release/commits/e61de633a3eddc6
This makes indentation more uniform and predictable, but produces more
spaces in intermediate situations. The WhiteSpace plugin of jEdit helps
to remove trailing space systematically, e.g. on buffer save.
I reckon there will be one more release candidate (RC5), before final
lift-off. If you want to test it right now, you need to use the above
repository version: http://isabelle.in.tum.de/devel is already back to
post-release mode and now delivers isabelle-dev snapshots instead of
release snapshots.
Makarius
Email Gateway (Aug 22 2022 at 14:46):From: Makarius <makarius@sketis.net>
The above apply-script indentation follows the traditional scheme from
about 18 years ago. In recent years I've actually got used to unindented
apply scripts. Since I was unsure if it is always such a good idea, I
have provided the option "indent_script" to control that.
So you could try disabling that and see how you feel about it.
I think systematic apply-script indentation is today mainly used (and
enforced) by the seL4 people at Data61 (formerly NICTA). It would be
interesting to get some feedback from Down Under like "This is great" or
"This sucks".
Makarius
Email Gateway (Aug 22 2022 at 14:47):From: Gerwin.Klein@data61.csiro.au
This is great :-)
The indentation of auto looks a bit silly but carries information, and should be the way it is.
This indentation is also what the AFP expects. We’re not going to argue (much) about this particular case, but it’s usually better to have consistency over beauty in code layout.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 14:47):From: Lawrence Paulson <lp15@cam.ac.uk>
I agree with Gerwin. The default indentation makes it clear how many subgoals are being solved at each point. It’s worth knowing that, even if it looks silly.
Larry Paulson
Last updated: Apr 19 2024 at 16:20 UTC