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/README.md b/README.md index a92ff5c..33cba84 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. 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 ` ` + +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} +``` diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..534e520 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,16 @@ +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 + supportInterpreter := true +} 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"