The Lean 4 read-eval-print loop (REPL)

[karlcuinju]

Could you please share more information about how to develop the REPL, I tried to use repl but still can not run successfully...

[objecti0n]

How do you use repl to check the correctness of our LEAN-Workbook? For our implemented repl, we are still working on organizing the source codes.

[objecti0n]

Our lean4repl implementation is basically based on LeanDojo/src/lean_dojo/interaction/Lean4Repl.lean at main · lean-dojo/LeanDojo (github.com). To use this repl, just include the file as a lean_lib dependency in your lakefile.lean

[karlcuinju]

How do you use repl to check the correctness of our LEAN-Workbook? For our implemented repl, we are still working on organizing the source codes.

I just concat the header (mentioned here), formal_statement and formal proof (sample one from proof list), and communicate with repl. Then get an error like "unknown namespace 'BigOperators'", "unknown namespace 'Nat'" and so on.

Here is an example

import Mathlib.Algebra.Algebra.Basic
import Mathlib.Algebra.Order.Floor
import Mathlib.Algebra.Associated
import Mathlib.Algebra.BigOperators.Basic

import Mathlib.Algebra.BigOperators.Pi
import Mathlib.Algebra.GeomSum
import Mathlib.Algebra.Group.Pi.Basic
import Mathlib.Algebra.Group.Pi.Lemmas
import Mathlib.Algebra.Group.Commute.Basic
import Mathlib.Algebra.Group.Commute.Defs
import Mathlib.Algebra.Group.Commute.Hom
import Mathlib.Algebra.Group.Commute.Units
import Mathlib.Algebra.GroupPower.Basic
import Mathlib.Algebra.GroupPower.Identities
import Mathlib.Algebra.Order.Floor
import Mathlib.Algebra.QuadraticDiscriminant
import Mathlib.Algebra.Ring.Basic
import Mathlib.Analysis.MeanInequalitiesPow
import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Exponential
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fintype.Card

import Mathlib.Data.Int.GCD
import Mathlib.Data.Int.ModEq
import Mathlib.Data.Int.Parity
import Mathlib.Data.List.Intervals
import Mathlib.Data.List.Palindrome
import Mathlib.Data.Multiset.Basic

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Digits
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Data.Nat.Fib.Basic
import Mathlib.Data.Nat.Fib.Zeckendorf
import Mathlib.Data.Nat.ModEq
import Mathlib.Data.Nat.Multiplicity
import Mathlib.Data.Nat.Parity
import Mathlib.Data.Nat.Prime
import Mathlib.Data.PNat.Basic
import Mathlib.Data.PNat.Prime

import Mathlib.Data.Rat.BigOperators
import Mathlib.Data.Rat.Cast.CharZero
import Mathlib.Data.Rat.Cast.Defs
import Mathlib.Data.Rat.Cast.Lemmas
import Mathlib.Data.Rat.Cast.Order
import Mathlib.Data.Rat.Defs
import Mathlib.Data.Rat.Denumerable
import Mathlib.Data.Rat.Encodable
import Mathlib.Data.Rat.Field
import Mathlib.Data.Rat.Floor
import Mathlib.Data.Rat.Init
import Mathlib.Data.Rat.Lemmas
import Mathlib.Data.Rat.Order
import Mathlib.Data.Rat.Sqrt

import Mathlib.Data.Rat.Star
import Mathlib.Data.Real.Basic
import Mathlib.Data.ENNReal.Basic
import Mathlib.Data.ENNReal.Inv
import Mathlib.Data.ENNReal.Operations
import Mathlib.Data.ENNReal.Real
import Mathlib.Data.Real.ENatENNReal
import Mathlib.Data.Real.Irrational
import Mathlib.Data.Real.NNReal
import Mathlib.Data.Real.Sqrt

import Mathlib.Data.Set.Finite
import Mathlib.Data.Sym.Sym2
import Mathlib.Data.ZMod.Basic
import Mathlib.Dynamics.FixedPoints.Basic

