Re: [isabelle] Structuring a Modular Project



Thanks to everyone for the responses. The reason I'm using a Makefile is
because several of the theories are being generated by ott, and Make helps
to coordinate that process; at the moment I don't see a feasible
cross-platform option.

The solution I'm leaning towards is one where A, B, and P can be their own
standalone git repositories, but the use of P expects A and B to be cloned
within P at pre-specified locations. This is analogous to the way the
LLVM/clang project is set up: LLVM and clang must be cloned in specific
locations relative to one another.

Scott

On Wed, Sep 21, 2016 at 5:16 AM, Makarius <makarius at sketis.net> wrote:

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