From 51515fc7da49f222191d90da79b31839d44e65f2 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 29 Jan 2026 20:29:43 +0100 Subject: [PATCH] copilot instructions --- .github/copilot-instructions.md | 139 ++++++++++++++++++++++++++++++++ CONTRIBUTING.md | 13 +++ 2 files changed, 152 insertions(+) create mode 100644 .github/copilot-instructions.md diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md new file mode 100644 index 00000000..991077d4 --- /dev/null +++ b/.github/copilot-instructions.md @@ -0,0 +1,139 @@ +# Copilot Instructions for CSLib + +## Repository Overview + +**CSLib** is the Lean library for Computer Science (CS), formalising CS theories and tools in the Lean programming language. It provides APIs for formal verification, certified software, and connecting different CS developments. + +- **Language:** Lean 4 +- **Build System:** Lake +- **Primary Dependency:** Mathlib (leanprover-community/mathlib4) +- **Project Type:** Lean library + +## Build & Validation Commands + +**Always run commands from the repository root.** The project uses `lake`. + +### Essential Commands (in order of typical usage) + +| 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 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 | + +### Full CI Validation Sequence + +Run these commands **in order** to replicate CI checks locally: + +```bash +lake build --wfail --iofail +lake exe mk_all --module --check +lake test +lake lint +lake exe lint-style +``` + +### Additional Commands + +| Command | Purpose | +|---------|---------| +| `lake clean` | Remove build outputs (use if build state is corrupted) | +| `lake update` | Update dependencies (rarely needed) | +| `lake exe lint-style --fix` | Auto-fix style errors | +| `lake exe shake Cslib` | Check for minimized imports | + +## Project Structure + +``` +/ +├── Cslib.lean # Root module (imports all library files) +├── CslibTests.lean # Root test module +├── CONTRIBUTING.md # Contribution guidelines +├── lakefile.toml # Lake configuration (linters, dependencies) +├── lean-toolchain # Lean version specification +├── lake-manifest.json # Locked dependency versions +├── Cslib/ # Main library source +│ ├── Init.lean # Must be imported by all Cslib modules +│ ├── Foundations/ # General-purpose definitions (semantics, data types, etc.) +│ ├── Computability/ # Automata and computability theory +│ ├── Languages/ # Programming language formalisations (e.g., Calculus of Communicating Systems, Lambda Calculus) +│ └── 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 +└── .github/workflows/ # CI workflows +``` + +## Critical Requirements + +### 1. All Cslib Modules Must Import Cslib.Init +Every file in `Cslib/` must transitively import `Cslib/Init.lean`. This sets up default linters and tactics. The test suite verifies this. + +**Exceptions** (documented in `scripts/CheckInitImports.lean`): +- `Cslib.Foundations.Lint.Basic` (circular dependency) +- `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: +```bash +lake exe mk_all --module +``` + +### 3. PR Title Convention +PR titles **must** follow the format: `type(scope): description` + +Valid types: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf` + +Examples: +- `feat(LTS): add weak bisimulation` +- `fix(Lambda): correct substitution lemma` +- `doc: improve README` + +### 4. File Headers +Every `.lean` file must have a copyright header: +```lean +/- +Copyright (c) $YEAR $AUTHOR_NAME. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: $LIST_OF_AUTHORS +-/ +``` + +## 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 + +## Linter Configuration + +Linters are configured in `lakefile.toml`. + +## Common Patterns + +### 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` +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 +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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e625fcc4..37424653 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -32,6 +32,19 @@ The library hosts a number of languages with their own syntax and semantics, so - If you want notation for a common concept, like reductions or transitions in an operational semantics, try to find an existing typeclass that fits your need. - If you define new notation that in principle can apply to different types (e.g., syntax or semantics of other languages), keep it locally scoped or create a new typeclass. +## Documentation + +Document your definitions and theorems to ease both use and reviewing. +When formalising a concept that is explained in a published resource, please reference the resource in your documentation. + +# Design principles + +## Reuse + +A central focus of CSLib is providing reusable abstractions and their consistent usage across the +library. New definitions should instantiate existing abstractions whenever appropriate: a +labelled transition system should use `LTS`, a reduction system `ReductionSystem`, etc. + # Continuous Integration There are a number of checks that run in continuous integration. Here is a brief guide that includes