[Agda] Can't build index.html in HoTT-Agda repository

[Colin Adams]

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.

I can find Agda/Primitive.agda in

~/.cabal/share/Agda-2.4.2.2/lib/prim/Agda/Primitive.agda
~/.local/share/Trash/files/Agda-2.4.2.2/src/data/lib/prim/Agda/Primitive.agda

I assume it's the first one I want.

If I type:

echo $Agda_datadir

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.

But if I first do:

export Agda_datadir=/.cabal/share/Agda-2.4.2.2/lib/prim/Agda/Primitive.agda

it doesn't help.
 -v 20 doesn't reveal anything interesting either. How am I supposed to set
this library search path?


On 2 May 2015 at 14:43, Andreas Abel <abela at chalmers.se> wrote:

> Agda.Primitive is a boot-module that should be shipped with agda.
>
> Can you locate Agda/Primitive.agda ?
>
> If you install Agda via cabal, it is e.g. in
>
>   abel at agda2:~/.cabal/share/x86_64-linux-ghc-7.8.3/Agda-2.4.3/lib/prim$ l
> Agda/
>   -rw-r--r-- 1 abel abel  885 Mai  2 15:31 Primitive.agda
>
> If you call Agda with the extra option
>
>   -v import.main:20
>
> it should print something like (among possibly other things)
>
>   Importing the primitive modules.
>   Library dir =
> "/home/abel/.cabal/share/x86_64-linux-ghc-7.8.3/Agda-2.4.3/lib"
>   Done importing the primitive modules.
>
> This directory is obtained from the environment variable
>
>   Agda_datadir
>
> Maybe this helps to get your debugging process started...
>
> Cheers,
> Andreas
>
>
> On 02.05.2015 14:56, Colin Adams wrote:
>
>> Agda beginner here.
>>
>> I've checked out https://github.com/hott/hott-agda/ and tried typing:
>>
>> make html
>>
>> in order to build index.html. But it appears I need to set up something
>> in the environment first, as I get:
>>
>> [colin at localhost HoTT-Agda]$ make html
>> rm -f
>> agda index.agda --html
>> Checking index (/home/colin/HoTT-Agda/index.agda).
>>   Checking homotopy.LoopSpaceCircle
>> (/home/colin/HoTT-Agda/homotopy/LoopSpaceCircle.agda).
>>    Checking HoTT (/home/colin/HoTT-Agda/HoTT.agda).
>>     Checking lib.Basics (/home/colin/HoTT-Agda/lib/Basics.agda).
>>      Checking lib.Base (/home/colin/HoTT-Agda/lib/Base.agda).
>> /home/colin/HoTT-Agda/lib/Base.agda:30,13-27
>> Failed to find source of module Agda.Primitive in any of the
>> following locations:
>>    /home/colin/HoTT-Agda/Agda/Primitive.agda
>>    /home/colin/HoTT-Agda/Agda/Primitive.lagda
>> when scope checking the declaration
>>    open import Agda.Primitive public
>>                               using (lzero)
>>                               renaming (Level to ULevel; lsuc to lsucc;
>> _⊔_ to lmax)
>> Makefile:9: recipe for target 'html' failed
>> make: *** [html] Error 1
>>
>> Typing agda --help suggests to me that I edit Makefile to add some -I
>> directives, but presumably this shouldn't be necessary. I have Agda
>> 2.3.2 installed (via yum install Agda - I'm using Fedora 21).
>>
>> What steps am I missing?
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150502/1ae84941/attachment.html