On 05/30/2013 03:51 PM, Makarius wrote:
So back to this now:
* 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.
Yes, I think Spec_Check is the name to go with.
* Formal licensing. As part of the main source tree it implicitly
joins the toplevel LICENSE. It is possible to have a 1-line
add-on in
each theory header, e.g. see ~~/src/HOL/SPARK/SPARK.thy, but not a
separate LICENSE file.
There is no need for a separate LICENSE file here.
The README could also say in plain words that the original code-base
by Christopher League has been relicensed under the 3-clause BSD
license of Isabelle -- i.e. a slightly reduced version of what is in
the README of f0a79be57a4b already.
Yes, I was trying to point this out, but did not state it in such
precise words.
* NEWS and CONTRIBUTORS entries.
Summary and Authors are in the README file from that NEWS and
CONTRIBUTORS can be derived.
Further (less important hints on the README):
3. As Isabelle can run heavily in parallel, we avoid reference types.
Sounds like someone got surprised after 10 years of multicores in the
consumer market that parallel programming is just the normal
situation. When I was a young student, we did learn parallel and
concurrent programming by default, instead of the oo-nonsense that
came on later generations. (Times have changed again already, so we
don't have to revisit this old topic.)
4. Isabelle has special naming conventions and documentation of source
code is only minimal to avoid parroting.
Sounds a bit depressing for me, since I've tried to explain the good
old high-quality code writing techniques in the implementation manual,
and then the young people don't even fit sources on the screen (much
more than the 80--100 char line length). BTW, I've seen really good
sources recently: ACL2. They have a *strict* 80 char limit, and
really good writing style of "essays", not "code documentation".
Anyway, we stick to what Isabelle/ML is, and don't have to make
excuses for it.
These are no excuses, but they simply describe the reasons for the
differences between the original QCheck and the Isabelle's Spec_Check
implementation.
Dou you want to have a toplevel Isar command for "check_property
@{context}"? That is relatively easy to have these days. What should
be its name?
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.
All of this is possible future work, but more importantly, I would like
to see some volunteer that advertises and mentors a follow-up student
project for Spec_Check.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
