Re: [isabelle] Structuring a Modular Project



Hi,

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




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