[isabelle-dev] Spec_Check

[Lukas Bulwahn]

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