lean_dojo_v2/__init__.py,sha256=6tpWYe0197WsdS1FtzPR6fBXCMWBpP9-Eb4Y8ACDAGc,371
lean_dojo_v2/agent/__init__.py,sha256=ns_SmTnaEdJKiKoZvBeZ9dpiDwBoKW-yHARvEiHn9eg,515
lean_dojo_v2/agent/base_agent.py,sha256=Ap5Sdqi2-SLd9XTHXc560TGb7tXzaNq_sDUwfSaW-KM,4051
lean_dojo_v2/agent/external_agent.py,sha256=AzAVKWXPrkOJY8-SjFzFtiaf8tQ_Az3Oz_rEQ9FoXp4,969
lean_dojo_v2/agent/hf_agent.py,sha256=YSGUPlr1WR0WGbIYjatWqPVjZkDqvZYcoOc4o3Vbg1I,1969
lean_dojo_v2/agent/lean_agent.py,sha256=MNPMTfYAGlnfREEFA95QWaxOHiRZTmKcrCbNBTjsRm8,1644
lean_dojo_v2/external_api/ExternalAPI.lean,sha256=Cw_uwFhyO1cPMevxC7GVF-n7EfbSJ5uxxncyMLf1GnM,266
lean_dojo_v2/external_api/LeanCopilot.lean,sha256=efttcVbU2imSJbDye5ybGJqEBl3XxRGEAzo-1KxCUAA,81
lean_dojo_v2/external_api/lakefile.lean,sha256=y-ust39W8CM7bhdXr5ziyh352HKFA9yAVtUFvvkv-RQ,241
lean_dojo_v2/external_api/LeanCopilot/Frontend.lean,sha256=LLPeGgNMM2bmPj5NoFc0k3C6813lJ4uLAu1JHbqDhWk,3333
lean_dojo_v2/external_api/LeanCopilot/Models.lean,sha256=UpTMHZFrHy_tjVEeOIHd9s-JgDfq9FfpE4H9ZMqVaHc,71
lean_dojo_v2/external_api/LeanCopilot/Tactics.lean,sha256=jLvBIO451oZPhxAq_9tg2-ZQzmZHZK8H9h9Bty6FdyI,1449
lean_dojo_v2/external_api/LeanCopilot/Models/External.lean,sha256=4gzKiTAJlyrXP6NPZskZrUnAsxmKApzYEpWlFAvSOTA,5635
lean_dojo_v2/external_api/LeanCopilot/Models/Interface.lean,sha256=ys0pdlIEBtTrIy4UyZFAFwF_dRHCO0PtpsHXHE9cs_U,587
lean_dojo_v2/external_api/python/models.py,sha256=_gmxYxYjOvS5IERzPqWJ7imjmqyz6mZ2Q2917o-GByU,5640
lean_dojo_v2/external_api/python/server.py,sha256=k3DsKCu7jt37nEqSM5E-Sj6l4LRu51-1bGoWKnAXjfY,2503
lean_dojo_v2/external_api/python/external_models/__init__.py,sha256=WHCXrmz8GUbibJ6zxNYBGKtpUvIJ9VbjCqKiSlCffW8,212
lean_dojo_v2/external_api/python/external_models/claude_runner.py,sha256=ZslIDkIc_n3bDpaYi96IWWtpmVqkg1dJ9B7wJecAsz0,1283
lean_dojo_v2/external_api/python/external_models/external_parser.py,sha256=rneuH716rW-0cWbkMwMNyYK3ky8YbiHhjmPjZRroVs4,3714
lean_dojo_v2/external_api/python/external_models/gemini_runner.py,sha256=GomCdaITZojROrtYG9VYXB7KqBQXkKnLaybbH5v_Wyg,2199
lean_dojo_v2/external_api/python/external_models/hf_runner.py,sha256=bNseSzO1xl9PNZAofV6g8OmTRw6wro4osnMdMkfAj64,3316
lean_dojo_v2/external_api/python/external_models/oai_runner.py,sha256=1h2CU4I37yyEXNOvZm-z7kiCt11pAW4s5MQIe2S2AGk,2665
lean_dojo_v2/external_api/python/external_models/vllm_runner.py,sha256=dPzWDL2reFHcqf9ewjjDNGfbMDFO_YN8d_QiJdMPPbM,2714
lean_dojo_v2/lean_agent/__init__.py,sha256=cVwcSFcm_1tfHSVeQwNfLJud1PRf8hIdy6fQXxuDwoc,461
lean_dojo_v2/lean_agent/__main__.py,sha256=e3FoLrA97fLSoo_DzkNwtsfxDCuBlkaso_l4F-pZhOI,184
lean_dojo_v2/lean_agent/common.py,sha256=C0ivhvq3b9M-okz6JEKlKtO_8Qdy7_NsFZ8qDVgDV3s,15248
lean_dojo_v2/lean_agent/config.py,sha256=YfZBqLFMVO_J4co4HSncpNXDyLjCLa7rCRycCm8Xy0g,12709
lean_dojo_v2/lean_agent/database/__init__.py,sha256=YlCDzPUX1e8NIrz5Bq0xazur3DIH4cqd74WGKizHJFo,312
lean_dojo_v2/lean_agent/database/dynamic_database.py,sha256=Mqr6G5GFzUsAqch4vnRrDXlW80jzprQxobrTVWEA9ac,22443
lean_dojo_v2/lean_agent/database/models/__init__.py,sha256=DoT4ZB36a1gQuZI-rWWoSjyjGKUBLAtGl-kLkR4QJLU,284
lean_dojo_v2/lean_agent/database/models/annotations.py,sha256=rp-Tb8If3p8qcEyGNFEkUWIZuzhGgJ1tkX1R29uv_WA,3815
lean_dojo_v2/lean_agent/database/models/premises.py,sha256=LPhyTel_ho6acgBnr_FCy12qrjEFi5IFmISWYkRomBY,2319
lean_dojo_v2/lean_agent/database/models/repository.py,sha256=TjZqnwgCvOfHvs7hoOX3foaqCBSw6nd2fL8iTycecu4,10705
lean_dojo_v2/lean_agent/database/models/theorems.py,sha256=TMPdGXNOvdo3JFiaPWv0_6WdmJ1zINM3oEWotg0Nugg,3293
lean_dojo_v2/lean_agent/generator/__init__.py,sha256=afdBgqzRPwjVo14LmDFm0gKt-lMeccY9J-P0FdiQhZQ,182
lean_dojo_v2/lean_agent/generator/datamodule.py,sha256=rlRyOekc13uGD5_E70dQT7HF0oS6LYvbGM_hDsH0G9Q,8110
lean_dojo_v2/lean_agent/generator/main.py,sha256=0Z8-f0MTRMM-jMi3wg2HeNxY42WAK9QfolCWl_8nW2M,808
lean_dojo_v2/lean_agent/generator/model.py,sha256=i4KrKKGvwqn3YEjA8oAqzFKnFpLR0uVWTIMF10W1m9w,22749
lean_dojo_v2/lean_agent/generator/confs/cli_lean4_random.yaml,sha256=0QulfZb-_VW61lmE_RToLt72V3voc8bZBFxPohsEu1c,1570
lean_dojo_v2/lean_agent/prover/__init__.py,sha256=r4IIq0KpriYF9QLU7_SeF6fG7npYpLYY3T3gwlBcyqg,330
lean_dojo_v2/lean_agent/prover/proof_search.py,sha256=08OGBxOn3yuG9dHt_YZ5ejv0HFDhRcCxdvGkMJLTgG8,18187
lean_dojo_v2/lean_agent/prover/search_tree.py,sha256=OS_IDxz7LGz8Y5gvj2RIfHZ6e2l9DlmjmtekJ4NeQks,8884
lean_dojo_v2/lean_agent/retrieval/__init__.py,sha256=l60nWpXv3zb5uUeGww1mEcKp50HUyMsBEI8JlZ1kjDg,184
lean_dojo_v2/lean_agent/retrieval/datamodule.py,sha256=bUQo1b6SPN2rXLbMJZeqUMds56ciB6TnM5mcTseFPg0,14986
lean_dojo_v2/lean_agent/retrieval/main.py,sha256=3u0dNp3akIVUL5I1oOtXCaRAmvNc-q_J1r9RGhUN_30,2190
lean_dojo_v2/lean_agent/retrieval/model.py,sha256=yYVrlyoCqY9tUle8-lSel_3ITX7z0Xwht4a1CC6y9as,19224
lean_dojo_v2/lean_agent/retrieval/confs/cli_lean4_random.yaml,sha256=j6cmrtSfTrmr_vZpmdJkI_wctYgY47wuB4ryvxIqIK0,994
lean_dojo_v2/lean_dojo/__init__.py,sha256=zYJg1oV150ZOGijX-JvhE9zQKcnSOiUBVY5cG8pjFo4,738
lean_dojo_v2/lean_dojo/data_extraction/ExtractData.lean,sha256=304QjOIXFb4j8qxvwcVcf3Hvrwxp8JJY2crK04TV8co,17136
lean_dojo_v2/lean_dojo/data_extraction/ast.py,sha256=xhUGIocOMgIF9jwYDbBK0YPYPp-Flri9Qqd2jYwrlRE,50663
lean_dojo_v2/lean_dojo/data_extraction/cache.py,sha256=P1GGeaNrHlY5fD7Sln6sKr4rT-Q-0Kmv6_x6LJDIo9c,3128
lean_dojo_v2/lean_dojo/data_extraction/dataset.py,sha256=M-t5s_lEISfJyP4cY0XsUDPhSC5_ruKtRWmYO_FFDys,14191
lean_dojo_v2/lean_dojo/data_extraction/lean.py,sha256=xl79Lxs9LLscJPrtzqrnNUUHC1WP8unnvH-XrGfuD3E,29956
lean_dojo_v2/lean_dojo/data_extraction/trace.py,sha256=B3bg2gsR5pOH6uhZgS7iZs8RM8c7W5xk2sHoJaf5GCk,11407
lean_dojo_v2/lean_dojo/data_extraction/traced_data.py,sha256=BA-WLj7VqYiHuLX-A5FEpNndPUb_E8XtGlE-SzzV8G0,42254
lean_dojo_v2/lean_dojo/interaction/Lean4Repl.lean,sha256=OBm3wR3NGUE5MpVmUtvNlpqgYGX6XsRd-jBOytFAaAI,11223
lean_dojo_v2/lean_dojo/interaction/dojo.py,sha256=1wCFxU8fFQmYrXh-SkPEP8W_i5_rIP5Lzo_3ptL1K_0,17912
lean_dojo_v2/lean_dojo/interaction/parse_goals.py,sha256=HxmZGKnW-ewMUdJi4qQwPZ_kfN_gY3HSYqR7T_cQPGs,1771
lean_dojo_v2/lean_dojo/interaction/test.lean,sha256=0NKvO9mcURy7mXXYvLTUTBLUVaITN9E2xP1WYBFBoAw,229
lean_dojo_v2/prover/__init__.py,sha256=_qs18KcS2PdvWrzvD5mmDXqfXknPBgOgVZ90xT7t63A,288
lean_dojo_v2/prover/base_prover.py,sha256=3vyokXppLxAbW3wSqYpT5RP8GAljZEME66_0U-WOnRc,9273
lean_dojo_v2/prover/external_prover.py,sha256=idNvDkDcLL-9tdxKZaNGwkO5cyQ45L3jjZDgdtMNpsk,1140
lean_dojo_v2/prover/hf_prover.py,sha256=G-AeTKST2McZw9IbJDpKyRy-_eRnn461SwEtD14upWw,4437
lean_dojo_v2/prover/retrieval_prover.py,sha256=mi51Rmf9jWcZcr6g8DAR0lTTQ8R_FBwXBgnQAtYN8oA,2685
lean_dojo_v2/trainer/__init__.py,sha256=pfnTl2zvYkXtOu1mqfbgNtyImlGrNArF9TGQjMyF7iE,239
lean_dojo_v2/trainer/grpo_trainer.py,sha256=H28YYyWuPNYXnD5zyg7LUvjl7aOnyoyMI8CXwoqPeTQ,5508
lean_dojo_v2/trainer/retrieval_trainer.py,sha256=HZ9k3aNQkjNyzDEdIZOg_h85tA_Tm44-wW25t7XoPeM,7107
lean_dojo_v2/trainer/sft_trainer.py,sha256=wbhGRLE6_i-1gtL3g84SVZDxW03kknodt0MDLlsEJok,5526
lean_dojo_v2/utils/__init__.py,sha256=pE78oWaaT5FZFiI1Ldnq4dO21t1mo3B1RY-MKYNLXr8,382
lean_dojo_v2/utils/common.py,sha256=L_rxjltmLGhyjjk-aJCBxOxO6uqcNAigzXEQ_GRsnvQ,5274
lean_dojo_v2/utils/constants.py,sha256=gfsI6lGXT_kgT0RJusswXlzOjNQc9s6M2lAFbqlbfZY,11648
lean_dojo_v2/utils/difficulty.py,sha256=ggzwVHlxCqnpimi9pXb9sHGYQ3FkNYuMPUYEaWIXU-k,2828
lean_dojo_v2/utils/filesystem.py,sha256=TwTFjjLSJIjLKFAHF99nFXgR4YNCMpG9jyc-expX7tA,6957
lean_dojo_v2/utils/git.py,sha256=6AY2-Jbhems1TJC1--OCzUdf2Hdyighofm23KDpuDyI,14073
lean_dojo_v2/utils/lean.py,sha256=9fD0QszWsZ7gOU1Q1my1EWMFCyZdhTNrZ2cwFwuD1dM,5016
lean_dojo_v2/utils/repository.py,sha256=IX512mnDk5by1oZUh6jG5rxLyuZSR2uwXEkgt4HgSW4,1228
lean_dojo_v2-1.0.0.dist-info/licenses/LICENSE,sha256=xx0jnfkXJvxRnG63LTGOxlggYnIysveWIZ6H3PNdCrQ,11357
lean_dojo_v2-1.0.0.dist-info/METADATA,sha256=6pSQHcf0lisFrD8rMDLeohNVHeb-sylwtgSEeioku3A,3174
lean_dojo_v2-1.0.0.dist-info/WHEEL,sha256=_zCd3N1l69ArxyTb8rzEoP9TpbYXkqRFSNOD5OuxnTs,91
lean_dojo_v2-1.0.0.dist-info/top_level.txt,sha256=f7RRQ0hNuIhzS6ILLscRpCUqBk-OWVyZe0r2UdodWNY,13
lean_dojo_v2-1.0.0.dist-info/RECORD,,
