From 5e241ab0bc49c5971b5483aba3b6824cc0bb0fc2 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Tue, 2 Aug 2022 12:15:06 +0200 Subject: [PATCH 1/4] Try to update to recente Lean+lake --- .gitignore | 4 +++- Gym.lean => LeanGym.lean | 30 ++++++++++++------------------ Main.lean | 10 ++++++++++ Makefile | 12 ------------ lakefile.lean | 15 +++++++++++++++ lean-toolchain | 1 + leanpkg.toml | 4 ---- 7 files changed, 41 insertions(+), 35 deletions(-) rename Gym.lean => LeanGym.lean (87%) create mode 100644 Main.lean delete mode 100644 Makefile create mode 100644 lakefile.lean create mode 100644 lean-toolchain delete mode 100644 leanpkg.toml diff --git a/.gitignore b/.gitignore index ae7bf13..6370dc3 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,6 @@ /build *~ *#* -lean-gym \ No newline at end of file +lean-gym/build +/lean_packages/* +!/lean_packages/manifest.json diff --git a/Gym.lean b/LeanGym.lean similarity index 87% rename from Gym.lean rename to LeanGym.lean index 5c228ff..dc711b4 100644 --- a/Gym.lean +++ b/LeanGym.lean @@ -81,8 +81,6 @@ partial def replFor (problem : Problem) : IO Unit := do (welcome *> repl).run context |>.run' state let termElabCtx : Term.Context := { - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] }, declName? := some (problem.decl ++ "_gym_"), errToSorry := false } @@ -91,7 +89,11 @@ partial def replFor (problem : Problem) : IO Unit := do let coreM : CoreM Unit := metaM.run' let env ← importModules problem.imports {} 0 - let coreCtx : Core.Context := { currNamespace := problem.currNamespace, openDecls := problem.openDecls } + let coreCtx : Core.Context := { + currNamespace := problem.currNamespace, + openDecls := problem.openDecls, + fileName := "", + fileMap := { source := "", positions := #[0], lines := #[1] } } let coreState : Core.State := { env := env } let ((), _) ← coreM.toIO coreCtx coreState @@ -101,15 +103,15 @@ where welcome : GymM Unit := do println! "{toJson (← responseForBranch 0)}" - ppTacticState (s : Tactic.SavedState) : GymM Format := do +/- ppTacticState (s : Tactic.SavedState) : GymM Format := do let mut result : Format := Format.nil for goal in s.tactic.goals do result := result ++ "\n-----\n" ++ (← Meta.ppGoal goal) - return result + return result -/ responseForBranch (id : BranchId) : GymM Response := do let some savedState ← pure ((← get).branches.find? id) | throwError "invalid branch id: {id}" - let goals ← savedState.tactic.goals.mapM fun g => do toString (← Meta.ppGoal g) + let goals ← savedState.tactic.goals.mapM fun g => do pure $ toString (← Meta.ppGoal g) pure { branchId := id, goals := goals.toArray } repl : GymM Unit := do @@ -141,8 +143,8 @@ where let mvarId : MVarId := savedState.tactic.goals.head! try let unsolvedGoals ← Tactic.run mvarId tac - if (← getThe Term.State).messages.hasErrors then - let messages ← (← getThe Term.State).messages.getErrorMessages.toList.toArray + if (← getThe Core.State).messages.hasErrors then + let messages := (← getThe Core.State).messages.getErrorMessages.toList.toArray pure { errors := ← (messages.map Message.data).mapM fun md => md.toString } else let nextId := (← get).nextId @@ -152,20 +154,12 @@ where catch ex => pure { errors := #[← ex.toMessageData.toString] } - parseNat (s : String) : GymM Nat := + /- parseNat (s : String) : GymM Nat := match s.toNat? with | some k => pure k - | none => throwError "String '{s}' cannot be converted to Nat" + | none => throwError "String '{s}' cannot be converted to Nat" -/ end Gym def parseName (n : String) : Lean.Name := (n.splitOn ".").foldl Lean.Name.mkStr Lean.Name.anonymous - -def main (args : List String) : IO Unit := do - let some LEAN_PATH ← IO.getEnv "LEAN_PATH" | throw (IO.userError "LEAN_PATH not set") - initSearchPath LEAN_PATH - let [decl] ← pure args | throw (IO.userError "usage: lean-gym ") - let decl := parseName decl - let problem : Gym.Problem := { decl := decl, currNamespace := decl.getRoot } - Gym.replFor problem diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..1885b97 --- /dev/null +++ b/Main.lean @@ -0,0 +1,10 @@ +import LeanGym + +open Lean Lean.Meta Lean.Elab Lean.Elab.Tactic + +def main (args : List String) : IO Unit := do + initSearchPath (← findSysroot) + let [decl] ← pure args | throw (IO.userError "usage: lean-gym ") + let decl := parseName decl + let problem : Gym.Problem := { decl := decl, currNamespace := decl.getRoot } + Gym.replFor problem diff --git a/Makefile b/Makefile deleted file mode 100644 index 01e5ab8..0000000 --- a/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -PKG = Gym -include $(LEAN4_S1_MK) -all: gym - -GymEXE=lean-gym -LEAN4_PATH=$(LEAN4_S1_LIB) - -gym: $(BIN_OUT)/test - cp $(BIN_OUT)/test $(GymEXE) - -$(BIN_OUT)/test: $(LIB_OUT)/libGym.a $(CPP_OBJS) | $(BIN_OUT) - c++ -rdynamic -o $@ $^ `leanc --print-ldflags` diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..d12fa74 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,15 @@ +import Lake +open Lake DSL + +package «lean-gym» { + -- add package configuration options here +} + +lean_lib LeanGym { + -- add library configuration options here +} + +@[defaultTarget] +lean_exe «lean-gym» { + root := `Main +} diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..07a1c54 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2022-07-31 diff --git a/leanpkg.toml b/leanpkg.toml deleted file mode 100644 index 411e75c..0000000 --- a/leanpkg.toml +++ /dev/null @@ -1,4 +0,0 @@ -[package] -name = "Gym" -version = "0.1" -lean_version = "leanprover/lean4:master" From dfed8fa392db87f917763a9e96ef600be7560bbf Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Tue, 2 Aug 2022 12:57:10 +0200 Subject: [PATCH 2/4] Fix lakefile --- lakefile.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/lakefile.lean b/lakefile.lean index d12fa74..534e520 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,4 +12,5 @@ lean_lib LeanGym { @[defaultTarget] lean_exe «lean-gym» { root := `Main + supportInterpreter := true } From 9c463bc33393e630b12e49ca5a70c06eeb480edb Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Tue, 2 Aug 2022 12:59:32 +0200 Subject: [PATCH 3/4] Move explanations to README --- README.md | 29 ++++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index a92ff5c..6ba781a 100644 --- a/README.md +++ b/README.md @@ -1 +1,28 @@ -# lean-gym \ No newline at end of file +# lean-gym + +An extremely bare-bones REPL for proving in Lean4. + +Usage: `lean-gym ` will load `Init` and start a proving environment for `declName` +which expects commands in the form of ` ` + +It is straightforward to extend this to also take: +- module imports +- open declarations +- the current namespace + +However, there is currently no way to import *until* a given declaration. +We also currently do no checking that the proof avoids circularity. + +Note: unlike most RL environments, we use persistent datastructures and +so we store all active tactic states rather than relying on the user +to recompute each path on every action. + +Example (circular) run of `lean-gym Nat.add_comm`: + +``` +{"goals": ["⊢ ∀ (n m : Nat), n + m = m + n"], "errors": [], "branchId": 0} +> {"runTactic": [0, "intro n m"]} +{"goals": ["n m : Nat\n⊢ n + m = m + n"], "errors": [], "branchId": 1} +> {"runTactic": [1, "rw [Nat.add_comm]"]} +{"goals": [], "errors": [], "branchId": 2} +``` \ No newline at end of file From 3fa8c5f6c871617e8c062c439096b0c9d49f47be Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Tue, 2 Aug 2022 13:00:36 +0200 Subject: [PATCH 4/4] Compilation instructions --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 6ba781a..33cba84 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # lean-gym -An extremely bare-bones REPL for proving in Lean4. +An extremely bare-bones REPL for proving in Lean4. Compile as usual with `lake build`. This will produce a `lean-gym` executable in a `build/bin` folder. Usage: `lean-gym ` will load `Init` and start a proving environment for `declName` which expects commands in the form of ` ` @@ -25,4 +25,4 @@ Example (circular) run of `lean-gym Nat.add_comm`: {"goals": ["n m : Nat\n⊢ n + m = m + n"], "errors": [], "branchId": 1} > {"runTactic": [1, "rw [Nat.add_comm]"]} {"goals": [], "errors": [], "branchId": 2} -``` \ No newline at end of file +```