vscoq.md

A extensão VSCoq não funciona.

Hipóteses

• A linguagem Coq não foi instalada corretamente.

  • Me certifiquei de que a linguagem Coq está instalada corretamente pois após rodar o comando yay -S coq e opam install coq foi feita a instalação sem maiores problemas ou mensagens de aviso que indicassem alguma falha.
  • O REPL do Coq funciona perfeitamente pelo terminal quando é chamado.
  • O CoqIDE funciona perfeitamente quando é chamado pelo terminal ou pelo ícone do gnome.

• A instalação da linguagem está em conflito com uma ou mais instalações e/ou dependências.

  • Notei que instalar Coq em dois lugares diferentes podia vir a causar problemas então desinstalei com yay -R coq e mantive a versão instalada com opam install coq.
  • Descobri que eu preciso do binário que é instalado via opam, portanto opam install coq foi a decisão correta de instalação a se manter.

• Eu não configurei corretamente a extensão.

  • A extensão depende de configurar o caminho de instalação do binário de Coq, e foi feito corretamente configurado e clarificado por Karl e Paolo em https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/VSCoq.20extension.20for.20VSCode.20doesn't.20work

• Eu não tenho nenhum log ou informação que me diga o que eu estou fazendo de errado.

  • Em output não tenho nenhum dado que informe erro.
  • No próprio vscode tem a aba de "output" que permite selecionar por "Coq Language Server" para ver quaisquer alterações feitas no LSP ou no projeto.
  • Entretanto essa mensagem abaixo não me diz muito o que estou fazendo de errado.

   Coq Language Server: process.version: v16.14.2, process.arch: x64}
   Loaded project at /home/grandehe4rt/dev/ocaml/test
   Updated project root to .
   Coqtop binPath is: /home/grandehe4rt/.opam/default/bin/
  

• Eu não verifiquei como o vscode estava interpretando arquivos com a extensão .v

  • O vscode identificou que eu estava editando um arquivo com a extensão .v portanto assumiu que eu estivesse utilizando essa linguagem e não a linguagem Coq
  • Editei manualmente o modo como o vscode estava interpretando os arquivos .v para interpretá-los como linguagem de programação Coq ao em vez da linguagem de programação V
  • A extensão e seus atalhos começaram a funcionar perfeitamente.

Após modificar manualmente a interpretação do vscode para os arquivos que eu estava editando o log do output atualizou para:

Coq Language Server: process.version: v16.14.2, process.arch: x64}
Loaded project at /home/grandehe4rt/dev/lf
Updated project root to .
Coqtop binPath is: /home/grandehe4rt/.opam/default/bin
Listening at 127.0.0.1:45033
Listening at 127.0.0.1:36993
Listening at 127.0.0.1:40245
Listening at 127.0.0.1:38989