Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Commands not loaded (neovim) #61

Open
danjenson opened this issue Jan 12, 2023 · 4 comments
Open

Commands not loaded (neovim) #61

danjenson opened this issue Jan 12, 2023 · 4 comments

Comments

@danjenson
Copy link

danjenson commented Jan 12, 2023

I am just starting to use Agda, so I appreciate your patience.

I am using neovim and packer, and packer shows that I've loaded the package and the file type is set to agda. However, none of the commands are loaded, i.e. I can't run :AgdaVersion or :AgdaLoad -- these all return E492: Not an editor command AgdaLoad or the equivalent.

However, unicode commands like \B return the beta character, etc. So it seems the translations work. Other releavant info:

Void Linux, Kernel 6.1.3_1
Neovim 0.8.2
Lua 5.2.4
Agda path: ~/.cabal/bin/agda
Agda 2.6.2.2

Thank you very much.

@ShrykeWindgrace
Copy link

I observe the same with regular vim9.

@bogdankjastrzebski
Copy link

bogdankjastrzebski commented Jul 31, 2024

Same here, with regular vim9
An installation tutorial would be nice

@bogdankjastrzebski
Copy link

I solved it by using a fork of this repo: https://github.com/victortaelin/agda-vim

@datafatmunger
Copy link

datafatmunger commented Sep 13, 2024

FYI, if you're a macOS user, the default vim with macOS does NOT compile vim with Python support, so the plugin will not work. You can verify your flags in vim with :version you'll see -python3 in macOS. Homebrew's does include Python support, showing +python3. Remember to check your $PATH you are using Homebrew's vim or $ which vim, OR you can also build your own vim quickly https://github.com/vim/vim, just check the Makefile with how to enable Python, it's pretty clearly indicated.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants