Feature/v0.1 docs package 2026 06 01#3
Merged
Conversation
…page draft) README leads with the two checked v0.1 endpoints (finite-class Hoeffding confidence sequence and the unit-interval finite-net Dudley bridge), a fast verification path, and an explicit non-claims list. The technical note covers the verified finite-class confidence sequences and the finite-net Dudley bridge. The page draft is route-ready for the TheoremPath site. Verified on this branch: lake build FormalSLT green; the two headline endpoints print axioms [propext, Classical.choice, Quot.sound].
📝 WalkthroughWalkthroughThis PR introduces a reusable finite-dyadic Dudley API (bundled net sequence and Dudley instance), constructors from totally-bounded spaces, concrete instantiations for Bool and Fin n with embedded Rademacher processes, finite-union bound variants, many example/checker files, and extensive documentation and a doc-anchor validation script. ChangesFinite Dyadic Dudley API and Concrete Instantiations
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Poem
🚥 Pre-merge checks | ✅ 3 | ❌ 2❌ Failed checks (1 warning, 1 inconclusive)
✅ Passed checks (3 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Warning Review ran into problems🔥 ProblemsStopped waiting for pipeline failures after 30000ms. One of your pipelines takes longer than our 30000ms fetch window to run, so review may not consider pipeline-failure results for inline comments if any failures occurred after the fetch window. Increase the timeout if you want to wait longer or run a Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/formalslt-v0.1-release-review-2026-06-01.md`:
- Around line 25-28: Replace all machine-specific absolute paths and local
branch names in the memo (e.g. the path string
"/private/tmp/formalslt-nonfinite-unit-interval", the branch identifier
"local/nonfinite-unit-interval-20260531", and user-specific script paths like
"/Users/robsneiderman/Desktop/AI4MATH/scripts/audit_public_writing.py") with
repository-relative paths or neutral placeholders; update references to scripts
to use a relative path from the repo root (or a configurable variable), or mark
the memo as explicitly local/private and remove these absolute paths, and ensure
the memo header (the "local release-candidate memo" phrasing) reflects whether
the file is intended for public commit so readers know to adjust paths for their
environment.
In `@docs/formalslt-v0.1-technical-note.md`:
- Around line 572-574: Replace the machine-specific absolute path with a
repo-relative path or a placeholder: update the command that invokes
audit_public_writing.py so it references the script as
./scripts/audit_public_writing.py (or <path-to-scripts>/audit_public_writing.py)
and keep the output target as docs/formalslt-v0.1-artifact-map-2026-06-01.md;
alternatively add a brief parenthetical note that users must adjust the path to
their environment. Ensure you edit the line containing audit_public_writing.py
in the docs/formalslt-v0.1-technical-note.md so it no longer contains
/Users/robsneiderman/... and instead uses the relative path or placeholder.
🪄 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: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: b07d37df-dd35-47c5-b8ec-437ad6bc5fbb
📒 Files selected for processing (38)
FormalSLT.leanFormalSLT/Covering/FiniteDiscreteDudley.leanFormalSLT/Covering/FiniteSubGaussianChaining.leanFormalSLT/Covering/TotalBoundedDudley.leanFormalSLT/Covering/TwoPointDudley.leanFormalSLT/Covering/UnitIntervalDudley.leanFormalSLT/Probability/FiniteUnionBound.leanFormalSLT/UniformConvergence.leanFormalSLT/VC/SampleComplexity.leanREADME.mddocs/anytime-spine-handoff-2026-06-01.mddocs/assumptions-and-nonclaims.mddocs/diagrams.mddocs/formalslt-goal6-dyadic-net-sequence-handoff-2026-06-01.mddocs/formalslt-goal7-second-dyadic-net-instantiation-2026-06-01.mddocs/formalslt-v0.1-artifact-map-2026-06-01.mddocs/formalslt-v0.1-quickstart.mddocs/formalslt-v0.1-release-review-2026-06-01.mddocs/formalslt-v0.1-technical-note.mddocs/proof-frontier-manifest.jsondocs/proof-frontier.mddocs/public-release-checklist.mddocs/related-work.mddocs/roadmap.mddocs/superpowers/plans/2026-06-01-finite-dyadic-net-sequence.mddocs/theorem-map.mddocs/theorempath-formalslt-v0.1-page-draft.mdxdocs/unit-interval-dudley.mddocs/verified-slt-program-outline.mdexamples/CheckFiniteDiscreteDudley.leanexamples/CheckFiniteUnionBound.leanexamples/CheckTotalBoundedDudley.leanexamples/CheckTwoPointDudley.leanexamples/CheckUniformConvergence.leanexamples/CheckUnitIntervalDudley.leanexamples/CheckV01Usability.leanscripts/check_doc_anchors.pyscripts/generate_proof_frontier_manifest.py
Comment on lines
+25
to
+28
| - Path: `/private/tmp/formalslt-nonfinite-unit-interval` | ||
| - Branch: `local/nonfinite-unit-interval-20260531` | ||
| - HEAD: run `git rev-parse HEAD` before citing a commit | ||
| - Author: `Rob Sneiderman <robbysneiderman@gmail.com>` |
There was a problem hiding this comment.
Machine-specific paths in a repository-committed document.
This memo contains several local filesystem paths that are specific to one developer's machine:
- Lines 25-26:
/private/tmp/formalslt-nonfinite-unit-intervaland branchlocal/nonfinite-unit-interval-20260531 - Lines 198, 572:
/Users/robsneiderman/Desktop/AI4MATH/scripts/audit_public_writing.py
If this document is being committed to the public repository (as indicated by the PR context), these paths will not work for other developers or CI environments. Consider either:
- Using relative paths from the repository root for scripts
- Moving this to a separate local/private documentation location if it's truly a local-only memo
- Adding a note that paths should be adjusted for the user's environment
The memo header states this is a "local release-candidate memo" (line 4), which suggests it might be internal-only, but its presence in the PR indicates it will be public.
Also applies to: 198-204, 572-574
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/formalslt-v0.1-release-review-2026-06-01.md` around lines 25 - 28,
Replace all machine-specific absolute paths and local branch names in the memo
(e.g. the path string "/private/tmp/formalslt-nonfinite-unit-interval", the
branch identifier "local/nonfinite-unit-interval-20260531", and user-specific
script paths like
"/Users/robsneiderman/Desktop/AI4MATH/scripts/audit_public_writing.py") with
repository-relative paths or neutral placeholders; update references to scripts
to use a relative path from the repo root (or a configurable variable), or mark
the memo as explicitly local/private and remove these absolute paths, and ensure
the memo header (the "local release-candidate memo" phrasing) reflects whether
the file is intended for public commit so readers know to adjust paths for their
environment.
Comment on lines
+572
to
+574
| python3 /Users/robsneiderman/Desktop/AI4MATH/scripts/audit_public_writing.py \ | ||
| docs/formalslt-v0.1-technical-note.md \ | ||
| docs/formalslt-v0.1-artifact-map-2026-06-01.md |
There was a problem hiding this comment.
Machine-specific absolute path in public documentation.
Line 572 contains an absolute path /Users/robsneiderman/Desktop/AI4MATH/scripts/audit_public_writing.py that is specific to one developer's machine. Since this technical note is being committed to the repository, this path should either be:
- Made relative to a repository root (if the script is part of the repo)
- Replaced with a placeholder like
<path-to-scripts>/audit_public_writing.py - Documented as an example that users should adjust for their environment
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/formalslt-v0.1-technical-note.md` around lines 572 - 574, Replace the
machine-specific absolute path with a repo-relative path or a placeholder:
update the command that invokes audit_public_writing.py so it references the
script as ./scripts/audit_public_writing.py (or
<path-to-scripts>/audit_public_writing.py) and keep the output target as
docs/formalslt-v0.1-artifact-map-2026-06-01.md; alternatively add a brief
parenthetical note that users must adjust the path to their environment. Ensure
you edit the line containing audit_public_writing.py in the
docs/formalslt-v0.1-technical-note.md so it no longer contains
/Users/robsneiderman/... and instead uses the relative path or placeholder.
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@CONTRIBUTING.md`:
- Line 10: The CONTRIBUTING.md currently gives mixed guidance about the default
branch: it allows `main` for public mirrors but later step still hardcodes
`release-candidate`; update the later instruction so it conditionally references
the default branch name instead of a hardcoded `release-candidate`. Locate the
step that instructs contributors to target or use `release-candidate` (search
for the literal "release-candidate") and change the wording to use a variable
phrasing like "the repository's default branch (e.g., `release-candidate` or
`main`)" or provide two conditional bullets, one for `main` and one for
`release-candidate`, so all references to branch target are consistent across
the document.
🪄 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: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 89076b2b-d0c1-4e47-8542-0355fc6ac709
📒 Files selected for processing (4)
CONTRIBUTING.mdREADME.mddocs/next-lane.mddocs/public-release-checklist.md
💤 Files with no reviewable changes (1)
- README.md
✅ Files skipped from review due to trivial changes (2)
- docs/next-lane.md
- docs/public-release-checklist.md
|
|
||
| - Open pull requests against the repository default branch. In the private | ||
| preview repo this is currently `release-candidate`; in a public showcase | ||
| preview repo this is currently `release-candidate`; in a public release |
There was a problem hiding this comment.
Resolve branch-target guidance conflict in this file.
Line 10 says the default branch can be main in public mirrors, but Line 73 still hardcodes release-candidate. Please make the later step conditional too, so contributors get one consistent instruction path.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@CONTRIBUTING.md` at line 10, The CONTRIBUTING.md currently gives mixed
guidance about the default branch: it allows `main` for public mirrors but later
step still hardcodes `release-candidate`; update the later instruction so it
conditionally references the default branch name instead of a hardcoded
`release-candidate`. Locate the step that instructs contributors to target or
use `release-candidate` (search for the literal "release-candidate") and change
the wording to use a variable phrasing like "the repository's default branch
(e.g., `release-candidate` or `main`)" or provide two conditional bullets, one
for `main` and one for `release-candidate`, so all references to branch target
are consistent across the document.
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 by CodeRabbit
New Features
Documentation
Examples & Tools