Email Gateway (Aug 19 2022 at 10:36): Email Gateway (Aug 19 2022 at 10:36):From: Thomas Genet <thomas.genet@irisa.fr>
Dear all Isabelle users,
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?
Thanks in advance,
Thomas
Email Gateway (Aug 19 2022 at 10:37):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 27 2024 at 01:05 UTC