Repository navigation
Configure native Cursor Cloud Lean environment and diagnostics - #2
Merged
Merged
Conversation
Th0rgal
marked this pull request as ready for review
October 2, 2026 15:56
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
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.
Cursor Cloud initially used its default image because master lacked environment configuration. This optional infrastructure PR provides the pinned Lean Docker environment for durable repository configuration. A supported saved-snapshot route has since passed native validation and no longer requires merging this PR for activation.
The Dockerfile installs Lean 4.31.0. Setup preserves dependency pins, verifies solc 0.8.34, compiles the import/specification, and installs pinned Lean MCP diagnostics. Install/start readiness checks reject the fallback image. Existing proofs and specifications are preserved here; proof removal remains on cursor/proof-sandbox.
Validation: final no-ref Build bld-20261002-91c2b8c1-a253-43db-a9d1-0b096a5ec6d1 succeeded. Fresh native run https://cursor.com/agents/bc-4239dce6-60c6-5cf1-b699-ddba174538d1 passed automatic startup, doctor, and real MCP diagnostic/goal checks. Cursor accepted the environment proposal; Save in the Environment panel was still pending at last observation.
Existing GPT-5.6-requested proof run: https://cursor.com/agents/bc-0a652130-5c98-50ca-b2c7-928e3ca00765. Its actual model and theorem result remain unverified because the parent connector is stuck in incompatible after a deployment disconnect. No duplicate test was launched. Exact IDs, receipts, activation instructions, and recovery limitations are recorded in check/CURSOR_CLOUD_TEST.md.
This PR remains draft and must not be merged without approval.