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



On 02/20/2012 06:45 AM, Gerwin Klein wrote:

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.
Yes that was what I meant.

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.
I guess it would suffice, but I was more thinking of the following (again, like cabal for Haskell): you type on your machine the entry that you want to install, e.g.,

$ afp install Refine_Monadic

and then the above (i.e., downloading theory files and putting them into an appropriate place in the filesystem) happens for all files from the afp on which Refine_Monadic does depend on. Afterwards (as Brian pointed out) it should be possible without further ado, to import the "installed" entry in your own theories in a way that does not depend on any local setup.

cheers

chris





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