[Agda] Can't build index.html in HoTT-Agda repository
Colin Adams
colinpauladams at gmail.com
Sat May 2 14:56:34 CEST 2015
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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150502/ef1b1caf/attachment.html
More information about the Agda
mailing list