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

On 11/11/16 16:07, Andreas Lochbihler wrote:
> 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
> 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.)

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


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