<div dir="ltr"><div>I was referring to $HOME/.agda/libraries.</div><div><br></div>See here for more information:<div><br></div><div><a href="https://agda.readthedocs.io/en/latest/tools/package-system.html">https://agda.readthedocs.io/en/latest/tools/package-system.html</a><br></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 8, 2016 at 10:03 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Thu, 2016-12-08 at 21:43 +0100, Ulf Norell wrote:<br>
> You just need to put the path to the .agda-lib file in<br>
> your .agda/libraries file.<br>
> No further installation should be required.<br>
><br>
<br>
</span>I see agda/standard-library.agda-lib<br>
<br>
but do not see .agda/libraries<br>
anywhere.<br>
<br>
On the other hand, I use $adgaStLib in the command line<br>
that points to agda/std-lib/src,<br>
and it seems working.<br>
(?)<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
> On Thu, Dec 8, 2016 at 9:09 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
> On Thu, 2016-12-08 at 22:43 +0300, Sergei Meshveliani wrote:<br>
> > On Thu, 2016-12-08 at 19:30 +0100, Ulf Norell wrote:<br>
> > > Each commit of Agda contains a reference to the particular<br>
> commit of<br>
> > > the standard library<br>
> > > that it has been tested with. To find out which one you<br>
> can do the<br>
> > > following (after checking<br>
> > ><br>
> > > out the commit of Agda that you are interested in):<br>
> > ><br>
> > ><br>
> > > $ git submodule init<br>
> > > Submodule 'std-lib' (<a href="https://github.com/agda/agda-stdlib" rel="noreferrer" target="_blank">https://github.com/agda/agda-<wbr>stdlib</a>)<br>
> registered<br>
> > > for path 'std-lib'<br>
> > > $ git submodule update<br>
> > > Cloning into 'std-lib'...<br>
> > > Submodule path 'std-lib': checked out<br>
> > > '<wbr>7220ca3ee025e9339aa8e5d11efcd0<wbr>69764e7977'<br>
> > > $ cd std-lib<br>
> > > $ git status<br>
> > > HEAD detached at 7220ca3<br>
> > ><br>
> > ><br>
> > > So the commit of the standard library that works with the<br>
> Agda commit<br>
> > > I tested this on is<br>
> > > 7220ca3. This is probably the easiest way for your users<br>
> to get a<br>
> > > compatible version of<br>
> > > the standard library as well, saving them the trouble of<br>
> keeping track<br>
> > > of two commit hashes.<br>
> > ><br>
> ><br>
> ><br>
> > I am trying to find out what is the whole installation<br>
> process.<br>
> ><br>
> > For example, I have downloaded agda-2.5.2-dc9ffae<br>
> > by running the commands<br>
> ><br>
> > > git clone <a href="https://github.com/agda/agda.git" rel="noreferrer" target="_blank">https://github.com/agda/agda.<wbr>git</a><br>
> > > cd agda<br>
> > > git checkout dc9ffae<br>
> ><br>
> > Then I install Agda by<br>
> ><br>
> > > cabal update<br>
> > > cabal install<br>
> > > agda-mode compile<br>
> ><br>
> > Then I need to download the needed Standard library version.<br>
> > To do this, I command<br>
> ><br>
> > > cd agda<br>
> > > git submodule init<br>
> > Submodule 'std-lib' (<a href="https://github.com/agda/agda-stdlib" rel="noreferrer" target="_blank">https://github.com/agda/agda-<wbr>stdlib</a>)<br>
> > registered for path 'std-lib'<br>
> ><br>
> > > git submodule update<br>
> > Cloning into std-lib...<br>
> > ...<br>
> > Submodule path 'std-lib': checked out<br>
> > '<wbr>7220ca3ee025e9339aa8e5d11efcd0<wbr>69764e7977'<br>
> ><br>
> > > cd std-lib<br>
> ><br>
> > Initially this directory was empty. And now is has the files<br>
> of the<br>
> > needed library version.<br>
> > Right?<br>
> ><br>
> > To install the library, I command<br>
> ><br>
> > > cabal install<br>
><br>
><br>
><br>
> But there is not any .cabal file.<br>
> And I have an impression that<br>
><br>
> > git submodule update<br>
><br>
> has already installed the needed library.<br>
><br>
> ------<br>
> Sergei<br>
><br>
> ______________________________<wbr>_________________<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/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
><br>
<br>
<br>
</div></div></blockquote></div><br></div>