Modularize Scheme event AOT, parse TLA+ sets, and optimize parser core

.gitattributes

@@ -1,2 +1,2 @@
-languages/tla-plus/v1/grammar-source/tla+.jj -whitespace
-languages/fhirpath/v2.0.0/grammar-source/fhirpath.g4 -text -whitespace
+languages/tla-plus/grammar-source/tla+.jj -whitespace
+languages/fhirpath/grammar-source/fhirpath.g4 -text -whitespace

.github/actions/gerbil-setup/action.yml

@@ -0,0 +1,80 @@
+name: Immutable Gerbil SDK
+description: Admit a cached SDK by full digest and platform, using GCC
+inputs:
+  release-os:
+    required: true
+    description: release-os
+  release-arch:
+    required: true
+    description: release-arch
+  release-tag:
+    required: true
+    description: release-tag
+  release-sha256:
+    required: true
+    description: release-sha256
+runs:
+  using: composite
+  steps:
+    - name: Install Linux system dependencies
+      if: runner.os == 'Linux'
+      run: |
+        sudo apt-get update
+        sudo apt-get install -y \
+          build-essential \
+          ca-certificates \
+          curl \
+          git \
+          jq \
+          libsqlite3-dev \
+          libssl-dev \
+          openjdk-17-jre-headless \
+          openssl \
+          pkg-config \
+          sqlite3 \
+          zlib1g-dev
+      shell: bash
+    - name: Install macOS system dependencies
+      if: runner.os == 'macOS'
+      env:
+        HOMEBREW_NO_AUTO_UPDATE: 1
+        HOMEBREW_NO_INSTALL_CLEANUP: 1
+      run: |
+        brew list --formula ghostscript >/dev/null 2>&1 && brew unlink ghostscript || true
+        brew install gcc jq openssl pkg-config sqlite zlib
+        gcc_prefix="$(brew --prefix gcc)"
+        gcc_bin="$(
+          find "$gcc_prefix/bin" -maxdepth 1 -type f -name 'gcc-[0-9]*' \
+            | awk -F- '{print $NF "\t" $0}' \
+            | sort -n \
+            | tail -n 1 \
+            | cut -f2-
+        )"
+        test -x "$gcc_bin"
+        echo "GERBIL_GCC=$gcc_bin" >> "$GITHUB_ENV"
+        openssl_prefix="$(brew --prefix openssl@3 2>/dev/null || brew --prefix openssl)"
+        macos_major="$(sw_vers -productVersion | cut -d. -f1)"
+        echo "PKG_CONFIG_PATH=$openssl_prefix/lib/pkgconfig${PKG_CONFIG_PATH:+:$PKG_CONFIG_PATH}" >> "$GITHUB_ENV"
+        echo "MACOSX_DEPLOYMENT_TARGET=$macos_major.0" >> "$GITHUB_ENV"
+      shell: bash
+    - name: Install native task tool
+      uses: taiki-e/install-action@f7e5d7c961414b23f5b25b2da9294395d08513ad
+      with:
+        tool: just
+    - name: Cache immutable SDK archive
+      uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9
+      with:
+        path: ${{ runner.temp }}/gerbil-sdk.tar.gz
+        key: parser-sdk-v1-${{ runner.os }}-${{ runner.arch }}-${{ inputs.release-sha256 }}
+    - name: Extract immutable Gerbil host SDK
+      run: |
+        test -f "$RUNNER_TEMP/gerbil-sdk.tar.gz" || curl --fail --location --retry 3 --output "$RUNNER_TEMP/gerbil-sdk.tar.gz" \
+          "https://github.com/tao3k/gerbil-bazel/releases/download/${{ inputs.release-tag }}/${{ inputs.release-tag }}.tar.gz"
+        echo '${{ inputs.release-sha256 }}  '"$RUNNER_TEMP/gerbil-sdk.tar.gz" | shasum -a 256 --check
+        mkdir -p "$GERBIL_RELEASE_ROOT"
+        tar -xzf "$RUNNER_TEMP/gerbil-sdk.tar.gz" -C "$GERBIL_RELEASE_ROOT" --strip-components=1
+        GERBIL_HOME="$GERBIL_RELEASE_ROOT/current" \
+          GAMBOPT="~~=$GERBIL_RELEASE_ROOT/current,~~bin=$GERBIL_RELEASE_ROOT/current/bin,~~lib=$GERBIL_RELEASE_ROOT/current/lib" \
+          "$GERBIL_RELEASE_ROOT/current/bin/gxi" tools/ci/bootstrap.ss \
+            "$GERBIL_RELEASE_ROOT" '${{ inputs.release-os }}' '${{ inputs.release-arch }}'
+      shell: bash

