search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

"binding for LEVEL" #975

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From mech...@botik.ru on November 22, 2013 11:36:15

1. Agda-2.3.3 -development of Nov 22 2013, MAlonzo, lib-0.7 :

/home/mechvel/agda/lib-0.7/src/Level.agda:27,1-32 Duplicate binding for built-in thing LEVEL, previous binding to .Agda.Primitive.Level when checking the pragma BUILTIN LEVEL Level

This is the type-check report to any my program. What is the matter, please?

  1. After I get a new Agda version, I do

(a) ghc-pkg unregister , (b) install the new version, (c) cd .../lib-/ffi
cabal install

-- because I think that new Agda needs to somehow process the library source (??). And it says "reinstalling is always dangerous". And it always works, though. And Agda starts to do sometheng with the library source only when dealing with an application module which imports something from the library. Do I need (c) ?

Original issue: http://code.google.com/p/agda/issues/detail?id=975

UlfNorell commented 10 years ago

From vitus...@gmail.com on November 22, 2013 06:31:07

Agda now automatically imports Agda.Primitive ( http://code.haskell.org/Agda/src/data/lib/prim/Agda/Primitive.agda ), which conflicts with the BUILTIN declarations found in the Level module.

That means you need to update the standard library.

See http://www.cse.chalmers.se/~nad/repos/lib/src/Level.agda

UlfNorell commented 10 years ago

From mech...@botik.ru on November 22, 2013 08:07:11

What does this mean "to update the standard library" ? I have lib-0.7, and this is the last version. There has not been announced any later version.

UlfNorell commented 10 years ago

From vitus...@gmail.com on November 22, 2013 08:53:23

lib-0.7 is the last version in the same sense that Agda 2.3.2.2 is the last version. There are development version of both Agda and the standard library.

Either do a "darcs pull" on the repository mentioned above ( http://www.cse.chalmers.se/~nad/repos/lib ), or replace your Level.agda with http://www.cse.chalmers.se/~nad/repos/lib/src/Level.agda .

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 22, 2013 11:05:56

What vituscze said. The released version of Agda works with the released version of the standard library and the darcs version works with the darcs version of the library.

Status: Invalid