[isabelle-dev] Spec_Check

[Makarius]

On Thu, 30 May 2013, Lukas Bulwahn wrote:

> https://bitbucket.org/nicolai490/qcheck_tum
>
> @Makarius: Are you willing to include the current state in
> Isabelle's repository, e.g. under src/Tools/?
> The sources are in a stable state and maintenance in last
> half year boiled down to only one minor change. Hence, I
> believe that it is a low-maintenance part in Isabelle and can
> be easily maintained the next few years with almost no
> further effort.

"Low-maintenance" does not exist, but this looks indeed nice and clean. 
We've actually been close to include it some months ago, but then there 
were remaining questions, vacation on my side, move to new job on your 
side etc.

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.

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

     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.

   * NEWS and CONTRIBUTORS entries.


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.


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?


 	Makarius