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

[Mateusz Kowalczyk]

On 05/02/2015 01:56 PM, 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?
> 
> 

If you happen to be using nix, I can package hott-agda for you and it
will Just Work™. Let me know if you're interested.


-- 
Mateusz K.