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



On 20/02/2012, at 10:53 PM, Makarius wrote:

> On Mon, 20 Feb 2012, Gerwin Klein wrote:
> 
>> 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.
> 
> This sounds good.  The whole download is approx. 7MB compressed and 43MB uncompressed.  This is tiny compared with the main Isabelle distribution.
> 
> By providing a suitable etc/settings its file-space can be easily injected into Isabelle via some $AFP variable.  So imports can refer to theories like "$AFP/Foo/Bar".

Yes, exactly.


>> Florian has basically already done the rest. The AFP is still of a size where we don't really need to disentangle separate entries.
> 
> This probably refers to http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/5b970f669325

Yes.


> Florian has called it "rudimentary support for AFP as Isabelle component", but it looks fine to be.  The remaining odditiy is that is unavailable for actual users: the official downloads of AFP only contain the content of the thys directory, without this etc/settings file.

Good point. That can easily be fixed.

Gerwin






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