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

[Andreas Abel]

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/