search

derekelkins / agda-vim

Agda interaction in vim
BSD 2-Clause "Simplified" License
130 stars 47 forks source link

As of Agda 2.5.3-alpha1, agda-vim doesn't work #27

Closed madgen closed 7 years ago

madgen commented 7 years ago

I get "Goal not loaded" for everything after upgrading to 2.5.3-alpha1. I also tried HEAD which is 2.6.0-d1a6e83-dirty. That also doesn't work. Here's an example:

module Example where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

f : ℕ → ℕ
f a = ?

Is this an issue with Agda (their CHANGELOG doesn't mention changes to --vim option) or with the plugin?

derekelkins commented 7 years ago

It looks like they've made some changes to the emacs interaction which may have caused this. I'll look into it once 2.5.3 is released and I can test it. My understanding is that the protocol Agda uses to communicate to emacs is not considered public, so they can make changes that break this plugin at any time.

madgen commented 7 years ago

Ah, that is a bit inconsiderate of them, isn't it? Well, thank you.

madgen commented 7 years ago

2.5.3 is now released and this problem goes away on its own.