Re: [isabelle] Tab completion slow in Isabelle2014-RC2




Am 08.08.14 14:19, schrieb Makarius:
On Fri, 8 Aug 2014, Joachim Breitner wrote:
But UI guided interaction will always be limited in expressiveness and efficiency, compared to a textual interface. There is a reason why we _write_ Isar, and do not use a “proof block panel” to click together the fixes and assumes, and elsewhere select the initial proof method
Both the writing and clicking that is sketched here is cumbersome, and conceptually not really different. A more high-level editing model of interactice proof documents is required, and apply scripts should be left behind altogether.

I've started working on more than 15 years ago, but even today people still think of the source text as a "script" that is somehow linear.
Well I'd like a voice interface where I just explain the proof idea and sledgehammer and friends pick up keywords to generate a proof from that. But maybe let's focus on what can be improved on the current state of the art.






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