<html><head></head><body><div style="font-family: Verdana;font-size: 12.0px;"><div>
<div>Thanks!</div>
<div> </div>
<div>I am now attempting to use cabal to install the newest Agda. It keeps failing because of different programs I have not installed yet, so that's what I'm doing now. I am stuck at this point on one in particular, cpphs. What happened is I initially installed one version, 1.19.3, using "sudo apt install", but this was apparently not as new as the Agda 2.5 requires. I was able to use cabal to install the latest, cabal-1.20.8, but apparently this does not affect what is found under usr/bin/cpphs. Nor can I use the "sudo apt install cabal-1.20.8" at this point; it reports that it cannot find it. What is going on here?</div>
<div>
<div name="quote" style="margin:10px 5px 5px 10px; padding: 10px 0 10px 10px; border-left:2px solid #C3D9E5; word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">
<div style="margin:0 0 10px 0;"><b>Sent:</b> Saturday, December 02, 2017 at 3:30 PM<br/>
<b>From:</b> "Andreas Abel" <andreas.abel@ifi.lmu.de><br/>
<b>To:</b> "Manny Romero" <mannyromero@mail.com>, agda@lists.chalmers.se<br/>
<b>Subject:</b> Re: [Agda] Trying to load modules from Norell OPLSS tutorial</div>
<div name="quoted-content">Manny,<br/>
<br/>
you need to upgrade to a newer version of Agda. The latest release is<br/>
2.5.3.<br/>
<br/>
> 7,12 : Parse error<br/>
> constructor<ERROR><br/>
<br/>
This is because Agda 2.4 does not know about the "instance" keyword.<br/>
<br/>
Alternatively, you could try to get an old version of Ulf's Prelude, the<br/>
one he used for the OPLSS. I have no clue if this is possible, though.<br/>
<br/>
Best,<br/>
Andreas<br/>
<br/>
On 02.12.2017 21:24, Manny Romero wrote:<br/>
> I'm trying to follow the OPLSS 2014 Agda tutorial. As seen in the first<br/>
> two minutes here ( <a href="https://www.youtube.com/watch?v=NrSW7YsneVg" target="_blank">https://www.youtube.com/watch?v=NrSW7YsneVg</a> ), this<br/>
> requires loading some files from agda-summer-school-OPLSS and<br/>
> agda-prelude on this ( <a href="https://github.com/UlfNorell/agda-summer-school" target="_blank">https://github.com/UlfNorell/agda-summer-school</a> )<br/>
> website.<br/>
> Despite not knowing anything about computers, I think I've somehow<br/>
> managed to both download these files and tell emacs where to look for<br/>
> them successfully. The problem is that I now get error messages for<br/>
> Prelude files when I try to load Day1.agda. For instance, when I do so,<br/>
> the main screen shows "module Prelude.Unit where" followed by the rest<br/>
> of Unit.agda from the Prelude subdirectory<br/>
> -----------------------<br/>
><br/>
> module Prelude.Unit where<br/>
> open import Agda.Builtin.Unit public<br/>
> record ⊤′ {a} : Set a where<br/>
> instance constructor tt<br/>
> -- To keep changes from compat-2.4.0 to a minimum.<br/>
> Unit = ⊤<br/>
> pattern unit = tt<br/>
> -------------------------<br/>
> and the screen below reads something like<br/>
> -------------------------<br/>
> 7,12 : Parse error<br/>
> constructor<ERROR><br/>
> tt<br/>
> --------------------------<br/>
> When I comment out the text of this file and save, an error message for<br/>
> another Prelude file pops up.<br/>
> What might I be doing wrong? Surely there isn't really something wrong<br/>
> with all these files? Why might this be happening to me?<br/>
> I have Linux Mint 18, Agda 2.4.2.5, Emacs 24.5.1. And again, I am<br/>
> completely computer illiterate and it's a minor miracle I managed to get<br/>
> this far!<br/>
><br/>
><br/>
> _______________________________________________<br/>
> Agda mailing list<br/>
> Agda@lists.chalmers.se<br/>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br/>
><br/>
<br/>
<br/>
--<br/>
Andreas Abel <>< Du bist der geliebte Mensch.<br/>
<br/>
Department of Computer Science and Engineering<br/>
Chalmers and Gothenburg University, Sweden<br/>
<br/>
andreas.abel@gu.se<br/>
<a href="http://www.cse.chalmers.se/~abela/" target="_blank">http://www.cse.chalmers.se/~abela/</a></div>
</div>
</div>
</div></div></body></html>