[isabelle-dev] Spec_Check

Makarius makarius at sketis.net
Thu May 30 22:51:18 CEST 2013

On Thu, 30 May 2013, Lukas Bulwahn wrote:

> On 05/30/2013 03:51 PM, 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/
> Yes, I think Spec_Check is the name to go with.

See 2c893e0c1def ... cdba0c3cb4c2.

The initial 2c893e0c1def is your 
https://bitbucket.org/nicolai490/qcheck_tum/commits/f0a79be57a4b and the 
final cdba0c3cb4c2 the same after some polishing of Isabelle/ML style. 
There were no big problems, just various fine points, and the next student 
should have a chance to learn from a tidy situation.

>>   * NEWS and CONTRIBUTORS entries.
> Summary and Authors are in the README file from that NEWS and CONTRIBUTORS 
> can be derived.

That is still left to you.  (As usual I've put it on my TODO list for the 
next release, just to make sure.)

> I was thinking of a ML antiquotation for "check_property @{context}"  and I 
> was thinking of @{spec ...} and some context flags that lets spec either only 
> compile, or check with values.
> This should allow that @{spec ...} could be inlined in the implementation if 
> anyone wishes to do so.

Looking again how it is done, I don't see the purpose of an antiquotation 
-- apart from looking superficially like "annotations" that other people 
put into their language.

An Isabelle/ML antiquotation is evaluated at compile-time, in the static 
context *before* the compiler works on the whole module.  Thus you see 
only those ML bindings that were there beforehand, not what you define 
within the module itself.

I've done it a bit differently in 
http://isabelle.in.tum.de/repos/isabelle/rev/e7c47fe56fbd via some plain 
ML function with implicit use of the dynamic compilation context. This 
allows to refer to toplevel declarations incrementally, e.g. see the 
example with "thy" in 

Another note on http://isabelle.in.tum.de/repos/isabelle/rev/2c141c169624: 
Isabelle output is message oriented, i.e. you normally produce just one 
piece, not several "lines" sequentially.  Nice Isabelle messages use 
pretty printing (potentially with extra markup).


More information about the isabelle-dev mailing list