feat: add leanblueprint setup with GitHub Pages deployment#7
Merged
Conversation
E0.2: Add SignedEpistasisSkeleton to lakefile roots[] so all 37 .lean files are tracked by the build system (fixes orphaned module). E0.3: Extend CI trigger to epic/** branches so feature PRs get verified. E0.5: Update LintOptions.lean docs to enumerate all enforced checks (unusedVariables, funArgs, patternVars) and cross-reference the CI pipeline checks (sorry/axiom/admit/native_decide). E0.6: Add timeout-minutes: 25 to the build job (cold-cache SLA ≤ 25 min). CI: Add native_decide check step (kernel-bypass prevention) and native_decide counter to the job summary. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- Add blueprint/ folder with LaTeX structure for formalization dependency graph - Write comprehensive content.tex with 7 chapters covering all major results - Create GitHub Pages workflow for automatic deployment - Update lake-manifest.json and lean-toolchain The blueprint documents the formalization structure including: - Preliminaries (probability, Hoeffding) - Drift theorems (additive, multiplicative, negative) - Game theory (minimax, witness games, veto) - LBT preconditions (G1, G2, G3) - Coupling arguments - Applications (FIFO traps, epistasis, persistence) - Capstone validation (28 conjuncts)
📝 WalkthroughWalkthroughThis PR introduces a comprehensive blueprint documentation system for Level-Based Theorem Formalization, including LaTeX sources and auto-generated web pages, plus supporting CI infrastructure to enforce code constraints and deploy the blueprint to GitHub Pages. It updates toolchain versions and adds a lint enforcement mechanism. ChangesBlueprint Documentation System
CI/Workflow and Project Updates
Sequence DiagramsequenceDiagram
participant User
participant GitHub as GitHub Actions
participant LaTeX as LaTeX Engine
participant PlasTeX as PlasTeX
participant Web as GitHub Pages
User->>GitHub: Push to master
rect rgba(100, 150, 200, 0.5)
Note over GitHub,LaTeX: Blueprint Build Job
GitHub->>GitHub: Checkout repo
GitHub->>GitHub: Install Lean toolchain
GitHub->>GitHub: Build with lake
GitHub->>LaTeX: Run latexmk (print.tex)
LaTeX->>LaTeX: Compile PDF via XeLaTeX
GitHub->>PlasTeX: Run leanblueprint web (web.tex)
PlasTeX->>PlasTeX: Parse LaTeX + leanblueprint macros
PlasTeX->>PlasTeX: Generate HTML5 sections (sect*.html)
PlasTeX->>PlasTeX: Apply styles + theme CSS
end
GitHub->>GitHub: Upload blueprint/web artifact
rect rgba(150, 200, 150, 0.5)
Note over GitHub,Web: Deploy Job
GitHub->>Web: Deploy Pages artifact
Web-->>User: Serve blueprint/web/index.html
end
User->>Web: Browse sections
Web->>User: Render HTML with MathJax + interactive proofs
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes The PR introduces substantial new infrastructure spanning LaTeX document authoring (content structure, macros, configuration), CSS/HTML web output generation (multiple themes, interactive JavaScript), GitHub Actions workflows (build and deployment pipelines), and updates to toolchain/dependencies. While changes are largely self-contained within discrete file directories, the review requires understanding: the blueprint build pipeline coordination across
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Review rate limit: 0/5 reviews remaining, refill in 55 minutes and 17 seconds. Comment |
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request updates the project to Lean 4 v4.30.0-rc2, bumps several dependencies in lake-manifest.json, and introduces a comprehensive LaTeX blueprint for the formalization of level-based theorems. It also refines global linting options to include CI enforcement notes and adds the SignedEpistasisSkeleton module to the library. I have no feedback to provide.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 9
🧹 Nitpick comments (1)
blueprint/web/js/plastex.js (1)
65-68: ⚡ Quick winUse
.closest()for modal close targeting instead of fixed parent hops.Line 67 is tightly coupled to current markup depth and can silently break with minor HTML structure changes.
Refactor suggestion
- $(this).parent().parent().parent().hide(); + $(this).closest("div.modal-container").hide();🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@blueprint/web/js/plastex.js` around lines 65 - 68, The click handler on $("button.closebtn") uses brittle DOM traversal $(this).parent().parent().parent().hide(); — replace that traversal with a .closest(...) call that targets the modal/container element (e.g., .closest('.modal') or your component's specific container class) so the close button reliably hides the intended ancestor; update the handler in the $("button.closebtn").click function to call .closest(...) and then .hide() on the found element, falling back to a safe no-op if nothing is found.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In @.github/workflows/blueprint.yml:
- Around line 41-43: The workflow step named "Install Python dependencies"
currently runs pip install leanblueprint without a version constraint; update
that command to pin to a tested, explicit version (for example change to pip
install 'leanblueprint==<TESTED_VERSION>') or reference a workflow variable
(e.g., LEANBLUEPRINT_VERSION) and use pip install
"leanblueprint==${LEANBLUEPRINT_VERSION}" so future releases won't break the
pipeline; update any docs or tests to record the chosen <TESTED_VERSION>.
In @.github/workflows/ci.yml:
- Around line 89-99: The current raw-text grep for the banned token
native_decide (and the similar sorry/admit scans) produces false positives from
comments/docs; change the check to strip Lean comments before searching: remove
line comments starting with -- and remove block comments /- ... -/ from the
files (or otherwise filter them out) and then run the token search against the
comment-free content, and apply the same comment-stripping approach for the
sorry and admit checks so only real code (not documentation) triggers CI
failures; target the checks that reference native_decide, sorry, and admit in
the workflow to implement this filtering.
- Around line 21-24: Replace the insecure "Install Elan" step that runs the
unpinned curl | sh command (the lines invoking elan-init.sh and appending
$HOME/.elan/bin to $GITHUB_PATH) with the official leanprover/lean-action pinned
to a specific commit SHA (e.g. uses: leanprover/lean-action@<commit-sha>); this
action will install elan via the official elan.lean-lang.org endpoint and
perform integrity/hash verification of toolchain downloads, so remove the direct
curl invocation and the manual PATH echo and configure the action inputs as
needed.
In `@blueprint/src/content.tex`:
- Around line 239-253: The theorem labeled thm:full_paper_capstone currently
asserts that "The 28 conjuncts... are formally verified" but some dependencies
remain marked \notready; update the statement to avoid overstating verification
by either prefixing the theorem with \notready or weakening the claim text
(e.g., "Most of the 28 conjuncts are formally verified; remaining conjuncts are
pending") and ensure the change is applied to the theorem environment named Full
paper capstone (thm:full_paper_capstone) and its uses/dependencies list
(thm:linear_ranking, thm:runtime_bound, thm:fifo_trap_runtime,
lem:epistasis_bounds, thm:simultaneous_persistence) so the document accurately
reflects the unresolved \notready-marked items.
In `@blueprint/src/latexmkrc`:
- Line 4: The $pdflatex setting in the latexmkrc currently omits latexmk
placeholders so options and the source file aren't forwarded; update the
$pdflatex variable (the line setting $pdflatex) to include the %O and %S
placeholders so latexmk passes its options and the source filename to xelatex
(i.e., ensure the command string includes both %O and %S in the appropriate
positions).
In `@blueprint/web/sect0002.html`:
- Around line 10-11: The MathJax CDN script tag using
"https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js" is missing subresource
integrity and crossorigin attributes; update the <script> tag that loads MathJax
(the script src string
"https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js") to either include a
correct integrity="..." value and crossorigin="anonymous" for SRI or replace the
external reference with a self-hosted copy of the same file and adjust src
accordingly so the external CDN dependency is removed.
In `@blueprint/web/styles/theme-blue.css`:
- Line 1: The committed generated stylesheet (starts with `@charset` "UTF-8"; and
contains long concatenated selectors like a,abbr,... and rules such as
div.content, pre.verbatim) is triggering stylelint errors; either exclude this
generated asset from linting by adding its filename pattern to .stylelintignore,
or normalize it by prepending a stylelint disable comment (e.g. /*
stylelint-disable */) at the top and re-generating so CI will pass; update the
CI/lint configuration if necessary to ensure other generated theme files follow
the same ignore/disable approach.
In `@blueprint/web/styles/theme-white.css`:
- Line 1: The committed theme asset fails stylelint (Line 1) because the file
begins with a concatenated selector block after `@charset` ("@charset \"UTF-8\";
a,abbr,acronym,...") and contains style patterns that violate project lint
rules; fix by either (A) normalizing the CSS so it passes lint: split the
`@charset` onto its own line, reformat the large selector list into valid,
lowercased tokens and run stylelint autofix; target the top-of-file token
"@charset \"UTF-8\";" and the huge selector "a,abbr,acronym,address,..." and
adjust any keyword/casing to match rules, or (B) treat as vendor/generated and
exclude it from stylelint by adding an exclusion (e.g., a pattern in stylelint
config or a comment header like /* stylelint-disable */) so lint gates no longer
block the PR.
---
Nitpick comments:
In `@blueprint/web/js/plastex.js`:
- Around line 65-68: The click handler on $("button.closebtn") uses brittle DOM
traversal $(this).parent().parent().parent().hide(); — replace that traversal
with a .closest(...) call that targets the modal/container element (e.g.,
.closest('.modal') or your component's specific container class) so the close
button reliably hides the intended ancestor; update the handler in the
$("button.closebtn").click function to call .closest(...) and then .hide() on
the found element, falling back to a safe no-op if nothing is found.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 7da3e205-05ba-42d0-8e7b-f58cd5a4e1d2
⛔ Files ignored due to path filters (2)
blueprint/web/js/jquery.min.jsis excluded by!**/*.min.jsblueprint/web/symbol-defs.svgis excluded by!**/*.svg
📒 Files selected for processing (32)
.github/workflows/blueprint.yml.github/workflows/ci.ymlLintOptions.leanblueprint/src/blueprint.styblueprint/src/content.texblueprint/src/extra_styles.cssblueprint/src/latexmkrcblueprint/src/macros/common.texblueprint/src/macros/print.texblueprint/src/macros/web.texblueprint/src/plastex.cfgblueprint/src/print.texblueprint/src/web.pauxblueprint/src/web.texblueprint/web/index.htmlblueprint/web/js/plastex.jsblueprint/web/js/svgxuse.jsblueprint/web/sect0001.htmlblueprint/web/sect0002.htmlblueprint/web/sect0003.htmlblueprint/web/sect0004.htmlblueprint/web/sect0005.htmlblueprint/web/sect0006.htmlblueprint/web/sect0007.htmlblueprint/web/styles/amsthm.cssblueprint/web/styles/extra_styles.cssblueprint/web/styles/theme-blue.cssblueprint/web/styles/theme-green.cssblueprint/web/styles/theme-white.csslake-manifest.jsonlakefile.leanlean-toolchain
Comment on lines
+24
to
+27
| - name: Install Elan | ||
| run: | | ||
| curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none | ||
| echo "$HOME/.elan/bin" >> $GITHUB_PATH |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
# First, let's check if the workflow file exists and read the relevant section
git ls-files | grep -E "\.github/workflows"Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 142
🏁 Script executed:
# Read the blueprint workflow file
cat -n .github/workflows/blueprint.ymlRepository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 2122
🏁 Script executed:
# Check if there are other workflows that install Elan to see patterns
fd -e yml -e yaml . .github/workflows/ --exec grep -l "elan" {} \;Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 142
🏁 Script executed:
# Look for any version pinning patterns elsewhere in the repository
rg "ELAN|elan" --type yml -A 2 -B 2 .github/Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 113
🏁 Script executed:
# Read the ci.yml workflow
cat -n .github/workflows/ci.ymlRepository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 8886
🏁 Script executed:
# Check Elan repository for available version tags/releases
# First, let's see what the structure is and if version pinning is documented
curl -s https://api.github.com/repos/leanprover/elan/releases | head -100Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 5685
🏁 Script executed:
# Also check if there are any existing Lean toolchain specifications in the repo
# that might indicate version preferences
fd -e "lean-toolchain" -o -e "lakefile.lean" | xargs head -5Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 202
🏁 Script executed:
# Find and read lean-toolchain file
find . -name "lean-toolchain" -type fRepository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 102
🏁 Script executed:
# Check the content
cat lean-toolchainRepository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 113
🏁 Script executed:
# Look for any existing references to elan version in docs or CI setup
rg "elan.*version|v[0-9]+\.[0-9]+\.[0-9]+" --type-list | head -20Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 475
🏁 Script executed:
# Verify the structure of Elan releases - check if the init script exists at tag refs
curl -s -I "https://raw.githubusercontent.com/leanprover/elan/v4.2.1/elan-init.sh"Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 953
Pin the Elan installer source to an immutable release version.
Both .github/workflows/blueprint.yml (line 26) and .github/workflows/ci.yml (line 23) fetch the Elan installer from the mutable master branch, weakening supply-chain integrity and reproducibility. This conflicts with the project's existing practice of pinning the Lean toolchain (e.g., leanprover/lean4:v4.30.0-rc2 in lean-toolchain).
The Elan repository supports release tags and the init script is accessible at versioned references. Apply this pattern to both workflows:
Suggested hardening
- curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+ ELAN_VERSION="v4.2.1"
+ curl -sSfL "https://raw.githubusercontent.com/leanprover/elan/${ELAN_VERSION}/elan-init.sh" | sh -s -- -y --default-toolchain none📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| - name: Install Elan | |
| run: | | |
| curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Install Elan | |
| run: | | |
| ELAN_VERSION="v4.2.1" | |
| curl -sSfL "https://raw.githubusercontent.com/leanprover/elan/${ELAN_VERSION}/elan-init.sh" | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH |
Comment on lines
+41
to
+43
| - name: Install Python dependencies | ||
| run: | | ||
| pip install leanblueprint |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
cat -n .github/workflows/blueprint.ymlRepository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 2122
🏁 Script executed:
# Search for any requirements files that might contain version specifications
fd -type f \( -name "requirements*.txt" -o -name "setup.py" -o -name "pyproject.toml" -o -name "Pipfile" \)Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 256
🏁 Script executed:
# Check if there are other pip install commands in workflows for comparison
rg "pip install" .github/workflows/Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 153
🏁 Script executed:
# Search for requirements files
find . -maxdepth 3 -type f \( -name "requirements*.txt" -o -name "setup.py" -o -name "pyproject.toml" -o -name "setup.cfg" \)Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 67
🏁 Script executed:
# Check if other tools/dependencies are pinned in the workflow
rg "actions/checkout|actions/cache|actions/upload|actions/deploy" .github/workflows/blueprint.yml -A 1Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 273
🏁 Script executed:
# Search for any documentation about leanblueprint usage or version requirements
find . -type f \( -name "README*" -o -name "*.md" \) | head -5 | xargs grep -l "leanblueprint" 2>/dev/null || echo "No mentions found"Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 103
Pin leanblueprint to a tested version.
Line 43 installs leanblueprint without a version constraint, allowing breaking changes in future releases to unexpectedly break this pipeline. The workflow already pins versions for other tools (actions/checkout@v4, actions/cache@v4, etc.), so this dependency should follow the same pattern.
Suggested hardening
- pip install leanblueprint
+ pip install "leanblueprint==<tested-version>"📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| - name: Install Python dependencies | |
| run: | | |
| pip install leanblueprint | |
| - name: Install Python dependencies | |
| run: | | |
| pip install "leanblueprint==<tested-version>" |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In @.github/workflows/blueprint.yml around lines 41 - 43, The workflow step
named "Install Python dependencies" currently runs pip install leanblueprint
without a version constraint; update that command to pin to a tested, explicit
version (for example change to pip install 'leanblueprint==<TESTED_VERSION>') or
reference a workflow variable (e.g., LEANBLUEPRINT_VERSION) and use pip install
"leanblueprint==${LEANBLUEPRINT_VERSION}" so future releases won't break the
pipeline; update any docs or tests to record the chosen <TESTED_VERSION>.
Comment on lines
21
to
24
| - name: Install Elan | ||
| run: | | ||
| curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.6/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | ||
| ./elan-init -y --default-toolchain none | ||
| curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none | ||
| echo "$HOME/.elan/bin" >> $GITHUB_PATH |
There was a problem hiding this comment.
🧩 Analysis chain
🌐 Web query:
What is the currently recommended secure way to install elan in GitHub Actions for Lean 4, including pinning to a specific version or commit and integrity verification?
💡 Result:
The currently recommended secure way to install Elan in GitHub Actions for Lean 4 is to use the official leanprover/lean-action pinned to a specific version tag or commit SHA. This action handles Elan installation via its internal scripts/install_elan.sh, which downloads from the official elan.lean-lang.org endpoint (equivalent to curl https://elan.lean-lang.org/elan-init.sh | sh -s -- -y), adds ~/.elan/bin to PATH, and respects the project's lean-toolchain file for Lean version selection. For maximum security: - Pin the lean-action to a commit SHA (e.g., uses: leanprover/lean-action@534e91c... # latest as of Dec 2025 from PR #143). - Pin all other actions (e.g., actions/checkout@de0fac2 # v4). - Use lean-toolchain file to pin Lean version (e.g., leanprover/lean4:stable or v4.27.0). - Elan itself verifies toolchain downloads with hashes from GitHub releases. Example workflow (.github/workflows/ci.yml): name: CI on: [push, pull_request] jobs: build: runs-on: ubuntu-latest steps: - uses: actions/checkout@de0fac2 # v4.1.7 - uses: leanprover/lean-action@534e91c # Pin to latest known good commit; update via Dependabot This is used by mathlib4 (PR #23868, Apr 2025) and is the standard for Lean projects. Elan downloads toolchains from leanprover/lean4 GitHub releases with built-in integrity checks (SHA256). No additional verification needed beyond pinning actions and toolchain. For custom Elan pinning, download elan-init from a specific commit/release tarball, but lean-action suffices for standard use.
Citations:
- 1: https://github.com/leanprover/lean-action
- 2: https://github.com/leanprover/lean-action/blob/main/action.yml
- 3: [Merged by Bors] - ci: install Elan and configure Lean via
lean-actionleanprover-community/mathlib4#23868 - 4: https://github.com/leanprover/elan
- 5: https://github.com/leanprover/elan/blob/master/elan-init.sh
- 6: fix: fail lean-action if any command in
install_elan.shfails leanprover/lean-action#143 - 7: https://github.com/trishullab/clever/blob/main/.github/workflows/lean_action_ci.yml
- 8: https://www.stepsecurity.io/blog/pinning-github-actions-for-enhanced-security-a-complete-guide
- 9: https://dev.to/achiya-automation/i-just-hardened-my-oss-release-pipeline-to-11-layers-of-security-heres-the-playbook-4267
- 10: https://github.com/step-security/action-install-gh-release
Use the official leanprover/lean-action GitHub Action instead of unpinned curl | sh for elan installation.
The current approach downloads elan-init.sh from the master branch tip, which bypasses integrity verification and exposes the CI supply chain to risks. Use leanprover/lean-action pinned to a specific commit SHA, which handles elan installation via the official elan.lean-lang.org endpoint with built-in hash verification of toolchain downloads.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In @.github/workflows/ci.yml around lines 21 - 24, Replace the insecure "Install
Elan" step that runs the unpinned curl | sh command (the lines invoking
elan-init.sh and appending $HOME/.elan/bin to $GITHUB_PATH) with the official
leanprover/lean-action pinned to a specific commit SHA (e.g. uses:
leanprover/lean-action@<commit-sha>); this action will install elan via the
official elan.lean-lang.org endpoint and perform integrity/hash verification of
toolchain downloads, so remove the direct curl invocation and the manual PATH
echo and configure the action inputs as needed.
Comment on lines
+89
to
+99
| - name: Check for native_decide | ||
| run: | | ||
| echo "::group::Searching for native_decide" | ||
| FOUND=$(grep -rn 'native_decide' --include='*.lean' . \ | ||
| | grep -v '\.lake/packages/' \ | ||
| || true) | ||
| if [ -n "$FOUND" ]; then | ||
| echo "::error::Found native_decide in Lean sources (bypasses kernel — use decide instead)" | ||
| echo "$FOUND" | ||
| exit 1 | ||
| fi |
There was a problem hiding this comment.
Token scan will produce false positives and can hard-fail CI.
Line 92 scans raw .lean text, so comment/docs mentions are treated as violations. With this PR, documented policy text includes banned tokens, so these grep checks can fail even without forbidden code usage. Harden the scan to ignore documentation/comment hits (and apply the same approach to sorry/admit checks for consistency).
Suggested patch
- - name: Check for native_decide
+ - name: Check for native_decide
run: |
echo "::group::Searching for native_decide"
FOUND=$(grep -rn 'native_decide' --include='*.lean' . \
| grep -v '\.lake/packages/' \
+ | grep -v 'LintOptions.lean:' \
|| true)
if [ -n "$FOUND" ]; then
echo "::error::Found native_decide in Lean sources (bypasses kernel — use decide instead)"
echo "$FOUND"
exit 1
fi📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| - name: Check for native_decide | |
| run: | | |
| echo "::group::Searching for native_decide" | |
| FOUND=$(grep -rn 'native_decide' --include='*.lean' . \ | |
| | grep -v '\.lake/packages/' \ | |
| || true) | |
| if [ -n "$FOUND" ]; then | |
| echo "::error::Found native_decide in Lean sources (bypasses kernel — use decide instead)" | |
| echo "$FOUND" | |
| exit 1 | |
| fi | |
| - name: Check for native_decide | |
| run: | | |
| echo "::group::Searching for native_decide" | |
| FOUND=$(grep -rn 'native_decide' --include='*.lean' . \ | |
| | grep -v '\.lake/packages/' \ | |
| | grep -v 'LintOptions.lean:' \ | |
| || true) | |
| if [ -n "$FOUND" ]; then | |
| echo "::error::Found native_decide in Lean sources (bypasses kernel — use decide instead)" | |
| echo "$FOUND" | |
| exit 1 | |
| fi |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In @.github/workflows/ci.yml around lines 89 - 99, The current raw-text grep for
the banned token native_decide (and the similar sorry/admit scans) produces
false positives from comments/docs; change the check to strip Lean comments
before searching: remove line comments starting with -- and remove block
comments /- ... -/ from the files (or otherwise filter them out) and then run
the token search against the comment-free content, and apply the same
comment-stripping approach for the sorry and admit checks so only real code (not
documentation) triggers CI failures; target the checks that reference
native_decide, sorry, and admit in the workflow to implement this filtering.
Comment on lines
+239
to
+253
| \begin{theorem}[Full paper capstone] | ||
| \label{thm:full_paper_capstone} | ||
| The 28 conjuncts of the paper are formally verified, covering: | ||
| \begin{enumerate} | ||
| \item LBT preconditions (G1, G2, G3) | ||
| \item Linear ranking theorem | ||
| \item Selection amplification | ||
| \item Coupling arguments | ||
| \item Runtime bounds | ||
| \item Applications (FIFO traps, epistasis, persistence) | ||
| \end{enumerate} | ||
| \lean{UnifiedPaperValidation.full_paper_capstone} | ||
| \uses{thm:linear_ranking, thm:runtime_bound, thm:fifo_trap_runtime, lem:epistasis_bounds, thm:simultaneous_persistence} | ||
| \leanok | ||
| \end{theorem} |
There was a problem hiding this comment.
Capstone claim currently overstates verification completeness.
Line 241 states the 28 conjuncts are formally verified, but unresolved items are explicitly marked \notready at Line 158, Line 175, and Line 183. Please downgrade the statement (or mark this theorem \notready) until those dependencies are complete.
Suggested adjustment
\begin{theorem}[Full paper capstone]
\label{thm:full_paper_capstone}
- The 28 conjuncts of the paper are formally verified, covering:
+ The capstone target covers 28 conjuncts of the paper; items marked \notready remain open:
@@
\lean{UnifiedPaperValidation.full_paper_capstone}
\uses{thm:linear_ranking, thm:runtime_bound, thm:fifo_trap_runtime, lem:epistasis_bounds, thm:simultaneous_persistence}
- \leanok
+ \notready
\end{theorem}📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| \begin{theorem}[Full paper capstone] | |
| \label{thm:full_paper_capstone} | |
| The 28 conjuncts of the paper are formally verified, covering: | |
| \begin{enumerate} | |
| \item LBT preconditions (G1, G2, G3) | |
| \item Linear ranking theorem | |
| \item Selection amplification | |
| \item Coupling arguments | |
| \item Runtime bounds | |
| \item Applications (FIFO traps, epistasis, persistence) | |
| \end{enumerate} | |
| \lean{UnifiedPaperValidation.full_paper_capstone} | |
| \uses{thm:linear_ranking, thm:runtime_bound, thm:fifo_trap_runtime, lem:epistasis_bounds, thm:simultaneous_persistence} | |
| \leanok | |
| \end{theorem} | |
| \begin{theorem}[Full paper capstone] | |
| \label{thm:full_paper_capstone} | |
| The capstone target covers 28 conjuncts of the paper; items marked \notready remain open: | |
| \begin{enumerate} | |
| \item LBT preconditions (G1, G2, G3) | |
| \item Linear ranking theorem | |
| \item Selection amplification | |
| \item Coupling arguments | |
| \item Runtime bounds | |
| \item Applications (FIFO traps, epistasis, persistence) | |
| \end{enumerate} | |
| \lean{UnifiedPaperValidation.full_paper_capstone} | |
| \uses{thm:linear_ranking, thm:runtime_bound, thm:fifo_trap_runtime, lem:epistasis_bounds, thm:simultaneous_persistence} | |
| \notready | |
| \end{theorem} |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@blueprint/src/content.tex` around lines 239 - 253, The theorem labeled
thm:full_paper_capstone currently asserts that "The 28 conjuncts... are formally
verified" but some dependencies remain marked \notready; update the statement to
avoid overstating verification by either prefixing the theorem with \notready or
weakening the claim text (e.g., "Most of the 28 conjuncts are formally verified;
remaining conjuncts are pending") and ensure the change is applied to the
theorem environment named Full paper capstone (thm:full_paper_capstone) and its
uses/dependencies list (thm:linear_ranking, thm:runtime_bound,
thm:fifo_trap_runtime, lem:epistasis_bounds, thm:simultaneous_persistence) so
the document accurately reflects the unresolved \notready-marked items.
| # This file configures the latexmk command you can use to compile | ||
| # the pdf version of the blueprint | ||
| $pdf_mode = 1; | ||
| $pdflatex = 'xelatex -synctex=1'; |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Verify placeholder presence in latexmk config
rg -n '^\$pdflatex\s*=' blueprint/src/latexmkrc
rg -n '%O|%S' blueprint/src/latexmkrc
# Expected: the $pdflatex line should include both %O and %SRepository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 121
Add latexmk placeholders to $pdflatex command.
The $pdflatex variable is missing the %O (options) and %S (source file) placeholders. Without them, options and source files passed by latexmk will not reach xelatex, breaking latexmk-driven builds.
🔧 Proposed fix
-$pdflatex = 'xelatex -synctex=1';
+$pdflatex = 'xelatex -synctex=1 %O %S';📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| $pdflatex = 'xelatex -synctex=1'; | |
| $pdflatex = 'xelatex -synctex=1 %O %S'; |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@blueprint/src/latexmkrc` at line 4, The $pdflatex setting in the latexmkrc
currently omits latexmk placeholders so options and the source file aren't
forwarded; update the $pdflatex variable (the line setting $pdflatex) to include
the %O and %S placeholders so latexmk passes its options and the source filename
to xelatex (i.e., ensure the command string includes both %O and %S in the
appropriate positions).
Comment on lines
+10
to
+11
| <script type="text/javascript" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js"> | ||
| </script> |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Check MathJax CDN usage and integrity attributes across generated pages
rg -n 'cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js' blueprint/web
rg -n 'integrity=' blueprint/web
# Expected: all external script includes should be either integrity-pinned or replaced with local assets.Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 1082
Add integrity attributes or self-host MathJax to harden external script loading.
MathJax is loaded from cdn.jsdelivr.net without subresource integrity (SRI) attributes across 8 pages (sect0001.html through sect0007.html and index.html, all at line 10). This weakens trust guarantees for published docs. Add integrity and crossorigin attributes to the CDN script tag, or replace with a self-hosted copy.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@blueprint/web/sect0002.html` around lines 10 - 11, The MathJax CDN script tag
using "https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js" is missing
subresource integrity and crossorigin attributes; update the <script> tag that
loads MathJax (the script src string
"https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js") to either include a
correct integrity="..." value and crossorigin="anonymous" for SRI or replace the
external reference with a self-hosted copy of the same file and adjust src
accordingly so the external CDN dependency is removed.
| @@ -0,0 +1 @@ | |||
| @charset "UTF-8";a,abbr,acronym,address,applet,article,aside,audio,b,big,blockquote,body,canvas,caption,center,cite,code,dd,del,details,dfn,div,dl,dt,em,embed,fieldset,figcaption,figure,footer,form,h1,h2,h3,h4,h5,h6,header,hgroup,html,i,iframe,img,ins,kbd,label,legend,li,mark,menu,nav,object,ol,output,p,pre,q,ruby,s,samp,section,small,span,strike,strong,sub,summary,sup,table,tbody,td,tfoot,th,thead,time,tr,tt,u,ul,var,video{font:inherit;font-size:100%;margin:0;padding:0;border:0}article,aside,details,figcaption,figure,footer,header,hgroup,menu,nav,section{display:block}body{line-height:1;overflow-x:hidden;background:#f4f4f4}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:after,blockquote:before,q:after,q:before{content:"";content:none}table{border-spacing:0;border-collapse:collapse}.clear:after{font-size:0;display:block;visibility:hidden;clear:both;height:0;content:" "}.clear{display:inline-block}* html .clear{height:1%}.clear{display:block}*{box-sizing:border-box}hr{clear:both;border:none;outline:none}em{font-style:italic}a{text-decoration:underline}ul{list-style:disc}ol{list-style:decimal}ol,ul{font-size:14px;padding:0 0 0 33px}ol li,ul li{margin:0}blockquote{padding:0 15px 0 40px}table{font-size:13px;width:100%;margin:20px 0;background:#fff}table th{font-size:16px;font-weight:700}table tr td{padding:7px}::selection{color:#fff;background:#000}::-moz-selection{color:#fff;background:#000}body{height:100vh;margin:0;flex-direction:column;color:#0a0a14;background-color:#e8e8e8}body,div.wrapper{display:flex;overflow:hidden}div.wrapper{flex-grow:1}div.content-wrapper{max-width:75ch}@media (min-width:1024px){div.content-wrapper{margin-left:auto;margin-right:auto}}div.content{flex-grow:1;display:flex;flex-direction:column;overflow:auto;padding:.5rem;margin-bottom:2.5rem}@media (min-width:1024px){div.content{padding:1rem;margin-bottom:0}}div.centered{display:flex;flex-direction:column;flex-wrap:wrap;align-items:center;justify-content:space-around;min-width:100%;margin:0 auto}div.flushleft,div.raggedright{display:flex;justify-content:flex-start}div.flushright,div.raggedbottom,div.raggedleft{display:flex;justify-content:flex-end}div.raggedbottom{flex-direction:column}div.content{line-height:1.4rem}div.content>p{margin:2.1rem 0}li>p{margin:.28rem 0}.icon{display:inline-block;-webkit-user-select:none;-moz-user-select:none;user-select:none;width:1rem;height:1rem;stroke-width:0;stroke:currentColor;fill:currentColor}h1,h2,h3,h4,h5,h6{font-family:Lucida Grande,Arial,Helvetica,sans-serif}h1{font-size:2rem;line-height:2rem;margin:1rem 0}h1,h2{color:#0f2f48}h2{font-size:1.5rem;margin:.8rem 0}h3,h4{margin:.67rem 0;color:#0f2f48}h3,h4,p{font-size:1rem}p{margin:.5rem 0}.titlepage{text-align:center}.titlepage h1{font-weight:400}b,strong{font-weight:700}dfn{font-style:italic}code,kbd,pre,samp{font-family:monospace,serif;font-size:1rem}pre{white-space:pre-wrap}q{quotes:"“" "”" "‘" "’"}small{font-size:80%}sub,sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}sup{top:-.5rem}sub{bottom:-.25rem}.mdseries,.textmf{font-weight:400}.bfseries,.textbf{font-weight:700}.rmfamily,.textrm{font-family:serif}.sffamily,.textsf{font-family:sans-serif}.texttt,.ttfamily{font-family:monospace}.textup,.upshape{text-transform:uppercase}.itshape,.textit{font-style:italic}.slshape,.textsl{font-style:oblique}.scshape,.textsc{font-variant:small-caps}small.tiny{font-size:x-small}small.scriptsize{font-size:smaller}small.footnotesize,small.small{font-size:small}.normalsize{font-size:normal}big.large{font-size:large}big.xlarge,big.xxlarge{font-size:x-large}big.huge,big.xhuge{font-size:xx-large}.rm{font-family:serif;font-style:normal;font-weight:400}.cal,.it{font-style:italic}.cal,.it,.sl{font-family:serif;font-weight:400}.sl{font-style:oblique}.bf{font-family:serif;font-weight:700}.bf,.tt{font-style:normal}.tt{font-family:monospace;font-weight:400}.underbar{text-decoration:underline}.fbox,.framebox{border:1px solid #000;padding:1px 3px}.quotation p,.quote p,.verse p{margin-top:0;margin-bottom:.5em}hr{color:#000}dd{margin-left:3rem}dd p{padding:0;margin:0 0 1rem}ul.breadcrumbs{margin:0;padding:0;list-style:none;font-size:small}ul.breadcrumbs li{display:inline}ul.breadcrumbs a{text-decoration:none;color:#396282}li.crumb:after{content:" / "}div.equation{display:flex;align-items:center;margin:1rem}div.equation span.equation_label{margin-right:1rem}div.equation span.equation_label:before{content:"("}div.equation span.equation_label:after{content:")"}div.equation div.equation_content{margin:auto}figure{display:flex;flex-direction:column;vertical-align:bottom;overflow:auto}figure img{display:block;margin:0 auto}figcaption{display:block;text-align:center;margin-bottom:.1rem}span.caption_ref,span.caption_title,span.subcaption{font-weight:700}span.caption_ref:after{content:":"}span.subref:after{content:")"}footer#footnotes{clear:both;padding-top:1rem;padding-left:1rem;border-color:gray;border-top:1px solid}footer#footnotes h1{font-size:1.5rem;margin:0;margin-bottom:.5rem;color:#000}a.footnote{text-decoration:none}a.footnote sup:after{content:"]"}a.footnote sup:before{content:"["}body>header{background:linear-gradient(180deg,#6696bb 0,#396282);color:#fff;text-shadow:1px 2px 0 rgba(0,0,0,.8);display:flex;align-items:center;padding:.5rem}svg#toc-toggle{width:1.125rem;height:1.125rem;margin-right:.5rem}h1#doc_title{color:#fff;font-size:1.5rem;margin:auto}#doc_title a,#doc_title a:visited{text-decoration:none;color:#fff}.theindex li{list-style-type:none}nav.index-groups{margin-bottom:1rem}a[class^=index-group]{text-decoration:none}a.index-group:after{content:" |"}section.theindex{display:flex;flex-direction:row;flex-wrap:wrap;margin-top:1rem}section.theindex h2{min-width:100%;margin:1rem 0 .5rem}ul.index-column{min-width:100%}@media (min-width:1024px){ul.index-column{min-width:auto}}nav.prev_up_next a.index{font-size:small;padding-left:.5rem;padding-right:.5rem}dl.description dt{font-weight:700}table.list{margin-left:15px;margin-top:1em;margin-bottom:1em}table.list td{padding-right:5px}div.displaymath{overflow:auto}a.eqref:before{content:"("}a.eqref:after{content:")"}nav.prev_up_next{position:fixed;z-index:1;right:0;bottom:0;display:flex;height:2.5rem;background:linear-gradient(180deg,#6696bb 0,#396282)}nav.prev_up_next a{font-size:150%;margin:auto;padding:.5rem 1rem;text-decoration:none;color:#fff;text-shadow:1px 2px 0 rgba(0,0,0,.8)}hspace,vspace{margin:0;padding:0}div.bigskip{margin-bottom:4rem}div.medskip{margin:0;padding:0;margin-bottom:2rem}div.bigskip{margin:0;padding:0;margin-bottom:1rem}.tabular{border-collapse:collapse;color:#0a0a14;background-color:#e8e8e8;width:auto}.tabular td,.tabular th{vertical-align:baseline;text-align:left;padding:.3em .6em;empty-cells:show}td p:first-child,th p:first-child{margin-top:0;margin-bottom:0}td p,th p{margin-top:1em;margin-bottom:0}@keyframes a{0%{background-color:#c2c2c2}to{background-color:#e8e8e8}}div[class$=_thmwrapper]{margin-top:1rem}div[class$=_thmwrapper]:target{animation:a 1s ease}div[class$=_thmheading]{display:flex;font-weight:700;line-height:150%}span[class$=_thmtitle]:before{content:"("}span[class$=_thmtitle]:after{content:")"}div[class$=_thmcontent]{font-weight:400;margin-left:1rem;padding-top:.14rem;padding-left:1rem}span[class$=_thmlabel]{margin-left:.5rem;margin-right:.5rem}div[class$=proof_heading]{font-weight:700;line-height:120%;cursor:pointer}div.proof_content{font-weight:400;margin-left:1rem;padding-top:.5rem;padding-left:1rem}span.expand-proof{font-size:80%}div.hilite{animation:a 1s ease}span.qed{float:right}button.modal{border:none;text-align:center;text-decoration:none;background:transparent;cursor:pointer;padding:0}div.modal-container{position:fixed;z-index:2;top:0;left:0;display:none;width:100%;height:100%}div.modal-content{font-weight:400;overflow:auto;margin:auto;vertical-align:middle;border:1px solid #497da5;border-radius:5px;background-color:#fff;box-shadow:0 4px 8px 0 rgba(0,0,0,.2),0 6px 20px 0 rgba(0,0,0,.19)}div.modal-content header{position:relative;background:linear-gradient(180deg,#6696bb 0,#396282);color:#fff;text-shadow:1px 2px 0 rgba(0,0,0,.8);display:flex;flex-direction:row;min-height:1rem;min-width:100%;text-align:center;vertical-align:middle;padding:0 .5rem;justify-content:space-between}div.modal-content header button.closebtn{font-size:120%;font-weight:700;background:Transparent;border:none;margin:auto 0;padding-right:.3rem;text-decoration:none;color:#fff;cursor:pointer}div.modal-content header h1{font-size:120%;margin:auto 0;padding:.2rem;color:#fff}div.modal-content a{text-decoration:none}div.modal-content ul{padding:1rem;list-style:none}div.modal-content li{padding-left:.5rem}a.icon{text-decoration:none;color:#0a0a14;border:none;background-color:Transparent}div[class$=_thmheading]:hover div.thm_header_hidden_extras{display:inline-block}div.thm_header_hidden_extras{display:none}ul.quizz{display:flex;flex-direction:column;list-style:circle!important}ul.quizz li{display:flex;padding:.5rem;flex-direction:row;min-width:100%;min-height:3rem;flex-grow:1;align-items:center;justify-content:space-between}ul.quizz li.active-qright{background-color:green}ul.quizz li.active-qwrong{background-color:red}ul.quizz svg.icon{display:none;padding-right:.5rem;width:2rem;height:2rem}.tikzcd{overflow:auto}.tikzcd,.tikzpicture{display:block;margin:.5rem auto}.local_toc ul{padding-left:1rem;list-style:none}.local_toc ul a{text-decoration:none;color:#0a0a14}.local_toc ul li{padding:.2rem 0}nav.toc{flex-shrink:0;display:none;width:100%;overflow-x:hidden;overflow-y:auto;flex-direction:column;margin-right:1rem;padding:0;padding-right:1rem;transition:left .5s ease;background-color:#6696bb;border-right:none}@media (min-width:1024px){nav.toc{display:flex;max-width:25ch}}nav.active{width:100%}.toc ul{min-width:100%;padding-left:0;list-style:none}.toc ul a{display:inline-block;max-width:90%;padding-top:.5rem;padding-right:.5rem;padding-bottom:.5rem;transition:all .1s ease;text-align:left;text-decoration:none;font-size:1.125rem;color:#fff;text-shadow:2px 2px 2px rgba(0,0,0,.8);flex-grow:1}.toc ul a:hover{transition:all .2s ease;background:#497da5}.toc ul li{display:flex;min-width:100%;align-items:center;flex-wrap:wrap;justify-content:space-between;background-color:#6696bb}.toc ul li.current{background-color:#89aecb;font-weight:400}.sub-toc-0 a{padding-left:.8rem}.sub-toc-1 a{padding-left:1.6rem}.sub-toc-2 a{padding-left:2.4rem}.sub-toc-3 a{padding-left:3.2rem}.sub-toc-4 a{padding-left:4rem}ul.sub-toc-1,ul.sub-toc-2,ul.sub-toc-3,ul.sub-toc-4{display:none}span.expand-toc{min-width:.7rem;width:.8rem;height:.8rem;padding:0;padding-right:.5rem;font-size:125%}span.expand-toc,svg.close-toc{cursor:pointer;text-align:center;color:#fff;background-color:Transparent}svg.close-toc{min-width:1.3rem;min-height:1.3rem;margin:.5rem;margin-left:auto;display:none}nav.active svg.close-toc{display:inline-block}ul.active{display:block}code.verb{font-family:monospace;font-style:normal;font-weight:400}pre.verbatim{margin:1rem 2rem;background-color:#dbdbdb;padding:.5rem} No newline at end of file | |||
There was a problem hiding this comment.
Stylelint-blocking patterns are committed in this generated stylesheet.
Line 1 contains multiple stylelint errors already reported (unknown selectors, vendor-prefixed selector, keyword-case mismatches, keyframe selector notation). Given the lint-hardening work in this PR, this is likely to block CI unless these generated theme assets are excluded or normalized before commit.
🧰 Tools
🪛 Stylelint (17.9.0)
[error] 1-1: Expected quotes around "Lucida Grande" (font-family-name-quotes)
(font-family-name-quotes)
[error] 1-1: Expected "to" to be "100%" (keyframe-selector-notation)
(keyframe-selector-notation)
[error] 1-1: Vendor-prefixed selector "::-moz-selection" (selector-no-vendor-prefix)
(selector-no-vendor-prefix)
[error] 1-1: Unknown type selector "hspace" (selector-type-no-unknown)
(selector-type-no-unknown)
[error] 1-1: Unknown type selector "vspace" (selector-type-no-unknown)
(selector-type-no-unknown)
[error] 1-1: Expected "currentColor" to be "currentcolor" (value-keyword-case)
(value-keyword-case)
[error] 1-1: Expected "currentColor" to be "currentcolor" (value-keyword-case)
(value-keyword-case)
[error] 1-1: Expected "Transparent" to be "transparent" (value-keyword-case)
(value-keyword-case)
[error] 1-1: Expected "Transparent" to be "transparent" (value-keyword-case)
(value-keyword-case)
[error] 1-1: Expected "Transparent" to be "transparent" (value-keyword-case)
(value-keyword-case)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@blueprint/web/styles/theme-blue.css` at line 1, The committed generated
stylesheet (starts with `@charset` "UTF-8"; and contains long concatenated
selectors like a,abbr,... and rules such as div.content, pre.verbatim) is
triggering stylelint errors; either exclude this generated asset from linting by
adding its filename pattern to .stylelintignore, or normalize it by prepending a
stylelint disable comment (e.g. /* stylelint-disable */) at the top and
re-generating so CI will pass; update the CI/lint configuration if necessary to
ensure other generated theme files follow the same ignore/disable approach.
| @@ -0,0 +1 @@ | |||
| @charset "UTF-8";a,abbr,acronym,address,applet,article,aside,audio,b,big,blockquote,body,canvas,caption,center,cite,code,dd,del,details,dfn,div,dl,dt,em,embed,fieldset,figcaption,figure,footer,form,h1,h2,h3,h4,h5,h6,header,hgroup,html,i,iframe,img,ins,kbd,label,legend,li,mark,menu,nav,object,ol,output,p,pre,q,ruby,s,samp,section,small,span,strike,strong,sub,summary,sup,table,tbody,td,tfoot,th,thead,time,tr,tt,u,ul,var,video{font:inherit;font-size:100%;margin:0;padding:0;border:0}article,aside,details,figcaption,figure,footer,header,hgroup,menu,nav,section{display:block}body{line-height:1;overflow-x:hidden;background:#f4f4f4}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:after,blockquote:before,q:after,q:before{content:"";content:none}table{border-spacing:0;border-collapse:collapse}.clear:after{font-size:0;display:block;visibility:hidden;clear:both;height:0;content:" "}.clear{display:inline-block}* html .clear{height:1%}.clear{display:block}*{box-sizing:border-box}hr{clear:both;border:none;outline:none}em{font-style:italic}a{text-decoration:underline}ul{list-style:disc}ol{list-style:decimal}ol,ul{font-size:14px;padding:0 0 0 33px}ol li,ul li{margin:0}blockquote{padding:0 15px 0 40px}table{font-size:13px;width:100%;margin:20px 0;background:#fff}table th{font-size:16px;font-weight:700}table tr td{padding:7px}::selection{color:#fff;background:#000}::-moz-selection{color:#fff;background:#000}body{height:100vh;margin:0;flex-direction:column;color:#24292e;background-color:#fff}body,div.wrapper{display:flex;overflow:hidden}div.wrapper{flex-grow:1}div.content-wrapper{max-width:75ch}@media (min-width:1024px){div.content-wrapper{margin-left:auto;margin-right:auto}}div.content{flex-grow:1;display:flex;flex-direction:column;overflow:auto;padding:.5rem;margin-bottom:2.5rem}@media (min-width:1024px){div.content{padding:1rem;margin-bottom:0}}div.centered{display:flex;flex-direction:column;flex-wrap:wrap;align-items:center;justify-content:space-around;min-width:100%;margin:0 auto}div.flushleft,div.raggedright{display:flex;justify-content:flex-start}div.flushright,div.raggedbottom,div.raggedleft{display:flex;justify-content:flex-end}div.raggedbottom{flex-direction:column}div.content{line-height:1.4rem}div.content>p{margin:2.1rem 0}li>p{margin:.28rem 0}.icon{display:inline-block;-webkit-user-select:none;-moz-user-select:none;user-select:none;width:1rem;height:1rem;stroke-width:0;stroke:currentColor;fill:currentColor}h1,h2,h3,h4,h5,h6{font-family:Lucida Grande,Arial,Helvetica,sans-serif}h1{font-size:2rem;line-height:2rem;margin:1rem 0}h1,h2{color:#24292e}h2{font-size:1.5rem;margin:.8rem 0}h3,h4{margin:.67rem 0;color:#24292e}h3,h4,p{font-size:1rem}p{margin:.5rem 0}.titlepage{text-align:center}.titlepage h1{font-weight:400}b,strong{font-weight:700}dfn{font-style:italic}code,kbd,pre,samp{font-family:monospace,serif;font-size:1rem}pre{white-space:pre-wrap}q{quotes:"“" "”" "‘" "’"}small{font-size:80%}sub,sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}sup{top:-.5rem}sub{bottom:-.25rem}.mdseries,.textmf{font-weight:400}.bfseries,.textbf{font-weight:700}.rmfamily,.textrm{font-family:serif}.sffamily,.textsf{font-family:sans-serif}.texttt,.ttfamily{font-family:monospace}.textup,.upshape{text-transform:uppercase}.itshape,.textit{font-style:italic}.slshape,.textsl{font-style:oblique}.scshape,.textsc{font-variant:small-caps}small.tiny{font-size:x-small}small.scriptsize{font-size:smaller}small.footnotesize,small.small{font-size:small}.normalsize{font-size:normal}big.large{font-size:large}big.xlarge,big.xxlarge{font-size:x-large}big.huge,big.xhuge{font-size:xx-large}.rm{font-family:serif;font-style:normal;font-weight:400}.cal,.it{font-style:italic}.cal,.it,.sl{font-family:serif;font-weight:400}.sl{font-style:oblique}.bf{font-family:serif;font-weight:700}.bf,.tt{font-style:normal}.tt{font-family:monospace;font-weight:400}.underbar{text-decoration:underline}.fbox,.framebox{border:1px solid #000;padding:1px 3px}.quotation p,.quote p,.verse p{margin-top:0;margin-bottom:.5em}hr{color:#000}dd{margin-left:3rem}dd p{padding:0;margin:0 0 1rem}ul.breadcrumbs{margin:0;padding:0;list-style:none;font-size:small}ul.breadcrumbs li{display:inline}ul.breadcrumbs a{text-decoration:none;color:#3a434b}li.crumb:after{content:" / "}div.equation{display:flex;align-items:center;margin:1rem}div.equation span.equation_label{margin-right:1rem}div.equation span.equation_label:before{content:"("}div.equation span.equation_label:after{content:")"}div.equation div.equation_content{margin:auto}figure{display:flex;flex-direction:column;vertical-align:bottom;overflow:auto}figure img{display:block;margin:0 auto}figcaption{display:block;text-align:center;margin-bottom:.1rem}span.caption_ref,span.caption_title,span.subcaption{font-weight:700}span.caption_ref:after{content:":"}span.subref:after{content:")"}footer#footnotes{clear:both;padding-top:1rem;padding-left:1rem;border-color:gray;border-top:1px solid}footer#footnotes h1{font-size:1.5rem;margin:0;margin-bottom:.5rem;color:#000}a.footnote{text-decoration:none}a.footnote sup:after{content:"]"}a.footnote sup:before{content:"["}body>header{background:#f2f2f2;color:#24292e;text-shadow:none;display:flex;align-items:center;padding:.5rem}svg#toc-toggle{width:1.125rem;height:1.125rem;margin-right:.5rem}h1#doc_title{color:#24292e;font-size:1.5rem;margin:auto}#doc_title a,#doc_title a:visited{text-decoration:none;color:#24292e}.theindex li{list-style-type:none}nav.index-groups{margin-bottom:1rem}a[class^=index-group]{text-decoration:none}a.index-group:after{content:" |"}section.theindex{display:flex;flex-direction:row;flex-wrap:wrap;margin-top:1rem}section.theindex h2{min-width:100%;margin:1rem 0 .5rem}ul.index-column{min-width:100%}@media (min-width:1024px){ul.index-column{min-width:auto}}nav.prev_up_next a.index{font-size:small;padding-left:.5rem;padding-right:.5rem}dl.description dt{font-weight:700}table.list{margin-left:15px;margin-top:1em;margin-bottom:1em}table.list td{padding-right:5px}div.displaymath{overflow:auto}a.eqref:before{content:"("}a.eqref:after{content:")"}nav.prev_up_next{position:fixed;z-index:1;right:0;bottom:0;display:flex;height:2.5rem;background:#f2f2f2}nav.prev_up_next a{font-size:150%;margin:auto;padding:.5rem 1rem;text-decoration:none;color:#24292e;text-shadow:none}hspace,vspace{margin:0;padding:0}div.bigskip{margin-bottom:4rem}div.medskip{margin:0;padding:0;margin-bottom:2rem}div.bigskip{margin:0;padding:0;margin-bottom:1rem}.tabular{border-collapse:collapse;color:#24292e;background-color:#fff;width:auto}.tabular td,.tabular th{vertical-align:baseline;text-align:left;padding:.3em .6em;empty-cells:show}td p:first-child,th p:first-child{margin-top:0;margin-bottom:0}td p,th p{margin-top:1em;margin-bottom:0}@keyframes a{0%{background-color:#d9d9d9}to{background-color:#fff}}div[class$=_thmwrapper]{margin-top:1rem}div[class$=_thmwrapper]:target{animation:a 1s ease}div[class$=_thmheading]{display:flex;font-weight:700;line-height:150%}span[class$=_thmtitle]:before{content:"("}span[class$=_thmtitle]:after{content:")"}div[class$=_thmcontent]{font-weight:400;margin-left:1rem;padding-top:.14rem;padding-left:1rem}span[class$=_thmlabel]{margin-left:.5rem;margin-right:.5rem}div[class$=proof_heading]{font-weight:700;line-height:120%;cursor:pointer}div.proof_content{font-weight:400;margin-left:1rem;padding-top:.5rem;padding-left:1rem}span.expand-proof{font-size:80%}div.hilite{animation:a 1s ease}span.qed{float:right}button.modal{border:none;text-align:center;text-decoration:none;background:transparent;cursor:pointer;padding:0}div.modal-container{position:fixed;z-index:2;top:0;left:0;display:none;width:100%;height:100%}div.modal-content{font-weight:400;overflow:auto;margin:auto;vertical-align:middle;border:1px solid #e6e6e6;border-radius:5px;background-color:#fff;box-shadow:0 4px 8px 0 rgba(0,0,0,.2),0 6px 20px 0 rgba(0,0,0,.19)}div.modal-content header{position:relative;background:#f2f2f2;color:#24292e;text-shadow:none;display:flex;flex-direction:row;min-height:1rem;min-width:100%;text-align:center;vertical-align:middle;padding:0 .5rem;justify-content:space-between}div.modal-content header button.closebtn{font-size:120%;font-weight:700;background:Transparent;border:none;margin:auto 0;padding-right:.3rem;text-decoration:none;color:#24292e;cursor:pointer}div.modal-content header h1{font-size:120%;margin:auto 0;padding:.2rem;color:#464f59}div.modal-content a{text-decoration:none}div.modal-content ul{padding:1rem;list-style:none}div.modal-content li{padding-left:.5rem}a.icon{text-decoration:none;color:#24292e;border:none;background-color:Transparent}div[class$=_thmheading]:hover div.thm_header_hidden_extras{display:inline-block}div.thm_header_hidden_extras{display:none}ul.quizz{display:flex;flex-direction:column;list-style:circle!important}ul.quizz li{display:flex;padding:.5rem;flex-direction:row;min-width:100%;min-height:3rem;flex-grow:1;align-items:center;justify-content:space-between}ul.quizz li.active-qright{background-color:green}ul.quizz li.active-qwrong{background-color:red}ul.quizz svg.icon{display:none;padding-right:.5rem;width:2rem;height:2rem}.tikzcd{overflow:auto}.tikzcd,.tikzpicture{display:block;margin:.5rem auto}.local_toc ul{padding-left:1rem;list-style:none}.local_toc ul a{text-decoration:none;color:#24292e}.local_toc ul li{padding:.2rem 0}nav.toc{flex-shrink:0;display:none;width:100%;overflow-x:hidden;overflow-y:auto;flex-direction:column;margin-right:1rem;padding:0;padding-right:1rem;transition:left .5s ease;background-color:#fff;border-right:1px solid #f2f2f2}@media (min-width:1024px){nav.toc{display:flex;max-width:25ch}}nav.active{width:100%}.toc ul{min-width:100%;padding-left:0;list-style:none}.toc ul a{display:inline-block;max-width:90%;padding-top:.5rem;padding-right:.5rem;padding-bottom:.5rem;transition:all .1s ease;text-align:left;text-decoration:none;font-size:1.125rem;color:#464f59;text-shadow:none;flex-grow:1}.toc ul a:hover{transition:all .2s ease;background:#e6e6e6}.toc ul li{display:flex;min-width:100%;align-items:center;flex-wrap:wrap;justify-content:space-between;background-color:#fff}.toc ul li.current{background-color:#fff;font-weight:700}.sub-toc-0 a{padding-left:.8rem}.sub-toc-1 a{padding-left:1.6rem}.sub-toc-2 a{padding-left:2.4rem}.sub-toc-3 a{padding-left:3.2rem}.sub-toc-4 a{padding-left:4rem}ul.sub-toc-1,ul.sub-toc-2,ul.sub-toc-3,ul.sub-toc-4{display:none}span.expand-toc{min-width:.7rem;width:.8rem;height:.8rem;padding:0;padding-right:.5rem;color:#5c6976;font-size:125%}span.expand-toc,svg.close-toc{cursor:pointer;text-align:center;background-color:Transparent}svg.close-toc{min-width:1.3rem;min-height:1.3rem;margin:.5rem;margin-left:auto;color:#464f59;display:none}nav.active svg.close-toc{display:inline-block}ul.active{display:block}code.verb{font-family:monospace;font-style:normal;font-weight:400}pre.verbatim{margin:1rem 2rem;background-color:#f2f2f2;padding:.5rem} No newline at end of file | |||
There was a problem hiding this comment.
Stylelint errors are present in the committed theme asset.
Line 1 currently violates configured stylelint rules (e.g., unknown selectors and keyword/casing conventions). If lint runs as a gate, this blocks merges. Either normalize this stylesheet to pass lint, or treat it as generated/vendor CSS and exclude it from stylelint scope consistently.
🧰 Tools
🪛 Stylelint (17.9.0)
[error] 1-1: Expected quotes around "Lucida Grande" (font-family-name-quotes)
(font-family-name-quotes)
[error] 1-1: Expected "to" to be "100%" (keyframe-selector-notation)
(keyframe-selector-notation)
[error] 1-1: Vendor-prefixed selector "::-moz-selection" (selector-no-vendor-prefix)
(selector-no-vendor-prefix)
[error] 1-1: Unknown type selector "hspace" (selector-type-no-unknown)
(selector-type-no-unknown)
[error] 1-1: Unknown type selector "vspace" (selector-type-no-unknown)
(selector-type-no-unknown)
[error] 1-1: Expected "currentColor" to be "currentcolor" (value-keyword-case)
(value-keyword-case)
[error] 1-1: Expected "currentColor" to be "currentcolor" (value-keyword-case)
(value-keyword-case)
[error] 1-1: Expected "Transparent" to be "transparent" (value-keyword-case)
(value-keyword-case)
[error] 1-1: Expected "Transparent" to be "transparent" (value-keyword-case)
(value-keyword-case)
[error] 1-1: Expected "Transparent" to be "transparent" (value-keyword-case)
(value-keyword-case)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@blueprint/web/styles/theme-white.css` at line 1, The committed theme asset
fails stylelint (Line 1) because the file begins with a concatenated selector
block after `@charset` ("@charset \"UTF-8\"; a,abbr,acronym,...") and contains
style patterns that violate project lint rules; fix by either (A) normalizing
the CSS so it passes lint: split the `@charset` onto its own line, reformat the
large selector list into valid, lowercased tokens and run stylelint autofix;
target the top-of-file token "@charset \"UTF-8\";" and the huge selector
"a,abbr,acronym,address,..." and adjust any keyword/casing to match rules, or
(B) treat as vendor/generated and exclude it from stylelint by adding an
exclusion (e.g., a pattern in stylelint config or a comment header like /*
stylelint-disable */) so lint gates no longer block the PR.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Blueprint structure
The blueprint documents the formalization structure including:
Status
\notready(deferred proofs)\leanokNext steps
Summary by CodeRabbit
New Features
Chores