[Agda] [ANNOUNCE] Agda 2.5.1

[Thorsten Altenkirch]

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<mailto:agda-bounces at lists.chalmers.se>> on behalf of Ulf Norell <ulf.norell at gmail.com<mailto:ulf.norell at gmail.com>>
Date: Wednesday, 20 April 2016 14:48
To: Harley Eades III <harley.eades at gmail.com<mailto:harley.eades at gmail.com>>
Cc: Agda users <agda at lists.chalmers.se<mailto: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<mailto: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<mailto: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<mailto: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<mailto: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/20160423/1efa3bbd/attachment.html