agda-vim

Agda は Editor と組み合わせて使うわけなんですが、

　　まぁ、VSCode でしょ

ってわけですが、自分は emacs + viper 。なんだそれ。ところが、学生に「やってみて」と言ったら

　　vim でやりたい

と。え〜。いや、それで使えるなら自分が使ってるんですけどね。agda-vim という plugin があるんだが...

　　またっく動かない。ピクリとも。

いや、前に動かした時は、まぁ、動かなくはなかったんだが。で、朝いろいろ調べてみたんですが...

　　そもそも、AgdaReload とかが定義されてない
　　そして、それは python 側にある(はぁ?)

で、発見したのは

　　そもそも、macOSのdefaultのvim は python2/python3 support を切ってある
　　brew の vim は、python2 は切ってある
　　brew の neovim は、python 側に neovim 用に python module を入れれば動作する

で、さらに

　　agda-vim は python2 (古いからな、おそらく、その頃は vim script は python2 only)
　　agda-vim の python3 patch はあるが、7年前のもの
　　agda-vim-async なるものもある

ってのを、vim 三種類、vim plugin三種類の組合せで試す感じ。ところが、

　　その間に、macOSのupdateをしたら、python2 が消される羽目に

お前らそういうことするなら「世の中のすべてのpython2 script がそのまま動くようにしてからやれ」

agda-vim の python3 patch + neovim では動いたみたい。でも、割と残念な感じ。

VSCode 側もご機嫌斜めな感じで、動いたり動かなかったり。Emacs は、まぁ、動いているみたいだが。

ずいぶん前に見捨てたものだが、agda-vim-async は何かが足りないらしくまったく動かないが面白いかも。

でも、こういうものじゃなくて、editor とは関係なく横で agda の検査結果を表示するもので良いんじゃないか?

そういうものつくるか?

それとは別に maplocalleader が、まったく動作してないのも発見したのでなんとかする予定。