Re: [isabelle] Isabelle style guide



> On 28.05.2015, at 22:21, Makarius <makarius at sketis.net> wrote:
>
> On Sat, 23 May 2015, Gerwin Klein wrote:
>
>> Updating lots of proofs to Isabelle2015-RCx and discussions about submission rules for the AFP inspired me to write up guidelines that may be of more widespread use and interest:
>>
>> http://proofcraft.org/blog/isabelle-style.html
>
> This is indeed a quite fitting style guide.  The Prover IDE should gradually formalize more of such fine points, to make it easier to avoid bad style by default.

I agree, it would be nice to gradually converge to more support for such things over time.


> * Concerning bad internal names like xa, xb, xaa: Isabelle2015 produces
>  formal markup for that in the slightly reformed rule_tac family, with
>  the faint read color scheme of improper material.  Maybe we should also
>  revisit rename_tac at some point, to clarify its meaning in that
>  respect, or to eliminate the need for rename_tac / rule_tac altogether
>  due to newly emerging subgoal focus in Isar "scriptsâ.

The subgoal focus mechanism sounds promising. I didnât have enough practical experience with it yet to make it a recommendation, but when it has withstood the test of time for a while, that could indeed become the main way of doing things.


> I am curious to see part 2, and especially part 3 about layout; the latter category is more easily accessible in the Prover IDE.

Part 3 will probably be the most controversial one - not because Iâm planning to write anything special, but because layout is the easiest to have strong opinions on.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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