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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
