itp_interface/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/agent/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/agent/simple_proof_agent.py,sha256=9dWwimFaPMPJzFjuWeRHMtVHhlJ3S3n03y7ogzTJthE,4033
itp_interface/coq_ser_api/__init__.py,sha256=fHI4ZGgPPXKvWyv3_12ZlUBV22izjgnU4i4KtS-CgTg,7504
itp_interface/coq_ser_api/contexts.py,sha256=8jMV6E4UaabxenEA6PVICXxOey5oXunUXdlE0QMhRWI,11213
itp_interface/coq_ser_api/coq_agent.py,sha256=-GJ_5YvQ5Q1mZ0zTqMfWbgyGdaASGuQC0wMO1N1aRfs,17800
itp_interface/coq_ser_api/coq_backend.py,sha256=H96ps0iE7foicq63RvQZ6s9c5CvEwFZhagBwpFC1aAw,2456
itp_interface/coq_ser_api/coq_util.py,sha256=fo3xdrF_yij-4v-s0uJXg_zyNrQ6KPRrBRrTROCmAC8,32087
itp_interface/coq_ser_api/example.py,sha256=2iyMv-xJRAlkN-vfGzyQD3pYAqmvpZR9MECOIF_gnCg,2340
itp_interface/coq_ser_api/lsp_backend.py,sha256=RKlDiy3EyxXi79IqYOTTdRV7mfezMfAp4YST6gwbjJM,15920
itp_interface/coq_ser_api/py.typed,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/coq_ser_api/serapi_backend.py,sha256=eO55vWEMl4m-xkNeqz8Hv9_0GKxhHRlX2vxI7s8pBac,38242
itp_interface/coq_ser_api/util.py,sha256=CiQyFl3NSqev-EpB2JXXpIueN6zldl02qqg7deJpFpw,4017
itp_interface/coq_ser_api_old/__init__.py,sha256=zyb3QTZDpg1g5MkezFjlq-lwcOSdS_90fvTJ7eoluAA,104209
itp_interface/coq_ser_api_old/contexts.py,sha256=zfxBzT1xJxTnCzy7nEmVRSHWMGpzprSPtsIRiEhamEc,5670
itp_interface/coq_ser_api_old/util.py,sha256=NqGiimaTp9PmQQ-Vd7Rq-xeJIz6PlwMObKjwq64UylQ,4034
itp_interface/lean_server/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/lean_server/commands.py,sha256=OxXT5MFPpk4VMRCb0Jleon4seQJsH3z7dGuyf_Fsu6c,11799
itp_interface/lean_server/lean3_search_tool.py,sha256=28KbIzEGI8tta-AtI_WoHWdS02EcRHW3zjrzorJT5Js,12731
itp_interface/lean_server/lean4_repl_interface.py,sha256=_vle7Ff6ySXE1CZRPvHpg0gEBtUcOGAe2626US0RGv4,6448
itp_interface/lean_server/lean4_utils.py,sha256=BkTK7epCwC9jXU0sk8AJRoJwWeu7uwLLFETuHpIs_MU,11220
itp_interface/lean_server/lean_cmd_server.py,sha256=bHEbQoGDn-JO3qR88EYt_xo1jSxDJVXryuIHtRUg2ic,4182
itp_interface/lean_server/lean_context.py,sha256=R2rxgCP8Eb6WPTpZDjiD7btxpz_tIKgG2Pdo_HqZzjQ,2029
itp_interface/lean_server/lean_sync_server.py,sha256=0wDAwfVMezsCCsC6TlofyqvX-YZJfbaT2DL4PbdshAo,6416
itp_interface/lean_server/lean_utils.py,sha256=RTDk_lLo_g7AySxep8_NgWGOBPzh02hfhAOlGcIkBBA,8315
itp_interface/lean_server/py.typed,sha256=8PjyZ1aVoQpRVvt71muvuq5qE-jTFZkK-GLHkhdebmc,26
itp_interface/main/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/config.py,sha256=BuaulyUV7FvbcVxSaZV-nlFkmOSlxLHz1GjAZ-4PmxU,6746
itp_interface/main/extract_benchmark_dataset.py,sha256=2W4qiNBfqZAuOvlWBu9dRLmuWw73hiTwsLOsHnxmLZM,4737
itp_interface/main/filter_dataset.py,sha256=2YjYbYiX6Vxiz5citvAZbXAGpJUQq8B5mt02a-QhKLg,4390
itp_interface/main/install.py,sha256=PZ-HY_qZFjMzCUVk5I1sVQAmJ5K5JNsOLBGSdhMp8jc,4223
itp_interface/main/merge_dataset.py,sha256=gN6xZ8WMKvhEmlof4sbseLF7T-9xh2jnCCQAg6j6NE0,4067
itp_interface/main/run_tool.py,sha256=QHm6wtMG9P5zHMDvQTGFz0iH4G8R9ZRWxW1G0jGOOQQ,25787
itp_interface/main/configs/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/afp_data_gen.yaml,sha256=bLaG5Klq0RTPYHYT0XZ8ZhIXqAMOivkvqK8nE97-0LE,400
itp_interface/main/configs/category_theory_data_gen.yaml,sha256=ifm8tZGsG7_S3QfSAhCyh4FfZ0ULsZ1uR5x9X8iLzNs,412
itp_interface/main/configs/category_theory_data_gen_random.yaml,sha256=kZy-yqp-vMnjUGNXfw5I_MPck3STkgavOz3pJavuw38,469
itp_interface/main/configs/compcert_data_gen_test.yaml,sha256=cJeD3ZumvZU1HB-wf08RR_cuzXqwOwIZ2qF7hn8GU64,353
itp_interface/main/configs/compcert_data_gen_train.yaml,sha256=_IvIKslmJaBdpQAX9d9VHVBzExRprC2RR-ETaHmzUcY,293
itp_interface/main/configs/experiments.yaml,sha256=lEo0y2JOzhqWWosz_Vmn63ZnsBrhC64wmvdh9xJOMGI,447
itp_interface/main/configs/geo_coq_data_gen.yaml,sha256=b8_YdIQgjNXtGvzWqjzv5KOCzUCcpKWZ8Zs8Ahp0VjU,392
itp_interface/main/configs/geo_coq_data_gen_random.yaml,sha256=ydbCe-OZcfRmtiFPW8sO8k8sZ8EdZx-g409dZTveziM,451
itp_interface/main/configs/leandojo_random_data_gen.yaml,sha256=RnQ9G8mT7DtE-6xrbC8UPNgT9jC9LAAUwD4OWnV6Fgo,452
itp_interface/main/configs/math_comp_data_gen.yaml,sha256=_1F-VI6BaVVjHxc9VecKcNsSIPYVKaTXttsoV25VIuQ,398
itp_interface/main/configs/math_comp_data_gen_random.yaml,sha256=zhUKe8a9cQnTpGChw90T0IHK4StIEpDbNDqx8HIzYTs,460
itp_interface/main/configs/mathlib_data_gen.yaml,sha256=f9YoZwwRslnvwTSGs39lFoYk6oNLrg7LwmkRoKx8750,418
itp_interface/main/configs/simple_coq_data_gen.yaml,sha256=x4sGvTsm2gCgiCFHcSoGNLczzZQoQx4Fcvtiv59i0Pg,462
itp_interface/main/configs/simple_coq_data_gen_random.yaml,sha256=K4uyy9lws1VxJpGpIlKPP2eSVi4Qag0J_gaNuHeqD0Q,539
itp_interface/main/configs/simple_lean_data_gen.yaml,sha256=3gxKQLoYMLIlDvsraMS4GHl-sEx09KTb_LLl73RVUks,470
itp_interface/main/configs/simple_rl_lean_data_gen.yaml,sha256=--MgYSkTeGi2DcwgW81obQ_dtCXOgHSBv_4qDOYyEek,476
itp_interface/main/configs/uni_math_data_gen.yaml,sha256=_rS_ckglFe9eSXLbZD9KAjskTIHsxUhAO67R98mTNws,394
itp_interface/main/configs/benchmark/CompCert.yaml,sha256=kjKxzyvrMMYASvRKtYool5DVUpnrzIHwdLGdn-n16NE,9507
itp_interface/main/configs/benchmark/GeoCoq.yaml,sha256=Qg2XoQLF5szjesbkruyip8NmEbdk3NDkU5ao-9MJjx0,40290
itp_interface/main/configs/benchmark/UniMath.yaml,sha256=Ds7-vBeLYz9kJiEJjT9CXuQL4mdTud9SRKOdxnD-7cM,114891
itp_interface/main/configs/benchmark/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/benchmark/afp_isabelle.yaml,sha256=JAYQTQ1lLpjWZWukRzu0L5ELjO7XRvKRgd0OVur6ZOc,1032894
itp_interface/main/configs/benchmark/agent_proverbot_hard.yaml,sha256=bjTE6YijeHYB5ywIl44W5lICXJk8RTu4ZCIMaxWjur0,8445
itp_interface/main/configs/benchmark/category-theory.yaml,sha256=l794XryNTlf_E3XNEnULK6lRqYpGGcRJw8iFfipGwsE,13100
itp_interface/main/configs/benchmark/compcert_118_subset.yaml,sha256=lwSWCyP-NBU638xPkQ8ZOI1-fdHZmDORFLRCaJNCmBo,4538
itp_interface/main/configs/benchmark/compcert_benchmark.yaml,sha256=pwhSii0v01iRe6vgfo5hB8-MgEYRaj10AmneVK61yFA,1196
itp_interface/main/configs/benchmark/compcert_benchmark_hard.yaml,sha256=-QHhSAPdDTOdUSXVJbJ7jd9USQzGKElGhsFtkGb4BcI,16183
itp_interface/main/configs/benchmark/compcert_benchmark_hard_1.yaml,sha256=EQRRgt0tFJaOf9Hf5FaHQPndgc-cQwq1X-AWT9Y1XUI,1723
itp_interface/main/configs/benchmark/compcert_benchmark_hard_2.yaml,sha256=Negvm2d7kMBxYdzHzF6VdC5-0oaL_Mlq98zRBekL1LA,872
itp_interface/main/configs/benchmark/compcert_benchmark_hard_3.yaml,sha256=4iC__e2YVNizMApS6kuasMLmIFEQVtf-n1_SwCgYucw,3312
itp_interface/main/configs/benchmark/compcert_benchmark_hard_7_per_cent.yaml,sha256=srlzxmf0XvFux4K9xBVvI1CV99VpXuAH-f5nTj3zAqM,2542
itp_interface/main/configs/benchmark/compcert_benchmark_test.yaml,sha256=R9jOzWDzLczP1MA5yJPjZbU5ChFbQ1ZnFMbj9xwKj48,1257
itp_interface/main/configs/benchmark/compcert_benchmark_train.yaml,sha256=5ANOdYPdhXQz2qXDQ4r9pb0lcSHUyhGTwnuPp18BcVA,9857
itp_interface/main/configs/benchmark/leandojo_novel_premises_test.yaml,sha256=BU-1DgeM6rlTiY9pvvrbvfd7XL1FMaoOTI-Uqcd-l4A,104295
itp_interface/main/configs/benchmark/leandojo_novel_premises_train.yaml,sha256=zpPA_0ws3GB-fiz0NGWtv7w7LzWovIcJb_akP_Sq3c4,3913741
itp_interface/main/configs/benchmark/leandojo_novel_premises_val.yaml,sha256=LK8JTP8TH3f_ppj2ez5HJ7iegUdA0EpwW7EBxeRl9bM,103891
itp_interface/main/configs/benchmark/leandojo_random.yaml,sha256=ic5sS9VaQOZxVlutN9gDLh1i5N6pt0M9cGDSznfZeUQ,132832
itp_interface/main/configs/benchmark/leandojo_random_test.yaml,sha256=2akL6l4OZ1AkSv9jAWzFbEuEZCQBDi8k0ijyM9Kb1cU,100268
itp_interface/main/configs/benchmark/leandojo_random_train.yaml,sha256=zq3Qzg_tQrSZDFpHRQZUjLrJconmIwcGFMfh59mqDVo,2424463
itp_interface/main/configs/benchmark/leandojo_random_val.yaml,sha256=0S2VVepyhEXT_i-kCXDYQ0FkCkgHLi4lf5lvnJAQSBY,104293
itp_interface/main/configs/benchmark/math-comp.yaml,sha256=PXnxWCAumkoslxUBBItrpv9xlR5xxCCR0ZdzLKhUwzI,6037
itp_interface/main/configs/benchmark/miniF2F_test.yaml,sha256=SUdQncXJ30h1LZ45Wmz0NQrTyBuvylCmIQMLobgtOrE,302
itp_interface/main/configs/benchmark/miniF2F_test_aime.yaml,sha256=tLlkAtYbsSXDLxNzTxUXXUt8ClP-4jnEuBsrtAH5X-A,649
itp_interface/main/configs/benchmark/miniF2F_test_algebra.yaml,sha256=Q6DmDwBZX31wQJULvhF0gVjhOMloso1fLI1lBP8QqOc,1209
itp_interface/main/configs/benchmark/miniF2F_test_amc12.yaml,sha256=LZ0X3CWjMFZCOzULEWri3KGhHoN4fpQITQ5BoImYwRM,1444
itp_interface/main/configs/benchmark/miniF2F_test_few_shot_hard.yaml,sha256=W_GUIDAS7alFN3uTPURMuEixaT6tq4-ILCb9SLQMlEw,7592
itp_interface/main/configs/benchmark/miniF2F_test_imo.yaml,sha256=qxg5BTacMdiALoNNkajydf8Guqfp910kAane_DT_lNc,793
itp_interface/main/configs/benchmark/miniF2F_test_induction.yaml,sha256=9kBUKJXZSKDiTtMJKJDvPM92f0LGV7CIKQXf8aN8D-o,626
itp_interface/main/configs/benchmark/miniF2F_test_mathd_algebra.yaml,sha256=RVP9vygleL0RVeXPMk7QHq53SeHkKAq9H5Op6X_Twyw,2405
itp_interface/main/configs/benchmark/miniF2F_test_mathd_algebra_hard.yaml,sha256=Pp5lhSibhcKJt5RiAlHwQoe9GTJUhgj7a1Fy2MuS0LM,2111
itp_interface/main/configs/benchmark/miniF2F_test_mathd_numbertheory.yaml,sha256=PZHQcaVVT8o1YyucHnqtK_3NgXlgIVSRDs-aGuXniZM,2408
itp_interface/main/configs/benchmark/miniF2F_test_numbertheory.yaml,sha256=HejMgDRqhr5CjO9Z8BY66vjqM9Yo7tDxJraaHnBVo-U,698
itp_interface/main/configs/benchmark/minicompcert_benchmark_1.yaml,sha256=jLguBEzySX2h3m8THMqyCniF120FLhW3Ot7RWKCsJdE,552
itp_interface/main/configs/benchmark/proverbot_hard.yaml,sha256=S8MCygnq-s1gFBa9bFL9yRk55_rXEd8Rp7ugO_Uu9OQ,3160
itp_interface/main/configs/benchmark/re_prover.yaml,sha256=G1Bh8HLdRLB2FncCpSIQk1k8H4kNmmou1YnPc1Lc5do,1992
itp_interface/main/configs/benchmark/re_prover_hard.yaml,sha256=ofMOaf0pv-Op0qdXPrlXww7JcKweW3aF1iMI-VsXkMM,1206
itp_interface/main/configs/benchmark/re_prover_very_hard.yaml,sha256=1223tuC0ol5d3q9143DsrHZbmS862s2Rggult_h-AQU,617
itp_interface/main/configs/benchmark/reprover_with_retrieval.yaml,sha256=8Q-y_BasSDeLd3Gyqs573qn6EP7JAwBpqXHj52XqjvM,2240
itp_interface/main/configs/benchmark/reprover_with_retrieval_hard.yaml,sha256=1YNC2Rb57lShuKkrtGFR3TIUfWdkukT2-JiwItK3yh0,901
itp_interface/main/configs/benchmark/reprover_with_retrieval_neg.yaml,sha256=CsBOArbvK285dX1__DpobmVRDbkZjnNPBKpyD-YNM5g,6285
itp_interface/main/configs/benchmark/simple_benchmark_1.yaml,sha256=hb_3_k23FUYVHjNjoKtu23kXTrczY3c9kbxhlTXefhI,872
itp_interface/main/configs/benchmark/simple_benchmark_8.yaml,sha256=9WlLJaYV-zHEu7W4e8K8nQyJKZZNnSdeGSqMnoQnCoA,1349
itp_interface/main/configs/benchmark/simple_benchmark_9.yaml,sha256=K738uKF-RMeHXrryh43hak9HUC3p_2tushLQOkYyTss,1974
itp_interface/main/configs/benchmark/simple_benchmark_isabelle.yaml,sha256=UP9AX0kbHid0HqZYbmdIu6nKcoYESbCO4p3_HZTl1Vs,519
itp_interface/main/configs/benchmark/simple_benchmark_lean.yaml,sha256=QT6sf7mDrMD9N6-9m7572z2MfBl_XI7-3Zasb1flCXg,318
itp_interface/main/configs/benchmark/simple_benchmark_lean_training_data.yaml,sha256=ZPCNaoYJzcn2UmxMm0C6FkfBt2njdm9NvrqkdtQL6xU,328
itp_interface/main/configs/benchmark/simple_rl_benchmark_lean.yaml,sha256=iX4VpPsGBlG0aHv3AQWeRE71QH2RNqFGu5SvXcC3YVE,425
itp_interface/main/configs/benchmark/stack_machine.yaml,sha256=tfqJJW5oPt5qatUQyspxwMXEaMly2jeN1kz-QdkaGJ4,347
itp_interface/main/configs/benchmark/stack_machine_hard.yaml,sha256=8J3iKNPEkKOLLMNLSv9vg5CDaffRYYylmVrVrxVElWU,406
itp_interface/main/configs/env_settings/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/env_settings/bm25_retrieval.yaml,sha256=QJ7X2Di82atJ5rnCSm06B6gkH7pw5yvNxHEbhfccshg,45
itp_interface/main/configs/env_settings/bm25_retrieval_no_dfns.yaml,sha256=NPo-e989ztHdouLivnhrm66shkuhDh4Pomd8joFbGBY,61
itp_interface/main/configs/env_settings/bm25_retrieval_only_local_no_dfns.yaml,sha256=1yZiRn7280k2GeZmUAIvHudMNfunYyX_JImgUiJ2RQU,83
itp_interface/main/configs/env_settings/bm25_retrieval_with_print.yaml,sha256=7P_PBJzDt_w9fLFeac6h2-lwv2x7D32bbM6gdJc7Ywo,67
itp_interface/main/configs/env_settings/bm25_retrieval_with_print_only_local.yaml,sha256=l6bQhIt1Yr-1Q0SHS_EXHbF3ZyQUJOSiE6MBNNCX6qc,89
itp_interface/main/configs/env_settings/bm25_retrieval_with_print_only_local_no_dfns.yaml,sha256=WZEot3Q3GrdkS6T4N0p9njfGJGYP8d50rWmRHIVxMrk,105
itp_interface/main/configs/env_settings/no_retrieval.yaml,sha256=lZqV63Sgp9Y6PTolB0P-W9NZ-CrO3LfajyrJBU-CU90,49
itp_interface/main/configs/repo/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/repo/coq_repos.yaml,sha256=cv48hMANb0wM6P_QU6xYCx6uwisSOd6DRtyH-YvoAi4,7408
itp_interface/main/configs/run_settings/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/run_settings/default_coq_data_generation_transforms.yaml,sha256=fUpCcPYlyZNgZawPx6Ezjt9seTg-xprZMx6fUsxuzWM,576
itp_interface/main/configs/run_settings/default_isabelle_data_generation_transforms.yaml,sha256=1Tuf-zUn68Hfkv4s0BKr928PuAxtoG66--IZBycjMH8,581
itp_interface/main/configs/run_settings/default_lean4_data_generation_transforms.yaml,sha256=Pn3ZzNhWd3XmZIb3pX9zwVwU99vCTDaTh92oxUDzp8w,580
itp_interface/main/configs/run_settings/default_lean_data_generation_transforms.yaml,sha256=RSdMqP7BDoEJCXzyzyywCIj6kMBFky2Px5g-ecxUfTY,578
itp_interface/pisa/.git,sha256=EkuyvvYn3GZmbU4Id7BUv1sIZJozUec8cDyR1f7E1pQ,53
itp_interface/pisa/.gitignore,sha256=tKu5c7EBxHQ3t7CMownYAuEEcnmWdsWQiAHF5TAMxEs,1373
itp_interface/pisa/.scalafmt.conf,sha256=hM9doZnlR0ApmY_xdMMcaLEMuINdNAVsbhJmUQ_D3bM,43
itp_interface/pisa/LICENSE,sha256=i28B8pLnQZrnoTQXiDedT9ftFaONTMnIeHx5WMgYr4A,1528
itp_interface/pisa/README.md,sha256=B5Gd-_rvNtE3lQAlZrLHYDTYoqorbztaCuQd0JsJsTc,10927
itp_interface/pisa/build.sbt,sha256=8yjmx0ZBwQ0Q0uI_fcwU7sEgJ6LkQmdZuTrp9sSoCC8,2431
itp_interface/pisa/build.sh,sha256=-rxj6w7G4J74MQv7I-pdTid7FlJ-6qgCH4bw7clp9yA,701
itp_interface/pisa/requirements.txt,sha256=j8qh33MtIh84pLd8_9muMo84PS1RK9pxjZ7IKNqwyLo,65
itp_interface/pisa/setup.sh,sha256=a1TeJfct-KReI82OA564fmBYX72iGBwfkS8PrCEbc1o,759
itp_interface/pisa/test.sh,sha256=qYTMbB724JnUpBojK9aznSKMpXI8rwQiOH16UHoYRYU,1223
itp_interface/pisa/universal_test_theorems.tar.gz,sha256=T7LaPjU5_BhkxPLLRwISoAEHenBN8iAlacVJ_tMw0GY,371201
itp_interface/pisa/.idea/.gitignore,sha256=cAA3xsNKKlXb0lHXGkXBgm81LlMI9Nz9HlocDL7tPSk,176
itp_interface/pisa/.idea/ClojureProjectResolveSettings.xml,sha256=lt4OMyhjjaS1MQcITPlKzt_XrHPi5yeRRdCsFj1-Zv0,176
itp_interface/pisa/.idea/misc.xml,sha256=nPeixMTb1ER34QdVq375HXZM8E3ttXN8Ibs8LNiPC-A,328
itp_interface/pisa/.idea/modules.xml,sha256=OxM0OVg-zJ4U-6szachHjVBTD3WY3UC-MoaPD1dNkeU,407
itp_interface/pisa/.idea/other.xml,sha256=26bEN5ObaZ7KIZ0TklPKvmypafDHAiiLOAsE2ff8vZg,186
itp_interface/pisa/.idea/sbt.xml,sha256=pnz0mKxSs9EVa-xkj8MpEVYf0mdqosOuL121WZRQDb4,754
itp_interface/pisa/.idea/scala_compiler.xml,sha256=2lz1ahwvN-hBMZLmI1AbES3Gp8MQAULEu2YRmKVR4P4,207
itp_interface/pisa/.idea/uiDesigner.xml,sha256=jXYZ7D6Dv-hxqZYqLLgWpyfnIrq7DTsSuglgyiPNx4o,8792
itp_interface/pisa/.idea/vcs.xml,sha256=YyPhJkiGKgqW_A14d2coF9bNkeLCo8PXjxCQ2yPG6I4,167
itp_interface/pisa/.idea/codeStyles/Project.xml,sha256=mQI80jGiD1GxH-Fu7VWlAAqqoRGqjPtXTSLhA0_g190,263
itp_interface/pisa/.idea/codeStyles/codeStyleConfig.xml,sha256=ZD-MbVm3MLWxyvxK2FMA7-MCUPLPNHU2JfcU3GVIQXI,149
itp_interface/pisa/.idea/inspectionProfiles/Project_Default.xml,sha256=YK047Tx1EVV6WsoGVcVEYji0SFZnwRB24jV7WuhSMOM,679
itp_interface/pisa/.idea/libraries/sbt__com_google_android_annotations_4_1_1_4_jar.xml,sha256=tavbO8UtkjbYLWeDHDGVwIGxxmnd5vlBAj-574joYKo,707
itp_interface/pisa/.idea/libraries/sbt__com_google_api_grpc_proto_google_common_protos_1_17_0_jar.xml,sha256=cailsfdZDt4pabKRE4TdxU7FWAxTDCB3AMFJqkdBNs0,809
itp_interface/pisa/.idea/libraries/sbt__com_google_code_findbugs_jsr305_3_0_2_jar.xml,sha256=2tLngb5ayV5S-rpx3ZmjBVl5FB4gFAK3Jr0ajOI8riM,682
itp_interface/pisa/.idea/libraries/sbt__com_google_code_gson_gson_2_8_6_jar.xml,sha256=phBxZIer2HNBPX3K0H1r2_Kl1E0VzCUlAinuj4Eaveg,652
itp_interface/pisa/.idea/libraries/sbt__com_google_errorprone_error_prone_annotations_2_3_4_jar.xml,sha256=_JH8VlFujGjPDQzkP7W1ghJyzes6J8EMn_hAFvIFSuQ,789
itp_interface/pisa/.idea/libraries/sbt__com_google_guava_failureaccess_1_0_1_jar.xml,sha256=y52LoXE2ppIQ5bg1SVYcbTvXK96NtVyyD0KL5cxyH6Q,699
itp_interface/pisa/.idea/libraries/sbt__com_google_guava_guava_30_0_jre_jar.xml,sha256=QcWKdNHDYs3tuwwTBAmoL1UO3vjibGMVnrVO-AU0JLA,664
itp_interface/pisa/.idea/libraries/sbt__com_google_guava_listenablefuture_9999_0_empty_to_avoid_conflict_with_guava_jar.xml,sha256=65zf4BfJaAQX5EgWpNykbW_Yko1TNM3it5IJvdTyOmQ,458
itp_interface/pisa/.idea/libraries/sbt__com_google_j2objc_j2objc_annotations_1_3_jar.xml,sha256=ysFs5Zxm662HiEb-Egaiz6FX9vXlXGV8kVVcstL2lkY,724
itp_interface/pisa/.idea/libraries/sbt__com_google_protobuf_protobuf_java_3_12_0_jar.xml,sha256=QBAS5GmTHk3XrFTJDyrK_Yvy3_3GAiTzZc-__uIS4C4,718
itp_interface/pisa/.idea/libraries/sbt__com_google_protobuf_protobuf_java_util_3_12_0_jar.xml,sha256=VlB4eB_JdISvWxS0kNvLKGI8HDOkAZNSoc1xt9Fcbqw,753
itp_interface/pisa/.idea/libraries/sbt__com_lihaoyi_fastparse_2_13_2_3_0_jar.xml,sha256=_C5pjtepsIyfpnZhoehWM4XIYBuLjp_uKySvQaODJZ4,686
itp_interface/pisa/.idea/libraries/sbt__com_lihaoyi_geny_2_13_0_6_0_jar.xml,sha256=xWBaV9QxnMRb8YvoYxPT0wWBj7Ryn3Mn0UrrCDZvD7c,651
itp_interface/pisa/.idea/libraries/sbt__com_lihaoyi_sourcecode_2_13_0_2_1_jar.xml,sha256=wRiwME_x2Xh__zKBEvmQKcgtGjTKzYcWcihjJwnZLiQ,693
itp_interface/pisa/.idea/libraries/sbt__com_thesamet_scalapb_lenses_2_13_0_10_9_jar.xml,sha256=q3sVd3dC3mVlpSh7N5LChHDnq8wm1mIzY9EihSDOva0,708
itp_interface/pisa/.idea/libraries/sbt__com_thesamet_scalapb_scalapb_runtime_2_13_0_10_9_jar.xml,sha256=DYrZLAVScAicP058K6kVMX2JDlWEU7o-lG7ZzyF6U_8,771
itp_interface/pisa/.idea/libraries/sbt__com_thesamet_scalapb_scalapb_runtime_grpc_2_13_0_10_9_jar.xml,sha256=3xZ0s0nTugFCYrIdCRDXDN1YNms1kqybOYRldXDXp6k,806
itp_interface/pisa/.idea/libraries/sbt__com_thesamet_scalapb_zio_grpc_zio_grpc_core_2_13_0_4_2_jar.xml,sha256=mJojWBliZgY6wfaqoxPxNoUpLIF3kYQE_uEh5LZCtKU,786
itp_interface/pisa/.idea/libraries/sbt__com_thoughtworks_paranamer_paranamer_2_8_jar.xml,sha256=d4yOgcoY4aRoQU6zRFsr7f41xJdAW0V6hSuHfB7z5o8,697
itp_interface/pisa/.idea/libraries/sbt__commons_io_commons_io_2_8_0_jar.xml,sha256=uHKRymAiW8KipLydngAiOaBbf_o9FAEScDESclBHfZM,654
itp_interface/pisa/.idea/libraries/sbt__de_unruh_java_patterns_0_1_0_jar.xml,sha256=zy9Dh7MlcIM_lyF28n3T3dJvkE1NeWqiynr3XBbJhLs,667
itp_interface/pisa/.idea/libraries/sbt__de_unruh_scala_isabelle_2_13_master_SNAPSHOT_jar.xml,sha256=P3SsmbtfB_isEAQfAg8k-hMBiF4Q2dBt0fBgbOaxYBE,614
itp_interface/pisa/.idea/libraries/sbt__dev_zio_izumi_reflect_2_13_1_0_0_M9_jar.xml,sha256=_sKMnsHL9Wxa330zb3XDCau6z0MNfOe71CbLEqljYVs,719
itp_interface/pisa/.idea/libraries/sbt__dev_zio_izumi_reflect_thirdparty_boopickle_shaded_2_13_1_0_0_M9_jar.xml,sha256=vmUI2excMaCTpHf0u_0Xl-la1YaEVWkUiVltYjuI_m0,915
itp_interface/pisa/.idea/libraries/sbt__dev_zio_zio_2_13_1_0_3_jar.xml,sha256=t4uhnfC2IbVMnYtD1L8dkte5t22-vG6Lku7BoF8-ZFs,628
itp_interface/pisa/.idea/libraries/sbt__dev_zio_zio_stacktracer_2_13_1_0_3_jar.xml,sha256=gtDHGloQafr3q7VLjjC9-YlLRF1P-Cz4j9wIRdaeNx4,712
itp_interface/pisa/.idea/libraries/sbt__dev_zio_zio_streams_2_13_1_0_3_jar.xml,sha256=ACcZIbQGm6xMal8mKKo9WCdx3jl1mpxBr8AYJ7k91dA,684
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_api_1_34_0_jar.xml,sha256=Bb5mQe6CphxwKTaPuYteAq4At3JH1ofK89gHMi0K1U8,635
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_context_1_34_0_jar.xml,sha256=AVi2yFJXs57fEVqMd---Pn0_GJwPBoMDtqtlXLpnB34,663
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_core_1_34_0_jar.xml,sha256=95ufG9t_25QhUzeoB7QqHaoW96bV3CZjnpsNYahz2QI,642
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_netty_1_34_0_jar.xml,sha256=HqVBHgn9ePCZeopJyk28M7PkVDvkgKOVBF8VEi069OA,649
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_protobuf_1_34_0_jar.xml,sha256=NHaq193cXMgCXO9TwNoYTsDyQkIvVmxy3Lii5FrIESU,670
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_protobuf_lite_1_34_0_jar.xml,sha256=GEgiYKecBet2luVZ52keyh9S4kToI40Hs305_DiXJfU,705
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_services_1_34_0_jar.xml,sha256=GLos04td0XnruOSn-WjaitS6Amby-ARTzwfQhDZ5AB4,670
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_stub_1_34_0_jar.xml,sha256=XJl_cJ12e7SHaq3r3I5ZnDf0HQHTfE5OjezUkQfRI2g,642
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_buffer_4_1_51_Final_jar.xml,sha256=BRMNG3XWdyeDRnOML6KSjYlVw9_M-Sg8z_OpwaAKIVs,709
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_codec_4_1_51_Final_jar.xml,sha256=Kw80IP41W_S5oJ2GqQZK4W5RuxKiChL-qO_DQaKi9A8,702
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_codec_http2_4_1_51_Final_jar.xml,sha256=gwsLg1R99485SLdm1LJgtBsRPw9GqsfGCjwC8L-xp6Q,744
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_codec_http_4_1_51_Final_jar.xml,sha256=Jn1Bc35rBwCiUuekuXdbj6wBJT_hpwMjkstiUltILIU,737
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_codec_socks_4_1_51_Final_jar.xml,sha256=sElPAa2vgZ5Gcf8pETFHtvA0bAvGL5TbkBDzLq_sX-Y,744
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_common_4_1_51_Final_jar.xml,sha256=nwl08cvMwnlnqP3IOgM0CDd1PrEIzv1RpB6mQrwRVcI,709
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_handler_4_1_51_Final_jar.xml,sha256=IMmByehD6zHTv5FznDcbTAWPE0B552WZdjBl8jf1cLw,716
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_handler_proxy_4_1_51_Final_jar.xml,sha256=jHiQvHRD0013sr1eLfSB5W918eOMp7Kv2WSotnw2S6U,758
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_resolver_4_1_51_Final_jar.xml,sha256=iXJv3SyRU_lCmQIKS8DIV8vQF7ZnoVwZiGjl4Ee0cmk,723
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_transport_4_1_51_Final_jar.xml,sha256=RVxILG_JEYdbmcHfF6aZxab2kcLVgKKbltJfeChmX1I,730
itp_interface/pisa/.idea/libraries/sbt__io_perfmark_perfmark_api_0_19_0_jar.xml,sha256=PJm6LA_y1h7O_XpAzyxOwMfNIX7jbvb_BhH1f-TcE8s,679
itp_interface/pisa/.idea/libraries/sbt__net_java_dev_jna_jna_5_3_1_jar.xml,sha256=YoJmpTVHrVUWCwEmaZyRyWaO2cn-BQb81N2MJxBfsIQ,629
itp_interface/pisa/.idea/libraries/sbt__net_liftweb_lift_json_2_13_3_4_3_jar.xml,sha256=wqdrSPWlaLRFCsbtGb39jW94GD3-GmislOkA_72qHRw,686
itp_interface/pisa/.idea/libraries/sbt__org_apache_commons_commons_lang3_3_11_jar.xml,sha256=ZddgisfkMtIaoUrVqGPFrdeGSPwOQNvoYoG0ZoazC98,700
itp_interface/pisa/.idea/libraries/sbt__org_apache_commons_commons_text_1_9_jar.xml,sha256=d5hxaTEnPx5FakO34_IfGg_W0-H_0X2G5s5uGT0j8eY,686
itp_interface/pisa/.idea/libraries/sbt__org_checkerframework_checker_qual_3_5_0_jar.xml,sha256=s3KAgcQETsUi9zhKhsLlkZe_ZQzy5-5t2SMSQr18Nsg,708
itp_interface/pisa/.idea/libraries/sbt__org_codehaus_mojo_animal_sniffer_annotations_1_18_jar.xml,sha256=3WXQYTl5XgKDXNgm2OFhojxRsZlvPCIvsagY1estzYU,787
itp_interface/pisa/.idea/libraries/sbt__org_jetbrains_annotations_20_1_0_jar.xml,sha256=NX0ViQG7oI4LpMYCSBunYXLVLD6NcBqM_SjpErDK8P8,680
itp_interface/pisa/.idea/libraries/sbt__org_jline_jline_3_16_0_jar.xml,sha256=piGWasIla6jWNp73-4znDimWWlh-36D6Zj4kLlaoda8,622
itp_interface/pisa/.idea/libraries/sbt__org_log4s_log4s_2_13_1_9_0_jar.xml,sha256=381FeZdX33l8AaMYXhXoJT5HIi93ES7fW3Az2WqKGhg,650
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_modules_scala_collection_compat_2_13_2_1_6_jar.xml,sha256=qWU6j1tHGkYNdt3GNajLkydy9AGJoMGvX-83Xby0WBM,828
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_modules_scala_xml_2_13_1_3_0_jar.xml,sha256=0jK4S6xgWGXS_rE3IoN5P8JFcmUI-Ev0x1iEYV-3xeg,730
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_scala_compiler_2_13_4_jar.xml,sha256=eaFdJ_UGJlXFV5ZtN7uR0r10Q6hsdVRX7W1YxIliZqQ,705
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_scala_library_2_13_4_jar.xml,sha256=Ga1Sqvle3aRBMe-aUd0-HRwnk50WkxcPgSmvsw9b1k0,1607
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_scala_reflect_2_13_4_jar.xml,sha256=q2DFZa1zh9mOJRQ49T3zauIY-d73TVYt2cv26dSnSVs,698
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_scalap_2_13_4_jar.xml,sha256=o7QAwq_Gg3AhU9AIqtnZe18Ek6oPxWA02LfMap9n714,649
itp_interface/pisa/.idea/libraries/sbt__org_scalaz_scalaz_core_2_13_7_3_2_jar.xml,sha256=iHZ_-DBwgAa59Fry-e3WF3xK4tDio1QbbbWrdi3tj6w,696
itp_interface/pisa/.idea/libraries/sbt__org_slf4j_slf4j_api_1_7_30_jar.xml,sha256=zGE03ofrEOhfCR4taecy2q41bcf6BEN_7S6Ww8hYcgQ,650
itp_interface/pisa/.idea/libraries/sbt__org_slf4j_slf4j_simple_1_7_30_jar.xml,sha256=NV4R-ak6x0CWCRHddZwZ0E3Em5u7Letu_z9AhcKvnYQ,671
itp_interface/pisa/.idea/modules/PISA-build.iml,sha256=p0U_Gls2ItZTFnnVY-3wGtSLyTUFaNiJ-ki2uMpkozA,14533
itp_interface/pisa/.idea/modules/PISA.iml,sha256=yIxJ7NDIQTMz5etQvp-HqBkGs-QBYAcgFyOCr7yqhwM,8415
itp_interface/pisa/command_generation/close_gaps.py,sha256=59dc6YhJrMpfrqWE7Bxi49OgncWd2jignGMH4hIbLeg,1379
itp_interface/pisa/command_generation/conjecture_normal_order.py,sha256=5XeeERBTvvAAMzhQLsnqvVSwg3MFTIa7LzEG0ighDYw,3060
itp_interface/pisa/command_generation/conjecturer_command_generator.py,sha256=pJnhn_9yErWMjURRd5qee1zZcVAGpqMYEdd7NHyC-Sk,1761
itp_interface/pisa/command_generation/create_dirs.py,sha256=wgUzEZQIQEeRO2pHMiys6ITsxAqr6GhVc8--aOsKRhs,384
itp_interface/pisa/command_generation/find_std.py,sha256=YHGPP1Hgo6VAckKLIeCIb7Y3IS3Fd2gsgXPIdU30KyM,3726
itp_interface/pisa/command_generation/generate_build_commands_afp.py,sha256=VGBZu177uiRJdabuF8yNWGMCLkuM8LKS3or-PGeTsUc,480
itp_interface/pisa/command_generation/generate_build_commands_std.py,sha256=oFhvrm0K28Ju0xplu2Z-kakhhl8C4WgmEOXPUdIaj1w,517
itp_interface/pisa/command_generation/generate_commands_afp.py,sha256=iQADP4ITDsh5oUYvHxExBxPv8SYiCM8jirdtMXsD_3s,4113
itp_interface/pisa/command_generation/generate_commands_mini.py,sha256=XwkBiI6Knm1MZnoLWIBGC8EXHVg4TP3FMNUPYzHfDCc,3250
itp_interface/pisa/command_generation/generate_commands_std.py,sha256=njhvBxLWU31AHfhOggPIjvrjDmwTuuxyTzg4cyNKVJo,3012
itp_interface/pisa/command_generation/generate_hammer_extraction_text.py,sha256=MnMqsc4KZaQpdwYA3DV8V2BM64Wm-haO8Ia8V_aQcgo,223
itp_interface/pisa/command_generation/hammer_command_generator.py,sha256=77WhleXSAuSGhHDV18DQ8u7uupgxBYhm-sPWExGc3Og,1944
itp_interface/pisa/command_generation/hp_search_command_generator.py,sha256=0P5MUO2UA0WV92F38dEcEHEMwaqRZF4M_5FiikhTasY,3561
itp_interface/pisa/command_generation/oracle_command_generator.py,sha256=R98GKb4bg5h27o4dUsifiTCawFUA44UcqvE1MiQbQos,2435
itp_interface/pisa/command_generation/search_command_generator.py,sha256=uc2Fu1Sz1_ML1GbhTSNLg3vQvBWe_IcZBJySnE3rMkI,3535
itp_interface/pisa/command_generation/summarise_problem_names.py,sha256=Zrln1GehwsxytX_PduBADB_6SeaR07bmNQEitF-gShw,1792
itp_interface/pisa/command_generation/tpu_hp_search.py,sha256=he8MLw5YzKFmsu2glEa-ZCE5mU4fNHVvYv8To2bnOSU,4232
itp_interface/pisa/docker/Dockerfile,sha256=2iJ5uyTf7y_0nmRK4gpMi_Hl0WshpSUMtLEQNfEzURc,1059
itp_interface/pisa/docker/docker_tutorial.md,sha256=c3tWzEa-hHIovQbOPiYYqaYUZ20WTnXdz7omnitVNoU,3172
itp_interface/pisa/eval_setup/copy_isabelle.py,sha256=UScqTAoTLoo1d8ZL6oR-APa7qW4goEbfdrFV0D33GHs,1845
itp_interface/pisa/eval_setup/copy_pisa_jars.py,sha256=KSiqDGygm_yob4c55m7ErXbNt5BPI0lI69MxgMoU66E,548
itp_interface/pisa/mesh_transformer_utils/tokenization.py,sha256=jgFOhfQSL-I2TTzj8WRj0DqFBVMcfLTYQHVSIKlcGNs,2271
itp_interface/pisa/project/build.properties,sha256=bT0BCGnSmlL_jBkYUlMmEuLBjlCP8GeFDJu5OhslQjA,17
itp_interface/pisa/project/plugins.sbt,sha256=lkwcz9ot4vSvJ55_qqh2Y2peCRJcX2PsIeiNcPNEsKM,238
itp_interface/pisa/scripts/extract_last_k_steps.py,sha256=b4anmpE95GG8qbDSCfsTY79ktMoDSGEr2u4jiWmWfvQ,1350
itp_interface/pisa/scripts/extract_proof_corpus.py,sha256=3-_3HH8rcFfmGXwoPAHOT5smoONnKz4qHJMMgWbwSJs,655
itp_interface/pisa/scripts/gather_hammer_results.py,sha256=yag_crWGBpIlmu9y9B2SKok_YJFw0Lh88WfU-yN9qqY,1133
itp_interface/pisa/scripts/length_in_char_stats.py,sha256=vnirnbkeWKjzv1UJ046iAZBWXnJKwrE9KffwZOHNfgs,815
itp_interface/pisa/scripts/mix.py,sha256=uq2WZEZwGdNqX_4swTr77Z5wn0U1K0VRVg8hFCAtCzQ,5133
itp_interface/pisa/scripts/results_stat.py,sha256=LS4c3oU5tHcJJVr9F2tZlXj43WE3tNYxkR-uz5GeMb8,1629
itp_interface/pisa/scripts/test_array_job.sh,sha256=5RW5w5OHwrQMUeyZU5s59A77TduahDo285efHvqgejA,1268
itp_interface/pisa/src/main/protobuf/server.proto,sha256=Rhts0ExxT6V3HNhXGvvy6vzPhP89ZVY2epYy_7DExtI,1526
itp_interface/pisa/src/main/python/pisa_client.py,sha256=dhE8PLAvENYSGGg8IkRIJCmpwj2vslS0od4cLPrDbCw,13866
itp_interface/pisa/src/main/python/server_pb2.py,sha256=a4BjfiwW4qGUUBUxZYGwrQOmT2PaQa62Az_EBHcKR8k,12704
itp_interface/pisa/src/main/python/server_pb2_grpc.py,sha256=hYu81g5JNmqTpOqTXee8TjosWtHwsmWlL9cgXPF5Hk0,10076
itp_interface/pisa/src/main/python/test_client.py,sha256=qC_s6HiV_fYGjGQISqN07jQm4tmn9wd_wOUU_Nfo4Ss,582
itp_interface/pisa/src/main/python/test_client2.py,sha256=R65RF5YBaoKpq_zxR1NPTILXHssoT0DNMtWrDBS44EY,2640
itp_interface/pisa/src/main/python/.idea/.gitignore,sha256=cAA3xsNKKlXb0lHXGkXBgm81LlMI9Nz9HlocDL7tPSk,176
itp_interface/pisa/src/main/python/.idea/misc.xml,sha256=WdkfFrZjLX4rXiDJ-01dO4gM-6zMut9OmKVddZ14JDo,278
itp_interface/pisa/src/main/python/.idea/modules.xml,sha256=qBvl8A1uBtIAvIFsJtAXz_ifRc9Qz7YvlHUPBqvB06s,264
itp_interface/pisa/src/main/python/.idea/python.iml,sha256=w0TW3o9qEaYr1iYR1jwYqlUBYm3KyxgnCK1PD03XvwQ,441
itp_interface/pisa/src/main/python/.idea/vcs.xml,sha256=ZEt22h_UABai6qzUWvAjkIdEIg4UUHoZBGut3J8go2M,189
itp_interface/pisa/src/main/python/.idea/inspectionProfiles/Project_Default.xml,sha256=0DOYP9n5RgCCFXLMl3jEQdSdLGyEdPAldPzyXg9IzFQ,743
itp_interface/pisa/src/main/python/.idea/inspectionProfiles/profiles_settings.xml,sha256=YXLFmX7rPNGcnKK1uX1uKYPN0fpgskYNe7t0BV7cqkY,174
itp_interface/pisa/src/main/python/conjecturing_parsing/conjecturer_postprocessing.py,sha256=sd-QF5boU6Bavk5PmXL4XmlhE0YZ929yb1h3qSg7mrM,2562
itp_interface/pisa/src/main/python/data_extraction/extract_data.py,sha256=Bqv3bP987ukDtqJVo9EB3wufOX3kF0P0jfLZAgq9Ef4,6623
itp_interface/pisa/src/main/python/data_extraction/find_premises.py,sha256=LIUl7WsaYavHc5XZBpqpsrdZBrwMyRjVe9dmANN1L8o,8686
itp_interface/pisa/src/main/python/data_extraction/process_data.py,sha256=UUYA4FU7PRBd6vSvLS5_FcxerSuOjeUEP50IK69l4mI,4890
itp_interface/pisa/src/main/python/legacy/PisaFlexibleClient.py,sha256=pfxIpjU2qMnaid8oGF729QyPkrIuVqbW1KoFa739MK4,6456
itp_interface/pisa/src/main/python/legacy/autof_test.py,sha256=Pw8N3LoJM9CVKoAreHXvRzWyWgBbwITbLnwfYvkgvQk,2181
itp_interface/pisa/src/main/python/legacy/cmd_client.py,sha256=_F47R0PDmzRNc5NaZ7X7t5cXzBs5Rk5KjQTOIv5RwtU,1029
itp_interface/pisa/src/main/python/legacy/convert_scala_dump_to_test_name_jsons.py,sha256=UcAiAftM4btdXDzCCun-ljhkJCn4sYLs0J4sCCZFZBo,667
itp_interface/pisa/src/main/python/legacy/create_data_txt.py,sha256=oIRswEuzbkd10MSRN9C4GYNLrlIqKQ2JfM0siYQKJxU,3430
itp_interface/pisa/src/main/python/legacy/create_finetune_tfrecords.py,sha256=CYMpL9381lpT7BZDX-oOhSZ4Xu16rSBPum3SnGfeDFw,11844
itp_interface/pisa/src/main/python/legacy/demo.py,sha256=6MHJn-S8yll40GaFkCqIN8HQeMEmun0WIxEmhQF9wrA,1731
itp_interface/pisa/src/main/python/legacy/evaluate.py,sha256=KwXLXsb5oXz3fWfwGC9SqV20h3y1CoIzbLILymqIxIs,5085
itp_interface/pisa/src/main/python/legacy/extract_first_step.py,sha256=-NGbtQguEhDdnG2ziB8FEUDm0FwWyGLsyzqyE6O-d-4,972
itp_interface/pisa/src/main/python/legacy/get_global_facts.py,sha256=sRQP7qD8pH9LkUPqVgI5nXzG0kPadgJTxbVha-4Tito,1405
itp_interface/pisa/src/main/python/legacy/mix_data.py,sha256=HHaaAfrYXesxNe8S91J0-rn7lE375GVZymHFcvS8cYo,964
itp_interface/pisa/src/main/python/legacy/one_stage_extraction.py,sha256=9FAVpkGzvGGoysk34nq8i6nvp5hbFE7Aia_3i0jizF0,4741
itp_interface/pisa/src/main/python/legacy/prepare_episodic_transitions.py,sha256=hbRXG0SVyWtuUteSi-pNx9NxzVdFLkFPXmapm-VkH_4,4612
itp_interface/pisa/src/main/python/legacy/prepare_translation_pairs.py,sha256=3L3txoUBF4o-PtnzIb-JlUM9Dl3DvWwA5yCu8jSmuXE,11168
itp_interface/pisa/src/main/python/utils/filters.py,sha256=-owsWZ8rNQuvQN0LRn9SNDvzYP30Cv30ujqh_881zBU,2575
itp_interface/pisa/src/main/python/utils/pisa_server_control.py,sha256=_gSQDDTbY15ulqjnv0RVx4WRAboyFWV6vEChDAcrvkk,922
itp_interface/pisa/src/main/scala/pisa/agent/CheckSyntax.scala,sha256=JYb8lppks_ismh-lQd3ytz-qT1HhCsYjAZPiqCLwDdI,10217
itp_interface/pisa/src/main/scala/pisa/agent/DepThms.scala,sha256=L8WQcLKXW3_o9J_-3J_p2q6GT7CDG6lwprB36YekTec,1034
itp_interface/pisa/src/main/scala/pisa/agent/PisaStat.scala,sha256=Yh64Fukl6UOIvu8F5_Pvj9pZVxV_XTPc_KptetSNb6g,1726
itp_interface/pisa/src/main/scala/pisa/agent/RefactorTest.scala,sha256=6W20rHLqDMvQo24kSfvLQMwRPnNfnBEzXjGUjN1MAnQ,1996
itp_interface/pisa/src/main/scala/pisa/agent/RepHammer.scala,sha256=oYYvplZPNA94QzkzztwcqJEDjPzp8lYyxTlmw1xjyzM,4500
itp_interface/pisa/src/main/scala/pisa/server/HammFacts.scala,sha256=uii2djDfIJMK_Y04hKpWe2g5A4Bn5SKp4JlXEqjJGzQ,2808
itp_interface/pisa/src/main/scala/pisa/server/PisaOS.scala,sha256=Wc30bWItiPgC3_QkpOtv_VQZDlHUIPRMsbipfTLLt1M,32964
itp_interface/pisa/src/main/scala/pisa/server/PisaOneStage.scala,sha256=YbhxKql-205yFUniCJ33NxISNrwkXZaYjW1gqlryngg,21885
itp_interface/pisa/src/main/scala/pisa/server/PisaOneStageServers.scala,sha256=yJeRpzq7fnHyVcfB6iulrq1_R6xyG80YcoYAhA3E6B8,33535
itp_interface/pisa/src/main/scala/pisa/utils/TheoryManager.scala,sha256=GwfzLfQuEbSdYJ5UxCq_0GGS0RPSWN_bD7rpmhyzWCk,4529
itp_interface/pisa/src/test/python/analyse_debug.py,sha256=IrqK0zjuJVI16zIcPrWBP8Bhq3qv0N7-FBe_uCcu-zI,1568
itp_interface/pisa/src/test/python/extract_test_seq2seq.py,sha256=xAPTL8j3-y4B2J63zkSsWtUTmxn7_1r7ojy1IwRreQ0,1753
itp_interface/pisa/src/test/python/extract_test_theorem_ground_truth_indices.py,sha256=vdiD5KnBZVQxxHG3W645SgX2oOTrTt5W07CNPDo7iDs,1154
itp_interface/pisa/src/test/python/proof_originality.py,sha256=fjZNKj3WFDWJNNqOAPXEV_CBPulUPXFPgzl4ZIbr71g,854
itp_interface/pisa/src/test/python/test_command_generator.py,sha256=sgPJPf5aWeB24y-L4svP7WT2m69sJJyIBuvVQXoOGW0,926
itp_interface/pisa/src/test/python/test_model_sequence_accuracy.py,sha256=O0duQt75tDuxN5OS8I5SpwLKEYvcf2edL1IA_Sfhrko,2420
itp_interface/pisa/src/test/scala/pisa/Easy.scala,sha256=8ft5vOqRn5nt64ZXZxcp9vLjaNxJl07udk684Y2vCzM,851
itp_interface/pisa/src/test/scala/pisa/TestCurl.scala,sha256=3u-5y_3rpPqa-8XAy_lfRLGnUEPzIZv8xejArcPhyeM,2819
itp_interface/pisa/src/test/scala/pisa/TestIsa.scala,sha256=6vH4B5Lt5P7xo_XNhRp2A7h1ggvjN4RBAmgC89F_Ev8,584
itp_interface/repo/build.py,sha256=taNMSja1OTGSnVZmRJt_AdGxRAFTYR1psrs_YC0VXVs,2985
itp_interface/repo/clone.py,sha256=ytQEt0jsz5K9C-LgnZ5tr7kFENAzcEjse5w5QsdUrvY,3256
itp_interface/repo/dataset_discovery.py,sha256=DMiUxynMYdi4w58faM0ns1G23hSKr6NivCz2OOyoFF8,3819
itp_interface/retrieval/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/retrieval/abstraction.py,sha256=5jbbZelSdccmJ6AzYuD936xnr_yFSwG2FRPcrZCaR0U,733
itp_interface/retrieval/coq_bm25_reranker.py,sha256=nrRAKGpXLkNE3yhKX4W8mbEIo3sW2-VKUdMVlq0qRyg,7185
itp_interface/retrieval/isabelle_bm25_reranker.py,sha256=_y9zasFxnjLP5wIPBn6HUSG2Tmrc787FuFjfMXM7LPY,3595
itp_interface/retrieval/lean3_bm25_reranker.py,sha256=F4L-LT6MDm9fIFphayFYJThQdz8w-4WIN_v9dnv-tzQ,3788
itp_interface/rl/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/rl/abstraction.py,sha256=6n2Mv7ZzCPC50lN85CWH_G5Wa0V-c1YW69MVPwa1JEQ,3236
itp_interface/rl/proof_action.py,sha256=SSJK7wDuh8LkCiFLYsXkVcjk4QRy3eI8jTIcIF2K1SQ,7352
itp_interface/rl/proof_state.py,sha256=QEHbZpgO77J_I7TkQD5yle6j0xci-WMbz1YbO8gqbZs,8384
itp_interface/rl/proof_tree.py,sha256=dQJxCcqIV8EFgOARCgXmKnP05osy_T6F1ylSkv64peI,4063
itp_interface/rl/simpl_proof_env_pool.py,sha256=g2WX7OOv8Cow8t12CVjN8GwIgYtuCAGPoGFdYxvw0oc,792
itp_interface/rl/simple_proof_env.py,sha256=AiL6Z2NAuVnSPDVFEqN-liRVD71qLonLJrlgT23PqK0,39045
itp_interface/rl/simple_proof_env_pool.py,sha256=WVVhf1gpO_TQQlB-emQjMfpxtramWDA8mP2kifUR8Bk,30335
itp_interface/scripts/setup.sh,sha256=DxP_JbHhNUiHwZBeLv5bIjfUbxGagB8rJhezaOO-nAM,8088
itp_interface/tools/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/tools/basic_utils.py,sha256=yQxzQhfdmyrRKIZKwUYROACtSyk1ANUwJxB-acq_7Z0,6344
itp_interface/tools/bin_packing.py,sha256=3XSo-bmEDSI40g3aK-lW4BhYfJX5NtatgnA2Wu-TV4c,3827
itp_interface/tools/cache.py,sha256=G-R4Cx5XiC3t2SzaPLDeXkWPLsoJOo6bbdHotRyJAYU,3018
itp_interface/tools/coq_build_spec.py,sha256=H_lehkWG0t8tLuJesm99AI49n6gp70MjyxqvmopPdA0,1081
itp_interface/tools/coq_context_helper.py,sha256=JVuiQkjVKYYvlpxZOFo2ec-ZKC3eTxrRF1lbQxRCJE0,23061
itp_interface/tools/coq_executor.py,sha256=VDC13wZJMtfJirKthobL4I_Bl8Juiwn-iuDGKlusONU,21561
itp_interface/tools/coq_local_data_generation_transform.py,sha256=WtRG1I2jOoAHAFNj4nYFz0Ujb9W-Pw4POBDsp7q4cAU,8975
itp_interface/tools/coq_parse_utils.py,sha256=PGtaNuF-M6iZigcIbsRGOvNQiMxV90NhhET4oYYso8w,6483
itp_interface/tools/coq_theorem_proof_pair_generation_transform.py,sha256=Ds01OnIFOeGXXANFKdxxxNGLVdD9RyUt_djiT49_7qY,8284
itp_interface/tools/coq_training_data_generator.py,sha256=m4VvY7Y5kflIGzEYIuQ_nEPUJlPJy6eDu6ugHGTJlC0,2660
itp_interface/tools/dynamic_coq_proof_exec.py,sha256=mcwOwbBvGwz8Yf8RWzs3FzbzxPC11xlTBhC7Xz8PdHw,10809
itp_interface/tools/dynamic_isabelle_proof_exec.py,sha256=aZSk8OnLBPgR7EECV4oaAMZSZ54udbO8Jc8sWe00DL4,11521
itp_interface/tools/dynamic_lean4_proof_exec.py,sha256=KM33bgeD6NtZbdWw-VG6kw2BXWbBBLzK2RMkb70BOGM,11767
itp_interface/tools/dynamic_lean_proof_exec.py,sha256=lSGXJ6Y19NZLw0jYXw9NgyIaXXpsrE8MeC8VcLTe_Os,11347
itp_interface/tools/isabelle_context_helper.py,sha256=eJIc3WlESchQoF80VhK0oyeZNgeqVMCQ_m5Ccgnq1lo,4105
itp_interface/tools/isabelle_executor.py,sha256=IAOyIDDknTCWeb_uSpVzrY52i7ccVZOAEBen1ojQS30,38299
itp_interface/tools/isabelle_local_data_generation_transform.py,sha256=GdKuCalTLmP0pETSl5HkwcedwRfh1KLw2JthMiI8JSE,8356
itp_interface/tools/isabelle_parse_utils.py,sha256=wzEc1NxVtjxywyvX61bDQ1uYOD33Ubgvzblby_ScL-Y,4932
itp_interface/tools/isabelle_server.py,sha256=3Rkjjwwc1lGnMxWc9BI871a11HHsSPHSFRoy7DIdLh8,3905
itp_interface/tools/lean4_context_helper.py,sha256=SATRwOsMEu9ZTGEvx281Jf3_ykzXC4ZenPPqzGZMR44,4462
itp_interface/tools/lean4_local_data_generation_transform.py,sha256=b8naxeWdU3vV-4ovXYoQQ4IzYPG84UFkwlrNqx5lbaY,6217
itp_interface/tools/lean4_sync_executor.py,sha256=9gfG2UokEpJrINMyC608qZyujbXu70QEB-SDK9-t-h8,58865
itp_interface/tools/lean_cmd_executor.py,sha256=Xec96vLnLVUXnRTYcmbPYxmlCuG5M0Ky1TNEwtJ0yac,37869
itp_interface/tools/lean_context_helper.py,sha256=24odp0aJ3Dr9CRDyAaFyech9XGrEdQXWf6XI8tJyltU,21936
itp_interface/tools/lean_dojo_data_generation_transform.py,sha256=2IXMWi8Tu8hYbqsjAx3PTltFRm4WOwFIRZRK_9ObZKs,11212
itp_interface/tools/lean_executor.py,sha256=grEJinlb_hT4q9bbJCZlHiiNDLyT-oeg-NyVVLaeG58,32209
itp_interface/tools/lean_local_data_generation_transform.py,sha256=k6LIjyEDi2xaTXWKjHlE3QmmNXZhzK5dBijdhG62JiU,7726
itp_interface/tools/lean_parse_utils.py,sha256=GEEGIDI7xL8EQ9gl5L6pPU5UfSbjVQRNo7QJkPNGSoY,1264
itp_interface/tools/log_utils.py,sha256=SygDUvTlZLUxxeiA-4p1kpGy7YB7gIkOQuN7gWi4xHw,562
itp_interface/tools/proof_exec_callback.py,sha256=IIxnGKvCKajG_wEgky_uleoCnC4QFWhY6QYaGrgOMew,6386
itp_interface/tools/ray_utils.py,sha256=C962wMEcAeAbAuVObKY2UCa7l3x1oODL0Md5Q-1okiA,10966
itp_interface/tools/run_data_generation_transforms.py,sha256=u2TH4jMEpja6InFUx06wlFkKnEHN2RQ5Y6ztRqLJoz4,22925
itp_interface/tools/theorem_details.py,sha256=Aeied3x0q3cMgDpnYYJiQJdsskYiD0HfCZg-X-oNmB4,830
itp_interface/tools/training_data.py,sha256=FFvuyKe_Z8CugZ_yjTUtjpPtEC1190yrcGH5jLeNmks,22100
itp_interface/tools/training_data_format.py,sha256=nihKz_oatlkhiYiYgLt0OFpXhHcFvb48Y7I1CcXVGBc,34240
itp_interface/tools/repl/.git,sha256=JsACm7wvQdCbsjejV8i2GEYv1KOga4kc3LHkKu6-gyw,62
itp_interface/tools/repl/.gitignore,sha256=cv1sOovuzoTbIi37rcbGUcNbg7111QqifetqVlZbWew,99
itp_interface/tools/repl/README.md,sha256=1ZAz0MNWesOWWIN4NS57chz-izFfkcAjNcGwwgtY9Mk,5021
itp_interface/tools/repl/REPL.lean,sha256=uEPB67EZJSLzpkrKSzIWjdvTZbMKGRRTilO6AQql2VQ,81
itp_interface/tools/repl/lake-manifest.json,sha256=laEJd0QSCWY8_4m3-qmMx7DZqZd1vNwBYzVJT90mRs0,104
itp_interface/tools/repl/lakefile.lean,sha256=_tPM9xvVaj_TDhE5asJv9z2eg-zEQFltNQ5HhAUAnl0,239
itp_interface/tools/repl/lean-toolchain,sha256=hpP7H7L_aq-ayACHG7abF3sEQ6JpZwTx2KcWFoJDoXU,28
itp_interface/tools/repl/test.sh,sha256=OLFbp9rZ3hbN_m63gohmTFr1vppObaqClFCUrAdMaUY,1083
itp_interface/tools/repl/.github/workflows/ci.yml,sha256=E37MjrvdwJowcIdjldlE8aZk0gY6CuJxs2a3Dv0k29Q,522
itp_interface/tools/repl/.vscode/copyright.code-snippets,sha256=Yxvq5EWxIBkQzq93t7Iwyu9L9c08LHz_AZE1CUMLWWE,273
itp_interface/tools/repl/.vscode/extensions.json,sha256=kQeb1JmqB4cCDbyakYNnXDfMuQmUJgMiBBmGQj_sZ8M,485
itp_interface/tools/repl/.vscode/module-docstring.code-snippets,sha256=3bRL7E2bsmcq5SkkNy_oMWFakjqq4BjE28l9meCQ4gM,536
itp_interface/tools/repl/.vscode/settings.json,sha256=OlcKRIcoVQKN361xK3iffrfdtuos4Kyxo98R2xxrEIo,301
itp_interface/tools/repl/REPL/Frontend.lean,sha256=217fStvj4kzIV61B12u-f54RmMZ-iCfPMVnB26hIugY,1909
itp_interface/tools/repl/REPL/JSON.lean,sha256=R953Qd2yPgTelGwllhidh4mmd2tskDgRzEiQZJemd1U,4842
itp_interface/tools/repl/REPL/Main.lean,sha256=8hoEsp7HDEhRTGhfllWNhScP5jjq_8ZY5Y1g3A3m_AE,12198
itp_interface/tools/repl/REPL/Snapshots.lean,sha256=dvdczcJ_VbeqNl3VtcBJJNQlR0dI1fd12c-QXXdE6qQ,11824
itp_interface/tools/repl/REPL/Lean/ContextInfo.lean,sha256=frgYburPj69mkNzZY2riBUc0Pdx7NoPssxPhbtZD184,306
itp_interface/tools/repl/REPL/Lean/Environment.lean,sha256=kIvojIhGcsgJCaICqenduXqHbXTkHNLgAZywLWlIl60,909
itp_interface/tools/repl/REPL/Lean/InfoTree.lean,sha256=NgGQm_5LkCyCUO_Hzw2aVSNjV-ajjXp8Yf44Iec04hE,10345
itp_interface/tools/repl/REPL/Lean/InfoTree/ToJson.lean,sha256=GyZtO-3quowiayeDtwDkXZPGtLi0QsV37MOSzUk-mso,3722
itp_interface/tools/repl/REPL/Util/Path.lean,sha256=TvKRqMG3Y-HuV1DUbc1rxvm-WonGqfe1d4FK1hGTsWE,1216
itp_interface/tools/repl/REPL/Util/Pickle.lean,sha256=fUulkI1e46F6qda7emBjUpt8bBeaWqkHQ7oG59Tu-VU,1578
itp_interface/tools/repl/test/all_tactics.expected.out,sha256=lWxC08nKtLfUmX4h2FsZ2btwhmwRI0e0VBJtBWPlJoc,328
itp_interface/tools/repl/test/all_tactics.in,sha256=ij6NPBNKHY-xNy6Nr-xv5aPVMLORpO7U63k6Zsgh3kY,71
itp_interface/tools/repl/test/by_cases.expected.out,sha256=w7ZhZB_hUCN6rXCjETN9wpT8U5GMPsCnFFjGYt_hDOk,701
itp_interface/tools/repl/test/by_cases.in,sha256=qScl0aS0yBDKxpOD9WhBt5PWW9AQz3d6LQgSLgyOJyE,204
itp_interface/tools/repl/test/by_cases.lean,sha256=3g-tTWDLYZFmoaTdiYhNam1BajLUcSp_0ptMzGuDnhw,85
itp_interface/tools/repl/test/calc.expected.out,sha256=GGEVNkJLIIyB1ZEjWkGcL6FxZIWQpBJbYuJPVxkaPHw,913
itp_interface/tools/repl/test/calc.in,sha256=xQDQTyYYybHeiWNyIsML8acWHA53fzxnSxgTgo4dOr4,101
itp_interface/tools/repl/test/def_eval.expected.out,sha256=oT6oYHCQJWQJrSIDjFJehXl6aYrvW4F3I2cN5438Wl0,163
itp_interface/tools/repl/test/def_eval.in,sha256=zBBJKJ7p1yKF0SHNIJ8MROW3XN5NNCVpTnO4K8pQZqc,67
itp_interface/tools/repl/test/enableInitializersExecution.expected.out,sha256=bZwUHIcXc9ENfG9oPBGKB_fDYtIfDi8jmd5durqJylo,12
itp_interface/tools/repl/test/enableInitializersExecution.in,sha256=3zz_FKPqbs6TnGeePTvJjEFjqwYV6NHHZhp7vnssfL0,50
itp_interface/tools/repl/test/file.expected.out,sha256=mjYCGQBlaJZWlHth6UsYhEh9W_YicpfVDtjeaHozWtk,179
itp_interface/tools/repl/test/file.in,sha256=yED0oLwIcU0HC4Hw8mqc60dzfEg4PYZVYMPiUan9DzA,47
itp_interface/tools/repl/test/file.lean,sha256=8z-cjiSdD0PTJm0tfJr_UDAxYmtWL7ii5HvVesxi5ns,70
itp_interface/tools/repl/test/have_by_sorry.expected.out,sha256=iPHd-KtHbS0AgjRAOaN9IQZtSwv1lJRNpsoAAGnNFVA,771
itp_interface/tools/repl/test/have_by_sorry.in,sha256=-HiIFL0u6XDrSyJJxEeGhUPNn6wjFtLzP5LHs26Uf1c,192
itp_interface/tools/repl/test/import_lean.in,sha256=ZXglsGn75acpOMahmlp8vXDxpxE9NN2h48QDgWO4_E8,24
itp_interface/tools/repl/test/incomplete.expected.out,sha256=eBveOkX-BVEZwrP3bpdfFYcyTRSRnwwdMbmojZU1ZLE,548
itp_interface/tools/repl/test/incomplete.in,sha256=TtnbkU0mLJjGKR4rImSQ3O5UysYX5ZnpUL9iPNQmjYY,121
itp_interface/tools/repl/test/incomplete.lean,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/tools/repl/test/infotree.expected.out,sha256=lMeGkDz39LyjlzGWekkWTPEqp-fL49h9pCelW64x8kk,531
itp_interface/tools/repl/test/infotree.in,sha256=Vq9yzvspj1BaaINvusb4253-cPuEuejJTvYj5xIHPyQ,79
itp_interface/tools/repl/test/invalid_tactic.expected.out,sha256=l4_Ryzqdk8lPizoTpBf5zdO29EsT2Tmk50CR-6A6IeA,510
itp_interface/tools/repl/test/invalid_tactic.in,sha256=SgRVAir5kn0PAA-w4g-BnwW4EZS0RvUaVFr_wpWWm8k,114
itp_interface/tools/repl/test/name_generator.expected.out,sha256=IZ8mEhJcDXvPo7pqaA3DOaPA_eiIpNw58I_zoz-VtbQ,1399
itp_interface/tools/repl/test/name_generator.in,sha256=YuUWWUP6SJwGFHSvNWjhfQbJYC5TbmRUx0Djn3f1kc0,578
itp_interface/tools/repl/test/no_goal_sorry.expected.out,sha256=AjDX53SLqACV3d42QXcZglwqsg_r7xn_UePMf0W6O7o,323
itp_interface/tools/repl/test/no_goal_sorry.in,sha256=5gYCNhM5TNv3WtZHEDOxa7VM77qvV83sP7_A4C82M2k,74
itp_interface/tools/repl/test/no_goal_sorry_2.expected.out,sha256=hC1mEHqu-g3iRu4axr81C0bTikzQUYo1pwGN_NoaYZA,294
itp_interface/tools/repl/test/no_goal_sorry_2.in,sha256=kNd6HfBzaND5A_t-t3PbP2OkrF99zFhZp-Meq-dte1I,51
itp_interface/tools/repl/test/options.expected.out,sha256=y0AmQf4fo8w43VZNm87Ru1cTohHmBu0Y-e3FLzCY7JI,447
itp_interface/tools/repl/test/options.in,sha256=TG933yqDYvWpVYsald0e3Gw3VSUxcD0dOaVw3IhXB0E,109
itp_interface/tools/repl/test/pickle_environment.expected.out,sha256=KIVudHv9tQZamopmL5nhGFH6h4FT0Q2FpZMDMLOcU3c,48
itp_interface/tools/repl/test/pickle_environment.in,sha256=zUeWr2B-oSBh_Zl6H5lWu4VM005DywgXBT8uIvcUrkg,149
itp_interface/tools/repl/test/pickle_environment_with_imports.expected.out,sha256=EBWr72rVwKogxQO27B-Nl8gTi2RztBDMnFdXKMMjKPs,60
itp_interface/tools/repl/test/pickle_environment_with_imports.in,sha256=2EN-dZV6PaezCXFmWcaomBHY-slQcCOp71KOJ0Lx1p4,183
itp_interface/tools/repl/test/pickle_open.expected.out,sha256=sJdocb6RIMh-hJUFYbkURcr_I-wVnOLpg9ppc3KagMg,48
itp_interface/tools/repl/test/pickle_open.in,sha256=PzwITCprt1c9jvLEpwNb4tvwZhrTUwnEvEsZkry788s,146
itp_interface/tools/repl/test/pickle_open_2.expected.out,sha256=WBzCu9vpOqnS7W5jF28xKjO9uqco3UDVVP2xwe7yR2I,24
itp_interface/tools/repl/test/pickle_open_2.in,sha256=62Lf_-xn1WExDvcp-7RrIzvhQob_XRZKU6OEg86H3Zo,82
itp_interface/tools/repl/test/pickle_open_scoped.expected.out,sha256=IbmOGA0dWiBABpWDuvu2OeNPmdhNnGBDwUHJJvFpNY4,337
itp_interface/tools/repl/test/pickle_open_scoped.in,sha256=OfgHwDAfTCyu9JhCNga-VaQd5ItuQTD7R_fA4TPZK2U,157
itp_interface/tools/repl/test/pickle_open_scoped_2.expected.out,sha256=N2VNAji2c8suABekaHdEkyEWceyWkpHWd_rmlNS0aRo,313
itp_interface/tools/repl/test/pickle_open_scoped_2.in,sha256=Ph-zGJuX32H5GtRkFjF3F6nZqs01mf_1mqeGYRd0yo8,88
itp_interface/tools/repl/test/pickle_proof_state_1.expected.out,sha256=lKYKFNjnNxyqkFe5aR9QIZ2OfJshmqtbQAktBohj5j4,576
itp_interface/tools/repl/test/pickle_proof_state_1.in,sha256=01W4ymneqt_s5EZSllOgrLgIsR0Sk9k1QfYULl5dR08,344
itp_interface/tools/repl/test/pickle_proof_state_2.expected.out,sha256=N4p4KZTeJhjv7vuRIzRI_Uzcd6mkwV_8NdF_lWtaJzQ,82
itp_interface/tools/repl/test/pickle_proof_state_2.in,sha256=v8CKqf83luvHG0wfB5IlUXpkbaRJnkdHv_XO_scuDgk,83
itp_interface/tools/repl/test/pickle_proof_state_env.expected.out,sha256=lKYKFNjnNxyqkFe5aR9QIZ2OfJshmqtbQAktBohj5j4,576
itp_interface/tools/repl/test/pickle_proof_state_env.in,sha256=XdLjfFpAyLHTgF-tKQ92OF7nNnexxDao8vFZ77jdPUA,364
itp_interface/tools/repl/test/pickle_scoped_notation.in,sha256=zJJMgI3B20vvB31kj8h2YB3-KUqvHG-agAdm08-OMWU,310
itp_interface/tools/repl/test/pickle_scoped_notation_2.in,sha256=t8n30u5D2t_WS7dzUEGCuhVT5JSllBoP9E1TXIiS7_U,84
itp_interface/tools/repl/test/proof_step.expected.out,sha256=Hua-5a49E4DMM7ID9zof12h129K7ocSIIExlTNUczaA,423
itp_interface/tools/repl/test/proof_step.in,sha256=M3zfMaxksPqriZ0eIwH7He7jd--4o5kDgutocrIA6vo,176
itp_interface/tools/repl/test/readme.expected.out,sha256=zamQN_JETRPopERZLkY_Q4bw_KrzdDVRUuPiI93CTAk,393
itp_interface/tools/repl/test/readme.in,sha256=X7ZeO2dgJYzVWI3pUQZ9BHq1nOr8SEjcbhfNX2PEBSY,138
itp_interface/tools/repl/test/sorry_hypotheses.expected.out,sha256=n_IwDSe5bfrNa6GToNtlo7H-ENgU9smtuZbs0Z1tCAc,439
itp_interface/tools/repl/test/sorry_hypotheses.in,sha256=hPXGN4jyrYkQdS597uF-fQVzjla_pOjOA9FQf5D72FQ,111
itp_interface/tools/repl/test/synthesize_placeholder.expected.out,sha256=lEGc5EfvyPV6gWoaT2Rrt7MFYqf6o3EYL4iLdQplvXs,202
itp_interface/tools/repl/test/synthesize_placeholder.in,sha256=qapdR7L57dVDK5xGF9p4nOo4N6MY2s6Qc7LWh2wySdk,28
itp_interface/tools/repl/test/tactic_mode_sorry.expected.out,sha256=6Owwt9yW6b-I_tGsf5i2KgEZYh6bYzSlHN27XE5PNxE,383
itp_interface/tools/repl/test/tactic_mode_sorry.in,sha256=OnbTqShdFsb3J7bKHoQwCMBeV3-Cv99YXy8wSL3AWcA,73
itp_interface/tools/repl/test/tactic_sorry.expected.out,sha256=wExThghHHP1cCMEr4F-zEdMkb5hMc4qsUTD7g6m6mqw,300
itp_interface/tools/repl/test/tactic_sorry.in,sha256=aaqWiqqumms7UaTtTjwSeLt0RCRIfI4i7ANtK-8CZ9U,35
itp_interface/tools/repl/test/term_sorry.expected.out,sha256=JD2Rd9UFO6zf9_KNUf_Csl0pyoPFwYGPxtrH6JyPXNo,300
itp_interface/tools/repl/test/term_sorry.in,sha256=eEiaAWb96dPeGEFRm0xKsKLeQWT0Spr3jiLWkxjjJVg,32
itp_interface/tools/repl/test/trace_simp.expected.out,sha256=DaU9HyuZK_SfDNFtBNp6lVG-KX-NWx-TQ0fOzFnLCG4,956
itp_interface/tools/repl/test/trace_simp.in,sha256=S9zg4CV90HBWaGMxehSndDdIT7wANYfSxFrkVCfyhWQ,389
itp_interface/tools/repl/test/unfinished_tactic_block.expected.out,sha256=04F4tAw7KyUgjcD40GJZUKttiMJkfncAIX9fMbk-NJE,299
itp_interface/tools/repl/test/unfinished_tactic_block.in,sha256=Z-lSdemNLocjNk5Zsbx7bo-tOtVMENpCnerwhGfH3sI,29
itp_interface/tools/repl/test/unknown_environment.expected.out,sha256=ruH7s89H_HUXtOr0g6uJw_xIof2Ll5RDakXAPWfaPoE,37
itp_interface/tools/repl/test/unknown_environment.in,sha256=XX8PjA9vdd27DXYnMYYXeYJBx_Gc05qTL1l7MlXZjQA,45
itp_interface/tools/repl/test/unknown_proof_state.expected.out,sha256=jk7-V4PE2mkTlrxx9Qo45zJQ4alHy6voYfP4kDrBmL4,337
itp_interface/tools/repl/test/unknown_proof_state.in,sha256=SPwS6pWa_t5yPM1195zaExPwDaGkwj4CyHc490hQBWs,77
itp_interface/tools/repl/test/unknown_tactic.expected.out,sha256=xFE3uJ6oSOZg4ifSOiHJIwfhym7swNMonLpVVKFrqFQ,357
itp_interface/tools/repl/test/unknown_tactic.in,sha256=HY1oE_7an4Xey8Bym2gB8lfdcnCw2j-hKpdHQxQ7tqU,76
itp_interface/tools/repl/test/variables.expected.out,sha256=W8xfHYtc18_jRTU26lZ8nEqlW4ACUzw6iC2Z8RSV4IM,776
itp_interface/tools/repl/test/variables.in,sha256=2Mp3QDtTvUppQVUxZz3tnUKnVf5YK-XgL5fnhl9EZqA,237
itp_interface/tools/repl/test/Mathlib/.gitignore,sha256=4zIzbyKXApFqgDE8l3uo9OGKfRvuYvP2AN3HXjiH0Y0,72
itp_interface/tools/repl/test/Mathlib/H20231110.sh,sha256=fh1WzHusunE0Hyz8jSjDZiVe2rniYx9sH79tXETu5NA,120
itp_interface/tools/repl/test/Mathlib/ReplMathlibTests.lean,sha256=EBX49GdqJ-pjeAswzJFnEiMoVwl7K99jXcYcuUnBB_s,15
itp_interface/tools/repl/test/Mathlib/lake-manifest.json,sha256=yk6459Q1Ud0YWAlg6jlhcxua2lotwSten_fU53g2bYA,2184
itp_interface/tools/repl/test/Mathlib/lakefile.lean,sha256=0aZMB78gyqGPNRSLBwtJzufDP3WRqQ_CJvI97sAXpnU,332
itp_interface/tools/repl/test/Mathlib/lean-toolchain,sha256=hpP7H7L_aq-ayACHG7abF3sEQ6JpZwTx2KcWFoJDoXU,28
itp_interface/tools/repl/test/Mathlib/test.sh,sha256=GgbOi24KeSbJ3fbw8sE_MHotQ8GGCZ_d6esdO4RTLOc,1051
itp_interface/tools/repl/test/Mathlib/test/20240209.expected.out,sha256=duUyxQQU0mKuZbi55gVssljhxBD_RI6MtEFF8jeZiFQ,489
itp_interface/tools/repl/test/Mathlib/test/20240209.in,sha256=yt76LmeaXAXIrg7X-6DcO1fqWavnp7X8ZmG4kHTk79U,102
itp_interface/tools/repl/test/Mathlib/test/20240209.lean,sha256=WmVu5bnBAn6cI4rEZ2u3wVX5IWdyLKzswckCj-klxR4,80
itp_interface/tools/repl/test/Mathlib/test/H20231020.expected.out,sha256=JIj77iGXLnP5vlSmtO6tYkCkXxWzK6T7lU5EUTJiMfg,48
itp_interface/tools/repl/test/Mathlib/test/H20231020.in,sha256=XzrUwG8iHdJ5idv-WeFbWAMzf3c8LX0bUUY88K9jNVM,870
itp_interface/tools/repl/test/Mathlib/test/H20231020.lean,sha256=INehzwOeWNaiYo4iVVe38xNpBamYVsYQivq4beNz1Jc,782
itp_interface/tools/repl/test/Mathlib/test/H20231110.expected.out,sha256=WBzCu9vpOqnS7W5jF28xKjO9uqco3UDVVP2xwe7yR2I,24
itp_interface/tools/repl/test/Mathlib/test/H20231110.in,sha256=kX42DYKDWmNqyqOrEY2TmTH_2yL6nwo8q_f3mUPFzHc,368
itp_interface/tools/repl/test/Mathlib/test/H20231115.expected.out,sha256=WY54UzGYYf_B6YtNxH7032SAdwEli1c7nrgObw006i8,474
itp_interface/tools/repl/test/Mathlib/test/H20231115.in,sha256=WaZP0FoHV_nzJxZg1xbMs0dKkzFewsnF5DORiauPLWs,158
itp_interface/tools/repl/test/Mathlib/test/H20231115_2.expected.out,sha256=Jjs0ITcOKs7Hfyj4DuNWaqv4M613qAeex-jivrtmU5A,523
itp_interface/tools/repl/test/Mathlib/test/H20231115_2.in,sha256=blx8N5WjBV7MyqMWfcSXBg8ZQSNyK7cP7pU0KSpv9Sk,143
itp_interface/tools/repl/test/Mathlib/test/H20231115_3.expected.out,sha256=cekSe2kT-Ht86NNr7Mg8BNlOOmsAaYtNE4v5URFN_6A,283
itp_interface/tools/repl/test/Mathlib/test/H20231115_3.in,sha256=yU-v5Yu98IpdUHM0l4_ajFLeRgUgZWT8xzSSqsO3y48,124
itp_interface/tools/repl/test/Mathlib/test/H20231214.in,sha256=_Z7sLyE0LUQeik5rfAedOh10nu7Ix4OWB-rA3ueWKYU,481
itp_interface/tools/repl/test/Mathlib/test/H20231214.lean,sha256=GoZQweuQNOHZl7MrdTs68DnQBHOLcnL9EFQG6rTa4jo,663
itp_interface/tools/repl/test/Mathlib/test/H20231215.expected.out,sha256=XHGkNeBBF2tUJw0NjzSpPttSF5vUbV9qaiSkXZbQbMg,24
itp_interface/tools/repl/test/Mathlib/test/H20231215.in,sha256=DYRxEbbUoaOO3db_ww4nbVPOGZnxVPL46C1WHliJuAc,115
itp_interface/tools/repl/test/Mathlib/test/H20231215_2.expected.out,sha256=n3oL4RcF2VVUdQkE3W_lKJgBvQ18xxE3Ii-h4zfEaL4,321
itp_interface/tools/repl/test/Mathlib/test/H20231215_2.in,sha256=RwOEhr1JU5dRxrp-rpLj3myUIfl9325cJkJ0sgfNqEQ,126
itp_interface/tools/repl/test/Mathlib/test/exact.expected.out,sha256=nKkjmLFjk1Fy-bS2ljk7cvJNz75kOc8w537IWARKKys,916
itp_interface/tools/repl/test/Mathlib/test/exact.in,sha256=5fLkm7tPTv1b8u1tqPtzSuwy_kyikCMBDIAvyB0d-bU,250
itp_interface/tools/repl/test/Mathlib/test/import_Mathlib.lean,sha256=EBX49GdqJ-pjeAswzJFnEiMoVwl7K99jXcYcuUnBB_s,15
itp_interface/tools/repl/test/Mathlib/test/induction.expected.out,sha256=L775_PJw6bKj9m85c_JZ2v_sfmEw74ugzdx43-n8yOk,806
itp_interface/tools/repl/test/Mathlib/test/induction.in,sha256=essP7h1h-eVmRYCwDf4tX2PteQwTpJx6BvtAwGRc6ko,268
itp_interface/tools/repl/test/Mathlib/test/induction.lean,sha256=J-_5QnoGVoWvGk_MZsQiQqiqIUPMWI1LOaXk5jiD1zw,112
itp_interface/tools/repl/test/Mathlib/test/on_goal.expected.out,sha256=_Km-07VKKaePw6o3DZyX8i79ONksf49kisTFQZm9DBg,716
itp_interface/tools/repl/test/Mathlib/test/on_goal.in,sha256=aeYwHa_1bhrElSMkS0P8EV9kU2tc_I-g14O2mc0wj2Y,259
itp_interface/tools/repl/test/Mathlib/test/pickle.expected.out,sha256=oHksgBR50YjVF7EcXe5fKdyKtXmqbEFxCRJho2hzSec,444
itp_interface/tools/repl/test/Mathlib/test/pickle.in,sha256=sNiZED6ATOmn0p8VZq6pO1czKV1OcigCsR9pmj2fldU,241
itp_interface/tools/repl/test/Mathlib/test/pickle_2.expected.out,sha256=J7cLLgBnwAhW80rgrMgsDSKOHe1zd4Zl2HxFgfb9_so,172
itp_interface/tools/repl/test/Mathlib/test/pickle_2.in,sha256=I67KImQsl4UskMK3vU7Tl_5BL8jVIHtoqW9Zl0gjVkg,95
itp_interface-1.1.2.dist-info/METADATA,sha256=Fs5ErVjdQGUL0MXVIUz7O_sHpPiAmZfOWfXrPNcD4gc,11398
itp_interface-1.1.2.dist-info/WHEEL,sha256=qtCwoSJWgHk21S1Kb4ihdzI2rlJ1ZKaIurTj_ngOhyQ,87
itp_interface-1.1.2.dist-info/entry_points.txt,sha256=pgxfpZ5WUt7E4tIWKPppHc4zOXHJorBkpdA0kmbqxF4,208
itp_interface-1.1.2.dist-info/licenses/LICENSE,sha256=Ja0zK0mghvyO3342OSoi9LPoKvj92RqN17fXcYOcMME,1066
itp_interface-1.1.2.dist-info/RECORD,,
