<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>