Query squash

.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

.github/workflows/bump_toolchain_nightly-testing.yml

@@ -12,28 +12,45 @@ jobs:
     if: github.repository == 'leanprover/cslib'
     runs-on: ubuntu-latest
     steps:
+    - name: Generate app token
+      id: app-token
+      uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+      with:
+        app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
+        private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
+    # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+
     - name: Checkout code
       uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
       with:
         ref: nightly-testing # checkout nightly-testing branch
-        token: ${{ secrets.NIGHTLY_TESTING }}
+        token: ${{ steps.app-token.outputs.token }}
 
     - name: Get latest release tag from leanprover/lean4-nightly
       id: get-latest-release
+      env:
+        GH_TOKEN: ${{ steps.app-token.outputs.token }}
       run: |
-        RELEASE_TAG="$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')"
+        RELEASE_TAG=$(gh api -X GET repos/leanprover/lean4-nightly/releases \
+          -f per_page=1 --jq '.[0].tag_name')
+        if [ -z "$RELEASE_TAG" ] || [ "$RELEASE_TAG" = "null" ]; then
+          echo "::error::Could not determine latest lean4-nightly release"
+          exit 1
+        fi
         echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}"
 
     - name: Check if nightly-testing tag exists in mathlib4-nightly-testing
       id: check-nightly-testing
+      env:
+        GH_TOKEN: ${{ steps.app-token.outputs.token }}
       run: |
         # Extract date from RELEASE_TAG (format: nightly-YYYY-MM-DD)
         DATE_PART=$(echo "$RELEASE_TAG" | sed 's/nightly-//')
         NIGHTLY_TESTING_TAG="nightly-testing-${DATE_PART}"
         echo "NIGHTLY_TESTING_TAG=$NIGHTLY_TESTING_TAG" >> "${GITHUB_ENV}"
 
         # Check if the tag exists in leanprover-community/mathlib4-nightly-testing
-        if curl -s -f "https://api.github.com/repos/leanprover-community/mathlib4-nightly-testing/git/ref/tags/${NIGHTLY_TESTING_TAG}" > /dev/null; then
+        if gh api "repos/leanprover-community/mathlib4-nightly-testing/git/ref/tags/${NIGHTLY_TESTING_TAG}" > /dev/null 2>&1; then
           echo "Tag ${NIGHTLY_TESTING_TAG} exists in mathlib4-nightly-testing"
           echo "tag_exists=true" >> "${GITHUB_OUTPUT}"
         else
@@ -70,10 +87,8 @@ jobs:
     - name: Commit and push changes
       if: steps.check-nightly-testing.outputs.tag_exists == 'true'
       run: |
-        # For now we reuse a bot managed by Mathlib,
-        # but it is fine to update this if Cslib wants to create its own bot accounts.
-        git config user.name "leanprover-community-mathlib4-bot"
-        git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
+        git config user.name "mathlib-nightly-testing[bot]"
+        git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"
         git add lean-toolchain lakefile.toml lake-manifest.json
         # Don't fail if there's nothing to commit
         git commit -m "chore: bump to ${RELEASE_TAG} with mathlib at ${NIGHTLY_TESTING_TAG}" || true

.github/workflows/merge_main_into_nightly-testing.yml

@@ -13,13 +13,21 @@ jobs:
     if: github.repository == 'leanprover/cslib'
     runs-on: ubuntu-latest
     steps:
-      - name: Checkout nightly-testing 
+      - name: Generate app token
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
+      # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+
+      - name: Checkout nightly-testing
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
         with:
           repository: leanprover/cslib
           ref: nightly-testing
           path: nightly-testing
-          token: ${{ secrets.NIGHTLY_TESTING }} # This secret needs repo access to leanprover/cslib
+          token: ${{ steps.app-token.outputs.token }}
           fetch-depth: 0
 
       - name: Configure Lean
@@ -33,10 +41,8 @@ jobs:
       - name: Configure Git User
         run: |
           cd nightly-testing
-          # For now we reuse a bot managed by Mathlib,
-          # but it is fine to update this if Cslib wants to create its own bot accounts.
-          git config user.name "leanprover-community-mathlib4-bot"
-          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
+          git config user.name "mathlib-nightly-testing[bot]"
+          git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"
 
       - name: Merge main to nightly-testing favoring nightly-testing changes
         run: |
@@ -58,5 +64,5 @@ jobs:
           # If there's nothing to do (because there are no new commits from main),
           # that's okay, hence the '|| true'.
           git commit -m "Merge main into nightly-testing" || true
-          # Push 
+          # Push
           git push origin nightly-testing

.github/workflows/pr-title.yml

@@ -18,6 +18,6 @@ jobs:
           script: |
             const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
             console.log(`Message: ${msg}`)
-            if (!/^(feat|fix|doc|style|refactor|test|chore|perf)(\(.*\))?: .*[^.]($|\n\n)/.test(msg)) {
+            if (!/^(ci|feat|fix|doc|style|refactor|test|chore|perf)(\(.*\))?: .*[^.]($|\n\n)/.test(msg)) {
               core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
             }

.github/workflows/release.yml

@@ -0,0 +1,21 @@
+name: Release
+
+on:
+  push:
+    tags:
+      - "v[0-9]+.[0-9]+.[0-9]+"
+      - "v[0-9]+.[0-9]+.[0-9]+-rc[0-9]+"
+
+permissions:
+  contents: write
+
+jobs:
+  release:
+    runs-on: ubuntu-latest
+    if: github.repository == 'leanprover/cslib'
+    steps:
+      - name: Create GitHub Release
+        uses: softprops/action-gh-release@v2
+        with:
+          prerelease: ${{ contains(github.ref, 'rc') }}
+          make_latest: ${{ !contains(github.ref, 'rc') }}