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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and