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

[Andreas Abel]

Thanks Raghu, I guess I lost track of the releases, I thought we had 
added Agda.Primitive earlier...  --Andreas

On 02.05.2015 15:47, N. Raghavendra wrote:
> 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/
>
> _______________________________________________
> 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/