<div dir="ltr">Agda beginner here.<div><br></div><div>I&#39;ve checked out <a href="https://github.com/hott/hott-agda/">https://github.com/hott/hott-agda/</a> and tried typing:</div><div><br></div><div>make html</div><div><br></div><div>in order to build index.html. But it appears I need to set up something in the environment first, as I get:</div><div><br></div><div><div>[colin@localhost HoTT-Agda]$ make html</div><div>rm -f </div><div>agda index.agda --html</div><div>Checking index (/home/colin/HoTT-Agda/index.agda).</div><div> Checking homotopy.LoopSpaceCircle (/home/colin/HoTT-Agda/homotopy/LoopSpaceCircle.agda).</div><div>  Checking HoTT (/home/colin/HoTT-Agda/HoTT.agda).</div><div>   Checking lib.Basics (/home/colin/HoTT-Agda/lib/Basics.agda).</div><div>    Checking lib.Base (/home/colin/HoTT-Agda/lib/Base.agda).</div><div>/home/colin/HoTT-Agda/lib/Base.agda:30,13-27</div><div>Failed to find source of module Agda.Primitive in any of the</div><div>following locations:</div><div>  /home/colin/HoTT-Agda/Agda/Primitive.agda</div><div>  /home/colin/HoTT-Agda/Agda/Primitive.lagda</div><div>when scope checking the declaration</div><div>  open import Agda.Primitive public</div><div>                             using (lzero)</div><div>                             renaming (Level to ULevel; lsuc to lsucc; _⊔_ to lmax)</div><div>Makefile:9: recipe for target &#39;html&#39; failed</div><div>make: *** [html] Error 1</div></div><div><br></div><div>Typing agda --help suggests to me that I edit Makefile to add some -I directives, but presumably this shouldn&#39;t be necessary. I have Agda 2.3.2 installed (via yum install Agda - I&#39;m using Fedora 21).</div><div><br></div><div>What steps am I missing?</div></div>