import Mathlib.LinearAlgebra.AffineSpace.AffineMap
import Mathlib.LinearAlgebra.AffineSpace.Independent
import Mathlib.LinearAlgebra.AffineSpace.Ordered
import Mathlib.LinearAlgebra.FiniteDimensional
import Mathlib.Logic.Equiv.Basic

import Mathlib.Order.Filter.Basic

import Mathlib.Order.WellFounded
import Mathlib.Topology.Basic
import Mathlib.Topology.Instances.NNReal

import Mathlib.Data.ZMod.Basic
import Mathlib.RingTheory.Int.Basic


import Aesop
import ProofWidgets
open BigOperators

open Nat

open Real

open Rat
theorem lean_workbook_18 :
  (29 * 31 + 37 - 41) % 4 = 3  :=  by 
    simp [Nat.mod_lt]

lake exe repl

{"cmd":"import Mathlib.Algebra.Algebra.Basic\nimport Mathlib.Algebra.Order.Floor\nimport Mathlib.Algebra.Associated\nimport Mathlib.Algebra.BigOperators.Basic\n\nimport Mathlib.Algebra.BigOperators.Pi\nimport Mathlib.Algebra.GeomSum\nimport Mathlib.Algebra.Group.Pi.Basic\nimport Mathlib.Algebra.Group.Pi.Lemmas\nimport Mathlib.Algebra.Group.Commute.Basic\nimport Mathlib.Algebra.Group.Commute.Defs\nimport Mathlib.Algebra.Group.Commute.Hom\nimport Mathlib.Algebra.Group.Commute.Units\nimport Mathlib.Algebra.GroupPower.Basic\nimport Mathlib.Algebra.GroupPower.Identities\nimport Mathlib.Algebra.Order.Floor\nimport Mathlib.Algebra.QuadraticDiscriminant\nimport Mathlib.Algebra.Ring.Basic\nimport Mathlib.Analysis.MeanInequalitiesPow\nimport Mathlib.Analysis.Asymptotics.AsymptoticEquivalent\nimport Mathlib.Analysis.NormedSpace.Basic\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\nimport Mathlib.Analysis.SpecialFunctions.Log.Base\nimport Mathlib.Combinatorics.SimpleGraph.Basic\nimport Mathlib.Data.Complex.Basic\nimport Mathlib.Data.Complex.Exponential\nimport Mathlib.Data.Finset.Basic\nimport Mathlib.Data.Fintype.Card\n\nimport Mathlib.Data.Int.GCD\nimport Mathlib.Data.Int.ModEq\nimport Mathlib.Data.Int.Parity\nimport Mathlib.Data.List.Intervals\nimport Mathlib.Data.List.Palindrome\nimport Mathlib.Data.Multiset.Basic\n\nimport Mathlib.Data.Nat.Choose.Basic\nimport Mathlib.Data.Nat.Digits\nimport Mathlib.Data.Nat.Factorial.Basic\nimport Mathlib.Data.Nat.Fib.Basic\nimport Mathlib.Data.Nat.Fib.Zeckendorf\nimport Mathlib.Data.Nat.ModEq\nimport Mathlib.Data.Nat.Multiplicity\nimport Mathlib.Data.Nat.Parity\nimport Mathlib.Data.Nat.Prime\nimport Mathlib.Data.PNat.Basic\nimport Mathlib.Data.PNat.Prime\n\nimport Mathlib.Data.Rat.BigOperators\nimport Mathlib.Data.Rat.Cast.CharZero\nimport Mathlib.Data.Rat.Cast.Defs\nimport Mathlib.Data.Rat.Cast.Lemmas\nimport Mathlib.Data.Rat.Cast.Order\nimport Mathlib.Data.Rat.Defs\nimport Mathlib.Data.Rat.Denumerable\nimport Mathlib.Data.Rat.Encodable\nimport Mathlib.Data.Rat.Field\nimport Mathlib.Data.Rat.Floor\nimport Mathlib.Data.Rat.Init\nimport Mathlib.Data.Rat.Lemmas\nimport Mathlib.Data.Rat.Order\nimport Mathlib.Data.Rat.Sqrt\n\nimport Mathlib.Data.Rat.Star\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.ENNReal.Basic\nimport Mathlib.Data.ENNReal.Inv\nimport Mathlib.Data.ENNReal.Operations\nimport Mathlib.Data.ENNReal.Real\nimport Mathlib.Data.Real.ENatENNReal\nimport Mathlib.Data.Real.Irrational\nimport Mathlib.Data.Real.NNReal\nimport Mathlib.Data.Real.Sqrt\n\nimport Mathlib.Data.Set.Finite\nimport Mathlib.Data.Sym.Sym2\nimport Mathlib.Data.ZMod.Basic\nimport Mathlib.Dynamics.FixedPoints.Basic\n\nimport Mathlib.LinearAlgebra.AffineSpace.AffineMap\nimport Mathlib.LinearAlgebra.AffineSpace.Independent\nimport Mathlib.LinearAlgebra.AffineSpace.Ordered\nimport Mathlib.LinearAlgebra.FiniteDimensional\nimport Mathlib.Logic.Equiv.Basic\n\nimport Mathlib.Order.Filter.Basic\n\nimport Mathlib.Order.WellFounded\nimport Mathlib.Topology.Basic\nimport Mathlib.Topology.Instances.NNReal\n\nimport Mathlib.Data.ZMod.Basic\nimport Mathlib.RingTheory.Int.Basic\n\n\nimport Aesop\nimport ProofWidgets\nopen BigOperators\n\nopen Nat\n\nopen Real\n\nopen Rat\ntheorem lean_workbook_18 :\n  (29 * 31 + 37 - 41) % 4 = 3  :=  by \n    simp [Nat.mod_lt]"}

