Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type



On 20/02/2012, at 7:55 AM, Brian Huffman wrote:

> On Sun, Feb 19, 2012 at 9:19 PM, Makarius <makarius at sketis.net> wrote:
>>> - installing entries (+ dependencies; something like cabal for Haskell)
>> 
>> What means "installing"?  Once we have a proper session specification in the
>> source trees (not ROOT.ML nor IsaMakefile) you merely point to such points
>> in the file space without "installation".  Or did you mean installation of
>> so-called Isabelle components?
> 
> I would interpret "installing" to mean downloading theory files and
> putting them into an appropriate place in the user's filesystem. After
> "installing" an entry or theory library, users should be able to
> easily import that library into their own theory files, by writing
> something reasonable on the "imports" line (i.e., no absolute or
> user-specific path names, but rather something portable that would
> work also for anyone else who has installed the same library).

Yes, that would be precisely the idea.

It may be enough to just put a download of the entire AFP wherever the users wants and add the appropriate line to the user components file. Florian has basically already done the rest. The AFP is still of a size where we don't really need to disentangle separate entries.

Dependency management is then reduced to downloading the version of the AFP that fits to the Isabelle version the user has installed.

Cheers,
Gerwin






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