docs: add a getting-started guide, and link the two open feature-request issues - #20
Open
kondylidou wants to merge 3 commits into
Open
kondylidou wants to merge 3 commits into
kondylidou wants to merge 3 commits into
Conversation
kondylidou
force-pushed
the
docs/onboarding
branch
4 times, most recently
from
September 24, 2026 10:51
a7d82b5 to
673ca39
Compare
kondylidou
force-pushed
the
docs/onboarding
branch
from
September 24, 2026 10:56
673ca39 to
1debaed
Compare
The guide introduces Boole as the intermediate language of the CSLib code-reasoning platform, separates what exists today from what is expected to change, and covers build and test, a first program to write and break, how tests pin verifier output, and the shape of adding a feature. Four files under StrataBooleTest/FeatureRequests were never imported in StrataBooleTest.lean, so `lake test` never built them, and all four had rotted: - scalar_reduce: obligation labels embed byte offsets, which had drifted. - montgomery_loop_invariant: loop obligations have since been renamed. - sha256_compact_indexed: `Set bv W32` parses as two arguments, and the file declared `type Set`, which is now a reserved builtin. Renamed its abstract type to AbstractSet, since Boole's grammar exposes no Set type former. - seq_empty_literal: `Procedure.body` is now an `Imperative.Body`, so iterating it needs `getStructured`. All four are now imported, taking the suite from 278 to 282 targets. docs/BooleFeatureRequests.md points at #18 and #19 from the two entries they concern. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
kondylidou
force-pushed
the
docs/onboarding
branch
from
September 24, 2026 10:57
1debaed to
2094af5
Compare
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.
docs/onboarding.mdis a getting-started guide for new contributors. It introduces Boole as the intermediate language of the CSLib code-reasoning platform, separates what exists today from what is expected to change (more front ends, a shallow embedding, more provers), and covers the practical side: build and test, a first program to write and then deliberately break, how tests pin verifier output, the files that matter, and the shape of adding a feature. The example was run on this branch; it verifies as written, and the suggested edit makes it fail with the model the text quotes.Writing it turned up a gap. Four files under
StrataBooleTest/FeatureRequestswere never imported inStrataBooleTest.lean, solake testnever built them, and all four had rotted:scalar_reduce: obligation labels embed byte offsets, which had drifted.montgomery_loop_invariant: loop obligations have since been renamed.sha256_compact_indexed:Set bv W32parses as two arguments, and the file declaredtype Set, which is now a reserved builtin. Its abstract type is renamed toAbstractSet, since Boole's grammar exposes noSettype former.seq_empty_literal:Procedure.bodyis now anImperative.Body, so iterating it needsgetStructured.All four are now imported, taking the suite from 278 to 282 targets.
docs/BooleFeatureRequests.mdpoints at #18 and #19 from the two entries they concern.