[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