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

[Andreas Abel]

Maybe the wrong agda is run?  Check your PATH; ~/.cabal/bin should 
precede the path where your yum-installed agda is found.  Try

   which agda
   agda-mode locate

--Andreas

On 02.05.2015 20:42, Colin Adams wrote:
> 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
> <mailto: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 <mailto: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 <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~abel/
>
>

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