$cat ~/posts/extensoes-bend2-vscode-nvim

bilíngue · en / pt

← /blog

fiz duas extensões pro bend2 em uma semana


O Bend2 saiu e, como eu já tinha escrito sobre a ideia dele, o passo natural era usar. Só que usar uma linguagem nova no editor que eu abro todo dia significa, no primeiro minuto, um arquivo .bend sem cor, sem formatação e sem ninguém me dizendo que errei. Então em vez de esperar alguém fazer, fiz duas: uma para o VS Code e uma para o Neovim.

Nunca tinha feito extensão de VS Code. De Neovim eu já tinha mexido em config e plugin pequeno, mas nunca suporte de linguagem do zero. Este post é o que elas fazem, como foram feitas e onde eu tropecei. Spoiler: foi muito mais divertido do que eu esperava.

as duas extensões

As duas são Apache-2.0, públicas, e cobrem quase a mesma lista, cada uma no idioma do seu editor.

bend2-vscode, publicada no Marketplace como Bend 2 Language Support by Nuxyel:

  • realce de sintaxe, snippets, configuração de linguagem e formatação
  • servidor de linguagem com hover, signature help, símbolos, ir-para-definição, referências, rename e call hierarchy
  • diagnósticos do compilador no painel Problems
  • 21 comandos: check, build, run, comparar backends (JavaScript, nativo, GPU), benchmark, gates de projeto e afins
  • Proof Explorer, uma barra lateral com as law do projeto e o estado de cada prova, mais integração com o Test Explorer
  • funciona também no VS Code Web, só sem os comandos que precisam rodar o bend

bend2-nvim, plugin Lua puro:

  • filetype, sintaxe, indentação, snippets e formatador
  • completion, signature help, símbolos, navegação, referências, rename e diagnósticos
  • :Bend2Check, :Bend2Build, :Bend2Run, :Bend2CompareBackends, :Bend2Benchmark e o resto da família
  • :Bend2Proofs, o Proof Explorer em um buffer
  • completion de Base puxada do próprio compilador (bend base), de forma assíncrona
  • sem Node, sem servidor LSP externo, sem dependência de outros plugins, sem mapeamento de tecla imposto

Nas duas, o que não precisa do compilador continua funcionando sem ele instalado. Sem bend no PATH você perde check e proofs, mas não o editor.

como foram feitas

No VS Code a arquitetura é a de manual: um cliente fino (extension.ts), um servidor de linguagem em TypeScript falando LSP, e um pacote toolchain que sabe achar o bend, descobrir versão, rodar processo e cancelar. O realce é uma gramática TextMate de 41 linhas, o que me surpreendeu: para uma linguagem com def, type e law, dá um resultado decente com pouquíssimo:

{ "match": "\\b(law)\\s+([A-Za-z_][A-Za-z0-9_]*)",
  "captures": { "1": { "name": "keyword.other.law.bend" },
                "2": { "name": "entity.name.function.law.bend" } } }

O resto do VS Code é volume: 21 comandos, uma view container, o Test Explorer, o pipeline de release. A parte que eu não esperava é que tudo precisa rodar também no navegador (o VS Code Web não tem processo, só um worker), então o parser existe em duas embalagens.

No Neovim foi o contrário: nenhum framework, só as APIs do próprio editor. vim.system para rodar o compilador, vim.diagnostic para mostrar erro, omnifunc para completion e módulos Lua para o resto. Nem servidor LSP tem: a inteligência mora dentro do próprio plugin. Os módulos: parser, workspace, formatter, toolchain, proof, editor. No total são pouco mais de 2 mil linhas de Lua, bem menos do que o lado do VS Code, porque o Neovim já traz quase tudo que o plugin precisa.

O fluxo de trabalho foi parecido nos dois: primeiro um plano do que uma v1 estável precisava ter, depois a implementação, com uma regra fixa: um commit pequeno por entrega lógica. Isso rendeu um histórico que dá para ler como um diário. O do Neovim, por exemplo, começa em feat: add Bend2 filetype and syntax support e segue pelo parser, formatador, navegação, diagnósticos e provas, na ordem em que cada coisa passou a funcionar.

onde doeu

não existe AST pra consumir

