copra/agent/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/agent/dfs_hammer_policy_prompter.py,sha256=3UpeoC9RyrS_O8-9WbFDWqVcp90WvGS9TBRTLVM0xY0,3138
copra/agent/dfs_policy_prompter.py,sha256=ID_VNJmzAtQUtENldoDkwQQ2fTgw_qpIj4cjlOm_boQ,31148
copra/agent/dfs_tree_search_with_stack.py,sha256=etXkO5BLk4lBhbZtlVxc3HH1RUyWgkIRNRacM1wboFI,23549
copra/agent/gpt_guided_tree_search_policy.py,sha256=u3xtrgZ_3H-a4TlOBOEwP91pyKt2PPl7Y4BPx8E6EFM,10047
copra/agent/handle_have_tactic.py,sha256=QLASfTkgtAZhcu_wrKyfnsKiPiEIT8GKLCVvF4vdujM,11132
copra/agent/human_policy.py,sha256=q7N4xwWupfukzYCyF4nuCro3nYFHPuHQvsyi5Hl8JKI,3806
copra/agent/rate_limiter.py,sha256=1f3HRvHOE1XrUmDMz51TiWuYb1LJxulP8ygyMpfS0Sk,1694
copra/agent/simple_policy_prompter.py,sha256=UZXuy6AcldGMIw3hOp8FaT_lBdVS-WgMBwqZYgEUkSM,24567
copra/agent/simple_proof_agent.py,sha256=_lkw4M91Sv9Nlt3IPeHsVpBjjCoycktnSc4SWaowJ6s,8951
copra/agent/simple_string_policy_prompter.py,sha256=aw6_D53KtJ_HQ_VtWo5DNMO12eN99IoR9PATyOfc8UY,4593
copra/baselines/gpt4/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/baselines/gpt4/few_shot_grammar.py,sha256=xsyos82Indp736zHKcnV72-e4GKwLok-5uWijXMT5yE,27762
copra/baselines/gpt4/few_shot_policy.py,sha256=57J3fV2o2OJqFP2NLPIYoqZspODQQ-YE1Zl13FfURrY,9942
copra/baselines/gpt4/few_shot_policy_prompter.py,sha256=jJN9u-0pE5ThRNgPQfLhn3fjL5GT1zRHfKgKtjzoYsg,22251
copra/baselines/gpt4/hammer_policy_prompter.py,sha256=P1s4yjA9msjAI2wL526iCfNjoR1F7XvaDfTE9C0_54c,7013
copra/baselines/gpt4/informal_few_shot_grammar.py,sha256=buPkPBm9_HNpF6vMh03M3lJI5ITIm4gFS5_A8IWu4aY,11206
copra/baselines/gpt4/informal_few_shot_policy.py,sha256=nwnDys0SsqVn2VUXUFdKPvUny7Hr16GqnMP3xjmmBaA,7865
copra/baselines/gpt4/informal_few_shot_policy_prompter.py,sha256=yfh39xKGqdvSxhbFwYpKVA-pbzVGamLgIpOdbn3Z_l8,22056
copra/gpts/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/gpts/gpt_access.py,sha256=DqHYSQgnCC8aKP8saj69Fco7D3Wo8l0VcLlHJ-yUOYs,33372
copra/gpts/llama2_chat_format.py,sha256=HzqEot9BhgSPnSkQOdCyjkwMIGfhc8Y-BSwnshStWJY,8263
copra/gpts/llama_access.py,sha256=0XR25kIRBi8SWazlD-4BO71X6LP6qreLixINWiQgC-E,14363
copra/gpts/start_llama.sh,sha256=Nr4cPSUOIlITNExaZHT9g-FRLv9wYh67o63SfEv6JpA,1102
copra/main/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/main/checkpoint_manager.py,sha256=TvIofxcgtFhbUxq5_HGu7qtviHbFwmxDjz_IHi0Ypi8,6024
copra/main/config.py,sha256=lLg9j0Bb_ML5AeQ-poQDrh6sP2UiYXywOXUaIRh0nkc,12082
copra/main/eval_benchmark.py,sha256=iKMhlMatZ3grU7qWz9VRcv0vvJANLV-VQcEJs_eWvao,38146
copra/main/lemma_discovery.py,sha256=SIFwzrhMu-RNXNcg-hO5Jgjgp6LXgf-FP7pxCPsZGx8,6413
copra/main/parallel_execution.py,sha256=c1oBOa6TtNSRbWxMZ27_HVEi_Co6qGmhFimWmVT2yVo,4840
copra/main/parallel_theorem_execution.py,sha256=9uh14gk3yHIeYSUNV5EjJKMDZHSVsi2hPb48FtlZ-PE,6607
copra/main/policy_factory.py,sha256=w1PDDh9YCbsY1hSWQ50KLiM_TonmA1hRSdPGgk3G1k0,10577
copra/main/proof_execution.py,sha256=mjv6b-5LpDADxUhEzVwr_wMDH8wgUx1qTVdoY8qyKlw,10507
copra/main/run.py,sha256=jcwHLp_t_k3kPXf0g11D3sQnCafmgPi_sNE6_VUtqXM,6081
copra/main/stats.py,sha256=v1PxWMUl0rKKBu_QiLmDJzTzubuGX_FUONa7w-DKe3I,5532
copra/main/config/coq_experiments.yaml,sha256=C_qYJBdtbbjn7SItRKX10iVeq5Xhr-k578rOW3F7GaA,2581
copra/main/config/experiments.yaml,sha256=jSfqCdPmDghKNNCKuAm1cRC31PvYAb9zFYpKarm5NgY,303
copra/main/config/lean4_simple_experiment.yaml,sha256=Mr-ThlV_FkHNBlm8pTzHxgZkNo11kkDkgfrwo3gYHvg,302
copra/main/config/lean4_simple_experiment_few_shot.yaml,sha256=CO3Rf5x18C4VgDD0GiFAN1iZzBL0fmWxn5PyuwTz338,265
copra/main/config/lean4_simple_experiment_few_shot_kimina.yaml,sha256=1d4Yg_YkdTd5bfEc3y1snfxIfJOdEd2kr7T5vQTZS3I,267
copra/main/config/lean4_simple_experiment_open_source.yaml,sha256=C1FUd0OHjiN5eqWM8iks3UF5WesmTlafqSNrf_PzLXo,307
copra/main/config/miniF2F_lean4_easy_to_hard_gpt_oss.yaml,sha256=EWzpw2tFvgN-eX0c9tk6YgqbzVtDzkJQjbR3VJecm8c,621
copra/main/config/miniF2F_lean4_imo_experiments.yaml,sha256=TCI5kChu4fdsTJHJXUqtyeKN1S5Av5bBlM6cAR1afaI,511
copra/main/config/stack_machine_lean_experiments.yaml,sha256=qjnM2NnaWJpWwtoGzgtXoTuYRMB9jdtu1r2hdg4flwo,613
copra/main/config/benchmark/agent_proverbot_hard.yaml,sha256=_9js5KnLcfG4ltlSos12VRhnqyCdmz5PzEZpNaEHKBA,8389
copra/main/config/benchmark/compcert_118_subset.yaml,sha256=yHauQUtmphUtHXDsJM5yoDY55Jx6wTacvNEOdP-qDOo,4482
copra/main/config/benchmark/compcert_benchmark.yaml,sha256=6yYz3qYAbif4yBe412TcPYu43Vuy-ToOWkYMCJm1UWY,1167
copra/main/config/benchmark/compcert_benchmark_hard.yaml,sha256=-QHhSAPdDTOdUSXVJbJ7jd9USQzGKElGhsFtkGb4BcI,16183
copra/main/config/benchmark/compcert_benchmark_hard_1.yaml,sha256=Ju7KLNC85Ibjcy6ITiWdcxM7aAiSDuB8VQSySuQI06M,1667
copra/main/config/benchmark/compcert_benchmark_hard_2.yaml,sha256=Y9qVr7f3898-lhQF3jzaD3ZCF6mMQc3CVQsTopST4_c,816
copra/main/config/benchmark/compcert_benchmark_hard_3.yaml,sha256=tgJEpqx4oJH-Ww4Nk2f03hMPx2E1F1aL1SPaa2K-9JQ,3256
copra/main/config/benchmark/compcert_benchmark_hard_7_per_cent.yaml,sha256=GZXsWeCPyHQRuOh3KQWUrMRnVCGhMKzpN4A_8XF-mWw,2486
copra/main/config/benchmark/miniF2F_lean4_test.yaml,sha256=FSeHQ5QHF2RvWtdGK_EaP5bSfv9KhE1vdU0sDpqrRMk,309
copra/main/config/benchmark/miniF2F_lean4_test_easy_to_hard.yaml,sha256=xy_PEFqx2Q3_DedB7vdf-TdhxtYMVIL4tJieVlr2K6o,8215
copra/main/config/benchmark/miniF2F_lean4_test_imo.yaml,sha256=SzZ0bMOysavLkuGv_PlzWT_CgjMVwSOVWyF5-az_cAs,801
copra/main/config/benchmark/miniF2F_test.yaml,sha256=SUdQncXJ30h1LZ45Wmz0NQrTyBuvylCmIQMLobgtOrE,302
copra/main/config/benchmark/miniF2F_test_aime.yaml,sha256=tLlkAtYbsSXDLxNzTxUXXUt8ClP-4jnEuBsrtAH5X-A,649
copra/main/config/benchmark/miniF2F_test_algebra.yaml,sha256=Q6DmDwBZX31wQJULvhF0gVjhOMloso1fLI1lBP8QqOc,1209
copra/main/config/benchmark/miniF2F_test_amc12.yaml,sha256=LZ0X3CWjMFZCOzULEWri3KGhHoN4fpQITQ5BoImYwRM,1444
copra/main/config/benchmark/miniF2F_test_easy_to_hard.yaml,sha256=4NVrzE1EsRtkDbYXQg49LAmUcV3SwZ0e6AbThY8bO8E,8208
copra/main/config/benchmark/miniF2F_test_few_shot_hard.yaml,sha256=W_GUIDAS7alFN3uTPURMuEixaT6tq4-ILCb9SLQMlEw,7592
copra/main/config/benchmark/miniF2F_test_imo.yaml,sha256=VVNNKq7AADMm0UyUPm2DohzQNhtdbMQilX5dj3NWh0A,827
copra/main/config/benchmark/miniF2F_test_imo_isabelle.yaml,sha256=dU2SG2-gpgrVCgGWK058IVvbHzhVIMq9ulL0J7UgIIk,1363
copra/main/config/benchmark/miniF2F_test_induction.yaml,sha256=9kBUKJXZSKDiTtMJKJDvPM92f0LGV7CIKQXf8aN8D-o,626
copra/main/config/benchmark/miniF2F_test_isabelle.yaml,sha256=_3K75gwOTYn1oOc6Ya1tyqzpVVrVov6-kIwP8bIs_d8,15036
copra/main/config/benchmark/miniF2F_test_isabelle_easy_to_hard.yaml,sha256=yx1S__ofkf8SzlVvG1I_Q8NNiAAn2mYzBxdHah8Sg08,15049
copra/main/config/benchmark/miniF2F_test_mathd_algebra.yaml,sha256=RVP9vygleL0RVeXPMk7QHq53SeHkKAq9H5Op6X_Twyw,2405
copra/main/config/benchmark/miniF2F_test_mathd_algebra_hard.yaml,sha256=Pp5lhSibhcKJt5RiAlHwQoe9GTJUhgj7a1Fy2MuS0LM,2111
copra/main/config/benchmark/miniF2F_test_mathd_numbertheory.yaml,sha256=PZHQcaVVT8o1YyucHnqtK_3NgXlgIVSRDs-aGuXniZM,2408
copra/main/config/benchmark/miniF2F_test_numbertheory.yaml,sha256=HejMgDRqhr5CjO9Z8BY66vjqM9Yo7tDxJraaHnBVo-U,698
copra/main/config/benchmark/miniF2F_test_proved_in_lean.yaml,sha256=JdJanisgYqe72E2RgZxuZHC7v1bg_R4c70BelYUFckk,4643
copra/main/config/benchmark/mini_miniF2F_test.yaml,sha256=xyb_jkWMtyfZyBvYe6lQ-wY27-5JPW2iwe0btcamtTU,1456
copra/main/config/benchmark/mini_miniF2F_test_isabelle.yaml,sha256=RFPppXugagUUIUQlKnyOxZxD2JQIV2GCDb9d79BUu4E,2485
copra/main/config/benchmark/minicompcert_benchmark_1.yaml,sha256=rIPEKfBjzOIINVdkpm8PRQhICWIjXYixHqIWnBAtQG4,496
copra/main/config/benchmark/proverbot_hard.yaml,sha256=O15wWxGi_1NqHptMHsDNhX9CgLbSfjZTAKPPTZucKAY,3116
copra/main/config/benchmark/re_prover.yaml,sha256=G1Bh8HLdRLB2FncCpSIQk1k8H4kNmmou1YnPc1Lc5do,1992
copra/main/config/benchmark/re_prover_hard.yaml,sha256=ofMOaf0pv-Op0qdXPrlXww7JcKweW3aF1iMI-VsXkMM,1206
copra/main/config/benchmark/re_prover_very_hard.yaml,sha256=1223tuC0ol5d3q9143DsrHZbmS862s2Rggult_h-AQU,617
copra/main/config/benchmark/reprover_with_retrieval.yaml,sha256=8Q-y_BasSDeLd3Gyqs573qn6EP7JAwBpqXHj52XqjvM,2240
copra/main/config/benchmark/reprover_with_retrieval_hard.yaml,sha256=1YNC2Rb57lShuKkrtGFR3TIUfWdkukT2-JiwItK3yh0,901
copra/main/config/benchmark/reprover_with_retrieval_neg.yaml,sha256=CsBOArbvK285dX1__DpobmVRDbkZjnNPBKpyD-YNM5g,6285
copra/main/config/benchmark/simple_benchmark_1.yaml,sha256=Ol33KlnXnsXpEFaCeeDs0hhC-yw8OtGMwgnXNul0ILQ,828
copra/main/config/benchmark/simple_benchmark_8.yaml,sha256=TGu0i2nyv_8gD6yUsB9zv9WqwbWltGfpi1_RF70msuQ,1305
copra/main/config/benchmark/simple_benchmark_9.yaml,sha256=tM5SfEa4cD6FE8rl-oYCWgi_wLNXxPfVtOhsBgQ9Z8o,1930
copra/main/config/benchmark/simple_benchmark_isabelle.yaml,sha256=3_ZFHnhPKxMWWSziYLGWhj5qvx8s5PyRPGq77GL48sw,341
copra/main/config/benchmark/simple_benchmark_lean.yaml,sha256=lX41Uu5T1tjM1Ec749F-NCql9gEOcsTmuRm49YbUamM,538
copra/main/config/benchmark/simple_benchmark_lean4.yaml,sha256=NjDt35565xXcKhjPNcO6E_BsfAhlfnD0VSmeKso7RuQ,379
copra/main/config/benchmark/stack_machine.yaml,sha256=dtqEs2q38Qzfyywvbct1TBupASxAF3Z6IKihpNEoY5s,303
copra/main/config/benchmark/stack_machine_hard.yaml,sha256=MyqJtmQf6q2CzS6TbKHJZi7RvtPtXdnkxspF9C3XUl8,362
copra/main/config/benchmark/stack_machine_lean_hard.yaml,sha256=FTN-n771ZSY5NjBSYOupJmFJnO-gFyZPk4bj-3_9Mp8,417
copra/main/config/env_settings/bm25_retrieval.yaml,sha256=QJ7X2Di82atJ5rnCSm06B6gkH7pw5yvNxHEbhfccshg,45
copra/main/config/env_settings/bm25_retrieval_no_dfns.yaml,sha256=NPo-e989ztHdouLivnhrm66shkuhDh4Pomd8joFbGBY,61
copra/main/config/env_settings/bm25_retrieval_only_local_no_dfns.yaml,sha256=1yZiRn7280k2GeZmUAIvHudMNfunYyX_JImgUiJ2RQU,83
copra/main/config/env_settings/bm25_retrieval_with_print.yaml,sha256=7P_PBJzDt_w9fLFeac6h2-lwv2x7D32bbM6gdJc7Ywo,67
copra/main/config/env_settings/bm25_retrieval_with_print_only_local.yaml,sha256=l6bQhIt1Yr-1Q0SHS_EXHbF3ZyQUJOSiE6MBNNCX6qc,89
copra/main/config/env_settings/bm25_retrieval_with_print_only_local_no_dfns.yaml,sha256=WZEot3Q3GrdkS6T4N0p9njfGJGYP8d50rWmRHIVxMrk,105
copra/main/config/env_settings/no_re_rank.yaml,sha256=jThuIVufmn4PUwpElzb9zGmi8W9nqsV7ebwt77vRip8,47
copra/main/config/eval_settings/n_10_dfs_gpt35.yaml,sha256=Mv3ypvlb97kjw_HgnpTTN9vEhiN4YY5sHKYpqODAcqs,733
copra/main/config/eval_settings/n_10_dfs_gpt35_always_retrieve.yaml,sha256=XNFapKyf0c9vJmAqcieHQ-9eY_UYcOYpLWUntfkxES8,780
copra/main/config/eval_settings/n_120_dfs_gpt4_always_retrieve_no_ex.yaml,sha256=HS4eZJtha3vHPnS38rwwIIIjVe6zvtnceNJC38xh3YQ,810
copra/main/config/eval_settings/n_30_dfs_gpt35.yaml,sha256=tOtUi5ndYsysCMKoBO3FFo-1s1OgqSzBRoaud4aSR68,763
copra/main/config/eval_settings/n_30_dfs_gpt35_7_per_cent.yaml,sha256=sDDwXK8qUYUDo1PF1G1qNfO9Ea0tEW9nGFCmurJDFsw,775
copra/main/config/eval_settings/n_30_dfs_gpt35_always_retrieve_no_ex.yaml,sha256=WwksJ4BcLFQNze8TXinDAjRik7j4K1prWrHvfSLLFnc,817
copra/main/config/eval_settings/n_30_dfs_gpt35_h_7_per_cent.yaml,sha256=P9DYvHbUIAZ-oD11a_mFWdIeuBjADepZpExzZukXyM0,776
copra/main/config/eval_settings/n_30_dfs_gpt4.yaml,sha256=vM_zyvC930KqJGp0CMI9t4oiDr573FCmxHMUdEivqUA,759
copra/main/config/eval_settings/n_30_dfs_gpt4_7_per_cent.yaml,sha256=pdCCFnn5ob6jy644xuZiwSMvCU5hgnxfpr5PG15mh0c,771
copra/main/config/eval_settings/n_30_dfs_gpt4_always_retrieve.yaml,sha256=YcNJWSBG2hfRkWJUjPS2td3TkPkuRnLFERPKNWbLDzM,801
copra/main/config/eval_settings/n_30_dfs_gpt4_always_retrieve_no_ex.yaml,sha256=fJxdyGBssc5cLEtPcuIwDZilOOxoBnr4jxentfpSpYk,808
copra/main/config/eval_settings/n_3_hammer_no_retrieve_no_ex.yaml,sha256=vbyCkL0O2991vySOGM8NigADHZ4bIxQcXdcg7rD-26c,803
copra/main/config/eval_settings/n_40_dfs_gpt35_7_per_cent.yaml,sha256=3G_1reVknY0myW0pxDMn_cdC9I6z4HF2W7VHpmotRaM,775
copra/main/config/eval_settings/n_40_dfs_gpt4_7_per_cent.yaml,sha256=dWmScG2Awslz8oDvrDwu37T0T4rYr7aqWdgFW5AcCCE,771
copra/main/config/eval_settings/n_4_few_codellama.yaml,sha256=W5u0TfHCs7l2xor9ifAQJjjqF4WiMNUKEBIKVLvLsGE,766
copra/main/config/eval_settings/n_4_few_gpt35.yaml,sha256=xio8cQvq3M2Bv6hvco4y5js91Wk-9Ybn3CNUpA7TjAk,708
copra/main/config/eval_settings/n_4_few_gpt35_7_per_cent.yaml,sha256=10dJcF8NMl1dRotnoEI49pflPwIggXpMM-5uqfNwjDA,720
copra/main/config/eval_settings/n_4_few_gpt4.yaml,sha256=cApDCjJDDMlF-PPap30FcoDuQ5AI6q_u_JhbBOhUBIQ,705
copra/main/config/eval_settings/n_4_few_gpt4_7_per_cent.yaml,sha256=xm9cqG-X1dQ3k9MAqTyPwc8hQypgS2jUMnzUKU-1o8s,716
copra/main/config/eval_settings/n_4_few_gpt4_o.yaml,sha256=aRY4V6tDKwTe77KjNp7mygd55ilCHubyxIYbKBCt6w4,714
copra/main/config/eval_settings/n_4_few_gpt4_turbo.yaml,sha256=Qt45rOOSwThif2M07zAhEwb9LUNpwr6sUMLNYrx0g6k,730
copra/main/config/eval_settings/n_4_few_gpt5.yaml,sha256=RBbC1jcVwgSMAkBVZBhuqY3X9DcyC0mP2SxWhLK6W-Y,711
copra/main/config/eval_settings/n_4_few_kimina.yaml,sha256=pukhK7g4RK0C8p5PeivmikdwKbjtj70zzvGnIvkvx80,844
copra/main/config/eval_settings/n_4_informal_gpt35.yaml,sha256=eEAsGtI7BhCUoAHdKTGRwMEozF6YfKwh3YmUXrTXZdA,731
copra/main/config/eval_settings/n_4_informal_gpt4_turbo.yaml,sha256=EIqPcpresXY95Y9fHAKacRMLx9OIWFdkRXRWbby8eAM,751
copra/main/config/eval_settings/n_500_dfs_codellama_always_retrieve_no_ex.yaml,sha256=HkdzvdC6NyfufRLc2d6H7rGhYWgM_ST3bcqj9ZG0M3A,876
copra/main/config/eval_settings/n_500_dfs_llemma_always_retrieve_no_ex.yaml,sha256=k-7H6aqSdmECO1OXDrFHQNu6caElQkJ5HGcWkFHsT_c,856
copra/main/config/eval_settings/n_500_dfs_morph_always_retrieve_no_ex.yaml,sha256=BBcKAPx9wtbP7hMYYCo8m6bZ8VYMblDsdsbz0g6PfM4,863
copra/main/config/eval_settings/n_50_dfs_gpt35.yaml,sha256=8XUaSHDaRBZXlPW3V42Na-1PUKRZXVy0oECma9QzkCU,732
copra/main/config/eval_settings/n_60_dfs_bedrock_claude_3_7_no_retrieve_no_ex.yaml,sha256=myIen1se5X7x5hmMfG1HCqOQxAE9sza6EquLfZMbnBA,926
copra/main/config/eval_settings/n_60_dfs_bedrock_deepseek_r1_no_retrieve_no_ex.yaml,sha256=IrM_5lt-gANHcyrJTHskpKWS6gKPLBICh4bexfpktPM,902
copra/main/config/eval_settings/n_60_dfs_claude_3_7_no_retrieve_no_ex.yaml,sha256=bNA8hyMyZPaHQGBNv1lkThFXiT7luckpU01gAsyn47s,903
copra/main/config/eval_settings/n_60_dfs_gpt35_always_retrieve.yaml,sha256=enavOXGsDHyNt65IDiBvwuTEi6Gn8EZXfV_vbqHo4JE,810
copra/main/config/eval_settings/n_60_dfs_gpt35_always_retrieve_no_ex.yaml,sha256=wwV5zlei4IC9hlNAQJJ12VsuYLbQ7o87oy17qKPokSc,816
copra/main/config/eval_settings/n_60_dfs_gpt35_no_retrieve_no_ex.yaml,sha256=Wl5pmJSA54wuEvYoHcrdOse_BECJN1FRj2L56Dk2qSc,814
copra/main/config/eval_settings/n_60_dfs_gpt4_0314_always_retrieve_no_ex.yaml,sha256=0n3_f20K4tvLqb45MjWDVU0Ce_fn73m1w3sAIJWWe58,818
copra/main/config/eval_settings/n_60_dfs_gpt4_0314_no_retrieve_no_ex.yaml,sha256=XW1XB8pTBBcgSueMBGLtsvk6xcQYsIigd-JJVE4lMTI,815
copra/main/config/eval_settings/n_60_dfs_gpt4_0613_always_retrieve_no_ex.yaml,sha256=BatVDJ5q-f-WOw4qDonD2agpszpaehF7r2g_Eo9rvtQ,818
copra/main/config/eval_settings/n_60_dfs_gpt4_0613_no_retrieve_no_ex.yaml,sha256=ymSDswR4u09sD5T1NUuURHtabwnzrGc79cOcaT7Cgm4,815
copra/main/config/eval_settings/n_60_dfs_gpt4_128k_always_retrieve_no_ex.yaml,sha256=DhEdMwwzsNnN9o6RpP9682dvBT_izK0F0mnH6edDy5g,826
copra/main/config/eval_settings/n_60_dfs_gpt4_128k_no_retrieve_no_ex.yaml,sha256=baHJGxpGB_DYS8ySOIOJqAEYcz1Gcogt4rDHe_seaEs,823
copra/main/config/eval_settings/n_60_dfs_gpt4_always_retrieve.yaml,sha256=qhlGJL2vMsYOxi0YV9vfhb4dEVhBPxw-dcQDqf3J1fw,801
copra/main/config/eval_settings/n_60_dfs_gpt4_always_retrieve_no_ex.yaml,sha256=pYUQH33XteA4dTjOiiMpkxPzqiDMhXlLGFRv0zqgB6k,808
copra/main/config/eval_settings/n_60_dfs_gpt4_o3_mini_no_retrieve_no_ex.yaml,sha256=zdRgEjY7e2FoCjH1zVDYT1CLchEpJGrwzsTmzzhzBLQ,880
copra/main/config/eval_settings/n_60_dfs_gpt4_o_no_retrieve_no_ex.yaml,sha256=b3cdGwlI2AmvjWuQOLzxfuef_icjxwg6C5E8gp6fxgE,808
copra/main/config/eval_settings/n_60_dfs_gpt5_mini_no_retrieve_no_ex.yaml,sha256=Yx2QYwoI58DGxt0W02REXzQ0O5vrfQZhMG-HjYejtF0,710
copra/main/config/eval_settings/n_60_dfs_gpt_oss_20b_no_retrieve_no_ex.yaml,sha256=sCV69EBMZLJ9vryk7J3nRvtMt3UfJwTNsNzKVC3pZWI,731
copra/main/config/eval_settings/n_60_dfs_vllm_kimina_no_retrieve_no_ex.yaml,sha256=okyR8sUtZhXM0FepHeuOpRCclfbWt2xdEjXHoDTJ4_c,947
copra/main/config/eval_settings/n_60_hammer_no_retrieve_no_ex.yaml,sha256=yDZynKByWc_qEPHk_BrhyniKhxlEKAAvdf-LcwgZjTU,805
copra/main/config/prompt_settings/coq_dfs_always_retrieve.yaml,sha256=ETeFvgmN-OqXbN0eRrR8uS6XqoB3KrZpy6yH4WN914s,223
copra/main/config/prompt_settings/coq_dfs_always_retrieve_stack_machine.yaml,sha256=-EIDtSS_C2LvbTeatqmjXr8RDiM-xDFUUMVB__xGv8k,251
copra/main/config/prompt_settings/coq_dfs_no_retrieve.yaml,sha256=bcZLETQc2vTwQ8dK0eGmqte11VeoFIDgy-Ix0HWxzXA,211
copra/main/config/prompt_settings/coq_few_shot.yaml,sha256=FIgXANiTz6b6v3XHADguWni1RmvQFgftU9LxoJCjodg,148
copra/main/config/prompt_settings/coq_few_shot_no_ret.yaml,sha256=-6vCycoBpxZuG0E1eXls3NvEZ8e-AzJ4VV558RJzyps,169
copra/main/config/prompt_settings/few_shot_informal.yaml,sha256=XaU8dfMVnUikTzJhhpT4H9IAAfouL_doCn6x9aJp5SU,223
copra/main/config/prompt_settings/isabelle_dfs.yaml,sha256=sOjLkv9G9YA7BGRWWhh6_7lzJysqqwuQg4dVGN2X2to,190
copra/main/config/prompt_settings/isabelle_dfs_hammer.yaml,sha256=2J_YG9o5HaqJbzQ2FmWvRAMuVt6zYcK21a3nAH07Xdc,378
copra/main/config/prompt_settings/isabelle_dfs_informal.yaml,sha256=zlSUQVkSOq3byvNQgWKL-ukZRAfigkApph05vDGtwmA,233
copra/main/config/prompt_settings/isabelle_dfs_informal_gpt4_turbo.yaml,sha256=P9CwGBDWLYUnSR4HtYm8b7Md0xCh1Q--LemF8HEK4-o,321
copra/main/config/prompt_settings/isabelle_few_shot.yaml,sha256=vY1vmJPtUlZxE1CO15YPef6lAKRLTr1EYu4cWLynPLI,171
copra/main/config/prompt_settings/isabelle_few_shot_hammer.yaml,sha256=lyM-mUHeKumoqjuNbENn7LlcpLnRiOvm-NA1T12RibM,192
copra/main/config/prompt_settings/isabelle_few_shot_informal_to_formal.yaml,sha256=unPlGYAeEEuOaiNlZ_U3-_lE5tmzLIUGZbhxn49dkoE,228
copra/main/config/prompt_settings/isabelle_few_shot_informal_to_formal_gpt4_turbo.yaml,sha256=wNKDRG35c-5_CR1fK7XJBKKRDMYKw3GRxywxeFUrqgg,336
copra/main/config/prompt_settings/lean4_dfs.yaml,sha256=aQrovbhcbGQDJQ1255uADY9t-ORW1yOTNLSRMXyiVqg,192
copra/main/config/prompt_settings/lean4_dfs_stack_machine.yaml,sha256=xVt76WnFr7-dtX8Dyjb_aTjJQXcMf_El3fA2DIi_HN8,295
copra/main/config/prompt_settings/lean4_few_shot.yaml,sha256=nX14nsWylLpA9BurQoqYK76hTtIF51PHjxkTaxnowS8,170
copra/main/config/prompt_settings/lean_dfs.yaml,sha256=D-eS42n6AECqe9B6Dg-D-tE4tdC648vTsPzdwCbivMA,177
copra/main/config/prompt_settings/lean_dfs_informal.yaml,sha256=GAvZFNtVywMzNZCUm55F_ljCawgOqKRqPUBbVnT336o,213
copra/main/config/prompt_settings/lean_dfs_informal_gpt4_turbo.yaml,sha256=1ByKJxahQDEyWssVtFNOUPTKDl0lR42U1TqYgWOrXzA,284
copra/main/config/prompt_settings/lean_dfs_retrieval.yaml,sha256=Ken0v-zzyHIiNFofRHmDxBrWxEDELc8lYlWqbuQq6AQ,196
copra/main/config/prompt_settings/lean_few_shot.yaml,sha256=LliRv6TzKrTIQ6sXllsHRHwkRCV8T7EZAx-cYZvARjI,159
copra/main/config/prompt_settings/lean_few_shot_informal.yaml,sha256=nC1RIezrvmmYQCFJJ3ZgZyb9b2SrhuZkBdHiUw2y3l0,186
copra/main/config/prompt_settings/lean_few_shot_informal_miniF2F_test.yaml,sha256=2wTLXGpiCN4sYKgbuJ0m0ZDza-k2QnijgvBM_iL1kG8,237
copra/main/config/prompt_settings/lean_few_shot_informal_to_formal.yaml,sha256=6XxBhczDX-ebBFztYBlEUBlTpzBth_5iDt2Yv4PMerA,216
copra/main/config/prompt_settings/lean_few_shot_informal_to_formal_gpt35.yaml,sha256=1iNNi-1n2GsM4lwaNkqrKTsmEVI6VHKYR1oKPRki7yE,309
copra/main/config/prompt_settings/lean_few_shot_informal_to_formal_gpt4_turbo.yaml,sha256=RWizIrhNVqmz4_hJ8BZ64shyR4PsojZ26PXX4xdcso0,319
copra/main/config/prompt_settings/lean_few_shot_informal_to_formal_human.yaml,sha256=X5SODJN_JryB_uEdX1B8pcvnrPF0Masz8keLgRzD1us,260
copra/main/config/prompt_settings/simplified_lean4_copra_math.yaml,sha256=9YXBGsJOgkqRYSS9uqyz2oUBVgc1ZMY9HG4gehV0EnI,241
copra/prompt_generator/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/prompt_generator/agent_grammar.py,sha256=jKspb1wr_lYjK-Ye07RaW0rahIUV9pV0MjagHmIF0Dc,11913
copra/prompt_generator/dfs_agent_grammar.py,sha256=jc8lPyesy9FsjPJzdqGqJ-I6gcT3_FiipIMV4E-OT7w,3925
copra/prompt_generator/dfs_gpt_response_grammar.py,sha256=reok46zwIuPgh_QstQ2YwN5tp1QgROX20EruHzBIQrI,17081
copra/prompt_generator/gpt_request_grammar.py,sha256=XBqamsHuNiIV5ntokZIQPvPpG6QF0Ip0e8TIZd9f-OA,10924
copra/prompt_generator/grammar_utils.py,sha256=aZqmHZ4GzOYQ50sgznQ6PdVvlSG4y3JvSe13-cXtIxc,1673
copra/prompt_generator/interpreter.py,sha256=r8xwpmtLUw6q-KjZupqvbF_Lg5XRIf6egIPyKHCwkmQ,3025
copra/prompt_generator/prompter.py,sha256=_219wdHHZi7JFMW5R59cD7fQBiN0iMy1zBBkf468CKE,735
copra/prompt_generator/simple_response_grammar.py,sha256=tLiK1kAw1XAZB0BRbrzWODiAiJ4wjzWjkFzvD3IgpJk,12145
copra/retrieval/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/retrieval/abstraction.py,sha256=XZP5yJfFmLnUCMwxAWTpR_yz_6TEgBM_GrVL-ET34vA,611
copra/retrieval/coq_bm25_reranker.py,sha256=S9QccqnPEBXbFppeHyqkemcA0FmzEXSsA6gz-vPKmdg,7031
copra/retrieval/isabelle_bm25_reranker.py,sha256=WEiFhzZ2l5xwKKlcGY0tcA3x6Mz1e0u8EXoDD0ce5so,3454
copra/retrieval/lean3_bm25_reranker.py,sha256=k8R_4DCSKprpblDL8JcUWE0IOMiDTCxmvYo6KcJFZNA,3913
copra/rl/q_tree.py,sha256=zBcu1FvEuOLWH5mPI7Drsm5GAhtBbdJQt-eWtL1fbz4,8421
copra/scripts/setup.sh,sha256=YZP7XrgXf4ToliPPImI59lUqJypK04TSsezFSlKZ698,7107
copra/simple/README.md,sha256=0hLYD-dov04Q8Dh8s-7QlcuXe0a_1i21oLQwr38oxPE,12326
copra/simple/__init__.py,sha256=OQGBEa9lZ-5TBby3pNPXP_GLyNc-wfUx8wLCPW2XW7U,548
copra/simple/__main__.py,sha256=PFAM5k66EeIPahJwkFlt4Y1zkYg49LIwpsiaW75-KtE,204
copra/simple/cli.py,sha256=xzREIH2JsJ4zRdP53pz5Byekkl5Z7lwQeMss3DHEPno,10165
copra/simple/core.py,sha256=e-Otli4but5u5v-dVfgnE8skn7xuOfXjSjPZgB-YAYg,14191
copra/tools/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/tools/basic_utils.py,sha256=XSCwEp43JYI6m1FaxOZlNxCBBv4S_suXvKNc1DwqPCU,6222
copra/tools/cache.py,sha256=3fwCmDgLbVh8rpTHBgxie76qec9hel2039X0SALKnKE,2709
copra/tools/informal_proof_repo.py,sha256=CEjeVosAsN9LvyhFWhdD1zpnjDAa8Vs4N9_s_veRyzU,1581
copra/tools/misc.py,sha256=6jZH1Cbkpu9dZgQCDsOAtufMp2_S00aQJUxphNamKoA,1583
copra/tools/vllm_tools.py,sha256=hUenzQvQ9UDZrNQ-F9UguL5Uw3Jnl5m5kqt4AWq4QO4,9713
copra_theorem_prover-1.3.0.dist-info/METADATA,sha256=K3Z65k48_QqbKHaoj0B9uMfGw4P3D0l4R687-lPeVjc,21508
copra_theorem_prover-1.3.0.dist-info/WHEEL,sha256=qtCwoSJWgHk21S1Kb4ihdzI2rlJ1ZKaIurTj_ngOhyQ,87
copra_theorem_prover-1.3.0.dist-info/entry_points.txt,sha256=69A6w5-dzyc0GgvdFlGlw-AoTS00XB3B2Ux68xHmuV4,60
copra_theorem_prover-1.3.0.dist-info/RECORD,,
