Re: [isabelle] Structuring a Modular Project



On 20/09/16 17:33, scott constable wrote:
> 
> I'm working on a medium-sized project with two libraries, call them A and
> B, and a main project P which uses A and B. A and B are both general enough
> that many other projects could use them, i.e. I want them to be treated
> like static libraries. Eventually I would like to post A, B, and P on
> Github so that others can use A and B independently, or use P with A and B.

The canonical way is to post things to the Archive of Formal Proofs
https://www.isa-afp.org -- once they have reached a certain maturity and
stability.

Material on AFP has the advantage that it follows changes of Isabelle
"automagically". Sometimes people have tried to follow Isabelle releases
independently (e.g. see
https://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html), but
usually there comes a point where isolated projects are longer updated
and thus fall into decay. (Luckily the CSP-Prover guys seem to have made
it again for Isabelle2016, after some years stagnation.)


> Right now it looks like these are my two options:
> 
>    1. Configure A and B each with a Makefile which performs, for example,
>    $ isabelle build -b -d . A

What is the purpose of the Makefile here? Dependencies are already
managed by isabelle build and the ROOT files. Also note that "make"
tools are not portable and merely cause problems to users. We managed to
get rid of make in Isabelle2012.

Generally, Isabelle session heap images should not be taking too
seriously. This is not a C compiler that turns .c into .o files. It is
more like a "dumped world snapshot" like in the old LISP times. This
aspect might become again more visible, when the Isabelle Prover IDE
supports its own model of persistence, without command-line builds
getting in the way.

In Isabelle2016 we still see a bit of a hybrid of quasi-static builds,
but the general move is away from it. Think of it is a formal word
processor that somehow provides ways to make system snapshots persistent.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.