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

[N. Raghavendra]

At 2015-05-02T13:56:34+01:00, Colin Adams wrote:

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

The file HoTT-Agda/lib/Base.agda needs a module called Agda.Primitive.
According to the Agda CHANGELOG file:

  "Release notes for Agda 2 version 2.4.0: Important changes since
   2.3.2.2: Installation and infrastructure: A new module called
   Agda.Primitive has been introduced."

So the module Agda.Primitive isn't available in Agda 2.3.2, which you're
using, and you need to upgrade to a more recent version of Agda.  In
fact, it's better to use the development version from GitHub.  See

http://ncatlab.org/homotopytypetheory/show/Agda

and

https://groups.google.com/d/topic/homotopytypetheory/rTDiu9YX_Vc/discussion

for the reasons.

Cheers,
Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/