[isabelle-dev] NEWS: Isabelle sessions and build management

[Makarius]

On Thu, 2 Aug 2012, Gerwin Klein wrote:

> LighweightJava is a worrisome example, because it needs an external tool 
> to generate the sources which in the meantime have been updated manually 
> during maintenance, despite multiple rather prominent warnings of the 
> form:
>
>    Note:        This file should _not_ be modified directly. Please see the
>                 accompanying README file.
>
> Instead, as the README file says, the author/maintainer should be bugged 
> to update his external tool and resubmit. This can still be done 
> periodically, though, so no need for immediate action.

This is what Mercurial has to say:

hg log -l10 Lightweight_Java_Definition.thy

changeset:   2138:7cfc5c99166c
parent:      2135:e7f228c72455
user:        kleing
date:        Wed Mar 02 09:05:31 2011 +1100
LightweightJava submission by Rok Strniša

changeset:   2151:d2cbcd3d195c
user:        wenzelm
date:        Thu Mar 03 18:47:01 2011 +0100
files:       thys/LightweightJava/Lightweight_Java_Definition.thy
description:
modernized imports -- in generated (!) file;

changeset:   2314:97c459a0d76a
user:        Brian Huffman <brianh at cs.pdx.edu>
date:        Thu Aug 18 09:18:53 2011 -0700
description:
use lemma setsum_divide_distrib instead of divide.setsum

changeset:   2315:0f719fec84d2
user:        Brian Huffman <brianh at cs.pdx.edu>
date:        Thu Aug 18 14:21:06 2011 -0700
description:
revert previous commit 97c459a0d76a, which accidentally included way too 
much stuff

changeset:   2403:51c847dfb37a
user:        wenzelm
date:        Tue Sep 20 12:22:04 2011 +0200
modernized specifications;
tuned proofs;

changeset:   2499:746a395ceab4
user:        haftmann
date:        Wed Oct 12 08:06:20 2011 +0200
files:       thys/LightweightJava/Lightweight_Java_Definition.thy
description:
observe set/pred distinction (due to Larry Paulson)


BTW, I did send an email to Rok in March 2011, including some hints how 
Ott needs to be updated to work with newer versions of Isabelle.  He said 
"I will inform the Ott team of this, so they can make appropriate 
updates", which was also the last I've heard from him.


Everybody knows how such things work in practive: generated source files 
always get edited at some point.  And it is the fault of the generating 
side, not the editors. To generate a "source" file is evil by definition. 
"Source" means it is directly edited by humans, not produced by another 
tool.

Sometimes there is no way to avoid evil things, but they should not be 
declared legitimate.


>> Note that generated theory sources are not supported by isabelle build 
>> -- it simply does not fit into the concept; this is no longer shell + 
>> make scripting.
>
> So, what do we do with the entries that need them? It might not fit the 
> concept of isabelle build, but it's a legitimate, not that infrequent 
> use case for Isabelle. Maybe it is possible to kick off theory 
> generation from the ML/thy level.

Are you serious about "theory generation from the ML/thy level"?  Who is 
doing such things?

The known solution is to load other sources directly into the formal 
context, using ML or Scala functions for it.  Many tools do that already 
quite successfully, such as HOL-Boogie or HOL-SPARK.  This is also more 
stable and maintainable than the Ott-way.  BTW, Why3 has also discontinued 
the Isabelle source generation of Why2, because it was too fragile (and 
not used very often).

Conceptually, the build management is about managing a large collection of 
static sources, potentially in the presence of editing of sources by the 
user, or some other front-end.  The latter IDE aspect is particularly 
important.  There might be agents to propose edits to the user, but not 
arbitary ML code doing self-modification of the theory sources.


 	Makarius