Re: [isabelle-dev] Spec_Check
On Tue, 25 Jun 2013, David Greenaway wrote: (There is a conceptual problem with putting such explanations into the sources, since they are built in bottom-up manner, but explanations should be more top-down; this is also relevant for worked examples that are actually run.) Again, users don't need a function-by-function running commentary of the sources, but just need to get a high-level idea of what is going on: And this is the problem: you cannot give high-level explanations in a bottom up manner. The manuals are there to do that, and people are urged to study them (over and over again). I know that many people just want to know things from a quick glancy at the header of some file, but this does not work due to the inherent complexity of what we are doing here. There is no way around spending a lot of time, both with the sources and the manuals. meaning that often the choice boils down to either having quick-and-dirty notes in the source that exist, versus polished documentation outside the sources that doesn't. Sources need to be clean by definition -- no place for quick-and-dirty things here. The manuals are usually less polished, and actually a bit removed from the sources, so that is not a problem. On this note, if you would like someone to go through and add documentation inline to the Isabelle sources, I would be willing to put my hand up to help out. (Assuming, of course, there was an interest in committing the patches, and a willing expert to review them.) Not that again. It will end up with tons of private scribbling by people who think they know something about what the sources do. We had lots of bad jokes from that department in distant past, from less clean sources. Isabelle development has emerged over several decades. Your should invest a bit more time to learn about how things work. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On Sun, 2 Jun 2013, Alexander Krauss wrote: On 05/30/2013 03:51 PM, Makarius wrote: 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. This sounds interesting. Can you point to some examples of such essays? I've come across this when studying the parallel proof support in recent ACL 6.x, e.g. http://www.cs.utexas.edu/users/moore/acl2/v6-2/distrib/acl2.tar.gz with its acl2-sources/parallel-raw.lisp and the Essay on Parallelism. There are many more such essays in the ACL2 sources. The general impression is that these guys take a lot of care of their sources and the articles that are inline here, although it is not clear how far it is formally correct in the face of changing definitions in the actual source code -- or maybe these guys are just very conservative and don't change things so much. For us, the essays with the general explanations of concepts and examples are the manuals. Just recently (d9fed6e99a57) I have managed to eliminate the last remains of the old ref manual, which was still in informal/unchecked LaTeX. The implementation manual has taken over the role of explaining concepts and the main ML entry points, and also some examples, with some degree of formal checking. That is a lot of work to maintain in any case. Just to brush up the 180 pages of old ref I've required approx. 5 years. Last week, I actually intended to make a proper exposition about Isabelle/ML futures in the implementation manual, but for now it just points to ~~/src/Pure/Concurrent/future.ML with its slightly odd Notes at the beginning. That needs to be turned into proper text outside the sources, as part of the manual. (There is a conceptual problem with putting such explanations into the sources, since they are built in bottom-up manner, but explanations should be more top-down; this is also relevant for worked examples that are actually run.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On 24/06/13 21:20, Makarius wrote: Last week, I actually intended to make a proper exposition about Isabelle/ML futures in the implementation manual, but for now it just points to ~~/src/Pure/Concurrent/future.ML with its slightly odd Notes at the beginning. That needs to be turned into proper text outside the sources, as part of the manual. As a single data-point: I personally find the Notes at the top of the file far more useful than out-of-line documentation. In particular, I never think to look in the implementation manual because only a very small percentage of the Isabelle sources are documented there. (There is a conceptual problem with putting such explanations into the sources, since they are built in bottom-up manner, but explanations should be more top-down; this is also relevant for worked examples that are actually run.) Again, users don't need a function-by-function running commentary of the sources, but just need to get a high-level idea of what is going on: I would claim that a description at the top of the file---and perhaps a few sentences on top of important functions---helps just as much as pages of carefully typeset prose. Further, the latter tends to require much more effort, meaning that often the choice boils down to either having quick-and-dirty notes in the source that exist, versus polished documentation outside the sources that doesn't. On this note, if you would like someone to go through and add documentation inline to the Isabelle sources, I would be willing to put my hand up to help out. (Assuming, of course, there was an interest in committing the patches, and a willing expert to review them.) Cheers, David The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On 05/30/2013 03:51 PM, Makarius wrote: 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. This sounds interesting. Can you point to some examples of such essays? Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On Thu, 30 May 2013, 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/ 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. Now that everything is in-place (and SML/NJ partially happy in 2bbeab01c0ea) I have realized that despite the import of theory HOL/Main, the tool does not depend on HOL at all. So it could just import Pure, and then be session Spec_Check in ~~/src/Tools/Spec_Check/. Thus it would conform to the idea of a general Quickcheck tool for Isabelle/ML -- understanding Isabelle/ML as the brand name for this cutting-edge Standard ML implementation. Of course we should avoid repeated alternation of source locations. So there is a second chance here, but then it should be really right. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Spec_Check
On Thu, 30 May 2013, Lukas Bulwahn wrote: I used the Bavarian holiday today to get the aforementioned Quickcheck tool into a stable state. The latest stable version is at: https://bitbucket.org/nicolai490/qcheck_tum I've started looking, and will come back on this in a few minites. (For now just a fresh mail thread on a fresh topic.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On 05/30/2013 05:32 PM, Makarius wrote:
On Thu, 30 May 2013, Lukas Bulwahn wrote:
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.
Do you know how to define the ML antiquotation, or shall I do it?
Please go ahead and do it when you have time.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
There is a funny comment here: http://isabelle.in.tum.de/repos/isabelle/file/cdba0c3cb4c2/src/HOL/Spec_Check/base_generator.ML#l94 (* Isabelle does not use vectors? *) Isn't live nice without vectors, arrays, a host of int types that are not int at all? The one exception is src/Pure/Syntax/parser.ML, where arrays are used internally due to some historic optimization. It probably wastes a lot of space, since every grammar update needs a fresh copy of the whole thing. Working routinely on the JVM now (due to Scala), I've found so many inefficiencies in the libraries due to the historic predominance of these mutable bulk data structures (aka arrays). This is particularly bad when working with plain text, aka strings. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
