Docs: accuracy pass, OpenRouter story, remote-manifest documentation, hygiene#32
Merged
Conversation
README.md: - Add Project page link (GitHub Pages portfolio at cuuper22.github.io/Erdos) - Update provider story: OpenRouter recommended (OPENROUTER_API_KEY, default google/gemini-2.5-flash); direct Gemini SDK now an optional `gemini` extra - Recount tests: 320+ test functions across 14 test files (was stale 323/13) - Document manifest.remote.json as a sample remote-campaign format - Fix CI trigger wording (pushes and pull requests, not every push) Plan.md: add dated Status note at top separating shipped components (solver loop, validator, sandbox, environment manager, packager, GUI, CI) from aspirational ones (remote artifact submission, min_app_version enforcement, auto-update, process-level sandboxing, published installers). ASSESSMENT.md: fix broken test counts (test_bug_fix_demos.py has 16 tests, not 20; method total adjusted to match its own breakdown). examples/README.md: state that example .lean files are intentionally unsolved with `sorry` placeholders the solver fills in; list intermediate.lean and manifest.json; explain root manifest.json vs manifest.remote.json. manifest.remote.json: sharpen _note to say it is an unconsumed format sample referencing the un-vendored google-deepmind/formal-conjectures repo. .gitignore: ignore .coverage and .coverage.* coverage artifacts. All factual claims verified against the repo: pytest green (314 passed, 9 skipped), documented mock-mode and --setup commands run as described, all referenced file paths exist. https://claude.ai/code/session_01KAKnLjpFZ9oF74GNW9QNtN
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
2 participants
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.
What
Docs accuracy pass and repo hygiene, written to reflect the full batch landing together.
[gemini]extra), project-page link added, paths re-verified.manifest.remote.jsondocumented truthfully as the remote-campaign sample format.Plan.mdgains a dated status header (shipped vs aspirational);ASSESSMENT.mdfactual refs fixed only.examples/README.mdmatches the restored unsolved (sorry) example state..gitignore: runtime outputs (work dirs, solutions, coverage) covered.Part of the project-wide polish batch.
https://claude.ai/code/session_01KAKnLjpFZ9oF74GNW9QNtN
Generated by Claude Code