feat: add a neovim plugin as the canonical lsp client implementation (#1842)

* fix: bad link

* feat(neovim): init lsp

* feat(neovim): add bootstrap script

* build: add notice

.dockerignore

@@ -0,0 +1,10 @@
+# Ignored for `Dockerfile` build tinymist cli
+target
+node_modules
+editors
+tools
+refs
+local
+syntaxes
+docs
+contrib

Dockerfile

@@ -0,0 +1,48 @@
+# ```shell
+# docker build -t myriaddreamin/tinymist:latest .
+# ```
+#
+# ## References
+#
+# https://stackoverflow.com/questions/58473606/cache-rust-dependencies-with-docker-build
+# https://stackoverflow.com/a/64528456
+# https://depot.dev/blog/rust-dockerfile-best-practices
+
+ARG RUST_VERSION=1.85.1
+
+FROM rust:${RUST_VERSION}-bookworm AS base
+RUN apt-get install -y git
+RUN cargo install sccache --version ^0.7
+RUN cargo install cargo-chef --version ^0.1
+ENV RUSTC_WRAPPER=sccache SCCACHE_DIR=/sccache
+# to download the toolchain
+RUN --mount=type=cache,target=/usr/local/cargo/registry \
+    --mount=type=cache,target=$SCCACHE_DIR,sharing=locked \
+    cargo --version
+
+FROM base as planner
+WORKDIR app
+# We only pay the installation cost once, 
+# it will be cached from the second build onwards
+RUN cargo install cargo-chef 
+COPY . .
+RUN --mount=type=cache,target=/usr/local/cargo/registry \
+    --mount=type=cache,target=$SCCACHE_DIR,sharing=locked \
+    cargo chef prepare --recipe-path recipe.json
+
+FROM base as builder
+WORKDIR app
+RUN cargo install cargo-chef
+COPY --from=planner /app/recipe.json recipe.json
+RUN --mount=type=cache,target=/usr/local/cargo/registry \
+    --mount=type=cache,target=$SCCACHE_DIR,sharing=locked \
+    cargo chef cook --release --recipe-path recipe.json
+COPY . .
+RUN --mount=type=cache,target=/usr/local/cargo/registry \
+    --mount=type=cache,target=$SCCACHE_DIR,sharing=locked \
+    cargo build -p tinymist --release
+
+FROM debian:12
+WORKDIR /app/
+COPY --from=builder /app/target/release/tinymist /usr/local/bin
+ENTRYPOINT ["/usr/local/bin/tinymist"]

docs/tinymist/frontend/neovim.typ

@@ -193,4 +193,5 @@ autocmd BufNewFile,BufRead *.typ setfiletype typst
 
 = Contributing
 <contributing>
-You can submit issues or make PRs to #link("https://github.com/Myriad-Dreamin/tinymist")[GitHub];.
+
+Please check the #github-link("/editors/neovim/CONTRIBUTING.md")[contributing guide] for more information on how to contribute to the project.

editors/neovim/.gitignore

@@ -0,0 +1 @@
+target

editors/neovim/CONTRIBUTING.md

@@ -0,0 +1,16 @@
+
+# Contributing
+
+This guide extends the root [CONTRIBUTING.md](/CONTRIBUTING.md) file with editor-specific information for Neovim integrations.
+
+# Running Spec Editor Setup
+
+```
+./bootstrap.sh editor
+```
+
+# Running Tests
+
+```
+./bootstrap.sh test
+```

editors/neovim/Dockerfile

@@ -0,0 +1,43 @@
+# Not for end users! This is a Dockerfile to develop the Neovim plugin it self.
+# https://github.com/Julian/lean.nvim/tree/1b2752069d700a3e6c7953f5c117d49c134ec711/.devcontainer/lazyvim
+
+FROM debian:12 AS builder
+
+RUN apt-get update && apt-get install -y \
+    git \
+    file \
+    ninja-build gettext cmake unzip curl build-essential
+
+RUN git clone --filter=blob:none --branch stable https://github.com/neovim/neovim && cd neovim && make CMAKE_BUILD_TYPE=RelWithDebInfo
+USER root
+RUN cd neovim/build && cpack -G DEB && dpkg -i nvim-linux-x86_64.deb
+
+FROM myriaddreamin/tinymist:0.13.14
+
+COPY --from=builder /neovim/build/nvim-linux-x86_64.deb /tmp/nvim-linux-x86_64.deb
+RUN apt-get update && apt-get install -y curl git ripgrep build-essential unzip
+RUN apt-get update && apt-get install -y python3
+RUN apt-get install -y /tmp/nvim-linux-x86_64.deb \
+    && rm /tmp/nvim-linux-x86_64.deb
+
+RUN useradd --create-home --shell /bin/bash runner
+USER runner
+WORKDIR /home/runner
+
+RUN for dependency in AndrewRadev/switch.vim andymass/vim-matchup neovim/nvim-lspconfig nvim-lua/plenary.nvim tomtom/tcomment_vim lewis6991/satellite.nvim; do git clone --quiet --filter=blob:none "https://github.com/$dependency" "packpath/$(basename $dependency)"; done
+RUN for dependency in Julian/inanis.nvim; do git clone --quiet --filter=blob:none "https://github.com/$dependency" "packpath/$(basename $dependency)"; done
+
+ENV XDG_CONFIG_HOME=/home/runner/.config
+ENV XDG_DATA_HOME=/home/runner/.local/share
+ENV XDG_STATE_HOME=/home/runner/.local/state
+ENV XDG_CACHE_HOME=/home/runner/.cache
+
+COPY init.lua $XDG_CONFIG_HOME/nvim/init.lua
+COPY plugins/dev.lua $XDG_CONFIG_HOME/nvim/lua/plugins/dev.lua
+COPY plugins/lsp-folding.lua $XDG_CONFIG_HOME/nvim/lua/plugins/lsp-folding.lua
+COPY plugins/mason-workaround.lua $XDG_CONFIG_HOME/nvim/lua/plugins/mason-workaround.lua
+COPY plugins/tinymist.lua $XDG_CONFIG_HOME/nvim/lua/others/tinymist.lua
+
+# SHELL isn't supported by OCI images
+ENTRYPOINT []
+

editors/neovim/LICENSES-LEAN-NVIM

@@ -0,0 +1,187 @@
+===============================================================================
+The Neovim logo, which has been modified in lean.nvim's logo, is authored by
+Jason Long & licensed under the Creative Commons Attribution 3.0 Unported
+license available at https://creativecommons.org/licenses/by/3.0/deed.en
+
+===============================================================================
+The abbreviations JSON file is maintained alongside the Lean VSCode extension,
+and the Lean logo is maintained alongside the Lean 4 codebase, both of which
+are licensed under the below Apache License.
+===============================================================================
+
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS

editors/neovim/NOTICE

@@ -0,0 +1,3 @@
+## Files in `lua` and `spec` directories
+
+- files in `lua/std` and `spec` are mostly copied from lean.nvim. They are licensed under [LICENSES-LEAN-NVIM](./LICENSES-LEAN-NVIM).

editors/neovim/README.md

@@ -195,5 +195,3 @@ autocmd BufNewFile,BufRead *.typ setfiletype typst
 ```
 
 ## Contributing
-
-You can submit issues or make PRs to [GitHub](https://github.com/Myriad-Dreamin/tinymist).

editors/neovim/bootstrap.sh

@@ -0,0 +1,19 @@
+# todo: it is in very early stage, so we are doing dirty things.
+
+# python3 ./spec/main.py
+
+DOCKER_ARGS=
+if [ "$1" = "test" ]; then
+    DOCKER_ARGS="python3 ./spec/main.py"
+elif [ "$1" = "bash" ]; then
+    DOCKER_ARGS="bash"
+elif [ "$1" = "editor" ]; then
+    DOCKER_ARGS="nvim ."
+else
+    echo "Usage: $0 [test|bash|editor]"
+    exit 1
+fi
+
+cd ../.. && docker build -t myriaddreamin/tinymist:0.13.14 .
+docker build -t myriaddreamin/tinymist-nvim:0.13.14 .
+docker run --rm -it -v $PWD/../../tests/workspaces:/home/runner/dev/workspaces -v $PWD:/home/runner/dev -v $PWD/target/.local:/home/runner/.local -v $PWD/target/.cache:/home/runner/.cache -w /home/runner/dev myriaddreamin/tinymist-nvim:0.13.14 $DOCKER_ARGS

editors/neovim/init.lua

@@ -0,0 +1,96 @@
+-- This is a single file that bootstraps neovim editor for development.
+-- Plus plugins in the `plugins` directory, it should be ready total edit typst files.
+
+-- -- bootstrap lazy.nvim and your plugins
+local lazypath = vim.fn.stdpath("data") .. "/lazy/lazy.nvim"
+if not (vim.uv or vim.loop).fs_stat(lazypath) then
+    local lazyrepo = "https://github.com/folke/lazy.nvim.git"
+    local out = vim.fn.system({ "git", "clone", "--filter=blob:none", "--branch=stable", lazyrepo, lazypath })
+    if vim.v.shell_error ~= 0 then
+        vim.api.nvim_echo({
+            { "Failed to clone lazy.nvim:\n", "ErrorMsg" },
+            { out,                            "WarningMsg" },
+            { "\nPress any key to exit..." },
+        }, true, {})
+        vim.fn.getchar()
+        os.exit(1)
+    end
+end
+vim.opt.rtp:prepend(lazypath)
+
+
+-- Sync clipboard between OS and Neovim.
+--  Remove this option if you want your OS clipboard to remain independent.
+--  See `:help 'clipboard'`
+vim.opt.clipboard:append 'unnamedplus'
+
+-- Fix "waiting for osc52 response from terminal" message
+-- https://github.com/neovim/neovim/issues/28611
+
+if vim.env.SSH_TTY ~= nil then
+    -- Set up clipboard for ssh
+
+    local function my_paste(_)
+        return function(_)
+            local content = vim.fn.getreg '"'
+            return vim.split(content, '\n')
+        end
+    end
+
+    vim.g.clipboard = {
+        name = 'OSC 52',
+        copy = {
+            ['+'] = require('vim.ui.clipboard.osc52').copy '+',
+            ['*'] = require('vim.ui.clipboard.osc52').copy '*',
+        },
+        paste = {
+            -- No OSC52 paste action since wezterm doesn't support it
+            -- Should still paste from nvim
+            ['+'] = my_paste '+',
+            ['*'] = my_paste '*',
+        },
+    }
+end
+
+-- important for running LSP servers
+-- vim.lsp.enable('tinymist')
+
+vim.api.nvim_set_keymap("n", "gd", "<cmd>lua vim.lsp.buf.definition()<CR>", { noremap = true, silent = true })
+
+require("lazy").setup({
+    spec = {
+        -- add LazyVim and import its plugins
+        { "LazyVim/LazyVim", import = "lazyvim.plugins" },
+        -- import/override with your plugins
+        { import = "plugins" },
+    },
+    defaults = {
+        -- By default, only LazyVim plugins will be lazy-loaded. Your custom plugins will load during startup.
+        -- If you know what you're doing, you can set this to `true` to have all your custom plugins lazy-loaded by default.
+        lazy = false,
+        -- It's recommended to leave version=false for now, since a lot the plugin that support versioning,
+        -- have outdated releases, which may break your Neovim install.
+        version = false, -- always use the latest git commit
+        -- version = "*", -- try installing the latest stable version for plugins that support semver
+    },
+    install = { colorscheme = { "tokyonight" } },
+    checker = {
+        enabled = true, -- check for plugin updates periodically
+        notify = false, -- notify on update
+    },                  -- automatically check for plugin updates
+    performance = {
+        rtp = {
+            -- disable some rtp plugins
+            disabled_plugins = {
+                "gzip",
+                -- "matchit",
+                -- "matchparen",
+                -- "netrwPlugin",
+                "tarPlugin",
+                "tohtml",
+                "tutor",
+                "zipPlugin",
+            },
+        },
+    },
+})

editors/neovim/lua/std/inductive.lua

@@ -0,0 +1,72 @@
+---@generic S
+---@alias Constructor fun(self: any, ...: any): S
+---@alias InductiveMethod fun(self: S, ...: any): any
+
+---@alias ConstructorDefs table<string, Constructor> | table<string, table<string, InductiveMethod>>
+
+---@class Inductive<S> : { [string]: InductiveMethod }
+---@operator call(table): `S`
+
+---Create a new inductive type.
+---@param name string The name of the new type, used only for errors
+---@param defs ConstructorDefs A table of constructor definitions
+---@return Inductive
+return function(name, defs)
+  local Type = {}
+
+  local to_obj
+
+  local _, first = next(defs)
+  if type(first) ~= 'table' then
+    to_obj = function(_, t)
+      return t
+    end
+  else
+    local methods = vim.tbl_keys(first)
+
+    to_obj = function(constructor_name, impl)
+      local obj = setmetatable({
+        serialize = function(self)
+          return { [constructor_name] = self[1] }
+        end,
+      }, { __index = Type })
+
+      for _, method_name in ipairs(methods) do
+        local method = impl[method_name]
+
+        if not method then
+          error(('%s method is missing for %s.%s'):format(method_name, name, constructor_name))
+        end
+        obj[method_name] = method
+        impl[method_name] = nil -- so we can tell if there are any extras...
+      end
+
+      local extra = next(impl)
+      if extra then
+        error(('%s method is unexpected for %s.%s'):format(extra, name, constructor_name))
+      end
+      return function(_, ...)
+        return setmetatable({ ... }, {
+          __index = obj,
+          __call = function(_, ...)
+            return Type[constructor_name](Type, ...)
+          end,
+        })
+      end
+    end
+  end
+
+  for constructor_name, impl in pairs(defs) do
+    Type[constructor_name] = to_obj(constructor_name, impl)
+  end
+  return setmetatable(Type, {
+    __call = function(self, data, ...)
+      local constructor_name, value = next(data)
+      local constructor = self[constructor_name]
+      if not constructor then
+        error(('Invalid %s constructor: %s'):format(name, constructor_name))
+      end
+      return constructor(self, value, ...)
+    end,
+  })
+end

editors/neovim/lua/std/lsp.lua

@@ -0,0 +1,119 @@
+local lsp = {}
+
+---Convert an LSP position to a (0, 0)-indexed tuple.
+---
+---These are used by extmarks.
+---See `:h api-indexing` for details.
+---@param position lsp.Position
+---@param bufnr integer the buffer whose position is referred to
+---@return { [1]: integer, [2]: integer } position
+function lsp.position_to_byte0(position, bufnr)
+  local line = vim.api.nvim_buf_get_lines(bufnr, position.line, position.line + 1, false)[1] or ''
+  local ok, col = pcall(vim.str_byteindex, line, position.character, true)
+  return { position.line, ok and col or position.character }
+end
+
+---Polyfill vim.fs.relpath-ish for Neovim < 0.11.
+---
+---Don't use this for real filesystem operations (as opposed to display),
+---its implementation is naive!
+local relpath = vim.fs.relpath
+  or function(base, target)
+    if vim.startswith(target, base .. '/') then
+      return target:sub(#base + 2)
+    end
+    return target
+  end
+
+---Convert LSP document params inside the current buffer to a human-readable (1, 1)-indexed string.
+---
+---Takes the workspace into account in order to return a relative path.
+---@param params UIParams
+function lsp.text_document_position_to_string(params)
+  local workspace = vim.lsp.buf.list_workspace_folders()[1] or vim.uv.cwd()
+  local filename = vim.uri_to_fname(params.textDocument.uri)
+
+  return ('%s at %d:%d'):format(
+    relpath(workspace, filename) or filename,
+    params.position.line + 1,
+    params.position.character + 1
+  )
+end
+
+---Convert an LSP range to a human-readable (1, 1)-indexed string.
+---
+---We use 1-based indexing here as the `gg` and `|` motions are 1-indexed,
+---which is the most likely way a human (you?) will interact with this
+---information.
+---@param range lsp.Range
+function lsp.range_to_string(range)
+  return ('%d:%d-%d:%d'):format(
+    range.start.line + 1,
+    range.start.character + 1,
+    range['end'].line + 1,
+    range['end'].character + 1
+  )
+end
+
+-- ~*~ vim.lsp._private_functions we still need... ~*~
+
+local format_line_ending = {
+  ['unix'] = '\n',
+  ['dos'] = '\r\n',
+  ['mac'] = '\r',
+}
+
+---@private
+---@param bufnr (number)
+---@return string
+local function buf_get_line_ending(bufnr)
+  return format_line_ending[vim.bo[bufnr].fileformat] or '\n'
+end
+
+---@private
+---Returns full text of buffer {bufnr} as a string.
+---
+---@param bufnr (number) Buffer handle, or 0 for current.
+---@return string # Buffer text as string.
+function lsp.buf_get_full_text(bufnr)
+  local line_ending = buf_get_line_ending(bufnr)
+  local text = table.concat(vim.api.nvim_buf_get_lines(bufnr, 0, -1, true), line_ending)
+  if vim.bo[bufnr].eol then
+    text = text .. line_ending
+  end
+  return text
+end
+
+-- vim.lsp.diagnostic has a *private* `diagnostic_lsp_to_vim` :/ ...
+--
+-- the below comes from there / is required for assembling vim.Diagnostic
+-- objects out of LSP responses
+
+---@param severity lsp.DiagnosticSeverity
+function lsp.severity_lsp_to_vim(severity)
+  if type(severity) == 'string' then
+    severity = vim.lsp.protocol.DiagnosticSeverity[severity] ---@type integer
+  end
+  return severity
+end
+
+---@param diagnostic lsp.Diagnostic
+---@param client_id integer
+---@return table?
+function lsp.tags_lsp_to_vim(diagnostic, client_id)
+  local tags ---@type table?
+  for _, tag in ipairs(diagnostic.tags or {}) do
+    if tag == vim.lsp.protocol.DiagnosticTag.Unnecessary then
+      tags = tags or {}
+      tags.unnecessary = true
+    elseif tag == vim.lsp.protocol.DiagnosticTag.Deprecated then
+      tags = tags or {}
+      tags.deprecated = true
+    else
+      vim.lsp.log.info(string.format('Unknown DiagnosticTag %d from LSP client %d', tag, client_id))
+    end
+  end
+  return tags
+end
+
+return lsp

editors/neovim/lua/std/nvim/buffer.lua

@@ -0,0 +1,25 @@
+---A Neovim buffer.
+---@class Buffer
+---@field bufnr integer The buffer number
+local Buffer = {}
+Buffer.__index = Buffer
+
+---Bind to a Neovim buffer.
+---@param bufnr? integer buffer number, defaulting to the current one
+---@return Buffer
+function Buffer:from_bufnr(bufnr)
+  return setmetatable({ bufnr = bufnr or vim.api.nvim_get_current_buf() }, self)
+end
+
+---Bind to the current buffer.
+function Buffer:current()
+  return self:from_bufnr(vim.api.nvim_get_current_buf())
+end
+
+---The buffer's name.
+---@return string name
+function Buffer:name()
+  return vim.api.nvim_buf_get_name(self.bufnr)
+end
+
+return Buffer

editors/neovim/lua/std/nvim/tab.lua

@@ -0,0 +1,55 @@
+local Window = require 'std.nvim.window'
+
+---A Neovim tab.
+---@class Tab
+---@field id integer The tab number
+local Tab = {}
+Tab.__index = Tab
+
+---Bind to a Neovim tab.
+---@param id? integer tab ID, defaulting to the current one
+---@return Tab
+function Tab:from_id(id)
+  return setmetatable({ id = id or vim.api.nvim_get_current_tabpage() }, self)
+end
+
+---Bind to the current tab.
+function Tab:current()
+  return self:from_id(vim.api.nvim_get_current_tabpage())
+end
+
+---All current tabs.
+---@return Tab[] tabs
+function Tab:all()
+  return vim
+    .iter(vim.api.nvim_list_tabpages())
+    :map(function(tab_id)
+      return self:from_id(tab_id)
+    end)
+    :totable()
+end
+
+---Open a new tab page.
+function Tab:new()
+  -- See https://github.com/neovim/neovim/pull/27223
+  vim.cmd.tabnew()
+  return self:current()
+end
+
+---Close the tab page.
+function Tab:close()
+  vim.cmd.tabclose(vim.api.nvim_tabpage_get_number(self.id))
+end
+
+---Return the windows present in the tab.
+---@return Window[] windows
+function Tab:windows()
+  return vim
+    .iter(vim.api.nvim_tabpage_list_wins(self.id))
+    :map(function(win_id)
+      return Window:from_id(win_id)
+    end)
+    :totable()
+end
+
+return Tab

editors/neovim/lua/std/nvim/window.lua

@@ -0,0 +1,153 @@
+local Buffer = require 'std.nvim.buffer'
+
+---A Neovim window.
+---@class Window
+---@field id integer The window ID
+local Window = {}
+Window.__index = Window
+
+---Bind to a Neovim window.
+---@param id? integer Window ID, defaulting to the current window
+---@return Window
+function Window:from_id(id)
+  return setmetatable({ id = id or vim.api.nvim_get_current_win() }, self)
+end
+
+---Bind to the current window.
+function Window:current()
+  return self:from_id(vim.api.nvim_get_current_win())
+end
+
+---Return the buffer shown in the window.
+---@return Buffer buffer
+function Window:buffer()
+  return Buffer:from_bufnr(self:bufnr())
+end
+
+---Return the buffer number of the window.
+---@return integer bufnr
+function Window:bufnr()
+  return vim.api.nvim_win_get_buf(self.id)
+end
+
+---Return the tab the window is on.
+---@return Tab tab
+function Window:tab()
+  return require('std.nvim.tab'):from_id(vim.api.nvim_win_get_tabpage(self.id))
+end
+
+---@class SplitOpts
+---@field buffer? Buffer the buffer to open in the new window (default current)
+---@field enter? boolean whether to enter the window (default false)
+---@field direction? 'left'|'right'|'above'|'below' the direction to split
+
+---Split a new window relative to this window.
+---@param opts? SplitOpts
+---@return Window
+function Window:split(opts)
+  opts = vim.tbl_extend('keep', opts or {}, { enter = false })
+  local direction = opts.direction or vim.o.splitright and 'right' or 'left'
+
+  local config = { win = self.id, split = direction }
+  local bufnr = opts.buffer and opts.buffer.bufnr or 0
+  local id = vim.api.nvim_open_win(bufnr, opts.enter, config)
+  return Window:from_id(id)
+end
+
+---Return the window's current cursor position.
+---
+---(1, 0)-indexed, like `nvim_win_get_cursor()`.
+---@return { [1]: integer, [2]: integer } pos
+function Window:cursor()
+  return vim.api.nvim_win_get_cursor(self.id)
+end
+
+---Set the window's current cursor position.
+---
+---(1, 0)-indexed, like `nvim_win_set_cursor()`.
+---@param pos { [1]: integer, [2]: integer } the new cursor position
+function Window:set_cursor(pos)
+  vim.api.nvim_win_set_cursor(self.id, pos)
+end
+
+---Is this the current window?
+function Window:is_current()
+  return vim.api.nvim_get_current_win() == self.id
+end
+
+---Make this window be the current one.
+function Window:make_current()
+  vim.api.nvim_set_current_win(self.id)
+end
+
+---Return the window's height.
+---@return integer height
+function Window:height()
+  return vim.api.nvim_win_get_height(self.id)
+end
+
+---Set the window's height.
+---@param height integer
+function Window:set_height(height)
+  vim.api.nvim_win_set_height(self.id, height)
+end
+
+---Return the window's width.
+---@return integer width
+function Window:width()
+  return vim.api.nvim_win_get_width(self.id)
+end
+
+---Set the window's width.
+---@param width integer
+function Window:set_width(width)
+  vim.api.nvim_win_set_width(self.id, width)
+end
+
+---Run a function with the window as temporary current window.
+function Window:call(fn)
+  vim.api.nvim_win_call(self.id, fn)
+end
+
+---Check if the window is valid.
+---
+---Do you wonder exactly what that corresponds to?
+---Well keep wondering because the Neovim docstring doesn't elaborate.
+---
+---But for one, closed windows return `false`.
+---@return boolean valid
+function Window:is_valid()
+  return vim.api.nvim_win_is_valid(self.id)
+end
+
+---Close the window.
+function Window:close()
+  vim.api.nvim_win_close(self.id, false)
+end
+
+-- Beyond the Neovim API...
+
+---Move the cursor to a given position.
+---
+---(1, 0)-indexed, like `nvim_win_set_cursor()`.
+---
+---Fires `CursorMoved` if (and only if) the cursor is now at a new position.
+---@param pos { [1]: integer, [2]: integer } the new cursor position
+function Window:move_cursor(pos)
+  local start = self:cursor()
+  self:set_cursor(pos)
+  if vim.deep_equal(self:cursor(), start) then
+    return
+  end
+  vim.api.nvim_exec_autocmds('CursorMoved', { buffer = self:bufnr() })
+end
+
+---Get the contents of the remainder of the line with the window's cursor.
+---@return string contents text from cursor position to the end of line
+function Window:rest_of_cursor_line()
+  local row, col = unpack(self:cursor())
+  local line = vim.api.nvim_buf_get_lines(self:bufnr(), row - 1, row, true)[1]
+  return line:sub(col + 1)
+end
+
+return Window

editors/neovim/lua/std/subprocess.lua

@@ -0,0 +1,22 @@
+local subprocess = {}
+
+---Run a subprocess, blocking on exit, and returning its stdout.
+---@return string: the lines of stdout of the exited process
+function subprocess.check_output(...)
+  local process = vim.system(...)
+  local result = process:wait()
+  if result.code == 0 then
+    return result.stdout
+  end
+
+  error(
+    string.format(
+      '%s exited with non-zero exit status %d.\nstderr contained:\n%s',
+      vim.inspect(process.cmd),
+      result.code,
+      result.stderr
+    )
+  )
+end
+
+return subprocess

editors/neovim/lua/std/text.lua

@@ -0,0 +1,29 @@
+local text = {}
+
+local function max_common_indent(str)
+  local _, _, common_indent, rest = str:find '^(%s*)(.*)'
+  local common_indent_len = #common_indent
+  local len
+  for indent in rest:gmatch '\n( +)' do
+    len = #indent
+    if len < common_indent_len then
+      common_indent, common_indent_len = indent, len
+    end
+  end
+  return common_indent
+end
+
+---Dedent a multi-line string.
+---@param str string
+function text.dedent(str)
+  str = str:gsub('\n *$', '\n') -- trim leading/trailing space
+  local prefix = max_common_indent(str)
+  return str:gsub('^' .. prefix, ''):gsub('\n' .. prefix, '\n')
+end
+
+---Build a single-line string out a multiline one, replacing \n with spaces.
+function text.s(str)
+  return text.dedent(str):gsub('\n', ' ')
+end
+
+return text

editors/neovim/lua/tinymist/init.lua

@@ -0,0 +1,16 @@
+local tinymist = {}
+
+---Setup function to be run in your init.lua.
+---@param opts lean.Config Configuration options
+function tinymist.setup(opts)
+    opts = opts or {}
+
+    opts.lsp = opts.lsp or {}
+    if opts.lsp.enable ~= false then
+        require('tinymist.lsp').enable(opts.lsp)
+    end
+
+    vim.g.tinymist_config = opts
+end
+
+return tinymist

editors/neovim/lua/tinymist/lsp.lua

@@ -0,0 +1,17 @@
+local lsp = {}
+
+---@param opts LeanClientConfig
+function lsp.enable(opts)
+    opts.capabilities = opts.capabilities or vim.lsp.protocol.make_client_capabilities()
+    opts = vim.tbl_deep_extend('keep', opts, {
+        init_options = {
+            -- editDelay = 10, -- see lean#289
+            hasWidgets = true,
+        },
+        on_init = function(_, response)
+        end,
+    })
+    require('lspconfig').tinymist.setup(opts)
+end
+
+return lsp

editors/neovim/plugins/dev.lua

@@ -0,0 +1,61 @@
+local tinymist = require("others.tinymist")[2]
+
+-- set binary path
+tinymist.opts.servers.tinymist.cmd = { "tinymist" }
+
+
+return {
+    { "mason-org/mason.nvim",           version = "^1.0.0" },
+    { "mason-org/mason-lspconfig.nvim", version = "^1.0.0" },
+
+    -- spread tinymist
+    tinymist,
+
+    -- change some telescope options and a keymap to browse plugin files
+    {
+        "nvim-telescope/telescope.nvim",
+        keys = {
+            -- add a keymap to browse plugin files
+            -- stylua: ignore
+            {
+                "<leader>fp",
+                function() require("telescope.builtin").find_files({ cwd = require("lazy.core.config").options.root }) end,
+                desc = "Find Plugin File",
+            },
+        },
+        -- change some options
+        opts = {
+            defaults = {
+                layout_strategy = "horizontal",
+                layout_config = { prompt_position = "top" },
+                sorting_strategy = "ascending",
+                winblend = 0,
+            },
+        },
+    },
+
+    -- add more treesitter parsers
+    {
+        "nvim-treesitter/nvim-treesitter",
+        opts = {
+            ensure_installed = {
+                "bash",
+                "json",
+                "lua",
+                "markdown",
+                "markdown_inline",
+                "vim",
+            },
+        },
+    },
+
+    -- add any tools you want to have installed below
+    {
+        "williamboman/mason.nvim",
+        opts = {
+            ensure_installed = {
+                "stylua",
+            },
+        },
+    },
+}

editors/neovim/plugins/mason-workaround.lua

@@ -0,0 +1,4 @@
+return {
+    { "mason-org/mason.nvim",           version = "^1.0.0" },
+    { "mason-org/mason-lspconfig.nvim", version = "^1.0.0" },
+}

editors/neovim/plugins/tinymist.lua

@@ -1,7 +1,39 @@
+-- https://github.com/neovim/neovim/blob/381806729db1016106b02d866c4f4f64f76a351f/src/nvim/highlight_group.c
+local links = {
+  -- Unable to pick a suitable highlight group for the following:
+  -- ['@lsp.type.raw.typst'] = '@markup.link',
+  -- ['@lsp.type.punct.typst'] = '@punctuation',
+  -- ['@lsp.mod.math.typst'] = '@',
+  -- "*.strong.emph": [
+  --     "markup.bold.typst markup.italic.typst"
+  -- ],
+
+  ['@lsp.mod.strong.typst'] = '@markup.strong',
+  ['@lsp.mod.emph.typst'] = '@markup.italic',
+
+  ['@lsp.type.bool.typst'] = '@boolean',
+  ['@lsp.type.escape.typst'] = '@string.escape',
+  ['@lsp.type.link.typst'] = '@markup.link',
+  ['@lsp.typemod.delim.math.typst'] = '@punctuation',
+  ['@lsp.typemod.operator.math.typst'] = '@operator',
+  ['@lsp.type.heading.typst'] = '@markup.heading',
+  ['@lsp.type.pol.typst'] = '@variable',
+  ['@lsp.type.error.typst'] = 'DiagnosticError',
+  ['@lsp.type.term.typst'] = '@markup.bold',
+  ['@lsp.type.marker.typst'] = '@punctuation',
+  ['@lsp.type.ref.typst'] = '@label',
+  ['@lsp.type.label.typst'] = '@label',
+}
+
+for newgroup, oldgroup in pairs(links) do
+  vim.api.nvim_set_hl(0, newgroup, { link = oldgroup, default = true })
+end
+
 return {
   -- requires tinymist
   {
     "williamboman/mason.nvim",
+    version = "^1.0.0",
     opts = {
       ensure_installed = {
         "tinymist",
@@ -23,31 +55,32 @@ return {
           root_dir = function()
             return vim.fn.getcwd()
           end,
-          --- See [Tinymist Server Configuration](https://github.com/Myriad-Dreamin/tinymist/blob/main/Configuration.md) for references.
+          single_file_support = true, -- Fixes LSP attachment in non-Git directories
+          --- See [Tinymist Server Configuration](https://github.com/Myriad-Dreamin/tinymist/blob/main/editors/neovim/Configuration.md) for references.
           settings = {
             --- You could set the formatter mode to use lsp-enhanced formatters.
             -- formatterMode = "typstyle",
-            
+
             --- If you would love to preview exported PDF files at the same time,
             --- you could set this to `onType` and open the file with your favorite PDF viewer.
             -- exportPdf = "onType",
           },
           on_attach = function(client, bufnr)
-              vim.keymap.set("n", "<leader>tp", function()
-                  client:exec_cmd({
-                      title = "pin",
-                      command = "tinymist.pinMain",
-                      arguments = { vim.api.nvim_buf_get_name(0) },
-                  }, { bufnr = bufnr })
-              end, { desc = "[T]inymist [P]in", noremap = true })
-      
-              vim.keymap.set("n", "<leader>tu", function()
-                  client:exec_cmd({
-                      title = "unpin",
-                      command = "tinymist.pinMain",
-                      arguments = { vim.v.null },
-                  }, { bufnr = bufnr })
-              end, { desc = "[T]inymist [U]npin", noremap = true })
+            vim.keymap.set("n", "<leader>tp", function()
+              client:exec_cmd({
+                title = "pin",
+                command = "tinymist.pinMain",
+                arguments = { vim.api.nvim_buf_get_name(0) },
+              }, { bufnr = bufnr })
+            end, { desc = "[T]inymist [P]in", noremap = true })
+
+            vim.keymap.set("n", "<leader>tu", function()
+              client:exec_cmd({
+                title = "unpin",
+                command = "tinymist.pinMain",
+                arguments = { vim.v.null },
+              }, { bufnr = bufnr })
+            end, { desc = "[T]inymist [U]npin", noremap = true })
           end,
         },
       },

editors/neovim/scripts/minimal_init.lua

@@ -0,0 +1,45 @@
+vim.o.display = 'lastline' -- Avoid neovim/neovim#11362
+vim.o.directory = ''
+vim.o.shada = ''
+
+local this_dir = vim.fs.dirname(debug.getinfo(1, 'S').source:sub(2))
+local lean_nvim_dir = vim.fs.dirname(this_dir)
+local packpath = vim.fs.joinpath('/home/runner/packpath/*')
+vim.opt.runtimepath:append(packpath)
+
+-- Doing this unconditionally seems to fail a random indent test?!?!
+-- Inanis/Plenary will automatically set rtp+. (which seems wrong, but OK)
+-- so really we need this just for `just nvim`...
+if #vim.api.nvim_list_uis() ~= 0 then
+    vim.opt.runtimepath:append(lean_nvim_dir)
+end
+
+vim.cmd [[
+  runtime! plugin/lspconfig.vim
+  runtime! plugin/matchit.vim
+  runtime! plugin/plenary.vim
+  runtime! plugin/switch.vim
+  runtime! plugin/tcomment.vim
+]]
+
+-- plenary forks subprocesses, so enable coverage here when appropriate
+if vim.env.LEAN_NVIM_COVERAGE then
+    local luapath = vim.fs.joinpath(lean_nvim_dir, 'luapath')
+    package.path = package.path
+        .. ';'
+        .. luapath
+        .. '/share/lua/5.1/?.lua;'
+        .. luapath
+        .. '/share/lua/5.1/?/init.lua;;'
+    package.cpath = package.cpath .. ';' .. luapath .. '/lib/lua/5.1/?.so;'
+    require 'luacov'
+end
+
+-- if vim.env.LEAN_NVIM_DEBUG then
+--     local port = 8088
+--     if vim.env.LEAN_NVIM_DEBUG ~= '' and vim.env.LEAN_NVIM_DEBUG ~= '1' then
+--         port = tonumber(vim.env.LEAN_NVIM_DEBUG)
+--     end
+--     require('osv').launch { host = '127.0.0.1', port = port }
+--     vim.wait(5000)
+-- end

editors/neovim/spec/fixtures.lua

@@ -0,0 +1,68 @@
+local this_file = debug.getinfo(1).source:match '@(.*)$'
+
+local root = vim.fs.joinpath(vim.fs.dirname(this_file), '../workspaces')
+local book_root = vim.fs.joinpath(root, 'book')
+local ind = vim.fs.joinpath(root, 'individuals')
+-- local indent = vim.fs.joinpath(root, 'indent')
+-- local widgets = vim.fs.joinpath(root, 'widgets')
+-- local project_root = vim.fs.normalize(vim.fs.joinpath(root, 'example-project'))
+
+local function child(name)
+  return vim.fs.joinpath(book_root, name)
+end
+
+local fixtures = {
+  -- indent = function()
+  --   return vim.iter(vim.fs.dir(indent)):map(function(each)
+  --     local name, replaced = each:gsub('.in.lean$', '')
+  --     if replaced == 0 then
+  --       return
+  --     end
+
+  --     ---@class IndentFixture
+  --     ---@field description string the name of the fixture
+  --     ---@field unindented string the path to the unindented version
+  --     ---@field expected string[] the expected indented lines
+
+  --     ---@type IndentFixture
+  --     return {
+  --       description = name:gsub('_', ' '),
+  --       unindented = vim.fs.joinpath(indent, each),
+  --       expected = vim.fn.readfile(vim.fs.joinpath(indent, name .. '.lean')),
+  --     }
+  --   end)
+  -- end,
+  -- widgets = widgets,
+
+  project = {
+    root = book_root,
+    child = child,
+
+    some_existing_file = child 'main.typ',
+    some_nonexisting_file = child 'bad.typ',
+    some_nested_existing_file = child 'chapters/chapter1.typ',
+    some_nested_nonexisting_file = child 'chapters/chapter3.typ',
+
+    -- some_dependency_file = child '.lake/packages/importGraph/ImportGraph/Imports.lean',
+  },
+}
+
+function fixtures.project:files()
+  return vim.iter {
+    ['existing'] = self.some_existing_file,
+    ['nonexisting'] = self.some_nonexisting_file,
+    ['nested existing'] = self.some_nested_existing_file,
+    ['nested nonexisting'] = self.some_nested_nonexisting_file,
+  }
+end
+
+assert.is.truthy(vim.uv.fs_stat(fixtures.project.some_existing_file))
+assert.is.falsy(vim.uv.fs_stat(fixtures.project.some_nonexisting_file))
+assert.is.truthy(vim.uv.fs_stat(fixtures.project.some_nested_existing_file))
+assert.is.falsy(vim.uv.fs_stat(fixtures.project.some_nested_nonexisting_file))
+-- assert.is.truthy(vim.uv.fs_stat(fixtures.project.some_dependency_file))
+
+-- assert.is.truthy(vim.uv.fs_stat(indent))
+-- assert.is.truthy(vim.uv.fs_stat(widgets))
+
+return fixtures

editors/neovim/spec/helpers.lua

@@ -0,0 +1,294 @@
+local Tab = require 'std.nvim.tab'
+local Window = require 'std.nvim.window'
+local assert = require 'luassert'
+local text = require 'std.text'
+local fixtures = require 'spec.fixtures'
+
+-- local progress = require 'lean.progress'
+-- local util = require 'lean._util'
+
+---@class LeanClientCapabilities : lsp.ClientCapabilities
+---@field silentDiagnosticSupport? boolean Whether the client supports `DiagnosticWith.isSilent = true`.
+
+---@class LeanClientConfig : vim.lsp.ClientConfig
+---@field lean? LeanClientCapabilities
+
+---Find the `vim.lsp.Client` attached to the given buffer.
+---@param bufnr? number
+---@return vim.lsp.Client?
+function client_for(bufnr)
+  local clients = vim.lsp.get_clients { name = 'tinymist', bufnr = bufnr or 0 }
+  return clients[1]
+end
+
+local helpers = { _clean_buffer_counter = 1 }
+
+---Feed some keystrokes into the current buffer, replacing termcodes.
+function helpers.feed(contents, feed_opts)
+  feed_opts = feed_opts or 'mtx'
+  local to_feed = vim.api.nvim_replace_termcodes(contents, true, false, true)
+  vim.api.nvim_feedkeys(to_feed, feed_opts, true)
+end
+
+---Insert some text into the current buffer.
+function helpers.insert(contents, feed_opts)
+  feed_opts = feed_opts or 'x'
+  helpers.feed('i' .. contents, feed_opts)
+end
+
+function helpers.all_lean_extmarks(buffer, start, end_)
+  local extmarks = {}
+  for namespace, ns_id in pairs(vim.api.nvim_get_namespaces()) do
+    if namespace:match '^lean.' then
+      vim.list_extend(
+        extmarks,
+        vim.api.nvim_buf_get_extmarks(buffer, ns_id, start, end_, { details = true })
+      )
+    end
+  end
+  return extmarks
+end
+
+---Move the cursor to a new location.
+---
+---Ideally this function wouldn't exist, and one would call `set_cursor`
+---directly, but it does not fire `CursorMoved` autocmds.
+---This function exists therefore to make tests which have slightly
+---less implementation details in them (the manual firing of that autocmd).
+---
+---@param opts MoveCursorOpts
+function helpers.move_cursor(opts)
+  local window = opts.window or Window:current()
+  window:move_cursor(opts.to)
+end
+
+---Search forward in the buffer for the given text.
+---
+---Fires `CursorMoved` if the cursor moves and fails if it does not.
+function helpers.search(string)
+  local cursor = vim.api.nvim_win_get_cursor(0)
+  vim.fn.search(string)
+  assert.are_not.same(cursor, vim.api.nvim_win_get_cursor(0), 'Cursor did not move!')
+  vim.api.nvim_exec_autocmds('CursorMoved', {})
+end
+
+function helpers.wait_for_ready_lsp()
+  local succeeded, _ = vim.wait(15000, function()
+    local client = client_for(0)
+    return client and client.initialized or false
+  end)
+  assert.message('LSP server was never ready.').True(succeeded)
+end
+
+---Wait until a window that isn't one of the known ones shows up.
+---@param known table
+function helpers.wait_for_new_window(known)
+  local ids = vim
+      .iter(known)
+      :map(function(window)
+        return window.id
+      end)
+      :totable()
+
+  local new_window
+  local succeeded = vim.wait(1000, function()
+    new_window = vim.iter(vim.api.nvim_tabpage_list_wins(0)):find(function(window)
+      return not vim.tbl_contains(ids, window)
+    end)
+    return new_window
+  end)
+  assert.message('Never found a new window').is_true(succeeded)
+  return Window:from_id(new_window)
+end
+
+-- Even though we can delete a buffer, so should be able to reuse names,
+-- we do this to ensure if a test fails, future ones still get new "files".
+local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr)
+  local counter = helpers._clean_buffer_counter
+  helpers._clean_buffer_counter = helpers._clean_buffer_counter + 1
+  local unique_name = fixtures.project.child(('unittest-%d.typ'):format(counter))
+  vim.api.nvim_buf_set_name(bufnr, unique_name)
+end
+
+---Create a clean Lean buffer with the given contents.
+---
+---Waits for the LSP to be ready before proceeding with a given callback.
+--
+---Yes c(lean) may be a double entendre, and no I don't feel bad.
+function helpers.clean_buffer(contents, callback)
+  local lines
+
+  -- Support a 1-arg version where we assume the contents is an empty buffer.
+  if callback == nil then
+    callback = contents
+    lines = {}
+  else
+    lines = vim.split(text.dedent(contents:gsub('^\n', '')):gsub('\n$', ''), '\n')
+  end
+
+  return function()
+    local bufnr = vim.api.nvim_create_buf(false, false)
+    set_unique_name_so_we_always_have_a_separate_fake_file(bufnr)
+
+    vim.bo[bufnr].swapfile = false
+    vim.bo[bufnr].filetype = 'typst'
+    vim.api.nvim_buf_set_lines(bufnr, 0, -1, false, lines)
+
+    -- isn't it fun how fragile the order of the below lines is, and how
+    -- BufWinEnter seems automatically called by `nvim_set_current_buf`, but
+    -- `BufEnter` seems not automatically called by `nvim_buf_call` so we
+    -- manually trigger it?
+    vim.api.nvim_set_current_buf(bufnr)
+    vim.api.nvim_exec_autocmds('BufEnter', { buffer = bufnr })
+    vim.api.nvim_buf_call(bufnr, callback)
+
+    -- FIXME: Deleting buffers seems good for keeping our tests clean, but is
+    --        broken on 0.11 with impossible to diagnose invalid buffer errors.
+    -- vim.api.nvim_buf_delete(bufnr, { force = true })
+  end
+end
+
+---Wait a few seconds for line diagnostics, erroring if none arrive.
+function helpers.wait_for_line_diagnostics()
+  local params = vim.lsp.util.make_position_params(0, 'utf-16')
+  local succeeded, _ = vim.wait(15000, function()
+    if progress.at(params) == progress.Kind.processing then
+      return false
+    end
+    local diagnostics = util.lean_lsp_diagnostics { lnum = params.position.line }
+    return #diagnostics > 0
+  end)
+  assert.message('Waited for line diagnostics but none came.').True(succeeded)
+end
+
+function helpers.wait_for_filetype()
+  local result, _ = vim.wait(15000, function()
+    return vim.bo.filetype == 'typst'
+  end)
+  assert.message('filetype was never set').is_truthy(result)
+end
+
+---Assert about the current word.
+local function has_current_word(_, arguments)
+  assert.is.equal(arguments[1], vim.fn.expand '<cword>')
+  return true
+end
+assert:register('assertion', 'current_word', has_current_word)
+
+---Assert about the current line.
+local function has_current_line(_, arguments)
+  assert.is.equal(arguments[1], vim.api.nvim_get_current_line())
+  return true
+end
+assert:register('assertion', 'current_line', has_current_line)
+
+---Assert about the current cursor location.
+local function has_current_cursor(_, arguments)
+  local window = arguments[1].window
+  if not window then
+    window = Window:current()
+  elseif type(window) == 'number' then
+    window = Window:from_id(window)
+  end
+  local got = window:cursor()
+
+  local column = arguments[1][2] or arguments[1].column or 0
+  local expected = { arguments[1][1] or got[1], column }
+
+  assert.are.same(expected, got)
+  return true
+end
+assert:register('assertion', 'current_cursor', has_current_cursor)
+
+---Assert about the current tabpage.
+local function has_current_tabpage(_, arguments)
+  assert.are.same(Tab:current(), arguments[1])
+  return true
+end
+assert:register('assertion', 'current_tabpage', has_current_tabpage)
+
+---Assert about the current window.
+local function has_current_window(_, arguments)
+  assert.are.same(Window:current(), arguments[1])
+  return true
+end
+assert:register('assertion', 'current_window', has_current_window)
+
+local function _expected(arguments)
+  local expected = arguments[1][1] or arguments[1]
+  -- Handle cases where we're indeed checking for a real trailing newline.
+  local dedented = text.dedent(expected)
+  if dedented ~= expected then
+    expected = dedented:gsub('\n$', '')
+  end
+  return expected
+end
+
+---Assert about the entire buffer contents.
+local function has_buf_contents(_, arguments)
+  local bufnr = arguments[1].bufnr or 0
+  local got = table.concat(vim.api.nvim_buf_get_lines(bufnr, 0, -1, false), '\n')
+  assert.is.equal(_expected(arguments), got)
+  return true
+end
+assert:register('assertion', 'contents', has_buf_contents)
+
+assert:register('assertion', 'diff_contents', has_diff_contents)
+
+local function has_highlighted_text(_, arguments)
+  local inspected = vim.inspect_pos(0)
+  local highlight = vim.iter(inspected.extmarks):find(function(mark)
+    return mark.opts.hl_group == 'widgetElementHighlight'
+  end)
+
+  assert.is_not_nil(highlight, ('No highlighted text found in %s'):format(vim.inspect(inspected)))
+
+  local got = vim.api.nvim_buf_get_text(
+    0,
+    highlight.row,
+    highlight.col,
+    highlight.end_row,
+    highlight.end_col,
+    {}
+  )[1]
+  assert.are.same(arguments[1], got)
+  return true
+end
+
+assert:register('assertion', 'highlighted_text', has_highlighted_text)
+
+local function has_all(_, arguments)
+  local contents = arguments[1]
+
+  if type(contents) == 'table' then
+    contents = table.concat(contents, '\n')
+  end
+  local expected = arguments[2]
+  for _, string in pairs(expected) do
+    assert.has_match(string, contents, nil, true)
+  end
+  return true
+end
+
+assert:register('assertion', 'has_all', has_all)
+
+---Assert a tabpage has the given windows open in it.
+local function has_open_windows(_, arguments)
+  local expected
+  if arguments.n == 1 and type(arguments[1]) == 'table' then
+    expected = arguments[1]
+    expected.n = #expected
+  else
+    expected = arguments
+  end
+  local got = vim.api.nvim_tabpage_list_wins(0)
+  got.n = #got
+  table.sort(expected)
+  table.sort(got)
+  assert.are.same(expected, got)
+  return true
+end
+
+assert:register('assertion', 'windows', has_open_windows)
+
+return helpers

editors/neovim/spec/lsp_spec.lua

@@ -0,0 +1,30 @@
+---@brief [[
+--- Tests for basic (auto-)attaching of LSP clients.
+---@brief ]]
+
+local fixtures = require 'spec.fixtures'
+local helpers = require 'spec.helpers'
+
+require('tinymist').setup {}
+
+describe('LSP', function()
+  assert.is.empty(vim.lsp.get_clients { bufnr = 0, name = 'tinymist', _uninitialized = true })
+
+  it('is attached to .typ files within projects', function()
+    vim.cmd.edit(fixtures.project.some_existing_file)
+    assert.is.same(1, #vim.lsp.get_clients { bufnr = 0, name = 'tinymist', _uninitialized = true })
+  end)
+
+  it(
+    'is attached to single .typ files',
+    helpers.clean_buffer(function()
+      assert.is.same(1, #vim.lsp.get_clients { bufnr = 0, name = 'tinymist', _uninitialized = true })
+    end)
+  )
+
+  it('is not attached to non-typst files', function()
+    vim.cmd.split 'some_non_typst_file.tmp'
+    assert.is.empty(vim.lsp.get_clients { bufnr = 0, name = 'tinymist', _uninitialized = true })
+    vim.cmd.close { bang = true }
+  end)
+end)

editors/neovim/spec/main.py

@@ -0,0 +1,64 @@
+# -- packpath := justfile_directory() / "packpath"
+# -- scripts := justfile_directory() / "scripts"
+# -- doc := justfile_directory() / "doc"
+# -- src := justfile_directory() / "lua"
+# -- lean := src / "lean"
+# -- spec := justfile_directory() / "spec"
+# -- fixtures := spec / "fixtures"
+# -- demos := justfile_directory() / "demos"
+
+# -- init_lua := scripts / "minimal_init.lua"
+# -- clean_config := justfile_directory() / ".test-config"
+
+# -- # Rebuild some test fixtures used in the test suite.
+# -- _rebuild-test-fixtures:
+# --     cd "{{ fixtures }}/example-project/"; lake build && lake build ProofWidgets Mathlib.Tactic.Widget.Conv
+
+# -- # Run the lean.nvim test suite.
+# -- [group('testing')]
+# -- test: _rebuild-test-fixtures _clone-test-dependencies
+# --     @just retest
+
+# -- # Run the test suite without rebuilding or recloning any dependencies.
+# -- [group('testing')]
+# -- retest *test_files=spec:
+# --     nvim --headless --clean -u {{ init_lua }} -c 'lua require("inanis").run{ specs = vim.split("{{ test_files }}", " "), minimal_init = "{{ init_lua }}", sequential = vim.env.TEST_SEQUENTIAL ~= nil }'
+
+
+import os
+import subprocess
+import sys
+
+def run_tests(test_files=None):
+    """
+    Run the Neovim test suite with the specified test files.
+    If no test files are specified, it runs all tests in the 'spec' directory.
+    """
+    init_lua = os.path.realpath(os.path.join(__file__, '../../scripts/minimal_init.lua'))
+    
+    if test_files is None:
+        # all test files in the 'spec' directory
+        test_files = []
+        for root, _, files in os.walk(os.path.dirname(__file__)):
+            test_files.extend(  os.path.join(root, f) for f in files if f.endswith('_spec.lua')  )
+    test_files = ' '.join(test_files)
+
+    command = [
+        'nvim',
+        '--headless',
+        '--clean',
+        '-u', init_lua,
+        '-c', f'lua require("inanis").run{{ specs = vim.split("{test_files}", " "), minimal_init = "{init_lua}", sequential = vim.env.TEST_SEQUENTIAL ~= nil }}'
+    ]
+
+    subprocess.run(command, check=True)
+
+if __name__ == "__main__":
+    # Check if any test files are provided as command line arguments
+    if len(sys.argv) > 1:
+        test_files = ' '.join(sys.argv[1:])
+    else:
+        test_files = None
+
+    run_tests(test_files)
+

lazyvim/Dockerfile

@@ -0,0 +1,41 @@
+FROM ubuntu:24.04 AS builder
+
+RUN apt-get update && apt-get install -y \
+    git \
+    file \
+    ninja-build gettext cmake unzip curl build-essential
+
+RUN git clone --filter=blob:none --branch stable https://github.com/neovim/neovim && cd neovim && make CMAKE_BUILD_TYPE=RelWithDebInfo
+RUN cd neovim/build && cpack -G DEB && dpkg -i nvim-linux64.deb
+
+
+FROM ubuntu:24.04
+
+COPY --from=builder /neovim/build/nvim-linux64.deb /tmp/nvim-linux64.deb
+RUN apt-get update && apt-get install -y \
+    /tmp/nvim-linux64.deb \
+    curl \
+    gcc \
+    git \
+    make \
+    ripgrep \
+    zsh \
+    && rm /tmp/nvim-linux64.deb
+
+RUN useradd --create-home --shell /bin/zsh lean
+USER lean
+WORKDIR /home/lean
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+ENV PATH="/home/lean/.elan/bin:${PATH}"
+
+RUN git clone --filter=blob:none https://github.com/LazyVim/starter ~/.config/nvim
+COPY lean.lua .config/nvim/lua/plugins/lean.lua
+
+ARG LEAN_PROJECT=https://github.com/leanprover-community/mathlib4
+
+RUN git clone --filter=blob:none $LEAN_PROJECT && cd $(basename "$LEAN_PROJECT") && lake exe cache get && elan default "$(cat lean-toolchain || echo stable)"
+
+# SHELL isn't supported by OCI images
+CMD ["zsh", "-l"]

lazyvim/devcontainer.json

@@ -0,0 +1,5 @@
+{
+  "name": "lazylean.nvim",
+  "build": { "dockerfile": "Dockerfile" },
+  "onCreateCommand": "git clone --filter=blob:none https://github.com/leanprover-community/Mathlib4.git && cd Mathlib4 && lake exe cache get! && nvim +quit"
+}

lazyvim/lean.lua

@@ -0,0 +1,18 @@
+return {
+  {
+    'Julian/lean.nvim',
+    dependencies = {
+      'nvim-lua/plenary.nvim',
+      'neovim/nvim-lspconfig',
+    },
+    ---@module 'lean'
+    ---@type lean.Config
+    opts = {
+      infoview = {
+        horizontal_position = 'top',
+        show_processing = false,
+      },
+      mappings = true,
+    },
+  },
+}

package.json

@@ -17,6 +17,7 @@
     "build:editor-tools": "cd tools/editor-tools/ && yarn run build",
     "build:preview": "cd tools/typst-preview-frontend && yarn run build && rimraf ../../crates/tinymist-assets/src/typst-preview.html && cpr ./dist/index.html ../../crates/tinymist-assets/src/typst-preview.html",
     "build:l10n": "yarn extract:l10n && node scripts/build-l10n.mjs",
+    "build:docker": "docker build -t myriaddreamin/tinymist:0.13.14 .",
     "extract:l10n": "yarn extract:l10n:ts && yarn extract:l10n:rs",
     "extract:l10n:ts": "cargo run --release --bin tinymist-l10n -- --kind ts --dir ./editors/vscode --output ./locales/tinymist-vscode-rt.toml",
     "extract:l10n:rs": "cargo run --release --bin tinymist-l10n -- --kind rs --dir ./crates --output ./locales/tinymist-rt.toml && rimraf ./crates/tinymist-assets/src/tinymist-rt.toml && cpr ./locales/tinymist-rt.toml ./crates/tinymist-assets/src/tinymist-rt.toml",

tests/workspaces/book/chapters/chapter1.typ

@@ -0,0 +1,4 @@
+
+= Chapter 1
+
+#lorem(50)

tests/workspaces/book/chapters/chapter2.typ

@@ -0,0 +1,4 @@
+
+= Chapter 2
+
+#lorem(50)

tests/workspaces/book/main.typ

@@ -0,0 +1,4 @@
+#include "chapters/chapter1.typ"
+#include "chapters/chapter2.typ"
+
+

tests/workspaces/individuals/tiny.typ

@@ -0,0 +1,5 @@
+
+= Hello
+
+#lorem(50)
+