<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    At some point I was looking for similar functionality, but am very
    content now using git sub-modules for tracking<br>
    specific versions of "funky" dependencies in the project repository.<br>
    <br>
    Assuming you are using git and that your dependencies are tracked in
    git, this makes it very easy to pull in the <br>
    correct versions and instead of using the 'depend' key in your
    .agda-lib file, you use the project-root relative<br>
    include paths.<br>
    <br>
    For an example see the following .agda-lib file and makefile in this
    repository [1].<br>
    The makefile is set up to do all the work for you when you run
    `make`.<br>
    <br>
    [1]: <a class="moz-txt-link-freetext" href="https://github.com/metaborg/mj.agda/">https://github.com/metaborg/mj.agda/</a><br>
    <br>
    Cheers,<br>
    <br>
    <br>
    Arjen<br>
    <br>
    <div class="moz-cite-prefix">On 11/10/2017 07:24 PM, Ulf Norell
      wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAJjNqYGeV8T-tesGkV7nbUf6SGHPqA+qyPfWm-KBB3sVU6gaoQ@mail.gmail.com">
      <div dir="ltr">One possibility might be to add support for local
        'libraries' files. That way you could distribute
        <div>your project together with a special libraries file for the
          funky dependencies, without cluttering</div>
        <div>the agda-lib file with explicit paths.</div>
        <div><br>
        </div>
        <div>/ Ulf</div>
        <div class="gmail_extra"><br>
          <div class="gmail_quote">On Fri, Nov 10, 2017 at 4:51 PM,
            Frederik Hanghøj Iversen <span dir="ltr"><<a
                href="mailto:fhi.1990@gmail.com" target="_blank"
                moz-do-not-send="true">fhi.1990@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 dir="ltr">I'm reading up on library management in
                Agda[1]. From what I gather it is not possible to
                install a certain library to be used in a specific
                project. Is this correct?
                <div><br>
                </div>
                <div>What I'm hoping for is the possibility to put
                  something like the following in my .agda-lib file:</div>
                <div><br>
                </div>
                <div>
                  <div>name: my-project</div>
                  <div>depend:</div>
                  <div>  funky-dep</div>
                  <div>include:</div>
                  <div>  src</div>
                  <div>libs:</div>
                  <div>  path-to-funky-dep</div>
                  <div><br>
                  </div>
                  <div>Where funky-dep is some dependencies I don't want
                    to make available to all agda projects on my
                    machine, but rather just for the purpose of
                    developing "my-project".</div>
                  <div><br>
                  </div>
                  <div>Is this is possible it would also make it a lot
                    easier to share code with other people. That way you
                    can package your code along with all it's
                    dependencies and you don't need the recipient to
                    make changes to their global configuration.</div>
                  <div><br>
                  </div>
                  <div>The way I understand it, at the moment it's only
                    possible to add path-to-funky-dep to
                    $AGDA_DIR/libraries (as per [1]).</div>
                  <div><br>
                  </div>
                  <div>[1]: <a
href="http://agda.readthedocs.io/en/v2.5.2/tools/package-system.html?highlight=agda-lib#installing-libraries"
                      target="_blank" moz-do-not-send="true">http://agda.readthedocs.<wbr>io/en/v2.5.2/tools/package-<wbr>system.html?highlight=agda-<wbr>lib#installing-libraries</a><span
                      class="HOEnZb"><font color="#888888"><br>
                      </font></span></div>
                </div>
                <span class="HOEnZb"><font color="#888888">
                    <div>
                      <div>
                        <div><br>
                        </div>
                        -- <br>
                        <div
                          class="m_-7665249937735035722gmail_signature">
                          <div>Regards</div>
                          <div><i>Frederik Hanghøj Iversen</i></div>
                        </div>
                      </div>
                    </div>
                  </font></span></div>
              <br>
              ______________________________<wbr>_________________<br>
              Agda mailing list<br>
              <a href="mailto:Agda@lists.chalmers.se"
                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/<wbr>mailman/listinfo/agda</a><br>
              <br>
            </blockquote>
          </div>
          <br>
        </div>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <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>
    <br>
  </body>
</html>