bilíngue · en / pt
fiz duas extensões pro bend2 em uma semana
Bend2 shipped, and since I had already written about its idea, the natural next step was to actually use it. But using a new language in the editor I open every day means, in the first minute, a .bend file with no colors, no formatting and nobody telling me I got something wrong. So instead of waiting for someone else to do it, I built two: one for VS Code and one for Neovim.
I had never made a VS Code extension. I had touched Neovim config and small plugins, but never language support from scratch. This post covers what they do, how they were built, and where I stumbled. Spoiler: it was a lot more fun than I expected.
the two extensions
Both are Apache-2.0, public, and cover almost the same list, each in its editor's idiom.
bend2-vscode, published on the Marketplace as Bend 2 Language Support by Nuxyel:
- syntax highlighting, snippets, language configuration and formatting
- a language server with hover, signature help, symbols, go-to-definition, references, rename and call hierarchy
- compiler diagnostics in the Problems panel
- 21 commands: check, build, run, compare backends (JavaScript, native, GPU), benchmark, project gates and more
- Proof Explorer, a sidebar with the project's
laws and the state of each proof, plus Test Explorer integration - it also works in VS Code Web, minus the commands that need to launch
bend
bend2-nvim, a pure Lua plugin:
- filetype, syntax, indentation, snippets and formatter
- completion, signature help, symbols, navigation, references, rename and diagnostics
:Bend2Check,:Bend2Build,:Bend2Run,:Bend2CompareBackends,:Bend2Benchmarkand the rest of the family:Bend2Proofs, the Proof Explorer in a bufferBasecompletion pulled from the compiler itself (bend base), asynchronously- no Node, no external LSP server, no dependency on other plugins, no key maps forced on you
In both, whatever doesn't need the compiler keeps working without it installed. Without bend on the PATH you lose check and proofs, but not the editor.
how they were made
In VS Code the architecture is the textbook one: a thin client (extension.ts), a TypeScript language server speaking LSP, and a toolchain package that knows how to find bend, detect its version, run processes and cancel them. Highlighting is a 41-line TextMate grammar, which surprised me: for a language with def, type and law, very little gets you a decent result:
{ "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" } } }The rest of the VS Code side is volume: 21 commands, a view container, the Test Explorer, the release pipeline. The part I didn't expect is that everything also has to run in the browser (VS Code Web has no processes, only a worker), so the parser ships in two wrappers.
In Neovim it was the opposite: no framework, just the editor's own APIs. vim.system to run the compiler, vim.diagnostic to show errors, omnifunc for completion and Lua modules for everything else. There isn't even an LSP server: the intelligence lives inside the plugin itself. The modules: parser, workspace, formatter, toolchain, proof, editor. It adds up to a little over 2 thousand lines of Lua, much less than the VS Code side, because Neovim already ships almost everything the plugin needs.
The workflow was similar on both: first a plan for what a stable v1 needed, then the implementation, with one fixed rule: one small commit per logical delivery. That produced a history you can read like a diary. The Neovim one, for example, starts at feat: add Bend2 filetype and syntax support and moves through the parser, formatter, navigation, diagnostics and proofs, in the order each piece started working.
where it hurt
there is no AST to consume
This is the biggest difficulty of all, and it affects both extensions. A decent language server wants to know where each declaration ends, which names exist, what type each one has. The Bend2 compiler exposes none of that in a stable way. It does check, run, build and prints errors. Whatever "semantics" the extension knows comes from a hand-written tolerant parser that reads line by line, strips comments and strings, and recognizes def, law, type and 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
-- becomes a symbol, with range and selectionRange
endIt works well for navigation and so-so for the rest, and the rest is the problem: hover, signature help and the inferred "proven" state are approximations. The decision I made (and it's written into the repository's principles) is to never sell an approximation as truth: whatever comes from the parser is marked provisional, and only the compiler can say a law was verified. The VS Code 2.0 roadmap is literally "when the compiler exposes types, spans and proof context, throw my parser away".
reading the compiler's error as text
Without structured diagnostics at the start, the extension read the human output. A Bend error looks like this:
Error:
- expected : a name (got the keyword 'match')
- observed : ' '
Location:
1 | def unfinished(value: Nat
2>| match value
You can parse Error: and Location:, but you're coupled to the text of one specific version. I still keep a fixture captured on Bend 2.0.23 as "legacy". Today the plugin asks for --diagnostics=json when the compiler supports it and falls back to the text parser if not:
local args = { path, "--check-only" }
if config().diagnostics_mode ~= "text" then args[#args + 1] = "--diagnostics=json" endNote the --check-only. That flag exists for a very concrete reason: checking a file must not execute its main. In a language whose main can print, read an environment variable or do IO, "check on save" that runs the program would be a security bug and a terrible surprise.
the language moves faster than you
Bend2 is new, so the compiler version is part of the contract. The rule became: minimum 2.0.28, anything below shows up as unsupported, and CI runs the matrix against 2.0.28 and 2.0.32, each downloaded at a pinned version with the official checksum verified. The repository's own proof project is compiled by both on every push. If bend changes the format of an error, the test breaks before a user notices.
a rename that renames too much
Cross-file rename looks easy until two modules have a function with the same name. Rename and references by name could edit the homonymous declaration in another file. The fix, two commits (fix: resolve cross-file references before rename and test: prevent rename across homonymous imports), was to confirm each candidate by resolving its definition through the import before editing. In Neovim the same risk was handled by the commit fix: resolve Bend workspace symbols by declaration identity. Rename by text is a trap, even with a dumb parser behind it: the declaration has an identity, and the word doesn't.
the Neovim gotchas
Almost every "Neovim" difficulty was an API detail nobody warns you about:
vim.systemcallbacks run in a fast context, where you can't touch buffers. The Proof Explorer smoke test broke because of it, and the fix was to wrap everything invim.schedule_wrap.foldmethodis a window option, not a buffer option. The autocmd assigned it as if it were buffer-local, and the automated tests caught the defect.- An async check result arrives late. If you edited the buffer while the compiler ran, publishing the stale diagnostic paints an error on the wrong line. Each result is now discarded if the buffer's
changedtickchanged since the check started. nvim -u NONEdoesn't turn on filetype detection. I found this taking the README screenshots: the buffer showed no highlighting and I was sure the extension was broken.- macOS is not Linux. The unit suite passed locally and failed on both macOS CI jobs, and the fix was the commit
test: compare canonical workspace paths on macOS. Without the macOS runner I wouldn't have found it.
porting the official formatter
Bend2's real formatter is bend-fmt-lsp, from the official repository. It makes no sense to invent another, so both extensions carry an adaptation of its lexer and rules: in TypeScript on VS Code, in Lua on Neovim, both with an attribution header in the file and, on Neovim, a NOTICE with the same license. That was also a project decision: when an official truth exists, the extension's job is to follow it, not to have opinions. The Lua version did drift out of sync with the official contract, and the release review caught it before the tag.
the last mile is bigger than the code
I thought "the extension is ready" and "the extension is published" were almost the same thing. They aren't. A few publishing stumbles, all real:
- the release workflow broke on the GitHub runner because a quoted shell expression that worked locally wasn't interpreted there
- the provenance generator still wrote
0.1.0into the file of a1.0.0VSIX; the post-commit validation caught it, and the fix came with a permanent check tying the metadata to the manifest version - the Marketplace rejected the name: "Bend 2 for VS Code" already existed. I cut a
1.0.1just to change thedisplayNameto Bend 2 Language Support by Nuxyel, and left1.0.0untouched with its SBOM - creating a publisher, an Azure DevOps token with
Marketplace (Manage)scope and a GitHub secret is a mini-tutorial of its own - after everything was uploaded, it still sat in verifying for a while
On the Neovim side the last mile was lighter, because there is no store: a plugin is a Git repository with SemVer tags. I documented lazy.nvim, vim.pack (Neovim 0.12+) and the native package layout for 0.11, and added a pkg.json as metadata only. There is no LuaRocks package and no registry.
using bend2 inside the extension
A question I asked myself midway was "where do these extensions use Bend2 itself?". Besides calling the compiler for everything, both have a real Bend project inside the repository, used as an example and as the dogfood test: a model, a laws file and a proofs file.
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}
{==}
CI checks that Bend accepts that proof, and the Proof Explorer shows the law as verified by the compiler. Two nice things here: the example and the test are the same file (one copy to keep), and seeing a proof language run in the editor built for it feels good in a way I can't quite explain. In the Neovim one, Base completion also comes from the compiler, which knows how to list what exists.
why this is fun
I went in expecting editor bureaucracy and found the opposite.
The feedback is immediate and visual: you tweak a grammar rule and the color changes, you write a hover and it shows up. Few projects respond that fast.
You also get to see the language from the inside. To build an extension you have to understand every Bend2 construct, what +d is, what 1n+p is, how a law connects to its proof. I learned more about the syntax writing the parser than reading the documentation.
The missing AST helped, in a strange way. It forced me to decide what is fact and what is guess, and to write that into the interface. I'd take that product honesty to any project.
And CI turns the whole thing into a kind of level-based game. The Neovim plugin only got its v1.0.0 tag with 12 green jobs: Neovim 0.11.7 and 0.12.5, Bend 2.0.28 and 2.0.32, Linux and macOS. Each combination that passes is an unlocked level, and the macOS level showed me a bug I would never have found on my own.
If you use Bend, install one of the two and open an issue when something breaks; if you've never built an editor extension, this is my invitation: pick a small language and build one. You'll most likely get lost halfway and love it.
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
lawdo 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,:Bend2Benchmarke o resto da família:Bend2Proofs, o Proof Explorer em um buffer- completion de
Basepuxada 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
endFunciona 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" endRepare 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.systemrodam 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 comvim.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
changedtickdo buffer mudou desde que o check começou. nvim -u NONEnã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.0no arquivo de um VSIX1.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.1só para trocar odisplayNamepara Bend 2 Language Support by Nuxyel, e mantive a1.0.0intacta 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.