[isabelle] Structuring a Modular Project

[scott constable]

Hi All,

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.
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
2. Expect any project which uses A and/or B to import them by providing
a path in the preamble, for example
theory P imports "<path-to-A>/A" "<path-to-B>/B" begin

I'm not fond of option 1 because it requires building two heaps which
amount to ~500MB, and requires the user to invoke Isabelle/JEdit from the
command line with paths to A and/or B. I'm also not fond of option 2
because then the user must hardcode into .thy file in his/her own project
the path to A or to B. Thus source code will become less portable. Are
there any better options?

Thanks in advance,

Scott Constable

[G***@data61.csiro.au]

There are two more:

3. <path-to-A> can be a relative path and you could expect the user to put A and B in specific relative locations to where they are used (e.g. using symlinks).

4. use "$A_HOME/A” in the import statement (i.e. a variable) and expect the user to have that variable set

Cheers,
Gerwin

Post by scott constable
Hi All,
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.
1. Configure A and B each with a Makefile which performs, for example,
$ isabelle build -b -d . A
2. Expect any project which uses A and/or B to import them by providing
a path in the preamble, for example
theory P imports "<path-to-A>/A" "<path-to-B>/B" begin
I'm not fond of option 1 because it requires building two heaps which
amount to ~500MB, and requires the user to invoke Isabelle/JEdit from the
command line with paths to A and/or B. I'm also not fond of option 2
because then the user must hardcode into .thy file in his/her own project
the path to A or to B. Thus source code will become less portable. Are
there any better options?
Thanks in advance,
Scott Constable

[Lars Hupel]

Hi,

Post by scott constable
1. Configure A and B each with a Makefile which performs, for example,
$ isabelle build -b -d . A
I'm not fond of option 1 because it requires building two heaps which
amount to ~500MB, and requires the user to invoke Isabelle/JEdit from the
command line with paths to A and/or B.

the upcoming Isabelle 2016-1 release features "incremental" heap images;
that is, heaps won't be cumulative anymore. That will drastically reduce
the total size of your ".isabelle" directory.

Note that it is impossible to "join" two different heap images: Each
Isabelle session must have exactly one parent. So when you want to
declare a "ROOT" file for your project "P", you have to choose either
"A" or "B" as the parent (or choose "HOL" instead). The other theories
then have to be imported, as Gerwin indicated, by either relative or
parametrized paths.

In the AFP, it is customary to use the relative path convention *inside*
the repository. But from the outside, users usually register the AFP as
a "component", so that they can write

imports "$AFP/Collections/..."

If looks like in your case, relative paths seem to be the way to go. You
could also consider using Git submodules for "A" and "B" in "P"; that
way, your users don't have to manually clone "A" and "B" to the expected
locations.

Cheers
Lars

[Makarius]

Post by scott constable
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.)

Post by scott constable
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

[scott constable]

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

Post by scott constable

Post by scott constable
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

Post by scott constable
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.)

Post by scott constable
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