Verus neovim configuration

.envrc

#!/bin/bash

base="$(dirname "$(realpath "$1")")"

PATH_add "$base"

export VERUS_BINARY_PATH="${VERUS_BINARY_PATH:-/usr/bin/verus}"
export VERUS_SINGULAR_PATH="${VERUS_SINGULAR_PATH:-/usr/bin/Singular}"

lspconfig.lua

  on_init = function(client)
    local path = os.getenv('PATH')

    if path and path:find('verus') then
      client.config.settings['rust-analyzer'] = {
        check = {
          extraArgs = { '--expand-errors' },
        },
        procMacro = {
          enable = false,
        },
        diagnostics = {
          disabled = {
            'unresolved-proc-macro',
          },
        },
      }
      client.notify('workspace/didChangeConfiguration', { settings = client.config.settings })
    end

    return true
  end,

rust-analyzer

ln -s /usr/bin/verus-analyzer rust-analyzer

rust-toolchain.toml

[toolchain]
channel = "1.88.0"
profile = "minimal"
components = ["rustfmt", "clippy"]

rustfmt

#!/bin/bash

set -euo pipefail

if [[ "$#" == 0 || "$*" == "--edition 20"[0-9][0-9] ]]; then
    tmp=$(mktemp --tmpdir verusfmt.XXXX.rs)
    cat > "$tmp"
    verusfmt --verus-only "$tmp"
    "$(rustup which rustfmt)" < "$tmp"
    rm "$tmp"
else
    "$(rustup which rustfmt)" "$@"
fi