OpenCode

Stream: Machine Learning for Theorem Proving

[Julian Berman]

A context-less idea which maybe someone might find interesting to play with -- opencode, which probably at least a few folks use/have heard of as an LLM-agnostic TUI coding agent, supports LSP for interacting with open files. Adding Lake to it should be trivial to do so that it can access the Lean LSP. But that isn't "enough" -- in order to make it useful one presumably also needs to give it access to the same LSP protocol extensions Lean adds (that editor integrations like VSCode+lean.nvim use), things which are used for getting goal state information at positions in the buffer (e.g. $/lean/plainGoal requests -- interactive goal state isn't even really needed to get a decent start). I think this may not be a huge amount to figure out how to wire up inside opencode, but would make it a lot easier for it to see what the state is without invoking lake or lean to get it.

Just a random Friday morning idea in case it nerd snipes anyone.

[Adam Topaz]

I have opencode set up with the lean lsp. It works great!

[Julian Berman]

Nice! I assume you just added lake serve support right? (I.e. my "first step" there?)

[Adam Topaz]

Yup. I also have a custom mcp server (wip!) for further lean interaction.

[Adam Topaz]

One note about opencode to keep in mind: it is supposed to have Claude oauth support, but that seems to be in flux at the moment.

[Adam Topaz]

FWIW, the following is a minimal but fairly effective opencode.json setup for Lean4 (meta)programming:

{
  "$schema": "https://opencode.ai/config.json",
  "lsp": {
    "lean": {
      "command": ["lake", "serve"],
      "extensions": [".lean"]
    }
  },
  "mcp": {
    "lean4": {
      "type": "remote",
      "url": "https://gitmcp.io/leanprover/lean4",
      "enabled": true
    }
  }
}

[Julian Berman]

Ah nice I was wondering how you did it -- I did it here by modifying OpenCode's source code, it has a file with all its LSP definitions and was planning on PRing it before deciding it wasn't likely to be super useful without the extra pieces quite yet

[Adam Topaz]

gitmcp.io is useful as well -- it creates remote mcp servers for reading any (public) github repo.

[Adam Topaz]

If you do figure out how to get the lsp functionality to be compatible with lsp commands like plainGoal, please let me know!

[Franz Huschenbeth]

@Julian Berman Are you still planning to open a PR to Opencode? Or do you think it is too niche and we should just have our own DIY modifications, as shown here?

[Julian Berman]

I definitely think we should, I just haven't gotten a moment to look at this again!

[Julian Berman]

@Franz Huschenbeth please feel free to beat me to it if you are asking whether you can :)

[Julian Berman]

Otherwise I'll get to it amongst the rest of the pile of stuff I want to get to.

[Franz Huschenbeth]

I mainly wondered if it is on your list, if I chose to work on it, I will let you know for sure :)

[David Wood]

I've been using Opencode with Lean using the same configuration. Although it works in theory, Opencode has unfortunately been authored with very strict hardcoded timeouts for LSP diagnostics, which I'm running into constantly. In Lean's case, the problematic timeout is the one between subsequent diagnostic messages. The Lean server seems to send a few of them even for simple files, and Opencode currently only waits 150ms to receive follow-ups to the latest received. In my case, the first messages have no content, so Opencode is always prematurely concluding that its slop outputs have been validated. :(

[David Wood]

Customising this kind of behaviour would be very useful, even without any additional Lean functionality. In the meantime, I'm considering making a non-lean-specific PR just to make the debounce period configurable for different language servers.

[Kim Morrison]

I am pretty much convinced that AIs should not be using the LSP at all. It forces them into a slow iterative loop. I have better experience with just lake build!

[Franz Huschenbeth]

To be honest, I have also come to that conclusion.