Add then proof continuations, wip(?e) holes, and beta-only defeq
#8
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
| name: CI | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| workflow_dispatch: | |
| # Cancel superseded runs on the same ref. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| build-test: | |
| name: Build, test, verify stdlib | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Rust (stable) | |
| uses: dtolnay/rust-toolchain@stable | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| # 1. The project compiles. | |
| - name: Build | |
| run: cargo build --locked --verbose | |
| # 2. All tests pass. | |
| - name: Test | |
| run: cargo test --locked --verbose | |
| # 3. Verify every proof in the standard library. | |
| - name: Verify stdlib proofs | |
| run: cargo run -p algae-cli --locked -- verify algae/stdlib/v1/ | |
| tree-sitter: | |
| name: Tree-sitter grammar | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: editors/tree-sitter | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Node | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: lts/* | |
| # Installs the pinned tree-sitter CLI (devDependency in package.json). | |
| - name: Install tree-sitter CLI | |
| run: npm install | |
| # 4. Tree-sitter compiles successfully: the grammar generates, the corpus | |
| # tests pass, the canonical stdlib parses with no ERROR nodes, and the | |
| # generated C parser compiles. | |
| - name: Generate parser | |
| run: make generate TS="npx tree-sitter" | |
| - name: Corpus tests | |
| run: make test TS="npx tree-sitter" | |
| - name: Parse the standard library | |
| run: make parse-stdlib TS="npx tree-sitter" | |
| - name: Compile the C parser | |
| run: cc -shared -Os -fPIC -I src -o /tmp/alg.so src/parser.c | |
| docs: | |
| name: Build docs and deploy to gh-pages | |
| runs-on: ubuntu-latest | |
| # Only the deploy step is gated on `main`; the build runs on every trigger | |
| # so pull requests and manual dispatches catch breakage before merge. | |
| permissions: | |
| contents: write | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Rust (stable) with wasm target | |
| uses: dtolnay/rust-toolchain@stable | |
| with: | |
| targets: wasm32-unknown-unknown | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| - name: Install wasm-pack | |
| uses: jetli/wasm-pack-action@v0.4.0 | |
| with: | |
| version: latest | |
| - name: Install Node | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: lts/* | |
| - name: Install Python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: "3.x" | |
| - name: Install Sphinx toolchain | |
| run: pip install -r docs/requirements.txt | |
| # Compiles algae-wasm, bundles the CodeMirror editor, stages runtime | |
| # assets into docs/_static, and runs Sphinx — identical to local builds. | |
| - name: Build the documentation site | |
| run: bash docs/build.sh | |
| - name: Disable Jekyll processing | |
| run: touch docs/_build/html/.nojekyll | |
| # Publish to the gh-pages branch only from main. Enable Pages in the repo | |
| # settings with source "Deploy from a branch: gh-pages". | |
| - name: Deploy to gh-pages | |
| if: github.ref == 'refs/heads/main' | |
| uses: peaceiris/actions-gh-pages@v4 | |
| with: | |
| github_token: ${{ secrets.GITHUB_TOKEN }} | |
| publish_dir: docs/_build/html | |
| publish_branch: gh-pages |