makarius at sketis.net
Fri May 31 12:24:17 CEST 2013
On Thu, 30 May 2013, Makarius wrote:
> * Canonical session name? It looks like the name of the tool is
> "Spec_Check", according to its main Spec_Check.thy
> So it would be session HOL-Spec_Check in ~~/src/HOL/Spec_Check/
> You still have a chance to rename "Spec_Check" now, before anything is
> pushed to main Isabelle. The directory location is given by having a
> session built on HOL, though.
Now that everything is in-place (and SML/NJ partially happy in
2bbeab01c0ea) I have realized that despite the import of theory HOL/Main,
the tool does not depend on HOL at all.
So it could just import Pure, and then be session Spec_Check in
Thus it would conform to the idea of a general Quickcheck tool for
Isabelle/ML -- understanding "Isabelle/ML" as the brand name for this
cutting-edge Standard ML implementation.
Of course we should avoid repeated alternation of source locations. So
there is a second chance here, but then it should be really right.
More information about the isabelle-dev