[Agda] lost in modules

[Michel Levy]

I found a fix for my mistake but I don't understand how it works.
In .agda/libraries I replaced the line
/home/michel/agda-stdlib-1.3/standard-library.agda-lib
by the actual location of the library
/home/michel/agda-stdlib-1.3/src/standard-library.agda-lib
and I copied the file
/home/michel/agda-stdlib-1.3/standard-library.agda-lib
in this library.

Why with this strange method, there is no more research of the module
Data.nat  in the old library  ?


Le 01/05/2020 à 13:59, Jonathan Steven Prieto Cubides a écrit :
> What do you have in .agda/defaults?
>
>
> From: Agda <agda-bounces at lists.chalmers.se> on behalf of Michel Levy <michel.levy.imag at free.fr>
> Date: Friday, 1 May 2020 at 13:55
> To: Agda Mailing List <agda at lists.chalmers.se>
> Subject: [Agda] lost in modules
>
>
> This morning, I have loaded (from GitHub) the standard library with the version 1.3.
>
> I have change .agda/libraries to the new version. That is my .agda/libraries file :
>
> /home/michel/Agda/PLFA-LIB/plfa.agda-lib
>
> /home/michel/agda-stdlib-1.3/standard-library.agda-lib
>
> But when I retry to load a file "relationsPLFA.agda", agda, on a command "open import Data.nat" is also searching (twice) in the old
>
> version of the standard libray and give the error :
>
>
>
> Ambiguous module name. The module name Data.Nat could refer to any
>
> of the following files:
>
>   /home/michel/agda-stdlib-1.3/src/Data/Nat.agda
>
>   /usr/share/agda-stdlib/Data/Nat.agda
>
>   /usr/share/agda-stdlib/Data/Nat.agda
>
> when scope checking the declaration
>
>   open import Data.Nat using (ℕ; zero; suc; _+_)
>
>
>
> What should I do to avoid this search in the old library ?
> --
> courriel : michel.levy.imag at free.fr<mailto:michel.levy.imag at free.fr>
> mobile : 06 59 13 42 53
> web : michel.levy.imag.free.fr
-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr