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

> On 4 Dec 2016, at 10:54 PM, Makarius <makarius at> wrote:
> 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 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.


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