chore(policy): recognise Agda + echo-types as canonical loss-with-residue formalism #268
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: PMPL-1.0 | |
| name: Language Policy Enforcement | |
| on: | |
| push: | |
| branches: [main, master] | |
| pull_request: | |
| branches: [main, master] | |
| permissions: | |
| contents: read | |
| jobs: | |
| check-banned-languages: | |
| name: Check for Banned Languages | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 | |
| - name: Check for TypeScript files | |
| run: | | |
| if find . -name "*.ts" -o -name "*.tsx" | grep -v node_modules | grep -v ".d.ts" | head -1 | grep -q .; then | |
| echo "::error::TypeScript files found. Use AffineScript instead." | |
| find . -name "*.ts" -o -name "*.tsx" | grep -v node_modules | grep -v ".d.ts" | |
| exit 1 | |
| fi | |
| echo "✓ No TypeScript files found" | |
| - name: Check for ReScript files | |
| run: | | |
| # Estate policy: RS/TS/JS -> AffineScript -> typed-wasm. | |
| # ReScript (.res) is no longer the TS replacement. | |
| if find . -name "*.res" | grep -v node_modules | head -1 | grep -q .; then | |
| echo "::error::ReScript files found. Use AffineScript instead." | |
| find . -name "*.res" | grep -v node_modules | |
| exit 1 | |
| fi | |
| echo "✓ No ReScript files found" | |
| - name: Check for Go files | |
| run: | | |
| if find . -name "*.go" | head -1 | grep -q .; then | |
| echo "::error::Go files found. Use Rust instead." | |
| find . -name "*.go" | |
| exit 1 | |
| fi | |
| echo "✓ No Go files found" | |
| - name: Check for Python files (except Ansible) | |
| run: | | |
| # Allow Python only in ansible/ directories or for Ansible-specific files | |
| PYTHON_FILES=$(find . -name "*.py" | grep -v __pycache__ | grep -v ".venv" | grep -v "ansible" | grep -v "molecule" || true) | |
| if [ -n "$PYTHON_FILES" ]; then | |
| echo "::error::Python files found outside Ansible context. Rewrite in Rust/AffineScript." | |
| echo "$PYTHON_FILES" | |
| exit 1 | |
| fi | |
| echo "✓ No unauthorized Python files found" | |
| - name: Check for Makefiles | |
| run: | | |
| MAKEFILES=$(find . -name "Makefile" -o -name "Makefile.*" -o -name "*.mk" | grep -v ".github" || true) | |
| if [ -n "$MAKEFILES" ]; then | |
| echo "::error::Makefiles found. Use Mustfile/justfile instead." | |
| echo "$MAKEFILES" | |
| exit 1 | |
| fi | |
| echo "✓ No Makefiles found" | |
| - name: Check for package.json (npm/node) | |
| run: | | |
| if [ -f "package.json" ]; then | |
| # Allow if it only contains devDependencies for tooling | |
| if grep -q '"dependencies"' package.json; then | |
| echo "::error::package.json with runtime dependencies found. Use deno.json instead." | |
| exit 1 | |
| fi | |
| fi | |
| echo "✓ No npm runtime dependencies found" | |
| - name: Check for Java/Kotlin files | |
| run: | | |
| if find . -name "*.java" -o -name "*.kt" -o -name "*.kts" | head -1 | grep -q .; then | |
| echo "::error::Java/Kotlin files found. Use Rust/Tauri/Dioxus instead." | |
| find . -name "*.java" -o -name "*.kt" -o -name "*.kts" | |
| exit 1 | |
| fi | |
| echo "✓ No Java/Kotlin files found" | |
| - name: Check for Swift files | |
| run: | | |
| if find . -name "*.swift" | head -1 | grep -q .; then | |
| echo "::error::Swift files found. Use Tauri/Dioxus instead." | |
| find . -name "*.swift" | |
| exit 1 | |
| fi | |
| echo "✓ No Swift files found" | |
| - name: Check for V-lang code | |
| run: | | |
| # V-lang is banned as of 2026-04-10. Migration target: Zig. | |
| # We detect by v.mod (V-lang's module manifest) rather than *.v | |
| # extension because .v collides with Verilog hardware sources. | |
| V_MOD_FILES=$(find . -name "v.mod" -not -path "*/node_modules/*" -not -path "*/.git/*" || true) | |
| if [ -n "$V_MOD_FILES" ]; then | |
| echo "::error::V-lang code found (detected via v.mod). V-lang is banned since 2026-04-10. Migrate to Zig." | |
| echo "$V_MOD_FILES" | |
| exit 1 | |
| fi | |
| # Also check for vpkg.json (alternative V package manifest) | |
| VPKG_FILES=$(find . -name "vpkg.json" -not -path "*/node_modules/*" -not -path "*/.git/*" || true) | |
| if [ -n "$VPKG_FILES" ]; then | |
| echo "::error::V-lang code found (detected via vpkg.json). V-lang is banned since 2026-04-10. Migrate to Zig." | |
| echo "$VPKG_FILES" | |
| exit 1 | |
| fi | |
| echo "✓ No V-lang code found" | |
| - name: Check for Flutter/Dart files | |
| run: | | |
| if find . -name "*.dart" -o -name "pubspec.yaml" | head -1 | grep -q .; then | |
| echo "::error::Flutter/Dart code found. Use Tauri/Dioxus instead (Google lock-in policy)." | |
| find . -name "*.dart" -o -name "pubspec.yaml" | |
| exit 1 | |
| fi | |
| echo "✓ No Flutter/Dart code found" | |
| - name: Check for ATS2 files | |
| run: | | |
| # ATS2 is rejected in favour of Idris2 (formal verification) and | |
| # Rust/SPARK (safety-critical operational code). See LANGUAGE-POLICY.adoc §Amendments v1.1.0. | |
| if find . -name "*.dats" -o -name "*.sats" -o -name "*.hats" | head -1 | grep -q .; then | |
| echo "::error::ATS2 files found. Use Idris2 (formal verification) or Rust/SPARK (safety-critical code) instead." | |
| find . -name "*.dats" -o -name "*.sats" -o -name "*.hats" | |
| exit 1 | |
| fi | |
| echo "✓ No ATS2 files found" | |
| check-required-files: | |
| name: Check Required Files | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 | |
| - name: Check for .machine_readable directory | |
| run: | | |
| if [ ! -d ".machine_readable" ]; then | |
| echo "::warning::.machine_readable/ directory not found" | |
| else | |
| echo "✓ .machine_readable/ directory exists" | |
| # Per estate policy: .a2ml is canonical; .scm is reserved for Guix. | |
| for a2ml in STATE META ECOSYSTEM AGENTIC NEUROSYM PLAYBOOK; do | |
| if [ ! -f ".machine_readable/6a2/${a2ml}.a2ml" ] && [ ! -f ".machine_readable/${a2ml}.a2ml" ]; then | |
| echo "::warning::Missing .machine_readable/6a2/${a2ml}.a2ml (or top-level fallback)" | |
| else | |
| echo "✓ ${a2ml}.a2ml present" | |
| fi | |
| done | |
| fi | |
| - name: Check for Mustfile/justfile | |
| run: | | |
| if [ ! -f "Mustfile" ] && [ ! -f "justfile" ]; then | |
| echo "::warning::Neither Mustfile nor justfile found" | |
| else | |
| echo "✓ Build system files present" | |
| fi | |
| - name: Check SPDX headers | |
| run: | | |
| MISSING_SPDX=0 | |
| for ext in rs affine js jsx mjs ts tsx py go java kt swift sh bash; do | |
| while IFS= read -r file; do | |
| if [ -n "$file" ] && ! head -5 "$file" | grep -q "SPDX-License-Identifier"; then | |
| echo "::warning::Missing SPDX header: $file" | |
| MISSING_SPDX=$((MISSING_SPDX + 1)) | |
| fi | |
| done < <(find . -name "*.$ext" -type f 2>/dev/null | grep -v node_modules | grep -v .git | head -50) | |
| done | |
| if [ $MISSING_SPDX -gt 0 ]; then | |
| echo "::warning::$MISSING_SPDX files missing SPDX headers" | |
| fi |