diff --git a/.github/workflows/check.yml b/.github/workflows/check.yml index d000f7b..f2cadba 100644 --- a/.github/workflows/check.yml +++ b/.github/workflows/check.yml @@ -20,26 +20,9 @@ jobs: if: github.event_name == 'pull_request' runs-on: ubuntu-latest steps: - - name: Check branch strategy - run: | - TARGET="${{ github.base_ref }}" - SOURCE="${{ github.head_ref }}" - # Feature branches → development only - if [[ "$SOURCE" =~ ^(feat|fix|chore|docs|refactor)/ && "$TARGET" != "development" ]]; then - echo "::error::Feature branches must target development, not $TARGET." - exit 1 - fi - # PRs to main → must come from development - if [[ "$TARGET" == "main" && "$SOURCE" != "development" ]]; then - echo "::error::PRs to main must come from development." - exit 1 - fi - echo "✓ branch strategy OK: $SOURCE → $TARGET" - - name: Check branch naming run: | SOURCE="${{ github.head_ref }}" - if [[ "$SOURCE" == "development" ]]; then exit 0; fi if [[ ! "$SOURCE" =~ ^(feat|fix|chore|docs|refactor)/ ]]; then echo "::error::Branch '$SOURCE' does not follow naming convention." echo "Must start with: feat/, fix/, chore/, docs/, or refactor/" diff --git a/CLAUDE.md b/CLAUDE.md index 5957121..f471303 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -10,10 +10,7 @@ enforcement lives in CI and the Lean type system, not here. - **No `import Mathlib`** — full import banned; Lean syntax linter `Util/Linter/ImportBan.lean` enforces at build time. - **Build green** — `lake build` must pass. -- **Branch protection** — `main` and `development` protected; - no direct push, PRs only. -- **Branch strategy** — feature branches (`feat/`/`fix/`/`chore/`/ - `docs/`/`refactor/`) → `development` → `main`. CI enforces. +- **Branch protection** — `main` protected; no direct push, PRs only. - **Branch naming** — branches must start with `feat/`/`fix/`/`chore/`/ `docs/`/`refactor/`. CI enforces. - **PR title** — must match `type(scope): summary`. CI enforces.