[isabelle] Structuring a Modular Project



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



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