Essa é a maior dificuldade de todas, e ela afeta as duas extensões. Um servidor de linguagem decente quer saber onde termina cada declaração, quais nomes existem, de que tipo é cada um. O compilador do Bend2 não expõe nada disso de forma estável. Ele faz check, run, build e imprime erros. O que a extensão sabe de "semântica" vem de um parser tolerante feito à mão, que lê linha por linha, tira comentários e strings, e reconhece def, law, type e import:

local keyword, name = declaration:match("^(%a+)%s+([A-Za-z_][A-Za-z0-9_.]*)")
if keyword == "def" or keyword == "law" or keyword == "type" then
  -- vira símbolo, com range e selectionRange
end

Funciona bem para navegar e mais ou menos para o resto, e o resto é o problema: hover, signature help e o estado "provado" inferido são aproximações. A decisão que eu tomei (e que está escrita nos princípios do repositório) é nunca vender aproximação como verdade: o que vem do parser é marcado como provisório, e só o compilador pode dizer que uma lei foi verificada. O roadmap da 2.0 do VS Code é literalmente "quando o compilador expuser tipos, spans e contexto de prova, jogar meu parser fora".

ler o erro do compilador como texto

Sem diagnóstico estruturado no começo, a extensão lia a saída humana. Um erro do Bend tem esta cara:

