QED LSP Developer Tutorial

QED is a custom language with a dedicated Language Server Protocol (LSP) service, providing basic features such as hover, goto definition, find references, and formatting.

This document introduces how to use the QED language server qed-lsp-server for a better development experience in VSCode, Neovim, and RustRover.

🛠️ Preparation

1. Clone repository:

  git clone https://github.com/QEDProtocol/qedlang-rust.git
  cd qed-lang

2. Compile qed-lsp-server：

  cd qed-lsp-server
  cargo build --release

⚠️ Note: Regardless of which IDE you are using, the qed-lsp-server binary is required for the language features to work properly.
Please make sure you have built it and remember its path.

💻 VSCode Usage Tutorial

Developer debugging mode (recommended for developers)

1. Start VSCode:

  cd qed-lsp-server/qed-lsp-vscode
  code .

2. Press F5 to enter plugin debugging mode. VSCode will start a new VSCode window and load the local plugin.
3. In the new window, open a QED project containing Dargo.toml to enable plugin features, such as:
   • Mouse hover → Show type information
   • Right click → Goto Definition / Find References / Format

💡 Note: In the file qed-lsp-vscode/src/extension.ts, the path to the qed-lsp-server binary is currently hardcoded:

const serverExecutable = path.join(
    // Warning: this path is hardcoded and may not be portable across systems.
    context.extensionPath, '..', '..', 'target', 'release', 'qed-lsp-server'
);

If you need to change the path (for example, to use a different build directory or binary location), please modify this line accordingly and then rebuild the extension by running:

  npm run build

🧑‍💻 Neovim usage tutorial (based on Lazy.nvim)

This guide demonstrates how to set up the QED language server (qed-lsp-server) in Neovim using the lazy.nvim plugin manager.

⚠️ Note: The qed-lsp-server binary must be compiled first and accessible in your system. Ensure the path to the binary is correct.

1️⃣ Plugin Installation

In your init.lua, make sure to install the necessary plugins:

require("lazy").setup({
  { "neovim/nvim-lspconfig" },             -- LSP support
  { "nvim-treesitter/nvim-treesitter", build = ":TSUpdate" }, -- syntax highlighting
  { "hrsh7th/nvim-cmp" },                  -- completion
  { "hrsh7th/cmp-nvim-lsp" },              -- LSP completion source
})

2️⃣ QED LSP Setup via Lazy

local lspconfig = require("lspconfig")
local configs = require("lspconfig.configs")

-- Register custom LSP
if not configs.qed_lsp then
configs.qed_lsp = {
   default_config = {
      cmd = {"/full path/to/qed-lsp-server" }, -- ⚠️ Note to fill in the full path
      filetypes = {"qed"},
      root_dir = lspconfig.util.root_pattern("Dargo.toml"),
      settings = {},
   },
}
end

lspconfig.qed_lsp.setup({})

-- Let Neovim recognize the `.qed` file type
vim.filetype.add({
   extension = {
      qed = "qed",
   },
})

Instead of manually configuring LSP in init.lua, you can configure it via Lazy plugin opts. Create a file like ~/.config/nvim/lua/plugins/lsp.lua and write:

return {
  "neovim/nvim-lspconfig",
  opts = function(_, opts)
    -- Tell Neovim `.qed` files are of type `qed`
    vim.filetype.add({ extension = { qed = "qed" } })

    -- Reuse Rust Tree-sitter highlighting for `.qed` files
    vim.treesitter.language.register("rust", "qed")

    -- Load LSP config
    local lspconfig = require("lspconfig")
    local configs = require("lspconfig.configs")

    -- Register qed_lsp_server only once
    if not configs.qed_lsp_server then
      configs.qed_lsp_server = {
        default_config = {
          cmd = { "/full/path/to/qed-lsp-server" }, -- 🔧 Replace with your built binary
          filetypes = { "qed" },
          root_dir = lspconfig.util.root_pattern("Dargo.toml", ".qed"),
          settings = {},
        },
      }
    end

    -- Attach server config to Lazy's LSP handler
    opts.servers.qed_lsp_server = {}
    return opts
  end,
}