.github/workflows/ci.yml

@@ -1,226 +1,110 @@
 name: CI
-
-on:
+'on':
   push:
     branches:
       - main
-  pull_request:
-
+  pull_request: null
+  workflow_dispatch: null
 permissions:
   contents: read
-
 concurrency:
-  group: ci-${{ github.workflow }}-${{ github.head_ref || github.ref_name }}
+  group: ci-${{ github.workflow }}-${{ github.event_name }}-${{ github.head_ref || github.ref_name }}
   cancel-in-progress: true
-
 jobs:
-  rust-rowan:
-    name: Rust/Rowan AOT runtime
+  rust-runtime:
+    name: Rust ${{ matrix.lane }}
     runs-on: ubuntu-latest
     timeout-minutes: 20
+    strategy:
+      fail-fast: false
+      matrix:
+        lane:
+          - contracts
+          - lints
+          - aot-performance
     steps:
       - name: Checkout gerbil-parser
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
-
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0
+      - name: Verify parser semantics and operation costs
+        if: matrix.lane == 'contracts'
+        uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865 # v1
+        with:
+          lake-package-directory: formal
+          auto-config: false
+          build: true
+          test: false
+          lint: false
+          use-mathlib-cache: false
+      - name: Set up uv
+        if: matrix.lane == 'contracts'
+        uses: astral-sh/setup-uv@94527f2e458b27549849d47d273a16bec83a01e9 # v7
+        with:
+          version: '0.11.3'
+      - name: Verify publication model and evidence host controls
+        if: matrix.lane == 'contracts'
+        run: |
+          npm ci --ignore-scripts --prefix formal/quint
+          npm --prefix formal/quint test
+          uv run --project formal/evidence --locked python -m unittest discover -s formal/evidence -k HostControls -v
+      - name: Identify Rust toolchain
+        id: rust-version
+        run: echo "version=$(rustc -Vv | shasum -a 256 | cut -d' ' -f1)" >> "$GITHUB_OUTPUT"
+      - name: Restore Rust build cache
+        uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9
+        with:
+          path: |-
+            ~/.cargo/registry
+            ~/.cargo/git
+            target
+            t/fixtures/runtime-record-assignments/target
+            t/fixtures/runtime-ascii-digit-run/target
+          key: parser-rust-v1-${{ runner.os }}-${{ runner.arch }}-${{ matrix.lane }}-${{ steps.rust-version.outputs.version }}-${{ hashFiles('**/Cargo.toml', '**/Cargo.lock') }}
       - name: Verify Rust formatting
         run: cargo fmt --all -- --check
-
-      - name: Verify ASP Rust source policy
-        run: cargo test -p gerbil-parser-build-support --test asp-rust-gate --locked -- --nocapture
-
+        if: matrix.lane == 'contracts'
       - name: Verify Rust contracts
