<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
quote a part from the doc:</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<blockquote style="margin-top: 0px; margin-bottom: 0px;">
<p>To be found by Agda a library file has to be listed (with its full path) in a <code>
<span>libraries</span></code> file</p>
<ul>
<li><code><span>AGDA_DIR/libraries-VERSION</span></code>, or if that doesn’t exist</li><li><code><span>AGDA_DIR/libraries</span></code></li></ul>
<p>where <code><span>VERSION</span></code> is the Agda version (for instance <code>
<span>2.5.1</span></code>). </p>
</blockquote>
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
This method works for 2.6, but not for 2.5.4.2. but for 2.6, since it uses libraries-2.6 first, I just make libaries-2.5.4.2 to be libraries and everything works well.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Jason -Zhong Sheng- Hu <fdhzs2010@hotmail.com><br>
<b>Sent:</b> May 20, 2019 4:20 PM<br>
<b>To:</b> a.j.rouvoet; agda@lists.chalmers.se<br>
<b>Subject:</b> Re: [Agda] Load libraries based on version?</font>
<div> </div>
</div>
<style type="text/css" style="display:none">
<!--
p
{margin-top:0;
margin-bottom:0}
-->
</style>
<div dir="ltr">
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
Hi all,</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
thx Guillaume, I found it in the doc:</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#installing-libraries" id="LPlnk624454">https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#installing-libraries</a></div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
I will try if it works.</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
Arjen, you are right. it's very good for projects, and submodule can make everything consistent. I should probably do it. but it would also be useful for a global configuration when the goal is to quickly try things out.<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div id="x_Signature">
<div></div>
<div id="x_divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font size="3" style="font-size:12pt"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
<div id="x_appendonsend"></div>
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="x_divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" color="#000000" style="font-size:11pt"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of a.j.rouvoet <a.j.rouvoet@gmail.com><br>
<b>Sent:</b> May 20, 2019 5:39 AM<br>
<b>To:</b> agda@lists.chalmers.se<br>
<b>Subject:</b> Re: [Agda] Load libraries based on version?</font>
<div> </div>
</div>
<div style="background-color:#FFFFFF">Alternatively you can checkout the libraries you need in your project in a `lib/` directory and use the project local `.agda-lib` file to<br>
include the paths by default on the project's agda path:<br>
<br>
name: example<br>
include:<br>
./src/<br>
./lib/stdlib.agda/src/<br>
./lib/cubical.agda/<br>
<br>
This works really well and has the additional benefit to be self contained.<br>
<br>
Arjen<br>
<br>
On 5/19/19 8:39 PM, Jesper Cockx wrote:<br>
<blockquote type="cite">
<div dir="ltr">
<div>This is currently not possible as far as I'm aware. You could try to just have different .agda folders and switch between them when you switch agda versions.</div>
<div><br>
</div>
<div>-- Jesper<br>
</div>
</div>
<br>
<div class="x_x_gmail_quote">
<div dir="ltr" class="x_x_gmail_attr">On Sun, May 19, 2019 at 8:34 PM Jason -Zhong Sheng- Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> wrote:<br>
</div>
<blockquote class="x_x_gmail_quote" style="margin:0px 0px 0px
0.8ex; border-left:1px solid rgb(204,204,204); padding-left:1ex">
<div dir="ltr">
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
Hi all,</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
since Agda and libraries aren't really in the most stable state, I figured it might be useful to use multiple versions of Agda for different things. My question is, is there a way to load libraries based on Agda's version? I am currently managing libraries
using ~/.agda folder. It would be nice if somehow there are configuration files that can tell what version to load what.<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div id="x_x_gmail-m_-573694310022695214Signature">
<div id="x_x_gmail-m_-573694310022695214divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b><a href="https://hustmphrrr.github.io/" target="_blank">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3" style="font-size:12pt"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"></span></span></font></div>
</div>
</div>
_______________________________________________<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>
</blockquote>
</div>
<br>
<fieldset class="x_x_mimeAttachmentHeader"></fieldset>
<pre class="x_x_moz-quote-pre">_______________________________________________
Agda mailing list
<a class="x_x_moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="x_x_moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</div>
</div>
</body>
</html>