[Agda] [ANNOUNCE] Agda 2.5.1

[Ulf Norell]

http://agda.readthedocs.org/en/latest/tools/package-system.html

/ Ulf

On Sun, Apr 24, 2016 at 12:45 AM, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Hi,
>
> I just installed the latest version and noticed that include-dirs doesn’t
> show up in agda2 mode under emacs. I guess this has to do with the new
> library management system (in which case the online documentation needs to
> be updated). How do I set it up to use the standard library?
>
> Cheers,
> Thorsten
>
> From: <agda-bounces at lists.chalmers.se> on behalf of Ulf Norell <
> ulf.norell at gmail.com>
> Date: Wednesday, 20 April 2016 14:48
> To: Harley Eades III <harley.eades at gmail.com>
> Cc: Agda users <agda at lists.chalmers.se>
> Subject: Re: [Agda] [ANNOUNCE] Agda 2.5.1
>
> Unless you have multiple Agda files needing different libraries in the
> same directory, the suggested way to do this is adding a .agda-lib file
> with a 'depend:' field to the directory (or a parent directory) containing
> the code.
>
> / Ulf
>
> On Wed, Apr 20, 2016 at 3:11 PM, Harley Eades III <harley.eades at gmail.com>
> wrote:
>
>> Hi, everyone.
>>
>> On Apr 20, 2016, at 5:14 AM, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
>> wrote:
>>
>> On 17 April 2016 at 00:54, Andrés Sicard-Ramírez <asr at eafit.edu.co>
>> wrote:
>> > Dear all,
>> >
>> > The Agda Team is very pleased to announce the release of Agda 2.5.1.
>>
>> I have a question about the new Library management features.
>>
>> I would like to be able to specify which named library to use from within
>> an .agda file. I hoped
>>
>> {-# OPTIONS --library=foo #-}
>>
>> would do it, but Agda says
>>
>> Unrecognized option: --library=foo
>>
>> so I guess this way of specifying a library is not possible — or did I
>> get the syntax wrong?
>>
>>
>> I was also hoping for this.  Are there any plans to add it?  It would
>> simplify things a lot.
>>
>> Best,
>> Harley
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160424/cf4ad2d5/attachment.html