-        run: cargo test --workspace --locked
-
-      - name: Verify downstream Cargo-only language consumer
-        run: cargo test --locked --manifest-path t/fixtures/rust-rowan-downstream/Cargo.toml
-
+        run: cargo test --workspace --all-features --locked
+        if: matrix.lane == 'contracts'
+      - name: Verify record assignments Cargo consumer
+        run: cargo test --locked --manifest-path t/fixtures/runtime-record-assignments/Cargo.toml
+        if: matrix.lane == 'contracts'
+      - name: Verify external ASCII digit adapter
+        run: |
+          cargo fmt --manifest-path t/fixtures/runtime-ascii-digit-run/Cargo.toml -- --check
+          cargo test --locked --manifest-path t/fixtures/runtime-ascii-digit-run/Cargo.toml
+        if: matrix.lane == 'contracts'
       - name: Verify Rust lints
-        run: cargo clippy --workspace --all-targets --locked -- -D warnings
-
+        run: cargo clippy --workspace --all-targets --all-features --locked -- -D warnings
+        if: matrix.lane == 'lints'
       - name: Verify publishable Rust products
-        run: cargo package -p gerbil-parser-rowan --locked --allow-dirty
-
-      - name: Verify generated-table Rowan engine red zones
-        run: cargo test --release -p gerbil-parser-rowan-scenarios --test performance_test -- --ignored --nocapture --test-threads=1
-
-  native-gerbil:
-    name: Native Gerbil parser and language packs (${{ matrix.os }})
-    runs-on: ${{ matrix.os }}
-    timeout-minutes: 240
+        run: cargo package -p gerbil-parser-artifact -p gerbil-parser-runtime --locked --allow-dirty
+        if: matrix.lane == 'lints'
+      - name: Verify generated-table AOT engine red zones
+        run: cargo test --release -p gerbil-parser-build-support --test performance_test -- --ignored --nocapture --test-threads=1
+        if: matrix.lane == 'aot-performance'
+  scheme:
+    name: Scheme ${{ matrix.os }}
     strategy:
       fail-fast: false
       matrix:
         include:
           - os: ubuntu-latest
             gerbil-label: release-v0.19-2591dcd
+            release-os: linux
+            release-arch: x86_64
+            release-tag: gerbil-v0.19-2591dcd9b7c6d2c4e9dd8611a17c5b1a5d82bbdb-linux-x86_64-portable-full-single-host-unlimited-patchf5cedd8168cb
+            release-sha256: 9844ba362fdf6f1c5e8a4411e462a466d52dee0d541f8e84f61091cec0e5e740
           - os: macos-latest
             gerbil-label: release-v0.19-2591dcd
