Skip to content

[codex] Make docs honest about current gates#488

Merged
TSavo merged 1 commit into
mainfrom
codex/docs-honest-bug-zoo
May 8, 2026
Merged

[codex] Make docs honest about current gates#488
TSavo merged 1 commit into
mainfrom
codex/docs-honest-bug-zoo

Conversation

@TSavo
Copy link
Copy Markdown
Owner

@TSavo TSavo commented May 8, 2026

Summary

  • Correct the public install story to use the source-built Rust CLI path and remove unpublished registry install snippets from current tutorials.
  • Narrow Bug Zoo docs so wild/ is described as metadata only until real upstream specimens are executable.
  • Clarify that local make ci is the Linux-profile gate, while full CI adds macOS Swift and per-kit verifier jobs.
  • Mark the first whitepaper install section as an early/future sketch instead of current CLI instructions.

Validation

  • make help
  • git diff --check
  • targeted rg check for stale install/conformance/wild overclaims

Summary by CodeRabbit

  • Documentation
    • Updated installation instructions across tutorials to build the CLI from source via the repository path.
    • Updated protocol status to v1.6.2 and clarified CI coverage across Linux and macOS profiles.
    • Expanded documentation on conformance gates, Bug Zoo specimen states, and CI workflow behavior.
    • Clarified that wild Bug Zoo specimens are tracked as metadata but not currently executed.

@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 8, 2026

Review Change Stack

Caution

Review failed

Pull request was closed or merged during review

Walkthrough

This pull request updates documentation across 26 files to reflect the current CI gate structure and source-based CLI distribution. The Linux-profile make ci gate is repositioned as the foundation for GitHub workflow jobs (macOS Swift minting and per-kit verifiers), and all installation instructions are changed from the published provekit crate to source builds via cargo install --path implementations/rust/provekit-cli.

Changes

CI Gate and Installation Documentation Update

Layer / File(s) Summary
Workflow and Make Configuration
.github/workflows/ci.yml, Makefile
Workflow comments clarify that Linux make ci serves as the base for macOS Swift and per-kit verifier jobs. Makefile documentation reframes make ci as a Linux-profile gate; mint coverage count adjusted from 10 to 11; determinism section references v1.6.2 catalog hash.
High-Level Reference and User Documentation
README.md, docs/contributing/build.md, docs/quickstart-extender.md, docs/how-to/bug-zoo.md, bug-zoo/README.md
README updates Status bullets for v1.6.2 protocol and canonical CLI source install; clarifies Bug Zoo wild specimens are metadata-only (not executed). Contributing and quickstart guides describe the Linux-profile gate and expanded make conformance checks (4→6 checks). Bug Zoo documentation specifies wildSightings entries are metadata without checked-in wild specimen execution.
Installation Instructions
docs/reference/per-language-status.md, docs/explanation/landing.md, docs/explanation/pitch.md, docs/explanation/product.md, docs/papers/01-whitepaper.md, docs/tutorials/c.md, docs/tutorials/cpp.md, docs/tutorials/csharp.md, docs/tutorials/go.md, docs/tutorials/java.md, docs/tutorials/python.md, docs/tutorials/ruby.md, docs/tutorials/rust.md, docs/tutorials/swift.md, docs/tutorials/typescript.md, docs/tutorials/zig.md
Canonical install command changed uniformly from cargo install provekit to cargo install --path implementations/rust/provekit-cli. Python, Ruby, TypeScript, and C# tutorials add explicit in-repo setup steps (virtual environments, bundle install, pnpm install). Rust tutorial troubleshooting updated to recommend the source-build install path.

Estimated code review effort

🎯 2 (Simple) | ⏱️ ~12 minutes

Possibly related PRs

  • TSavo/provekit#165: Introduced macOS Swift and per-kit verifier jobs; this PR documents those changes in comments and guides.
  • TSavo/provekit#480: Overlapping documentation updates to Makefile, README, and workflow for v1.6.2 and cicp framing.
  • TSavo/provekit#474: Related Makefile and conformance gate documentation changes (10→11 mint count, Linux-profile framing).

Poem

🐰 Hops through docs with CLI so bright,
From source to build, we've set things right!
Tutorials now point the way,
Install and verify—hooray!

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title clearly and specifically describes the main change: updating documentation to accurately reflect the current CI/conformance gates and installation procedures, which aligns with all file changes in the PR.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.

✏️ Tip: You can configure your own custom pre-merge checks in the settings.

✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch codex/docs-honest-bug-zoo

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands and usage tips.

@TSavo TSavo marked this pull request as ready for review May 8, 2026 13:40
Copilot AI review requested due to automatic review settings May 8, 2026 13:40
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 3ebf322686

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

# the TypeScript kit
pnpm add @provekit/kit @provekit/lift-zod @provekit/lift-class-validator @provekit/lift-fast-check
# the in-tree TypeScript kit
cd implementations/typescript && pnpm install --frozen-lockfile
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Keep TypeScript install step from changing cwd

Running the install block as written leaves the shell in implementations/typescript, so the next npx provekit-lift step runs against the in-repo kit workspace instead of the reader’s package. In the common walkthrough flow this produces a proof for the wrong sources (or no relevant mementos), which breaks the tutorial outcome; use a non-cwd-changing install form or explicitly tell readers to return to their project root before lifting.

Useful? React with 👍 / 👎.

Comment thread docs/tutorials/python.md
# the Python kit
pip install provekit
# the in-tree Python lift tests / adapter harness
cd implementations/python/provekit-lift-py-tests
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Keep Python install step from changing cwd

The new cd implementations/python/provekit-lift-py-tests line persists the working directory for subsequent commands in the same shell session, so provekit-lift-py in step 4 runs from the harness directory rather than the user’s Python package. That causes the tutorial to lift the wrong tree (or miss intended contracts), so the install instructions should avoid mutating cwd or explicitly instruct a cd back to the target project before lifting.

Useful? React with 👍 / 👎.

Comment thread docs/tutorials/ruby.md
provekit verify-protocol

gem install provekit
cd implementations/ruby && bundle install
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Keep Ruby install step from changing cwd

Because the install snippet now does cd implementations/ruby && bundle install, readers who execute the block line-by-line remain in the kit repo, so bundle exec provekit-lift-ruby runs there instead of in their gem. This makes the walkthrough produce proofs for the wrong codebase and undermines the advertised “your gem” flow; prefer an install command that does not change cwd or add an explicit step to return to the user project root.

Useful? React with 👍 / 👎.

@TSavo TSavo merged commit 68b4556 into main May 8, 2026
8 of 10 checks passed
@TSavo TSavo deleted the codex/docs-honest-bug-zoo branch May 8, 2026 13:46
@TSavo TSavo review requested due to automatic review settings May 8, 2026 14:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant