Re: [isabelle] Make quickcheck/nitpick/sledgehammer run in background in jEdit?



On Fri, 22 Mar 2013, Thomas Genet wrote:

I am using Isabelle/HOL for teaching "formal development) and we rely a lot on nitpick/quickcheck for students to debug their specifications. Many of them use the jEdit interface... but I find it surprising for each nitpick/quickcheck to be blocking.

I have seen that there is a similar demand for sledgehammer... Would it be possible to add nitpick/quickcheck on the same item of the TODO list? Or is it fundamentally different?

Yes, nitpick, quickcheck, sledgehammer, even just the old 'pr' command that hardly anyone remembers now, are all in the same category of diagnostic tools operating over given proof text.

The document-model behind Isabelle/jEdit still lacks proper support for that. It is in fact one of the oldest running gags in that project since 2009 -- too many other things have sucked up too many resources (including myself maintaining Proof General in parallel until October 2011).

Hopefully the list of running gags on this mailing list gets some refreshment eventually. Just yesterday I have given a talk where the long anticipated "asynchronous agents" approach was covered briefly. Now it only has to be implemented.


	Makarius




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