[isabelle-dev] Spec_Check

[Makarius]

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 
http://isabelle.in.tum.de/repos/isabelle/rev/f22d227a090c.


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).


 	Makarius