Skip to content

Add Lean 4 support#90

Open
RobertTLange wants to merge 77 commits intomainfrom
lean_support
Open

Add Lean 4 support#90
RobertTLange wants to merge 77 commits intomainfrom
lean_support

Conversation

@RobertTLange
Copy link
Collaborator

Summary

  • refresh Lean 4 support on top of current main
  • keep Lean-specific evaluation logic in examples/autoformalization
  • preserve current packaging, CLI, async runner, and provider refactors from main
  • add Lean language metadata, EVOLVE marker handling, and callable eval support for non-Python tasks

Why

PR #63 tracks Racemuis:lean_support, which cannot be repointed to SakanaAI:lean_support. This PR is the SakanaAI-hosted replacement branch for review and merge.

Testing

  • pytest tests/test_edit_lean.py tests/test_wrap_eval_parallel.py -q
  • ruff check tests/test_edit_lean.py shinka/core/wrap_eval.py shinka/utils/languages.py examples/autoformalization/evaluate.py examples/autoformalization/utils_lean.py

Context

  • supersedes the branch update attempt for Add Lean 4 support #63 by moving the refreshed branch into SakanaAI/ShinkaEvolve
  • Lean dependency availability was checked against current sources; the local pip index miss came from this machine using Python 3.9

RobertTLange and others added 30 commits September 25, 2025 06:38
fix: Fix database summary when patch_name metadata is missing
Fix packaging so pip install ships full shinka module tree
fix `apply_full.py` when the patch has incomplete markers
Doc explaining how to add suport for a local LLM and embedding model
docs: change repo name on the onboarding doc
add google gemini embeding model
Enhance docs, robustify wrap_eval, Visualization w/o API key
@RobertTLange RobertTLange mentioned this pull request Mar 13, 2026
3 tasks
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.