<div dir="ltr">Having got Agda 2.4.2 installed using cabal, and found everything to work, after reboot, it has stopped working, with the same problem as before.<div><br></div><div>I can find Agda/Primitive.agda in </div><div><br></div><div><div>~/.cabal/share/Agda-2.4.2.2/lib/prim/Agda/Primitive.agda</div><div>~/.local/share/Trash/files/Agda-2.4.2.2/src/data/lib/prim/Agda/Primitive.agda</div></div><div><br></div><div>I assume it's the first one I want.</div><div><br></div><div>If I type:</div><div><br></div><div>echo $Agda_datadir</div><div><br></div><div>I get nothing, so I guess my problem is that cabal install isn't permanently setting this environment variable, and I should set it myself in my .bash_profile.</div><div><br></div><div>But if I first do:</div><div><br></div><div>export Agda_datadir=/.cabal/share/Agda-2.4.2.2/lib/prim/Agda/Primitive.agda</div><div><br></div><div>it doesn't help.</div><div> -v 20 doesn't reveal anything interesting either. How am I supposed to set this library search path?</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 2 May 2015 at 14:43, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Agda.Primitive is a boot-module that should be shipped with agda.<br>
<br>
Can you locate Agda/Primitive.agda ?<br>
<br>
If you install Agda via cabal, it is e.g. in<br>
<br>
abel@agda2:~/.cabal/share/x86_64-linux-ghc-7.8.3/Agda-2.4.3/lib/prim$ l Agda/<br>
-rw-r--r-- 1 abel abel 885 Mai 2 15:31 Primitive.agda<br>
<br>
If you call Agda with the extra option<br>
<br>
-v import.main:20<br>
<br>
it should print something like (among possibly other things)<br>
<br>
Importing the primitive modules.<br>
Library dir = "/home/abel/.cabal/share/x86_64-linux-ghc-7.8.3/Agda-2.4.3/lib"<br>
Done importing the primitive modules.<br>
<br>
This directory is obtained from the environment variable<br>
<br>
Agda_datadir<br>
<br>
Maybe this helps to get your debugging process started...<br>
<br>
Cheers,<br>
Andreas<div><div class="h5"><br>
<br>
On 02.05.2015 14:56, Colin Adams wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Agda beginner here.<br>
<br>
I've checked out <a href="https://github.com/hott/hott-agda/" target="_blank">https://github.com/hott/hott-agda/</a> and tried typing:<br>
<br>
make html<br>
<br>
in order to build index.html. But it appears I need to set up something<br>
in the environment first, as I get:<br>
<br>
[colin@localhost HoTT-Agda]$ make html<br>
rm -f<br>
agda index.agda --html<br>
Checking index (/home/colin/HoTT-Agda/index.agda).<br>
Checking homotopy.LoopSpaceCircle<br>
(/home/colin/HoTT-Agda/homotopy/LoopSpaceCircle.agda).<br>
Checking HoTT (/home/colin/HoTT-Agda/HoTT.agda).<br>
Checking lib.Basics (/home/colin/HoTT-Agda/lib/Basics.agda).<br>
Checking lib.Base (/home/colin/HoTT-Agda/lib/Base.agda).<br>
/home/colin/HoTT-Agda/lib/Base.agda:30,13-27<br>
Failed to find source of module Agda.Primitive in any of the<br>
following locations:<br>
/home/colin/HoTT-Agda/Agda/Primitive.agda<br>
/home/colin/HoTT-Agda/Agda/Primitive.lagda<br>
when scope checking the declaration<br>
open import Agda.Primitive public<br>
using (lzero)<br>
renaming (Level to ULevel; lsuc to lsucc;<br>
_⊔_ to lmax)<br>
Makefile:9: recipe for target 'html' failed<br>
make: *** [html] Error 1<br>
<br>
Typing agda --help suggests to me that I edit Makefile to add some -I<br>
directives, but presumably this shouldn't be necessary. I have Agda<br>
2.3.2 installed (via yum install Agda - I'm using Fedora 21).<br>
<br>
What steps am I missing?<br>
<br>
<br></div></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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
</font></span></blockquote></div><br></div>