Error:
- expected : a name (got the keyword 'match')
- observed : ' '
Location:
1 | def unfinished(value: Nat
2>|   match value

Dá para parsear Error: e Location:, mas você está acoplado ao texto de uma versão específica. Ainda mantenho um fixture capturado no Bend 2.0.23 como "legado". Hoje o plugin pede --diagnostics=json quando o compilador suporta e cai para o parser de texto se não:

local args = { path, "--check-only" }
if config().diagnostics_mode ~= "text" then args[#args + 1] = "--diagnostics=json" end

Repare no --check-only. Esse flag existe por um motivo bem concreto: verificar um arquivo não pode executar o main dele. Numa linguagem cujo main pode imprimir, ler variável de ambiente ou fazer IO, "checar ao salvar" rodando o programa seria um bug de segurança e uma péssima surpresa.

a linguagem anda mais rápido que você

O Bend2 é novo, então a versão do compilador é parte do contrato. A regra virou: mínimo 2.0.28, tudo abaixo aparece como não suportado, e a CI roda a matriz contra 2.0.28 e 2.0.32, cada uma baixada por versão fixa e com o checksum oficial conferido. O projeto de prova do próprio repositório é compilado por elas em todo push. Se o bend mudar o formato de um erro, o teste quebra antes de um usuário perceber.

rename que renomeia demais

Rename entre arquivos parece fácil até dois módulos terem uma função com o mesmo nome. Rename e referências por nome podiam editar a declaração homônima de outro arquivo. A correção, dois commits (fix: resolve cross-file references before rename e test: prevent rename across homonymous imports), foi confirmar cada candidato resolvendo a definição pelo import antes de editar. No Neovim o mesmo risco foi tratado com o commit fix: resolve Bend workspace symbols by declaration identity. Rename por texto é armadilha, mesmo com parser bobo por trás: quem tem identidade é a declaração, e a palavra não.

as pegadinhas do Neovim

Quase toda dificuldade "de Neovim" foi um detalhe de API que ninguém avisa:

  • Callbacks de vim.system rodam em contexto rápido, onde você não pode tocar em buffers. O smoke test do Proof Explorer quebrou por isso, e a solução foi embrulhar tudo com vim.schedule_wrap.
  • foldmethod é opção de janela, não de buffer. O autocmd atribuía como se fosse do buffer, e os testes automatizados pegaram o defeito.
  • O resultado de um check assíncrono chega tarde. Se você editou o buffer enquanto o compilador rodava, publicar o diagnóstico velho pinta erro na linha errada. Cada resultado agora é descartado se o changedtick do buffer mudou desde que o check começou.
  • nvim -u NONE não liga a detecção de filetype. Descobri isso tirando os screenshots do README: o buffer aparecia sem realce e eu jurava que a extensão estava quebrada.
  • macOS não é Linux. A suíte unitária passou local e falhou nos dois jobs de macOS da CI, e a correção foi o commit test: compare canonical workspace paths on macOS. Sem o runner de macOS eu não teria descoberto.

portar o formatador oficial

O formatador de verdade do Bend2 é o bend-fmt-lsp, do repositório oficial. Não faz sentido inventar outro, então as duas extensões carregam uma adaptação do lexer e das regras dele: em TypeScript no VS Code, em Lua no Neovim, ambas com cabeçalho de atribuição no arquivo e, no Neovim, um NOTICE com a mesma licença. Isso também foi uma decisão de projeto: quando existe uma verdade oficial, o trabalho da extensão é seguir ela, não ter opinião. A versão Lua chegou a ficar dessincronizada do contrato oficial, e a revisão de release pegou isso antes da tag.

a última milha é maior que o código

Achei que "a extensão está pronta" e "a extensão está publicada" eram quase a mesma coisa. Não são. Alguns tropeços da parte de publicação, todos reais:

  • o workflow de release quebrou no runner do GitHub porque uma expressão de shell com aspas que funcionava local não foi interpretada lá
  • o gerador de proveniência ainda escrevia 0.1.0 no arquivo de um VSIX 1.0.0; a validação pós-commit pegou, e o conserto veio com uma checagem permanente que amarra os metadados à versão do manifesto
  • o Marketplace recusou o nome: "Bend 2 for VS Code" já existia. Virei 1.0.1 só para trocar o displayName para Bend 2 Language Support by Nuxyel, e mantive a 1.0.0 intacta com seu SBOM
  • criar publisher, um token do Azure DevOps com escopo Marketplace (Manage) e um secret no GitHub é um mini-tutorial por si só
  • depois de tudo enviado, ainda ficou um tempo em verifying

No lado do Neovim a última milha foi mais leve, porque não existe loja: plugin é repositório Git com tags SemVer. Documentei lazy.nvim, vim.pack (Neovim 0.12+) e o layout nativo de pacote para o 0.11, e adicionei um pkg.json só como metadado. Não há pacote LuaRocks nem registry.

usando o bend2 dentro da extensão

Uma pergunta que me fiz no meio do caminho foi "onde essas extensões usam o próprio Bend2?". Além de chamar o compilador para tudo, as duas têm um projeto Bend real dentro do repositório, usado como exemplo e como teste de dogfood: um modelo, um arquivo de leis e um de provas.

law adding_zero_preserves_value:
  for value: Nat
  {Model.add_zero(value) == value : Nat}
def add_zero_right(value: Nat) -> {Model.add_zero(value) == value : Nat}:
  match value:
    case 0n:
      {==}
    case 1n+predecessor:
      %add_zero_right(predecessor) : {1n+Model.add_zero(predecessor) == 1n+_ : Nat}
      {==}

A CI checa que o Bend aceita essa prova, e o Proof Explorer mostra a lei como verificada pelo compilador. Duas coisas gostosas aqui: o exemplo e o teste são o mesmo arquivo (uma cópia só para manter), e ver uma linguagem de provas rodando no editor que foi feito para ela dá uma sensação boa que não consigo explicar direito. Na do Neovim a completion de Base também sai do compilador, que sabe listar o que existe.

por que isso é divertido

Fui esperando a burocracia de um editor e achei o oposto.

O retorno é imediato e visual: você mexe numa regra da gramática e a cor muda, escreve um hover e ele aparece. Poucos projetos respondem tão rápido.

Também dá para ver a linguagem por dentro. Para fazer uma extensão você precisa entender cada construção do Bend2, o que é +d, o que é 1n+p, como uma law se liga à sua prova. Aprendi mais sobre a sintaxe escrevendo o parser do que lendo a documentação.

A falta de AST ajudou, de um jeito estranho. Ela me obrigou a decidir o que é fato e o que é palpite, e a escrever isso na interface. Essa honestidade de produto eu levaria para qualquer projeto.

E a CI transforma tudo numa espécie de jogo de fases. O plugin de Neovim só ganhou a tag v1.0.0 com 12 jobs verdes: Neovim 0.11.7 e 0.12.5, Bend 2.0.28 e 2.0.32, Linux e macOS. Cada combinação que passa é uma fase destravada, e foi a fase do macOS que me mostrou um bug que eu nunca teria achado sozinho.

Se você usa Bend, instale uma das duas e abra uma issue quando algo quebrar; se você nunca fez extensão de editor, este é meu convite: escolha uma linguagem pequena e faça. O mais provável é você se perder no meio e adorar.