error message

{"messages":
 [{"severity": "error",
   "pos": {"line": 98, "column": 5},
   "endPos": {"line": 98, "column": 17},
   "data": "unknown namespace 'BigOperators'"},
  {"severity": "error",
   "pos": {"line": 100, "column": 5},
   "endPos": {"line": 100, "column": 8},
   "data": "unknown namespace 'Nat'"},
  {"severity": "error",
   "pos": {"line": 102, "column": 5},
   "endPos": {"line": 102, "column": 9},
   "data": "unknown namespace 'Real'"},
  {"severity": "error",
   "pos": {"line": 104, "column": 5},
   "endPos": {"line": 104, "column": 8},
   "data": "unknown namespace 'Rat'"},
  {"severity": "error",
   "pos": {"line": 106, "column": 5},
   "endPos": {"line": 106, "column": 7},
   "data": "unexpected token '*'; expected ')', ',' or ':'"}],
 "env": 0}

Do I use the LEAN-Workbook in the right way or maybe my repl env has something wrong

[wzj423]

Well that seems to be an issue of Lean4 version. Our environment is built upon Lean v4.7.0 and its corresponding mathlib version. (See https://huggingface.co/datasets/internlm/Lean-Workbook/discussions/1#66630d2a8be3eff79febfdc5 for more information). The imports has some changes in newer version of Lean (e.g. Mathlib.Algebra.BigOperators.Basic is removed). So the code won't compile if you are using versions other than v4.7.0.

[karlcuinju]

Well that seems to be an issue of Lean4 version. Our environment is built upon Lean v4.7.0 and its corresponding mathlib version. (See https://huggingface.co/datasets/internlm/Lean-Workbook/discussions/1#66630d2a8be3eff79febfdc5 for more information). The imports has some changes in newer version of Lean (e.g. Mathlib.Algebra.BigOperators.Basic is removed). So the code won't compile if you are using versions other than v4.7.0.

Thanks a lot, I change the Lean version to v4.7.0, it works!