<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><br><div>According to the documentation (<a href="https://agda.readthedocs.io/en/latest/tools/package-system.html#installing-libraries">https://agda.readthedocs.io/en/latest/tools/package-system.html#installing-libraries</a>)</div><div>the `.agda` directory is <font face="arial, helvetica, sans-serif" color="#000000">called `<span style="white-space:nowrap">C:\Users\USERNAME\AppData\Roaming\agda` on Windows.</span></font></div><div><font face="arial, helvetica, sans-serif" color="#000000"><span style="white-space:nowrap"><br></span></font></div><div><font face="arial, helvetica, sans-serif" color="#000000"><span style="white-space:nowrap">/ Ulf</span></font></div></div></div></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">On Fri, Feb 8, 2019 at 2:44 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB">
<div class="gmail-m_-2245301413255194614WordSection1">
<p class="MsoNormal"><span style="font-size:11pt">Hi,<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">I am currently running a module using agda and was trying to help a student installing agda on windows. So far I have failed but maybe somebody can give me some advice. Or better produce an installer that
 installed emacs+agda+libraries on a windows machine.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">The first problem was that agda-locate couldn’t find emacs. Ok, instead I just copied the code into .emacs. That seemed to work. However, I had no fun with the library. I created the .agda directory with libraries
 and the correct content but no effect. I guess it is looking somewhere else but where. When I try to run files from inside the library it complains that it cannot update some .agdai files. I guess this may be because the agda version and library version don’t
 match?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">Any advice?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">Cheers,<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">Thorsten<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">P.S.<u></u><u></u></span></p>
<p style="margin:0cm 0cm 0.0001pt"><span style="font-size:12pt;color:black">Agda version 2.5.4.2<u></u><u></u></span></p>
<p style="margin:0cm 0cm 0.0001pt;font-variant-caps:normal;text-align:start;word-spacing:0px">
<span style="font-size:12pt;color:black">windows 10<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">agda library v.0.17 (I think)<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.



</pre></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></div>