-    env:
-      GERBIL_RELEASE_ROOT: ${{ github.workspace }}/.ci/gerbil-release/${{ matrix.gerbil-label }}
-    steps:
-      - name: Checkout gerbil-parser
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
-
-      - name: Install Linux system dependencies
-        if: runner.os == 'Linux'
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y \
-            build-essential \
-            ca-certificates \
-            git \
-            jq \
-            libsqlite3-dev \
-            libssl-dev \
-            openssl \
-            pkg-config \
-            sqlite3 \
-            zlib1g-dev
-
-      - name: Install macOS system dependencies
-        if: runner.os == 'macOS'
-        env:
-          HOMEBREW_NO_AUTO_UPDATE: 1
-          HOMEBREW_NO_INSTALL_CLEANUP: 1
-        run: |
-          brew list --formula ghostscript >/dev/null 2>&1 && brew unlink ghostscript || true
-          brew install gcc jq openssl pkg-config sqlite zlib
-          gcc_prefix="$(brew --prefix gcc)"
-          gcc_bin="$(
-            find "$gcc_prefix/bin" -maxdepth 1 -type f -name 'gcc-[0-9]*' \
-              | awk -F- '{print $NF "\t" $0}' \
-              | sort -n \
-              | tail -n 1 \
-              | cut -f2-
-          )"
-          test -x "$gcc_bin"
-          echo "GERBIL_GCC=$gcc_bin" >> "$GITHUB_ENV"
-          openssl_prefix="$(brew --prefix openssl@3 2>/dev/null || brew --prefix openssl)"
-          macos_major="$(sw_vers -productVersion | cut -d. -f1)"
-          echo "PKG_CONFIG_PATH=$openssl_prefix/lib/pkgconfig${PKG_CONFIG_PATH:+:$PKG_CONFIG_PATH}" >> "$GITHUB_ENV"
-          echo "MACOSX_DEPLOYMENT_TARGET=$macos_major.0" >> "$GITHUB_ENV"
-
-      - name: Detect native build capacity
-        run: |
-          cores="$(getconf _NPROCESSORS_ONLN 2>/dev/null || sysctl -n hw.ncpu)"
-          test "$cores" -gt 0
-          echo "GERBIL_BUILD_CORES=$cores" >> "$GITHUB_ENV"
-          echo "Native Gerbil capacity: $cores cores"
-
-      - name: Install immutable Gerbil v0.19 release
-        shell: bash
-        run: bash tools/ci/install-gerbil-v19-release.sh "$GERBIL_RELEASE_ROOT"
-
-      - name: Restore Gerbil package cache
-        id: package-cache
-        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
-        with:
-          path: |
-            .gerbil/pkg
-            .gerbil/lib
-            .gerbil/bin
-          key: gerbil-parser-packages-v2-${{ runner.os }}-${{ runner.arch }}-${{ matrix.gerbil-label }}-${{ hashFiles('gerbil.pkg') }}
-
-      - name: Install declared package dependencies
-        run: |
-          mkdir -p "$HOME/.gerbil/pkg"
-          gerbil pkg dir --add git.cons.io/mighty-gerbils/gerbil-directory
-          if [ "${{ steps.package-cache.outputs.cache-hit }}" = "true" ]; then
-            if ! gerbil env gerbil interactive -e '(begin (import :core/object-family/interface :asp-gerbil-scheme/building-api :asp-gerbil-scheme/src/benchmark/framework) (displayln "dependency-cache-ready"))'; then
-              gerbil deps --update
-            fi
-          else
-            gerbil deps --install
-          fi
-          gerbil env gerbil interactive -e '(begin (import :core/object-family/interface :asp-gerbil-scheme/building-api :asp-gerbil-scheme/src/benchmark/framework) (displayln "dependencies-ready"))'
-
-      - name: Save Gerbil package cache
-        if: steps.package-cache.outputs.cache-hit != 'true'
-        uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
-        with:
-          path: |
-            .gerbil/pkg
-            .gerbil/lib
-            .gerbil/bin
-          key: gerbil-parser-packages-v2-${{ runner.os }}-${{ runner.arch }}-${{ matrix.gerbil-label }}-${{ hashFiles('gerbil.pkg') }}
-
-      - name: Build parser and versioned language packs
-        run: |
-          gerbil clean
-          GERBIL_BUILD_VERBOSE=1 gerbil build
-          cc -std=c11 -Wall -Wextra -Werror \
-            -Wno-unused-command-line-argument -fsyntax-only \
-            -Iinclude t/native-ffi-header-smoke.c
-
-      - name: Build optional native commands
-        run: |
-          gerbil env gxi build-gparse.ss compile
-          gerbil env gxi build-rust-rowan-aot.ss compile
-
-      - name: Compile Scheme test support
-        run: |
-          gerbil env gxc t/line-structure-assertions.ss
-          gerbil env gxc \
-            t/fixtures/rust-rowan-downstream/languages/records/v1/grammar.ss \
-            t/fixtures/rust-rowan-downstream/languages/records/v1/parser.ss \
-            t/fixtures/rust-rowan-downstream/languages/records/v1/fixtures.ss
-
-      - name: Run native Gerbil tests
-        timeout-minutes: 15
-        run: gerbil test -v 3 t/... languages/...
-
-      - name: Verify Rust/Rowan AOT generation is current
-        run: |
-          arithmetic_generated="$(mktemp)"
-          gerbil env gxi generate-rust-rowan.ss "$arithmetic_generated"
-          rustfmt --edition 2024 "$arithmetic_generated"
-          cmp "$arithmetic_generated" rust/gerbil-parser-rowan-arithmetic/src/generated/mod.rs
-
-      - name: Verify Scheme event strategy AOT fixture
-        run: |
-          event_generated="$(mktemp)"
-          grammar_generated="$(mktemp)"
-          fold_ir_generated="$(mktemp)"
-          outline_ir_generated="$(mktemp)"
-          gerbil env gxi t/generate-event-strategy-fixture.ss "$event_generated"
-          gerbil env gxi t/generate-event-strategy-grammar.ss "$grammar_generated"
-          gerbil env gxi t/generate-event-fold-ir.ss "$fold_ir_generated"
-          gerbil env gxi t/generate-outline-fold-ir.ss "$outline_ir_generated"
-          rustfmt --edition 2024 "$event_generated" "$grammar_generated"
-          cmp "$event_generated" rust/gerbil-parser-rowan/tests/unit/event_strategy_generated.rs
-          cmp "$grammar_generated" rust/gerbil-parser-rowan/tests/unit/event_strategy_grammar.rs
-          cmp "$fold_ir_generated" t/fixtures/event_fold.ir.json
-          cmp "$outline_ir_generated" t/fixtures/outline_fold.ir.json
-
-      - name: Verify Scheme pure owned-string AOT fixture
-        run: |
-          owned_generated="$(mktemp)"
-          gerbil env gxi t/generate-owned-word-fixture.ss "$owned_generated"
-          cmp "$owned_generated" rust/gerbil-parser-rowan/tests/unit/owned_first_word_generated.rs
-
-      - name: Verify downstream custom Rust/Rowan language pack
-        run: |
-          fixture="t/fixtures/rust-rowan-downstream"
-          generated="$(mktemp)"
-          clean_home="$RUNNER_TEMP/rowan-aot-home"
-          mkdir -p "$clean_home"
-          gerbil env gxc \
-            "$fixture/languages/records/v1/grammar.ss" \
-            "$fixture/languages/records/v1/parser.ss" \
-            "$fixture/languages/records/v1/fixtures.ss" \
-            "$fixture/languages/records/v1/parser-test.ss"
-          env -i \
-            HOME="$clean_home" \
-            PATH=/usr/bin:/bin \
-            GERBIL_PATH="$PWD/.gerbil" \
-            GERBIL_PARSER_ROWAN_AOT_LIB="$PWD/.gerbil/lib:$GERBIL_HOME/lib" \
-            "$PWD/.gerbil/bin/gerbil-parser-rowan-aot" \
-            "$fixture/languages/records/v1/grammar.ss" \
-            "$generated"
-          rustfmt --edition 2024 "$generated"
-          cmp "$generated" "$fixture/src/generated/records_v1.rs"
-
-      - name: Verify native command
-        run: |
-          gerbil env gparse help
-          gerbil env gparse check "1 + 2 * value"
+            release-os: darwin
+            release-arch: aarch64
+            release-tag: gerbil-v0.19-2591dcd9b7c6d2c4e9dd8611a17c5b1a5d82bbdb-darwin-aarch64-gcc16-arm64-aot-tools-single-host-unlimited-patchf5cedd8168cb
+            release-sha256: 8d9c88434aed6301eaebb719bf52472f05c2368eafc630e8a9f1d67cc9895a21
+    uses: ./.github/workflows/scheme.yml
+    with:
+      os: ${{ matrix.os }}
+      gerbil-label: ${{ matrix.gerbil-label }}
+      release-os: ${{ matrix.release-os }}
+      release-arch: ${{ matrix.release-arch }}
+      release-tag: ${{ matrix.release-tag }}
+      release-sha256: ${{ matrix.release-sha256 }}