[Agda] darcs - dev-version fail
Sergei Meshveliani
mechvel at botik.ru
Thu Nov 21 17:51:14 CET 2013
Dear Agda developers,
I have the following problems.
1. Agda-2.3.2.2 fails to type-check my example, reporting
"Internal error"
-- there was a recent bug report on this.
2. You have responded that it is probably fixed in the development
version.
3. The code is so natural, that I doubt:
to change the code and to continue with Agda-2.3.2.2
(it allows this)
or to try the development Agda version ?
4. Then, I tried darcs.
This time darcs works differently than earlier, there were adventures,
it hungs for long, I pressed Ctrl-C a couple of times, then repeated
darcs. Finally it said "finished".
And there appeared ./Agda and ./Agda0.
I go to /Agda and install Agda from there, as usual. So that:
> agda -V
prints Agda version 2.3.3
But it cannot type-check anything:
module DPrelude
where
open import Level using (Level; suc; _⊔_)
...
/home/mechvel/doconA/0.03/source/DPrelude.agda:1,8-8
/home/mechvel/doconA/0.03/source/DPrelude.agda:1,8: Parse error
DPrelude<ERROR> where open import Level using ...
Probably, the files are darcs -ed wrongly.
Is it possible to get the development Agda version in a reliable way?
Regards,
------
Sergei
More information about the Agda
mailing list