<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#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"
cite="mid:CAEm=boy=ddZAsVQX-w6mTPjd6JhLCmY0+GBDzb0EVx7e5NQ_3w@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<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="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sun, May 19, 2019 at 8:34
PM Jason -Zhong Sheng- Hu <<a
href="mailto:fdhzs2010@hotmail.com" moz-do-not-send="true">fdhzs2010@hotmail.com</a>>
wrote:<br>
</div>
<blockquote class="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="gmail-m_-573694310022695214Signature">
<div id="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" moz-do-not-send="true">https://hustmphrrr.github.io/</a></b></font><br>
<font style="font-size:12pt" size="3"><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"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>