✅ Once you’ve saved this config, reopen Neovim and run :Lazy sync to apply it.

✅ Additional Notes

• vim.filetype.add(...) tells Neovim that .qed files should be handled as the qed filetype.
• vim.treesitter.language.register("rust", "qed") means .qedfiles will reuse Rust’s highlighting engine via Tree-sitter.
• Make sure the qed-lsp-server binary is either in your PATH or referenced using the full path.

3️⃣ Navigation & Reference Lookup in Neovim

Once your qed-lsp-server is properly registered and running in Neovim, you can use the following built-in LSP keybindings to navigate your QED code efficiently.

-- Place these in your init.lua or keymap config file if not already present
vim.keymap.set("n", "gd", vim.lsp.buf.definition, { noremap = true, desc = "Go to Definition" })
vim.keymap.set("n", "gr", vim.lsp.buf.references, { noremap = true, desc = "Find References" })
vim.keymap.set("n", "K", vim.lsp.buf.hover, { noremap = true, desc = "Hover Documentation" })
vim.keymap.set("n", "<leader>rn", vim.lsp.buf.rename, { noremap = true, desc = "Rename Symbol" })
vim.keymap.set("n", "<leader>f", vim.lsp.buf.format, { noremap = true, desc = "Format Document" })

📚 Common shortcut keys description

⚙️ RustRover usage tutorial (based on LSP4IJ plugin)

This tutorial assumes that you have already completed the configuration of Rust in RustRover.

We will use the LSP plugin LSP Support (lsp4ij) provided by RedHat to enable custom LSP support for .qed files, realizing functions such as jump, hover, reference lookup, code formatting, etc.

📦 Step 1: Install the LSP4IJ plugin

1. Open RustRover and click RustRover > Settings in the upper left corner (or use the shortcut Cmd + ,).
2. Go to Plugins > Marketplace.
3. Search for lsp4ij .
4. Click Install and restart the IDE after the installation is complete.

✅ Step 2: Create a QED file type

1. Open Settings → Editor → File Types

2. Click "+" Add at the top to create a new File Type

3. Name: QED

4. Description: QED language

5. Configure highlighting (optional) fill in the following fields:

Then click Save.

🧠 Step 3: Configure the Language Server of QED language

Open Settings > Languages && Frameworks > Language Servers, we need to add a new configuration, click the plus sign ➕, there are three tabs in the new interface: Server, Mapping and Configuration.

▶️ Server tab

Used to register a new LSP service.

• Name: Fill in QED language server.
• Environment Variables: Leave it blank (optional, if you need to set DARGO_STD_PATH, you can fill it in here).
• Command: Fill in the path of your compiled LSP executable file, for example: /Users/UserName/bin/qed-lsp-server

▶️ Mapping tab

Used to map file types to language services.

• Language: Leave it blank.
• FileType: Click ➕, select QED on the left, and enter qed on the right
  • Note: If there is no QED option, please go back to step 2 and add the file type again.
• Filename Patterns: Click ➕, enter *.qed on the left, and enter qed on the right

📌 Note:

• The left side is the file type inside the IDE .
• The right side is the Language ID of the LSP Server, which needs to match your textDocument.languageId

▶️ Configuration (optional)

You can set:

• Server Trace Level: Set to Verbose to view more debugging information

• Client Trace Level: Set to Verbose or Info

• To view LSP communication logs, it is recommended to open the LSP Console view

✅ Step 4: Verify if it works

1. Open a QED project with Dargo.toml
2. Open the .qed file
3. You can try:

• Hover to view the type
• Go to Definition
• Find References
• Format Document

You can check the debug log in View > Tool Windows > LSP Console to confirm whether LSP is started correctly.