<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;">
<div>Thank you : this did the trick.</div>
<div><br>
</div>
<div>I figured out what to put into libraries but I missed out on defaults. </div>
<div><br>
</div>
<div>Cheers,</div>
<div>Thorsten</div>
<div><br>
</div>
<span id="OLK_SRC_BODY_SECTION">
<div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt">
<span style="font-weight:bold">From: </span>John Leo <<a href="mailto:leo@halfaya.org">leo@halfaya.org</a>><br>
<span style="font-weight:bold">Date: </span>Sunday, 24 April 2016 14:02<br>
<span style="font-weight:bold">To: </span>Thorsten Altenkirch <<a href="mailto:thorsten.altenkirch@nottingham.ac.uk">thorsten.altenkirch@nottingham.ac.uk</a>><br>
<span style="font-weight:bold">Cc: </span>Ulf Norell <<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>>, Agda users <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>
<span style="font-weight:bold">Subject: </span>Re: [Agda] [ANNOUNCE] Agda 2.5.1<br>
</div>
<div><br>
</div>
<div>
<div>
<div dir="ltr">My personal setup, which works, is this.
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>I have the standard library installed in /Users/leo/agda/agda-stdlib</div>
<div><br>
</div>
<div>Now in ~/.agda, there are two files "defaults" and "libraries".</div>
<div><br>
</div>
<div>The file "defaults" has as contents the single line:</div>
<div>agda-stdlib<br>
</div>
<div><br>
</div>
<div>
<div>The file "libraries" has as contents the single line:</div>
</div>
<div>/Users/leo/agda/agda-stdlib/agda-stdlib.agda-lib<br>
</div>
<div><br>
</div>
<div>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".</div>
<div><br>
</div>
<div>John</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Sun, Apr 24, 2016 at 12:57 AM, Thorsten Altenkirch <span dir="ltr">
<<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="auto">
<div>I have read this but I don't know how to include the standard library. <br>
<br>
Sent from my iPhone</div>
<div><br>
On 24 Apr 2016, at 07:12, Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>> wrote:<br>
<br>
</div>
<blockquote type="cite">
<div>
<div dir="ltr"><a href="http://agda.readthedocs.org/en/latest/tools/package-system.html" target="_blank">http://agda.readthedocs.org/en/latest/tools/package-system.html</a><br>
<div><br>
</div>
<div>/ Ulf</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Sun, Apr 24, 2016 at 12:45 AM, Thorsten Altenkirch <span dir="ltr">
<<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif">
<div>Hi,</div>
<div><br>
</div>
<div>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?</div>
<div><br>
</div>
<div>Cheers,</div>
<div>Thorsten</div>
<div><br>
</div>
<span>
<div style="font-family:Calibri;font-size:11pt;text-align:left;color:black;BORDER-BOTTOM:medium none;BORDER-LEFT:medium none;PADDING-BOTTOM:0in;PADDING-LEFT:0in;PADDING-RIGHT:0in;BORDER-TOP:#b5c4df 1pt solid;BORDER-RIGHT:medium none;PADDING-TOP:3pt">
<span style="font-weight:bold">From: </span><<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>><br>
<span style="font-weight:bold">Date: </span>Wednesday, 20 April 2016 14:48<br>
<span style="font-weight:bold">To: </span>Harley Eades III <<a href="mailto:harley.eades@gmail.com" target="_blank">harley.eades@gmail.com</a>><br>
<span style="font-weight:bold">Cc: </span>Agda users <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<span style="font-weight:bold">Subject: </span>Re: [Agda] [ANNOUNCE] Agda 2.5.1<br>
</div>
<div>
<div>
<div><br>
</div>
<div>
<div>
<div dir="ltr">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.
<div><br>
</div>
<div>/ Ulf</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Wed, Apr 20, 2016 at 3:11 PM, Harley Eades III <span dir="ltr">
<<a href="mailto:harley.eades@gmail.com" target="_blank">harley.eades@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word">Hi, everyone.<span>
<div><br>
<div>
<blockquote type="cite">
<div>On Apr 20, 2016, at 5:14 AM, Andrew Pitts <<a href="mailto:Andrew.Pitts@cl.cam.ac.uk" target="_blank">Andrew.Pitts@cl.cam.ac.uk</a>> wrote:</div>
<br>
<div>
<div dir="ltr">On 17 April 2016 at 00:54, Andrés Sicard-Ramírez <<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>> wrote:<br>
> Dear all,<br>
><br>
> The Agda Team is very pleased to announce the release of Agda 2.5.1.<br>
<br>
I have a question about the new Library management features. <br>
<br>
I would like to be able to specify which named library to use from within an .agda file. I hoped<br>
<br>
{-# OPTIONS --library=foo #-}<br>
<br>
would do it, but Agda says<br>
<br>
Unrecognized option: --library=foo<br>
<br>
so I guess this way of specifying a library is not possible — or did I get the syntax wrong?</div>
</div>
</blockquote>
<br>
</div>
</div>
</span>
<div>I was also hoping for this. Are there any plans to add it? It would simplify things a lot.</div>
<div><br>
</div>
<div>Best,</div>
<div>Harley</div>
</div>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote>
</div>
<br>
</div>
</div>
</div>
</div>
</div>
</span>
<pre>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.
</pre>
</div>
</blockquote>
</div>
<br>
</div>
</div>
</blockquote>
<pre>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.
</pre>
</div>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote>
</div>
<br>
</div>
</div>
</div>
</span>
<PRE>
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.
</PRE></body>
</html>