Re: [isabelle] isabelle/jedit

I would say that it has nothing to do with constructibility and everything to do with usability. Even 20 years ago, there was hard evidence that people would not read manuals, no matter how carefully they were written. And that was before people got used to discovering what they can and cannot do using menus.

I'm sure that jEdit development will continue and will provide such things eventually. Makarius has asked for volunteers, and I hope one or two enthusiastic students will step forward to help him make jEdit what it should be.


On 9 Aug 2012, at 11:10, Gergely Buday wrote:

>> If you don't mind about a tiny re-interpretation, I would say a more
>> important question would be “is that really an issue?”. I believe there are
>> many purely intuitionist proof by exposition of good artifacts, that the
>> Isabelle jEdit tuple is a good one (teasing and playing with words).
>> Note that you have the option to set Isabelle's flag from within a theory
>> file, ex. like writing “using [[simp_trace=true]]” in a proof body. You may
>> hide from the produced PDF document, using a special comment syntax, like
>> writing “(*<*)using [[simp_trace=true]](*>*)”. By the way, I believe there
>> may be a tiny issue with the simp_trace flags, … will open a thread about it
>> later.
> Yannick,
> I am not a constructivist.
> And, I could accept that a menu entry would insert a forty letter long
> identifier in the proof text. My concern is usability, not theoretical
> elegance. Coming up with a proof is a challenging task in itself, and
> it is better that the user interface helps creating it, and you need
> not remember technicalities in order to advance your proof.
> What do the developers think?
> - Gergely

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