ffi: skip toolchain check for packages with no built IR #65
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: Build Documentation and Test Coverage | |
| on: | |
| push: | |
| branches: [ main, master ] | |
| pull_request: | |
| branches: [ main, master ] | |
| workflow_dispatch: | |
| jobs: | |
| docs-and-tests: | |
| runs-on: self-hosted | |
| permissions: | |
| contents: write | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - name: Install Elan (Lean toolchain manager) | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Install Lean toolchain | |
| run: | | |
| if [ -f lean-toolchain ]; then | |
| TOOLCHAIN="$(cat lean-toolchain)" | |
| echo "Lean toolchain: $TOOLCHAIN" | |
| elan toolchain install "$TOOLCHAIN" || true | |
| fi | |
| elan show | |
| - name: Install weasyprint for PDF generation | |
| id: weasyprint | |
| run: | | |
| # weasyprint requires system libraries: pango, cairo, gdk-pixbuf | |
| # On RHEL/Fedora these are: pango, cairo, gdk-pixbuf2, libffi-devel | |
| # On Debian/Ubuntu: libpango-1.0-0, libpangocairo-1.0-0, etc. | |
| # The self-hosted runner may not have sudo; skip system install if unavailable. | |
| if sudo -n true 2>/dev/null; then | |
| if command -v apt-get &>/dev/null; then | |
| sudo apt-get update -qq | |
| sudo apt-get install -y -qq libpango-1.0-0 libpangocairo-1.0-0 libgdk-pixbuf2.0-0 libffi-dev libcairo2 2>/dev/null || true | |
| elif command -v dnf &>/dev/null; then | |
| sudo dnf install -y pango cairo gdk-pixbuf2 libffi-devel 2>/dev/null || true | |
| fi | |
| else | |
| echo "No passwordless sudo — skipping system package install (must be pre-installed)" | |
| fi | |
| # Check if weasyprint is already available (e.g. pre-installed in venv), | |
| # otherwise try to install it. | |
| if python3 -c "import weasyprint" 2>/dev/null; then | |
| echo "weasyprint already available" | |
| echo "has_weasyprint=true" >> "$GITHUB_OUTPUT" | |
| elif python3 -m pip install weasyprint; then | |
| echo "has_weasyprint=true" >> "$GITHUB_OUTPUT" | |
| elif python3 -m pip install --user weasyprint; then | |
| echo "has_weasyprint=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "::warning::weasyprint install failed — PDF generation will be skipped" | |
| echo "has_weasyprint=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| echo "$HOME/.local/bin" >> "$GITHUB_PATH" | |
| # ------------------------------------------------------- | |
| # Phase 1: Build everything | |
| # ------------------------------------------------------- | |
| - name: Build parser and test tools | |
| run: | | |
| lake build L4YAML | |
| lake build suiterunner tryparse tryroundtrip trydump | |
| lake build tests demo explicitkeytests flowtests | |
| lake build validationtests dumproundtrip rawparsetests | |
| lake build specexamples schemadump scannertests scannerspecexamples | |
| lake build adversarialtests mutationtests propertytests productioncoverage | |
| lake build limittests | |
| lake build flowregressioncheck errorstagediag scalarstagediag | |
| - name: Build documentation (doc/ sub-project) | |
| run: | | |
| cd doc | |
| lake update | |
| lake build l4yaml-doc | |
| - name: Generate L4YAML import graph | |
| # Renders the runtime module-import graph that the Architecture | |
| # page embeds at `Architecture/Import-Graph/graphs/import-graph.svg`. | |
| # The Proofs subtree is excluded — `L4YAML.Surface.Surface` would | |
| # otherwise pull `L4YAML.Proofs.Production.DocumentProduction`, | |
| # and merging the full Proofs environment trips a duplicate | |
| # equation-lemma error in `lake exe graph`. Surface itself is | |
| # represented via `L4YAML.Surface.Document` (its non-Proofs leaf). | |
| run: | | |
| # graphviz `dot` is needed to render the .dot file to .svg. | |
| if ! command -v dot >/dev/null 2>&1; then | |
| if sudo -n true 2>/dev/null && command -v dnf >/dev/null 2>&1; then | |
| sudo dnf install -y graphviz | |
| elif sudo -n true 2>/dev/null && command -v apt-get >/dev/null 2>&1; then | |
| sudo apt-get update -qq && sudo apt-get install -y -qq graphviz | |
| else | |
| echo "::error::graphviz 'dot' not found and no passwordless sudo to install it" | |
| exit 1 | |
| fi | |
| fi | |
| mkdir -p doc/Doc/L4YAML/graphs | |
| lake build graph | |
| lake exe graph \ | |
| --to=L4YAML.Scanner.Scanner,L4YAML.Parser.Composition,L4YAML.Surface.Document,L4YAML.Output.Dump,L4YAML.Output.Emitter,L4YAML.FFI.FFI,L4YAML.Schema.Api,L4YAML.Config.Config \ | |
| doc/Doc/L4YAML/graphs/import-graph.dot | |
| dot -Tsvg doc/Doc/L4YAML/graphs/import-graph.dot \ | |
| -o doc/Doc/L4YAML/graphs/import-graph.svg | |
| ls -lh doc/Doc/L4YAML/graphs/import-graph.* | |
| # ------------------------------------------------------- | |
| # Phase 2: Generate Verso HTML documentation | |
| # ------------------------------------------------------- | |
| - name: Download theorem dependency graphs from L4YAML.FGM | |
| # We fetch only the headlines tarball — the ~20 SVGs for headline | |
| # and categoryCapstone entries embedded directly into the Verso | |
| # verification doc. The full-catalogue tarball | |
| # (`theorem-graphs-all.tar.gz`, ~400 SVGs) stays on the GitHub | |
| # release and is linked from the doc for on-demand download. | |
| run: | | |
| mkdir -p doc/Doc/L4YAML/graphs | |
| REPO="pass/L4YAML.FGM" | |
| TAG="graphs-latest" | |
| ASSET="theorem-graphs-headlines.tar.gz" | |
| API_URL="${GITHUB_SERVER_URL}/api/v3/repos/${REPO}/releases/tags/${TAG}" | |
| # Fetch the release metadata to find the asset download URL | |
| ASSET_URL=$(curl -sSf \ | |
| -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \ | |
| -H "Accept: application/vnd.github.v3+json" \ | |
| "${API_URL}" \ | |
| | python3 -c " | |
| import sys, json | |
| release = json.load(sys.stdin) | |
| for asset in release.get('assets', []): | |
| if asset['name'] == '${ASSET}': | |
| print(asset['url']) | |
| sys.exit(0) | |
| print('ERROR: asset not found', file=sys.stderr) | |
| sys.exit(1) | |
| ") | |
| # Download the asset | |
| curl -sSfL \ | |
| -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \ | |
| -H "Accept: application/octet-stream" \ | |
| "${ASSET_URL}" \ | |
| -o "doc/Doc/L4YAML/graphs/${ASSET}" | |
| # Extract SVGs | |
| tar xzf "doc/Doc/L4YAML/graphs/${ASSET}" -C doc/Doc/L4YAML/graphs/ | |
| rm -f "doc/Doc/L4YAML/graphs/${ASSET}" | |
| echo "Downloaded $(ls doc/Doc/L4YAML/graphs/*.svg 2>/dev/null | wc -l) SVG graphs from L4YAML.FGM release" | |
| - name: Generate Verso documentation | |
| run: | | |
| cd doc | |
| lake exe l4yaml-doc | |
| echo "Verso HTML generated in doc/_out/html-multi/" | |
| - name: Copy Verso output to docs/ | |
| run: | | |
| rm -rf docs | |
| cp -r doc/_out/html-multi docs | |
| echo "Verso HTML copied to docs/" | |
| - name: Generate doc-gen4 API documentation | |
| run: | | |
| lake build :docs | |
| cp -r .lake/build/doc docs/api | |
| echo "doc-gen4 API docs copied to docs/api/" | |
| # ------------------------------------------------------- | |
| # Phase 3: Run all test suites | |
| # ------------------------------------------------------- | |
| - name: Run Lean test suites | |
| run: | | |
| mkdir -p docs/reports | |
| bash scripts/run-all-tests.sh docs/reports | |
| - name: Build C shared library | |
| run: | | |
| cmake -B ffi/build -S ffi | |
| cmake --build ffi/build | |
| mkdir -p ffi/out | |
| cp ffi/build/libl4yaml.so ffi/out/libl4yaml.so 2>/dev/null || true | |
| - name: Build Rust tryparse binary | |
| run: | | |
| cd rust/l4yaml | |
| cargo build --release --example tryparse | |
| - name: Run Python FFI tests | |
| run: | | |
| RESULTS="docs/reports" | |
| echo "=== Python FFI Tests ===" | tee "$RESULTS/python-ffi-tests.txt" | |
| cd "$GITHUB_WORKSPACE" | |
| L4YAML_LIB="$GITHUB_WORKSPACE/ffi/out" \ | |
| LD_LIBRARY_PATH="$GITHUB_WORKSPACE/ffi/out:${LD_LIBRARY_PATH:-}" \ | |
| python3 -m pytest Tests/test_python_ffi.py \ | |
| -v --tb=short --no-header \ | |
| -p no:launch_ros -p no:launch_testing \ | |
| --junitxml="$RESULTS/python-ffi-junit.xml" \ | |
| 2>&1 | tee -a "$RESULTS/python-ffi-tests.txt" | |
| - name: Run Python package tests | |
| run: | | |
| RESULTS="docs/reports" | |
| echo "=== Python Package Tests ===" | tee "$RESULTS/python-package-tests.txt" | |
| cd "$GITHUB_WORKSPACE" | |
| L4YAML_LIB="$GITHUB_WORKSPACE/ffi/out" \ | |
| LD_LIBRARY_PATH="$GITHUB_WORKSPACE/ffi/out:${LD_LIBRARY_PATH:-}" \ | |
| python3 -m pytest python/tests/ \ | |
| -v --tb=short --no-header \ | |
| -p no:launch_ros -p no:launch_testing \ | |
| --junitxml="$RESULTS/python-package-junit.xml" \ | |
| 2>&1 | tee -a "$RESULTS/python-package-tests.txt" | |
| - name: Run cross-language yaml-test-suite comparison | |
| run: | | |
| RESULTS="docs/reports" | |
| echo "=== Cross-Language yaml-test-suite Comparison ===" | tee "$RESULTS/cross-lang-comparison.txt" | |
| L4YAML_LIB="$GITHUB_WORKSPACE/ffi/out" \ | |
| LD_LIBRARY_PATH="$GITHUB_WORKSPACE/ffi/out:${LD_LIBRARY_PATH:-}" \ | |
| python3 - "$RESULTS" <<'PYEOF' | tee -a "$RESULTS/cross-lang-comparison.txt" | |
| import subprocess, sys, json, pathlib | |
| results_dir = pathlib.Path(sys.argv[1]) | |
| BACKENDS = ["lean", "c", "python", "rust"] | |
| PRESETS = ["unlimited", "default", "strict", "permissive", "safe_tags"] | |
| suiterunner = ".lake/build/bin/suiterunner" | |
| results = {} | |
| all_match = True | |
| for preset in PRESETS: | |
| for backend in BACKENDS: | |
| cmd = [suiterunner, "--backend", backend, "--limits", preset] | |
| proc = subprocess.run(cmd, capture_output=True, text=True, timeout=600) | |
| output = proc.stdout + proc.stderr | |
| for line in output.splitlines(): | |
| if "TOTAL:" in line: | |
| parts = line.split() | |
| p, f, s, t = int(parts[1]), int(parts[3]), int(parts[5]), int(parts[7].strip("()")) | |
| results[(backend, preset)] = (p, f, s, t) | |
| break | |
| else: | |
| print(f"ERROR: no TOTAL line for {backend}/{preset}", file=sys.stderr) | |
| results[(backend, preset)] = (0, 0, 0, 0) | |
| all_match = False | |
| vals = [results[(b, preset)] for b in BACKENDS] | |
| if len(set(vals)) != 1: | |
| print(f"MISMATCH for preset '{preset}': {dict(zip(BACKENDS, vals))}") | |
| all_match = False | |
| else: | |
| p, f, s, t = vals[0] | |
| print(f"{preset:12s}: {p} passed, {f} failed, {s} skipped ({t} total) — all 4 backends identical") | |
| print() | |
| if all_match: | |
| print("✓ All backends produce identical results for every preset") | |
| else: | |
| print("✗ Backend mismatch detected!") | |
| sys.exit(1) | |
| json_data = {} | |
| for (backend, preset), (p, f, s, t) in results.items(): | |
| json_data.setdefault(preset, {})[backend] = {"passed": p, "failed": f, "skipped": s, "total": t} | |
| (results_dir / "cross-lang-results.json").write_text(json.dumps(json_data, indent=2)) | |
| PYEOF | |
| # ------------------------------------------------------- | |
| # Phase 4: Generate HTML reports from test data | |
| # ------------------------------------------------------- | |
| - name: Generate test result HTML reports | |
| run: | | |
| python3 scripts/generate-test-reports.py docs/reports | |
| - name: Collect stats (kernel-accurate axiom + sorry counts) | |
| # Runs after every other report under docs/reports/ has landed so | |
| # the JSON aggregates source-scan, env-scan (via Lean.collectAxioms | |
| # on the compiled L4YAML environment), and the existing test-runner | |
| # totals. Output: docs/reports/stats.json — picked up by the | |
| # `git add docs/` commit step below. | |
| run: | | |
| lake exe collect-stats | |
| test -f docs/reports/stats.json | |
| # ------------------------------------------------------- | |
| # Phase 5: Generate PDF from HTML | |
| # ------------------------------------------------------- | |
| - name: Generate PDF documentation | |
| if: steps.weasyprint.outputs.has_weasyprint == 'true' | |
| run: | | |
| python3 scripts/html-to-pdf.py \ | |
| docs \ | |
| docs/L4YAML.pdf | |
| echo "PDF generated: docs/L4YAML.pdf" | |
| - name: Add PDF download link to documentation | |
| if: steps.weasyprint.outputs.has_weasyprint == 'true' | |
| run: | | |
| if [ -f docs/L4YAML.pdf ]; then | |
| # Inject PDF download link into the landing page after the intro paragraph | |
| sed -i 's|strategy, security model, and FFI bindings for C, Python, and Rust.</p>|strategy, security model, and FFI bindings for C, Python, and Rust.</p>\n <p>\n A PDF version of this manual is available for download:\n<a href="L4YAML.pdf">L4YAML.pdf</a>.</p>|' docs/index.html | |
| echo "PDF download link added to docs/index.html" | |
| fi | |
| # ------------------------------------------------------- | |
| # Phase 6: Publish | |
| # ------------------------------------------------------- | |
| - name: Upload documentation as artifact | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: l4yaml-docs | |
| path: docs/ | |
| retention-days: 30 | |
| - name: Commit documentation to main branch | |
| if: github.ref == 'refs/heads/main' || github.ref == 'refs/heads/master' | |
| run: | | |
| git config user.name "github-actions[bot]" | |
| git config user.email "github-actions[bot]@users.noreply.github.com" | |
| git add docs/ | |
| git diff --staged --quiet || git commit -m "Update docs and test reports: ${{ github.sha }}" | |
| git push | |
| - name: Comment on PR with coverage summary | |
| if: github.event_name == 'pull_request' | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| const fs = require('fs'); | |
| let coverageLine = 'Statistics unavailable'; | |
| try { | |
| const coverage = fs.readFileSync('docs/reports/coverage-console.txt', 'utf8'); | |
| coverageLine = coverage.match(/Correct: .*/)?.[0] || coverageLine; | |
| } catch (e) {} | |
| let pythonSummary = ''; | |
| try { | |
| const ffiTests = fs.readFileSync('docs/reports/python-ffi-tests.txt', 'utf8'); | |
| const ffiLine = ffiTests.match(/\d+ passed.*/)?.[0] || ''; | |
| const pkgTests = fs.readFileSync('docs/reports/python-package-tests.txt', 'utf8'); | |
| const pkgLine = pkgTests.match(/\d+ passed.*/)?.[0] || ''; | |
| pythonSummary = `\n\n**Python API Tests:**\n- FFI integration: ${ffiLine}\n- Package tests: ${pkgLine}`; | |
| } catch (e) {} | |
| let crossLangSummary = ''; | |
| try { | |
| const crossLang = fs.readFileSync('docs/reports/cross-lang-comparison.txt', 'utf8'); | |
| const lines = crossLang.split('\n').filter(l => l.includes('identical') || l.includes('MISMATCH') || l.includes('✓') || l.includes('✗')); | |
| if (lines.length > 0) { | |
| crossLangSummary = `\n\n**Cross-Language Comparison (4 backends × 5 presets):**\n\`\`\`\n${lines.join('\n')}\n\`\`\``; | |
| } | |
| } catch (e) {} | |
| github.rest.issues.createComment({ | |
| issue_number: context.issue.number, | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| body: `## L4YAML Documentation & Test Coverage\n\n\`\`\`\n${coverageLine}\n\`\`\`${pythonSummary}${crossLangSummary}\n\n📄 [Download documentation artifact](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})` | |
| }); |