From 1e484c0b90dd84dc5f820bc3d8dc1d7dcf7e59bb Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 30 Jul 2026 09:55:53 +0200 Subject: [PATCH 1/5] move from copilot-instructions to AGENTS.md --- .github/copilot-instructions.md => AGENTS.md | 45 ++++++++++---------- 1 file changed, 22 insertions(+), 23 deletions(-) rename .github/copilot-instructions.md => AGENTS.md (75%) diff --git a/.github/copilot-instructions.md b/AGENTS.md similarity index 75% rename from .github/copilot-instructions.md rename to AGENTS.md index 991077d49d..afa7476616 100644 --- a/.github/copilot-instructions.md +++ b/AGENTS.md @@ -1,4 +1,4 @@ -# Copilot Instructions for CSLib +# Project Instructions ## Repository Overview @@ -18,12 +18,12 @@ | Command | Purpose | When to Use | |---------|---------|-------------| | `lake build` | Build the library | After any code change | -| `lake build --wfail --iofail` | Build with CI strictness (fails on warnings) | **Always use before committing** | +| `lake build --wfail --iofail` | Build with CI strictness (fails on warnings) | Before committing | | `lake test` | Run all tests (builds CslibTests + checks init imports) | After changes to verify correctness | | `lake lint` | Run environment linters (Batteries/Mathlib) | Before committing | | `lake exe lint-style` | Run text-based style linters | Before committing | -| `lake exe mk_all --module --check` | Verify Cslib.lean imports all modules | After adding new files | -| `lake exe mk_all --module` | Auto-update Cslib.lean imports | After adding new files | +| `lake exe mk_all --check` | Verify Cslib.lean imports all modules | After adding new files | +| `lake exe mk_all` | Auto-update Cslib.lean imports | After adding new files | ### Full CI Validation Sequence @@ -31,7 +31,7 @@ Run these commands **in order** to replicate CI checks locally: ```bash lake build --wfail --iofail -lake exe mk_all --module --check +lake exe mk_all --check lake test lake lint lake exe lint-style @@ -64,8 +64,7 @@ lake exe lint-style │ └── Logics/ # Logic formalisations (e.g., Linear Logic, Hennessy-Milner Logic) ├── CslibTests/ # Test files ├── scripts/ # Build and maintenance scripts -│ ├── noshake.json # Import exceptions for shake tool -│ └── nolints.json # Lint exceptions +│ └── noshake.json # Import exceptions for shake tool └── .github/workflows/ # CI workflows ``` @@ -79,9 +78,9 @@ Every file in `Cslib/` must transitively import `Cslib/Init.lean`. This sets up - `Cslib.Init` itself ### 2. New Files Must Be Added to Cslib.lean -When creating a new `.lean` file in `Cslib/`, add its import to `Cslib.lean`. Run: +When creating a new `.lean` file in `Cslib/`, add its import to `Cslib.lean` by running: ```bash -lake exe mk_all --module +lake exe mk_all ``` ### 3. PR Title Convention @@ -103,15 +102,22 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: $LIST_OF_AUTHORS -/ ``` +where $YEAR should be replaced with the current year, $AUTHOR_NAME with the name of the file creator, and $LIST_OF_AUTHORS with the list of authors (this is just the file creator if there are no additional authors). + +### 5. Always Read Local README.md Files + +Before working on any file or directory, **always read** all `README.md` files in all directories throughout the entire repository. + +These files contain essential context that must be understood before making changes. ## Code Style - Follow everything written in /CONTRIBUTING.md -- Follow [Mathlib style guide](https://leanprover-community.github.io/contribute/style.html) -- Use domain-specific variable names (e.g., `State` for state types, `μ` for transition labels) -- Keep proofs readable; golfing is welcome if proofs remain clear -- Use existing typeclasses for common concepts (transitions, reductions) -- Use `module` keyword at the start of files with `public import` statements +- Follow the [Mathlib code style](https://leanprover-community.github.io/contribute/style.html) +- Use domain-specific variable names when dealing with APIs that have a clear intention (e.g., `State` for state types, `μ` for transition labels). +- Keep proofs readable; golfing is welcome if proofs remain clear. +- Use existing typeclasses for common concepts (`Congruence`, `Context`, etc.). +- Use the `module` keyword at the start of files with `public import` statements. ## Linter Configuration @@ -122,18 +128,11 @@ Linters are configured in `lakefile.toml`. ### Creating a New Module 1. Create file in appropriate `Cslib/` subdirectory 2. Add `import Cslib.Init` (or import a module that imports it) -3. Run `lake exe mk_all --module` +3. Run `lake exe mk_all` 4. Run `lake build --wfail --iofail` 5. Run `lake test` to verify init imports ### Adding Tests 1. Create or modify a file in `CslibTests/` -2. Add import to `CslibTests.lean` if new file +2. Add import to `CslibTests.lean` if it is a new file 3. Run `lake test` - -## Trust These Instructions - -Only search for additional information if: -- A command fails with an unexpected error -- You need details about a specific module's API -- The instructions appear incomplete for your specific task From ea8cd1b61c8b4b1527de7a9466fd6eca2961688d Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 22 Sep 2026 21:16:29 +0200 Subject: [PATCH 2/5] cp header --- .devcontainer/Dockerfile | 26 ++++++++++++++++++++++++++ .devcontainer/devcontainer.json | 22 ++++++++++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 .devcontainer/Dockerfile create mode 100644 .devcontainer/devcontainer.json diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile new file mode 100644 index 0000000000..5f1d3f0971 --- /dev/null +++ b/.devcontainer/Dockerfile @@ -0,0 +1,26 @@ +# Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +# Released under Apache 2.0 license as described in the file LICENSE. +# Authors: Fabrizio Montesi + +FROM mcr.microsoft.com/devcontainers/base:ubuntu + +RUN apt-get update && apt-get install -y --no-install-recommends \ + build-essential \ + ca-certificates \ + curl \ + ripgrep \ + && rm -rf /var/lib/apt/lists/* + +# Install uv + uvx globally for Python CLI tooling (e.g., lean-lsp-mcp). +RUN curl -LsSf https://astral.sh/uv/install.sh | env UV_INSTALL_DIR=/usr/local/bin sh + +USER vscode +WORKDIR /home/vscode + +ENV PATH="/home/vscode/.elan/bin:/home/vscode/.local/bin:${PATH}" + +# Install elan +RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none + +# Install the Lean LSP MCP server +RUN uv tool install lean-lsp-mcp diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json new file mode 100644 index 0000000000..f89ecf7dae --- /dev/null +++ b/.devcontainer/devcontainer.json @@ -0,0 +1,22 @@ +{ + "name": "CSLib Devcontainer", + "build": { + "dockerfile": "Dockerfile" + }, + "postCreateCommand": "lake exe cache get && lake build", + "remoteUser": "vscode", + "mounts": [ + "source=cslib-elan-toolchains,target=/home/vscode/.elan/toolchains,type=volume", + "source=cslib-cache,target=/home/vscode/.cache,type=volume" + ], + "features": { + "ghcr.io/devcontainers/features/github-cli:1": {} + }, + "customizations": { + "vscode": { + "extensions": [ + "leanprover.lean4" + ] + } + } +} From 855c4fbb97fca9a109f065c989d91a572a1d3524 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 22 Sep 2026 21:43:23 +0200 Subject: [PATCH 3/5] setup for vibe --- scripts/README.md | 13 ++++ scripts/setup-mistral-vibe.sh | 125 ++++++++++++++++++++++++++++++++++ 2 files changed, 138 insertions(+) create mode 100755 scripts/setup-mistral-vibe.sh diff --git a/scripts/README.md b/scripts/README.md index 19d71dfa67..f1faeb1032 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -10,6 +10,19 @@ to learn about it as well! - `gendocs.sh` Generates the documentation for cslib using `lake`. +**Devcontainer helpers** +- `setup-mistral-vibe.sh` + Installs the Mistral Vibe VS Code extension (`mistralai.mistral-vibe-code`) if + missing and ensures required Mistral config entries for the `lean` agent and the `lean-lsp` MCP server are present. + + **Usage:** + ```bash + ./scripts/setup-mistral-vibe.sh + ``` + + **Optional environment variable:** + - `MISTRAL_CONFIG_FILE`: Override the path to `config.toml`. + **Managing nightly-testing and bump branches** - `create-adaptation-pr.sh` is a variant of the script from Batteries and implements some of the steps in the workflow for managing nightly and bump branches. diff --git a/scripts/setup-mistral-vibe.sh b/scripts/setup-mistral-vibe.sh new file mode 100755 index 0000000000..ec2e6fb60d --- /dev/null +++ b/scripts/setup-mistral-vibe.sh @@ -0,0 +1,125 @@ +#!/usr/bin/env bash + +# Configure Mistral Vibe for this development environment. +# - Installs the Mistral Vibe VS Code extension if missing. +# - Ensures required TOML entries exist in the Mistral config file. + +set -euo pipefail +IFS=$'\n\t' + +log() { + echo "[setup-mistral-vibe] $*" +} + +error() { + echo "[setup-mistral-vibe] ERROR: $*" >&2 +} + +ensure_code_cli() { + if ! command -v code >/dev/null 2>&1; then + error "The 'code' CLI is not available in PATH." + error "In VS Code, run: Command Palette -> 'Shell Command: Install code command in PATH'." + exit 1 + fi +} + +resolve_config_file() { + if [ -n "${MISTRAL_CONFIG_FILE:-}" ]; then + echo "$MISTRAL_CONFIG_FILE" + return + fi + + if [ -f "$HOME/.config/mistral/config.toml" ]; then + echo "$HOME/.config/mistral/config.toml" + return + fi + + if [ -f "$HOME/.mistral/config.toml" ]; then + echo "$HOME/.mistral/config.toml" + return + fi + + echo "$HOME/.config/mistral/config.toml" +} + +install_vibe_vscode_extension_if_missing() { + local extension_id="mistralai.mistral-vibe-code" + + if code --list-extensions | grep -Fxq "$extension_id"; then + log "VS Code extension '$extension_id' is already installed." + return + fi + + log "Installing VS Code extension '$extension_id'..." + code --install-extension "$extension_id" + log "Installed VS Code extension '$extension_id'." +} + +ensure_installed_agents_contains_lean() { + local config_file=$1 + + perl -0777 -i -pe ' + my $added = 0; + if (/^\s*installed_agents\s*=\s*\[(.*?)\]/ms) { + my $block = $&; + my $items = $1; + if ($items !~ /"lean"/) { + my $replacement = $block; + if ($replacement =~ /\[\s*\]/s) { + $replacement =~ s/\[\s*\]/[\n "lean",\n]/s; + } else { + $replacement =~ s/\]\s*$/ "lean",\n]/s; + } + s/\Q$block\E/$replacement/s; + $added = 1; + } + } else { + $_ .= "\ninstalled_agents = [\n \"lean\",\n]\n"; + $added = 1; + } + END { + if ($added) { + print STDERR "[setup-mistral-vibe] Added installed_agents entry for lean.\n"; + } + } + ' "$config_file" +} + +ensure_lean_lsp_mcp_server() { + local config_file=$1 + + if grep -Eq '^[[:space:]]*name[[:space:]]*=[[:space:]]*"lean-lsp"' "$config_file"; then + log "lean-lsp MCP server already configured." + return + fi + + cat >>"$config_file" <<'EOF' + +[[mcp_servers]] +name = "lean-lsp" +transport = "stdio" +command = "uvx" +args = [ + "lean-lsp-mcp", +] +tool_timeout_sec = 600 +EOF + log "Added lean-lsp MCP server configuration." +} + +main() { + ensure_code_cli + install_vibe_vscode_extension_if_missing + + local config_file + config_file=$(resolve_config_file) + mkdir -p "$(dirname "$config_file")" + touch "$config_file" + + ensure_installed_agents_contains_lean "$config_file" + ensure_lean_lsp_mcp_server "$config_file" + + log "Setup complete. Config updated at: $config_file" +} + +main "$@" \ No newline at end of file From ff4d41670fa0c2c822461820a5274ee9e7a4cfc1 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 22 Sep 2026 21:50:27 +0200 Subject: [PATCH 4/5] fix mistral vibe path --- scripts/setup-mistral-vibe.sh | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/scripts/setup-mistral-vibe.sh b/scripts/setup-mistral-vibe.sh index ec2e6fb60d..f01d106a30 100755 --- a/scripts/setup-mistral-vibe.sh +++ b/scripts/setup-mistral-vibe.sh @@ -29,17 +29,7 @@ resolve_config_file() { return fi - if [ -f "$HOME/.config/mistral/config.toml" ]; then - echo "$HOME/.config/mistral/config.toml" - return - fi - - if [ -f "$HOME/.mistral/config.toml" ]; then - echo "$HOME/.mistral/config.toml" - return - fi - - echo "$HOME/.config/mistral/config.toml" + echo "$HOME/.vibe/config.toml" } install_vibe_vscode_extension_if_missing() { From c06a14689ab183855ed01d0bbab9d000fb2dc4bf Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 22 Sep 2026 21:54:54 +0200 Subject: [PATCH 5/5] devcontainer-lock --- .devcontainer/devcontainer-lock.json | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 .devcontainer/devcontainer-lock.json diff --git a/.devcontainer/devcontainer-lock.json b/.devcontainer/devcontainer-lock.json new file mode 100644 index 0000000000..9b3c0997ad --- /dev/null +++ b/.devcontainer/devcontainer-lock.json @@ -0,0 +1,9 @@ +{ + "features": { + "ghcr.io/devcontainers/features/github-cli:1": { + "version": "1.1.2", + "resolved": "ghcr.io/devcontainers/features/github-cli@sha256:7c409bf6316ffd85f04fd92fba85a744282639e603417dd4796409866bdb6805", + "integrity": "sha256:7c409bf6316ffd85f04fd92fba85a744282639e603417dd4796409866bdb6805" + } + } +}