[isabelle] [Isabelle2016-1-RC2] Experience with auto-indentation



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).

1. Indentation does not work properly if I write a lemma statement from top to bottom.
For example, put the curser at the beginning of a line in a theory and type the following (<RET> denotes the return key which is bound to "Newline with indentation of Isabelle keywords"):

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"


2. 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. :-(

3. 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 get

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?

4. 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.)

5. 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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.