search

ashinkarov / nvim-agda

Agda interaction pluging for neovim
36 stars 5 forks source link

Libraries from MAlonzo/ #5

Closed siers closed 2 years ago

siers commented 2 years ago

Hi @ashinkarov!

I am trying out nvim-agda with agda from nix with standard-library. When I compile my code, it generates a MAlonzo/ directory with some additional libraries that are only found there, e.g. import Relation.Binary.PropositionalEquality as Eq which is used in PLFA. nvim-agda can't find it:

Failed to find source of module
Relation.Binary.PropositionalEquality in any of the following
locations:
  ~/code/plfa/Relation/Binary/PropositionalEquality.agda
  ~/code/plfa/Relation/Binary/PropositionalEquality.lagda
  /nix/store/ydhsl48is3whm5kglpw8gslk266rc8sh-Agda-2.6.1.3-data/share/ghc-8.10.4/x86_64-linux-ghc-8.10.4/Agda-2.6.1.3/lib/prim/Relation/Binary/PropositionalEquality.agda
  /nix/store/ydhsl48is3whm5kglpw8gslk266rc8sh-Agda-2.6.1.3-data/share/ghc-8.10.4/x86_64-linux-ghc-8.10.4/Agda-2.6.1.3/lib/prim/Relation/Binary/PropositionalEquality.lagda
when scope checking the declaration

It is in MAlonzo/ however,

% find MAlonzo | grep 'Prop.*Eq'
MAlonzo/Code/Relation/Binary/PropositionalEquality.hs
MAlonzo/Code/Relation/Binary/PropositionalEquality.o
...

If you have any clue, I would be delighted to fix this issue, because I think I am nearing the limits of what I can do without "intelligent support" from the editor. :grin:

ashinkarov commented 2 years ago

I am affraid this has nothing to do with nvim-agda. The haskell file in Malonzo is irrelevant, because the error message is saying that agda cannot find the module named Relation.Binary.PropositionalEquality. I guess you need to setup correct path to the standard library (in ~/.agda/libraries and ~/.agda/defaults) --- this is where the missing module is located. See https://agda.readthedocs.io/en/v2.6.2.2/tools/package-system.html#example-using-the-standard-library for more details on how to do this.

I just randomly tried to check src/plfa/part1/Negation.lagda.md, and it worked as expected.

siers commented 2 years ago

The path is probably the issue, I just noticed that the command line command I've been recalling through the shell history includes -i., so that probably accounts for the discrepancy between nvim-agda failures and my command line agda's successes.

Sorry for the non-issue and thank you for the feedback!

siers commented 2 years ago

Solved by adding standard-library in ~/.agda/defaults and the -i . does not make an appearance there and is magically no longer required in command line compiling either though the error that used to be there when compiling from the command line did not suggest why. :tada: :shrug: