copra/agent/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/agent/dfs_hammer_policy_prompter.py,sha256=z0bA7djPHZ6oqQbnHAK6zXLp8_KPKT0lU8osVwKlTPU,3088
copra/agent/dfs_policy_prompter.py,sha256=aVqe19X1r_sKRWkZ9s9Hh8P-cXXBmXZauLjw4iGrens,35828
copra/agent/dfs_tree_search_with_stack.py,sha256=2wRSRvXEOLnHbA5HYy_xseGOJXoJr90ZpxU6baP4dVo,23491
copra/agent/gpt_guided_tree_search_policy.py,sha256=u3xtrgZ_3H-a4TlOBOEwP91pyKt2PPl7Y4BPx8E6EFM,10047
copra/agent/handle_have_tactic.py,sha256=FpEe7VPAvUQM4j5zvX3jU0c4oagToJ0kk4RmUvAd3rY,9886
copra/agent/human_policy.py,sha256=dfJNbXiqljidsHlhaG21dO5sZbKPN_gwLf-JNdP1wA4,3654
copra/agent/rate_limiter.py,sha256=1f3HRvHOE1XrUmDMz51TiWuYb1LJxulP8ygyMpfS0Sk,1694
copra/agent/simple_proof_agent.py,sha256=tMw4d7qvhUuCQexUh4sAnAunKxWwr_OzmUizO_FtpC4,6409
copra/baselines/gpt4/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/baselines/gpt4/few_shot_grammar.py,sha256=oVvPRvMUwVPFO_AKQBHRNcoZPm8jYszHB09syiP3HgI,23094
copra/baselines/gpt4/few_shot_policy.py,sha256=57J3fV2o2OJqFP2NLPIYoqZspODQQ-YE1Zl13FfURrY,9942
copra/baselines/gpt4/few_shot_policy_prompter.py,sha256=MSTL7INCGo7tWZQSFN7tuLAlkTVVxxKKdnsWV3whj8k,22008
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=N0m6-pgKfPFj7yNWCftemYzXmRvJWl2bcY94k7o9Shs,22051
copra/coq_ser_api/__init__.py,sha256=fHI4ZGgPPXKvWyv3_12ZlUBV22izjgnU4i4KtS-CgTg,7504
copra/coq_ser_api/contexts.py,sha256=8jMV6E4UaabxenEA6PVICXxOey5oXunUXdlE0QMhRWI,11213
copra/coq_ser_api/coq_agent.py,sha256=-GJ_5YvQ5Q1mZ0zTqMfWbgyGdaASGuQC0wMO1N1aRfs,17800
copra/coq_ser_api/coq_backend.py,sha256=H96ps0iE7foicq63RvQZ6s9c5CvEwFZhagBwpFC1aAw,2456
copra/coq_ser_api/coq_util.py,sha256=fo3xdrF_yij-4v-s0uJXg_zyNrQ6KPRrBRrTROCmAC8,32087
copra/coq_ser_api/example.py,sha256=2iyMv-xJRAlkN-vfGzyQD3pYAqmvpZR9MECOIF_gnCg,2340
copra/coq_ser_api/lsp_backend.py,sha256=u2v6hpOmrymISD9RZ517AOuuzLR3yRyc8nFCKlbReQk,15812
copra/coq_ser_api/py.typed,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/coq_ser_api/serapi_backend.py,sha256=eO55vWEMl4m-xkNeqz8Hv9_0GKxhHRlX2vxI7s8pBac,38242
copra/coq_ser_api/util.py,sha256=CiQyFl3NSqev-EpB2JXXpIueN6zldl02qqg7deJpFpw,4017
copra/coq_ser_api_old/__init__.py,sha256=zyb3QTZDpg1g5MkezFjlq-lwcOSdS_90fvTJ7eoluAA,104209
copra/coq_ser_api_old/contexts.py,sha256=zfxBzT1xJxTnCzy7nEmVRSHWMGpzprSPtsIRiEhamEc,5670
copra/coq_ser_api_old/util.py,sha256=CiQyFl3NSqev-EpB2JXXpIueN6zldl02qqg7deJpFpw,4017
copra/gpts/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/gpts/gpt_access.py,sha256=E3nOePQ3ZD8Rz3uenSJTr9k_QLmBlN1UR5QDectCEa8,15129
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/lean_server/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/lean_server/commands.py,sha256=mnmwAXPvVSW3hxYTiP27XjAcvpRSZWz-MprQ9OuXIM0,11678
copra/lean_server/lean3_search_tool.py,sha256=OCMrPLAjTFxksycR7Nzbjo8S1r_bhDpOW3Z5mAAa844,12601
copra/lean_server/lean4_repl_interface.py,sha256=M64baQ5z-aLGJSVYr7NPk4yrP-9gEgR9y73Hpd8Rc3E,6394
copra/lean_server/lean4_utils.py,sha256=rxEr3BxrxuTnBHwvB3P1DhhXNgtT4pGGgB-KI_Q79-0,10120
copra/lean_server/lean_cmd_server.py,sha256=Rd0ipZlfo9toG5Co37q_dmJgOrxyruSGM2o_K_jAT9c,3862
copra/lean_server/lean_context.py,sha256=R2rxgCP8Eb6WPTpZDjiD7btxpz_tIKgG2Pdo_HqZzjQ,2029
copra/lean_server/lean_sync_server.py,sha256=E7Mx0Ahs4JsQuTmQSl63exH0ShQRaS90uDRBFABHgYs,6264
copra/lean_server/lean_utils.py,sha256=R9Y5bSnoiB05l2TnC6V-I4wYozFimu29fYpHIOsADsE,5804
copra/lean_server/py.typed,sha256=8PjyZ1aVoQpRVvt71muvuq5qE-jTFZkK-GLHkhdebmc,26
copra/main/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/main/config.py,sha256=h8FSFVCSQHyqCfRnNg5yYytgI_XjwjrTILrA-juHpY8,10188
copra/main/eval_benchmark.py,sha256=hh5AGQ8wYdp_frbD070V9RFVfaXIUdVz-FQIYZqBDZc,42920
copra/main/stats.py,sha256=v1PxWMUl0rKKBu_QiLmDJzTzubuGX_FUONa7w-DKe3I,5532
copra/main/config/coq_experiments.yaml,sha256=1MfZnkA5_yKufekbXUrQutgEa9g_648Uvs2dnARQyVc,2545
copra/main/config/experiments.yaml,sha256=OpinOA1LitFNNUl86hWmxEqBb9tLYipI5GJwcEl8IEo,288
copra/main/config/lean4_simple_experiment.yaml,sha256=Yo6Aub3fBQu38S8TSWz---fZDSvCmMd--1nH1y8YudU,281
copra/main/config/miniF2F_lean4_imo_experiments.yaml,sha256=TCI5kChu4fdsTJHJXUqtyeKN1S5Av5bBlM6cAR1afaI,511
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_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/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=Qoi6zmynnQCefKoeAvgpH2PY-cjhSPVYdP1uxxGCOrM,744
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_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=hgyQGW4s8qJnanXg1SgGINqUOeVekDICAsCFgcrzaaY,854
copra/main/config/eval_settings/n_500_dfs_llemma_always_retrieve_no_ex.yaml,sha256=wFX9QqDyzN1GwejKg4TfX1WATgP0Qr7rh9JapMzWRmg,834
copra/main/config/eval_settings/n_500_dfs_morph_always_retrieve_no_ex.yaml,sha256=j48jYfc9xxiJ5Hbk0c1cksxzh64ZNongh22MqeqQaBc,841
copra/main/config/eval_settings/n_50_dfs_gpt35.yaml,sha256=8XUaSHDaRBZXlPW3V42Na-1PUKRZXVy0oECma9QzkCU,732
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=gtT44676WEtgYPngvW1S58Di5zUeKnmgPkBpbwQMtSI,881
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_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=ipJmAF4cVBfzaBhUDDWJB1RfDAv4xjlmKRsJWVecQ8w,190
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/prompt_generator/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
copra/prompt_generator/agent_grammar.py,sha256=OZ5467VCNrukdwqtBMA1DS5iYQu87_BrkgOPEtqMHF4,12213
copra/prompt_generator/dfs_agent_grammar.py,sha256=6Ghz9njw1q5avJMsdBR1IXWKCqVw7MO3zgNn17vZ0TE,4224
copra/prompt_generator/dfs_gpt_response_grammar.py,sha256=zGeS8Vw66yCea3X_GoVCNVcIhk75O1tukwDK3tHjIAU,16835
copra/prompt_generator/gpt_request_grammar.py,sha256=aq40xbsOh73bePDCZycD_tNOejOBQEUX-iCS6G_W6N0,9305
copra/prompt_generator/interpreter.py,sha256=Ei_udxCVPD23O-HBEAU5gf9MB0HQVmR0k9fKnsEGzFs,2536
copra/prompt_generator/prompter.py,sha256=_219wdHHZi7JFMW5R59cD7fQBiN0iMy1zBBkf468CKE,735
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/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=uakFPticwVo-Xvl8yzUhQ35oC_nHXHFCsZKKSAEqAZA,457
copra_theorem_prover-1.1.1.dist-info/METADATA,sha256=8_KFMkjH-rfHWW6h-h0uUafzsjueI4dhAnLJP4IlwOw,4184
copra_theorem_prover-1.1.1.dist-info/WHEEL,sha256=qtCwoSJWgHk21S1Kb4ihdzI2rlJ1ZKaIurTj_ngOhyQ,87
copra_theorem_prover-1.1.1.dist-info/RECORD,,
