[Agda] [ANNOUNCE] Agda 2.5.1

[John Leo]

My personal setup, which works, is this.

I rely on the default value of AGDA_DIR, which is ~/.agda (on my machine ~
is /Users/leo, although this doesn't matter for the following).  Make sure
you haven't modified this, or if you have modified it, put everything there
instead.  It's been a while and I don't remember, but I might have tried to
modify this before, but had trouble getting it picked up properly, so I
just stuck with the default.

I have the standard library installed in /Users/leo/agda/agda-stdlib

Now in ~/.agda, there are two files "defaults" and "libraries".

The file "defaults" has as contents the single line:
agda-stdlib

The file "libraries" has as contents the single line:
/Users/leo/agda/agda-stdlib/agda-stdlib.agda-lib

A similar setup should work for you, with the only change being the
location of the standard library and the path to that in "libraries".

John

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

> I have read this but I don't know how to include the standard library.
>
> Sent from my iPhone
>
> On 24 Apr 2016, at 07:12, Ulf Norell <ulf.norell at gmail.com> wrote:
>
> 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.
>>
>>
>
>
> 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.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160424/afc46e82/attachment.html