Re: [isabelle] Structuring a Modular Project



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

> On 21.09.2016, at 01:33, scott constable <sdconsta at syr.edu> wrote:
> 
> 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.