diff --git a/experiments/dsp/README.md b/experiments/dsp/README.md index 222c7d0..e8e17ab 100644 --- a/experiments/dsp/README.md +++ b/experiments/dsp/README.md @@ -4,8 +4,16 @@ based on Sean Welleck's DSP for Isabelle: https://github.com/wellecks/ntptutoria ## Execution +First of all, build the experiment repo. + ``` sh -python3 experiments/dsp/main.py eval +# experiments/dsp +cd lean_src_proj +lake build +``` +Then run `main.py` +``` sh +python3 experiments/dsp/main.py -h ``` ## Related work diff --git a/experiments/dsp/lean_src_proj/lake-manifest.json b/experiments/dsp/lean_src_proj/lake-manifest.json index cce41a6..c0d830c 100644 --- a/experiments/dsp/lean_src_proj/lake-manifest.json +++ b/experiments/dsp/lean_src_proj/lake-manifest.json @@ -1,68 +1,75 @@ -{"version": 7, +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4", + [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "cbc437aed076ea3aeb83f318d572f8b6de38265d", - "name": "std", + "scope": "", + "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.10.0-rc1", + "inherited": false, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "fd760831487e6835944e7eeed505522c9dd47563", + "scope": "leanprover-community", + "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "rev": "82ac8cce559c3da0ade17cee3e275111fb7f1920", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "f5b2b6ff817890d85ffd8ed47637e36fcac544a6", + "scope": "leanprover-community", + "rev": "d1b33202c3a29a079f292de65ea438648123b635", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.28", + "inputRev": "v0.0.39", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec", + "scope": "", + "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f", + "scope": "leanprover-community", + "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "a6f770740f4c07b236c336115f4de99c28cd8910", + "scope": "", + "rev": "f5c3f06aa7f6d6c221786d2890c345a00e6341f8", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.10.0-rc1", "inherited": false, "configFile": "lakefile.lean"}], - "name": "lean_src_proj", + "name": "LeanSrcProj", "lakeDir": ".lake"} diff --git a/experiments/dsp/lean_src_proj/lakefile.lean b/experiments/dsp/lean_src_proj/lakefile.lean index 972f2a1..ecc34f5 100644 --- a/experiments/dsp/lean_src_proj/lakefile.lean +++ b/experiments/dsp/lean_src_proj/lakefile.lean @@ -1,20 +1,12 @@ import Lake open Lake DSL -package «lean_src_proj» { - -- add any package configuration options here -} -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" - --- ref: https://github.com/leanprover-community/aesop?tab=readme-ov-file#building --- ref2: https://chatgpt.com/c/fbb6dde3-46e7-4117-9c02-78e5df1e0df5 --- add aesop pkg as a depedency require aesop from git - "https://github.com/JLimperg/aesop" + "https://github.com/leanprover-community/aesop.git" @ "v4.10.0-rc1" +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ "v4.10.0-rc1" +package LeanSrcProj @[default_target] -lean_lib «LeanSrcProj» { - -- add any library configuration options here -} +lean_lib «LeanSrcProj» diff --git a/experiments/dsp/lean_src_proj/lean-toolchain b/experiments/dsp/lean_src_proj/lean-toolchain deleted file mode 100644 index cfcdd32..0000000 --- a/experiments/dsp/lean_src_proj/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.6.0-rc1 diff --git a/experiments/dsp/lean_src_proj/lean-toolchain b/experiments/dsp/lean_src_proj/lean-toolchain new file mode 120000 index 0000000..b494e97 --- /dev/null +++ b/experiments/dsp/lean_src_proj/lean-toolchain @@ -0,0 +1 @@ +../../../src/lean-toolchain \ No newline at end of file diff --git a/experiments/dsp/main.py b/experiments/dsp/main.py index ff800e2..cf188df 100644 --- a/experiments/dsp/main.py +++ b/experiments/dsp/main.py @@ -1,4 +1,4 @@ -import sys, os, json +import sys, os, json, subprocess from dataclasses import dataclass from pathlib import Path from typing import Union, Any, Tuple @@ -221,8 +221,14 @@ def full_proof_search_dsp_lean( server.gc() return + experiment_dir = Path(__file__).resolve().parent +def get_project_and_lean_path(): + cwd = experiment_dir / 'lean_src_proj' + p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd) + return cwd, p + # -- Main def main(args): @@ -231,7 +237,12 @@ def main(args): path_2_eval_dataset = Path(args.eval_dataset).expanduser() print(f'{path_2_eval_dataset=}') - server = Server() + project_path, lean_path = get_project_and_lean_path() + server = Server( + imports=["Mathlib", "Aesop"], + project_path=project_path, + lean_path=lean_path, + ) # - Start wandb run # print(f'\n\n-- Setup params') diff --git a/experiments/dsp/solve/prove.py b/experiments/dsp/solve/prove.py index 5ac032a..ddcc4b4 100644 --- a/experiments/dsp/solve/prove.py +++ b/experiments/dsp/solve/prove.py @@ -17,8 +17,7 @@ class HammerAgent(Agent): self, state: GoalState, goal_id: int, - informal_stmt: str, - informal_proof: str) -> Optional[Tactic]: + ) -> Optional[Tactic]: key = (state.state_id, goal_id) i = self.goal_tactic_id_map[key]