Skip to content

Commit

Permalink
re-run ipynb
Browse files Browse the repository at this point in the history
  • Loading branch information
Kaiyu Yang committed Mar 15, 2024
1 parent 929923e commit 18d41b7
Showing 1 changed file with 43 additions and 40 deletions.
83 changes: 43 additions & 40 deletions scripts/generate-benchmark-lean4.ipynb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -359,26 +359,26 @@
"name": "stderr",
"output_type": "stream",
"text": [
"\u001b[32m2024-03-14 19:43:28.334\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m116\u001b[0m - \u001b[1mLoading the traced repo from /Users/yangky/.cache/lean_dojo/leanprover-community-mathlib4-3c307701fa7e9acbdc0680d7f3b9c9fed9081740/mathlib4\u001b[0m\n",
"2024-03-14 19:43:30,651\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
"100%|██████████| 5042/5042 [12:52<00:00, 6.53it/s] \n",
"\u001b[32m2024-03-14 19:56:33.430\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='a751d21d4b68c999accb6fc5d960538af26ad5ec') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n",
"\u001b[32m2024-03-14 19:56:48.006\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n",
"\u001b[32m2024-03-14 19:56:57.443\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77') relies on an unsupported Lean version: 8fc1af650ad6d31cf766d9bc84119149330e7d4e\u001b[0m\n",
"\u001b[32m2024-03-15 12:50:10.722\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m116\u001b[0m - \u001b[1mLoading the traced repo from /Users/yangky/.cache/lean_dojo/leanprover-community-mathlib4-3c307701fa7e9acbdc0680d7f3b9c9fed9081740/mathlib4\u001b[0m\n",
"2024-03-15 12:50:12,915\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
"100%|██████████| 5042/5042 [15:05<00:00, 5.57it/s] \n",
"\u001b[32m2024-03-15 13:05:29.599\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='a751d21d4b68c999accb6fc5d960538af26ad5ec') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n",
"\u001b[32m2024-03-15 13:05:44.688\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n",
"\u001b[32m2024-03-15 13:05:54.625\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77') relies on an unsupported Lean version: 8fc1af650ad6d31cf766d9bc84119149330e7d4e\u001b[0m\n",
"Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356\n",
"\u001b[32m2024-03-14 19:57:00.938\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa') relies on an unsupported Lean version: 216d2460e0adec8317fdeeb6f2543cb7442564fd\u001b[0m\n",
"\u001b[32m2024-03-14 19:57:07.628\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='280d75fdfe7be8eb337be7f1bf8479b4aac09f71') relies on an unsupported Lean version: 0d7051497ea09b2b4a4ef608e371b8f317487c3c\u001b[0m\n",
"\u001b[32m2024-03-14 19:57:11.601\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1') relies on an unsupported Lean version: f6cd6c069587cfe62dd68cb6330f9ad794a56724\u001b[0m\n",
"\u001b[32m2024-03-14 19:59:59.133\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m6\u001b[0m - \u001b[1m116695 theorems in total\u001b[0m\n",
"\u001b[32m2024-03-14 19:59:59.168\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n",
"\u001b[32m2024-03-14 19:59:59.211\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n",
"\u001b[32m2024-03-14 20:02:16.104\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m112695 theorems and 234380 tactics saved to ../leandojo_benchmark_4/random/train.json\u001b[0m\n",
"\u001b[32m2024-03-14 20:02:21.292\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 4116 tactics saved to ../leandojo_benchmark_4/random/val.json\u001b[0m\n",
"\u001b[32m2024-03-14 20:02:24.068\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 3792 tactics saved to ../leandojo_benchmark_4/random/test.json\u001b[0m\n",
"\u001b[32m2024-03-14 20:03:40.016\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m111570 theorems and 229668 tactics saved to ../leandojo_benchmark_4/novel_premises/train.json\u001b[0m\n",
"\u001b[32m2024-03-14 20:03:45.758\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 5779 tactics saved to ../leandojo_benchmark_4/novel_premises/val.json\u001b[0m\n",
"\u001b[32m2024-03-14 20:03:47.246\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 5573 tactics saved to ../leandojo_benchmark_4/novel_premises/test.json\u001b[0m\n",
"\u001b[32m2024-03-14 20:05:22.288\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m73\u001b[0m - \u001b[1m158266 theorems/definitions from 5042 files saved to ../leandojo_benchmark_4/corpus.jsonl\u001b[0m\n"
"\u001b[32m2024-03-15 13:05:58.191\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa') relies on an unsupported Lean version: 216d2460e0adec8317fdeeb6f2543cb7442564fd\u001b[0m\n",
"\u001b[32m2024-03-15 13:06:05.265\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='280d75fdfe7be8eb337be7f1bf8479b4aac09f71') relies on an unsupported Lean version: 0d7051497ea09b2b4a4ef608e371b8f317487c3c\u001b[0m\n",
"\u001b[32m2024-03-15 13:06:09.519\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1') relies on an unsupported Lean version: f6cd6c069587cfe62dd68cb6330f9ad794a56724\u001b[0m\n",
"\u001b[32m2024-03-15 13:08:20.957\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m6\u001b[0m - \u001b[1m116695 theorems in total\u001b[0m\n",
"\u001b[32m2024-03-15 13:08:20.981\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n",
"\u001b[32m2024-03-15 13:08:21.017\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n",
"\u001b[32m2024-03-15 13:10:10.961\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m112695 theorems and 233473 tactics saved to ../leandojo_benchmark_4/random/train.json\u001b[0m\n",
"\u001b[32m2024-03-15 13:10:18.093\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 4248 tactics saved to ../leandojo_benchmark_4/random/val.json\u001b[0m\n",
"\u001b[32m2024-03-15 13:10:21.899\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 4567 tactics saved to ../leandojo_benchmark_4/random/test.json\u001b[0m\n",
"\u001b[32m2024-03-15 13:11:30.176\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m112695 theorems and 231240 tactics saved to ../leandojo_benchmark_4/novel_premises/train.json\u001b[0m\n",
"\u001b[32m2024-03-15 13:11:36.065\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 5357 tactics saved to ../leandojo_benchmark_4/novel_premises/val.json\u001b[0m\n",
"\u001b[32m2024-03-15 13:11:37.327\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 5691 tactics saved to ../leandojo_benchmark_4/novel_premises/test.json\u001b[0m\n",
"\u001b[32m2024-03-15 13:13:12.385\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m73\u001b[0m - \u001b[1m168515 theorems/definitions from 5042 files saved to ../leandojo_benchmark_4/corpus.jsonl\u001b[0m\n"
]
}
],
Expand Down Expand Up @@ -493,9 +493,12 @@
{
"data": {
"text/plain": [
"('Mathlib/Data/MvPolynomial/CommRing.lean',\n",
" ['Mathlib/Data/MvPolynomial/Variables.lean',\n",
" '.lake/packages/lean4/src/lean/Init.lean'])"
"('Mathlib/RingTheory/Polynomial/Content.lean',\n",
" ['Mathlib/Data/Polynomial/FieldDivision.lean',\n",
" 'Mathlib/Data/Polynomial/EraseLead.lean',\n",
" '.lake/packages/lean4/src/lean/Init.lean',\n",
" 'Mathlib/Data/Polynomial/CancelLeads.lean',\n",
" 'Mathlib/Algebra/GCDMonoid/Finset.lean'])"
]
},
"execution_count": 10,
Expand All @@ -516,7 +519,7 @@
{
"data": {
"text/plain": [
"23"
"49"
]
},
"execution_count": 11,
Expand Down Expand Up @@ -545,11 +548,11 @@
{
"data": {
"text/plain": [
"{'full_name': 'MvPolynomial.instCommRingMvPolynomial',\n",
" 'code': 'instance instCommRingMvPolynomial : CommRing (MvPolynomial σ R) :=\\n AddMonoidAlgebra.commRing',\n",
" 'start': [56, 1],\n",
" 'end': [57, 28],\n",
" 'kind': 'commanddeclaratio'}"
"{'full_name': 'Polynomial.IsPrimitive',\n",
" 'code': 'def IsPrimitive (p : R[X]) : Prop :=\\n ∀ r : R, C r ∣ p → IsUnit r',\n",
" 'start': [41, 1],\n",
" 'end': [43, 30],\n",
" 'kind': 'commanddeclaration'}"
]
},
"execution_count": 12,
Expand Down Expand Up @@ -640,8 +643,8 @@
"text/plain": [
"('https://github.com/leanprover-community/mathlib4',\n",
" '3c307701fa7e9acbdc0680d7f3b9c9fed9081740',\n",
" 'Mathlib/Algebra/Group/Pi/Lemmas.lean',\n",
" 'Pi.update_eq_div_mul_mulSingle')"
" 'Mathlib/Algebra/GCDMonoid/Multiset.lean',\n",
" 'Multiset.lcm_add')"
]
},
"execution_count": 15,
Expand Down Expand Up @@ -670,7 +673,7 @@
{
"data": {
"text/plain": [
"4"
"1"
]
},
"execution_count": 16,
Expand Down Expand Up @@ -699,14 +702,14 @@
{
"data": {
"text/plain": [
"{'tactic': 'rcases eq_or_ne i j with (rfl | h)',\n",
" 'annotated_tactic': ['rcases <a>eq_or_ne</a> i j with (rfl | h)',\n",
" [{'full_name': 'eq_or_ne',\n",
" 'def_path': 'Mathlib/Logic/Basic.lean',\n",
" 'def_pos': [208, 9],\n",
" 'def_end_pos': [208, 17]}]],\n",
" 'state_before': 'case h\\nι : Type u_1\\nα : Type u_2\\nI : Type u\\nf : I → Type v\\nx✝ y : (i : I) → f i\\ni j✝ : I\\ninst✝¹ : DecidableEq I\\ninst✝ : (i : I) → Group (f i)\\ng : (i : I) → f i\\nx : f i\\nj : I\\n⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j',\n",
" 'state_after': 'case h.inl\\nι : Type u_1\\nα : Type u_2\\nI : Type u\\nf : I → Type v\\nx✝ y : (i : I) → f i\\ni j : I\\ninst✝¹ : DecidableEq I\\ninst✝ : (i : I) → Group (f i)\\ng : (i : I) → f i\\nx : f i\\n⊢ Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i\\n\\ncase h.inr\\nι : Type u_1\\nα : Type u_2\\nI : Type u\\nf : I → Type v\\nx✝ y : (i : I) → f i\\ni j✝ : I\\ninst✝¹ : DecidableEq I\\ninst✝ : (i : I) → Group (f i)\\ng : (i : I) → f i\\nx : f i\\nj : I\\nh : i ≠ j\\n⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j'}"
"{'tactic': 'simp [lcm]',\n",
" 'annotated_tactic': ['simp [<a>lcm</a>]',\n",
" [{'full_name': 'Multiset.lcm',\n",
" 'def_path': 'Mathlib/Algebra/GCDMonoid/Multiset.lean',\n",
" 'def_pos': [39, 5],\n",
" 'def_end_pos': [39, 8]}]],\n",
" 'state_before': 'α : Type u_1\\ninst✝¹ : CancelCommMonoidWithZero α\\ninst✝ : NormalizedGCDMonoid α\\ns₁ s₂ : Multiset α\\n⊢ lcm (s₁ + s₂) = fold GCDMonoid.lcm (GCDMonoid.lcm 1 1) (s₁ + s₂)',\n",
" 'state_after': 'no goals'}"
]
},
"execution_count": 18,
Expand All @@ -715,7 +718,7 @@
}
],
"source": [
"proof[\"traced_tactics\"][1]"
"proof[\"traced_tactics\"][0]"
]
},
{
Expand Down

0 comments on commit 18d41b7

Please sign in to comment.