search

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
80 stars 21 forks source link

Bug for long commands #36

Closed xinhjBrant closed 8 months ago

xinhjBrant commented 8 months ago

When the command is too long to be parsed by Lean 4 JSON parser (e.g. a whole Mathlib file), the REPL will throw an exception. Here is an example:

>>> lake exe repl
{"cmd": "/-\nCopyright (c) 2018 Kenny Lau. All rights reserved.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthors: Kenny Lau, Yury Kudryashov\n-/\nimport Mathlib.Algebra.Algebra.Basic\nimport Mathlib.Algebra.Algebra.NonUnitalHom\nimport Mathlib.Algebra.GroupPower.IterateHom\nimport Mathlib.LinearAlgebra.TensorProduct\n\n#align_import algebra.algebra.bilinear from \"leanprover-community/mathlib\"@\"657df4339ae6ceada048c8a2980fb10e393143ec\"\n\n/-!\n# Facts about algebras involving bilinear maps and tensor products\n\nWe move a few basic statements about algebras out of `Algebra.Algebra.Basic`,\nin order to avoid importing `LinearAlgebra.BilinearMap` and\n`LinearAlgebra.TensorProduct` unnecessarily.\n-/\n\nopen TensorProduct Module\n\nnamespace LinearMap\n\nsection RestrictScalars\n\nvariable\n  (R : Type*) {A M N P : Type*}\n  [CommSemiring R] [CommSemiring A]\n  [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]\n  [Algebra R A]\n  [Module R M] [Module R N] [Module R P]\n  [Module A M] [Module A N] [Module A P]\n  [IsScalarTower R A M] [IsScalarTower R A N] [IsScalarTower R A P]\n\n/-- A version of `LinearMap.restrictScalars` for bilinear maps.\n\nThe double subscript in the name is to match `LinearMap.compl₁₂`. -/\n@[simps!]\ndef restrictScalars₁₂ (f : M →ₗ[A] N →ₗ[A] P) : M →ₗ[R] N →ₗ[R] P :=\n  (f.flip.restrictScalars _).flip.restrictScalars _\n\nend RestrictScalars\n\nsection NonUnitalNonAssoc\n\nvariable (R A : Type*) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A]\n  [SMulCommClass R A A] [IsScalarTower R A A]\n\n/-- The multiplication in a non-unital non-associative algebra is a bilinear map.\n\nA weaker version of this for semirings exists as `AddMonoidHom.mul`. -/\ndef mul : A →ₗ[R] A →ₗ[R] A :=\n  LinearMap.mk₂ R (· * ·) add_mul smul_mul_assoc mul_add mul_smul_comm\n#align linear_map.mul LinearMap.mul\n\n/-- The multiplication map on a non-unital algebra, as an `R`-linear map from `A ⊗[R] A` to `A`. -/\nnoncomputable def mul' : A ⊗[R] A →ₗ[R] A :=\n  TensorProduct.lift (mul R A)\n#align linear_map.mul' LinearMap.mul'\n\nvariable {A}\n\n/-- The multiplication on the left in a non-unital algebra is a linear map. -/\ndef mulLeft (a : A) : A →ₗ[R] A :=\n  mul R A a\n#align linear_map.mul_left LinearMap.mulLeft\n\n/-- The multiplication on the right in an algebra is a linear map. -/\ndef mulRight (a : A) : A →ₗ[R] A :=\n  (mul R A).flip a\n#align linear_map.mul_right LinearMap.mulRight\n\n/-- Simultaneous multiplication on the left and right is a linear map. -/\ndef mulLeftRight (ab : A × A) : A →ₗ[R] A :=\n  (mulRight R ab.snd).comp (mulLeft R ab.fst)\n#align linear_map.mul_left_right LinearMap.mulLeftRight\n\n@[simp]\ntheorem mulLeft_toAddMonoidHom (a : A) : (mulLeft R a : A →+ A) = AddMonoidHom.mulLeft a :=\n  rfl\n#align linear_map.mul_left_to_add_monoid_hom LinearMap.mulLeft_toAddMonoidHom\n\n@[simp]\ntheorem mulRight_toAddMonoidHom (a : A) : (mulRight R a : A →+ A) = AddMonoidHom.mulRight a :=\n  rfl\n#align linear_map.mul_right_to_add_monoid_hom LinearMap.mulRight_toAddMonoidHom\n\nvariable {R}\n\n@[simp]\ntheorem mul_apply' (a b : A) : mul R A a b = a * b :=\n  rfl\n#align linear_map.mul_apply' LinearMap.mul_apply'\n\n@[simp]\ntheorem mulLeft_apply (a b : A) : mulLeft R a b = a * b :=\n  rfl\n#align linear_map.mul_left_apply LinearMap.mulLeft_apply\n\n@[simp]\ntheorem mulRight_apply (a b : A) : mulRight R a b = b * a :=\n  rfl\n#align linear_map.mul_right_apply LinearMap.mulRight_apply\n\n@[simp]\ntheorem mulLeftRight_apply (a b x : A) : mulLeftRight R (a, b) x = a * x * b :=\n  rfl\n#align linear_map.mul_left_right_apply LinearMap.mulLeftRight_apply\n\n@[simp]\ntheorem mul'_apply {a b : A} : mul' R A (a ⊗ₜ b) = a * b :=\n  rfl\n#align linear_map.mul'_apply LinearMap.mul'_apply\n\n@[simp]\ntheorem mulLeft_zero_eq_zero : mulLeft R (0 : A) = 0 :=\n  (mul R A).map_zero\n#align linear_map.mul_left_zero_eq_zero LinearMap.mulLeft_zero_eq_zero\n\n@[simp]\ntheorem mulRight_zero_eq_zero : mulRight R (0 : A) = 0 :=\n  (mul R A).flip.map_zero\n#align linear_map.mul_right_zero_eq_zero LinearMap.mulRight_zero_eq_zero\n\nend NonUnitalNonAssoc\n\nsection NonUnital\n\nvariable (R A : Type*) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A]\n  [IsScalarTower R A A]\n\n/-- The multiplication in a non-unital algebra is a bilinear map.\n\nA weaker version of this for non-unital non-associative algebras exists as `LinearMap.mul`. -/\ndef _root_.NonUnitalAlgHom.lmul : A →ₙₐ[R] End R A :=\n  { mul R A with\n    map_mul' := by\n      intro a b\n      ext c\n      exact mul_assoc a b c\n    map_zero' := by\n      ext a\n      exact zero_mul a }\n#align non_unital_alg_hom.lmul NonUnitalAlgHom.lmul\n\nvariable {R A}\n\n@[simp]\ntheorem _root_.NonUnitalAlgHom.coe_lmul_eq_mul : ⇑(NonUnitalAlgHom.lmul R A) = mul R A :=\n  rfl\n#align non_unital_alg_hom.coe_lmul_eq_mul NonUnitalAlgHom.coe_lmul_eq_mul\n\ntheorem commute_mulLeft_right (a b : A) : Commute (mulLeft R a) (mulRight R b) := by\n  ext c\n  exact (mul_assoc a c b).symm\n#align linear_map.commute_mul_left_right LinearMap.commute_mulLeft_right\n\n@[simp]\ntheorem mulLeft_mul (a b : A) : mulLeft R (a * b) = (mulLeft R a).comp (mulLeft R b) := by\n  ext\n  simp only [mulLeft_apply, comp_apply, mul_assoc]\n#align linear_map.mul_left_mul LinearMap.mulLeft_mul\n\n@[simp]\ntheorem mulRight_mul (a b : A) : mulRight R (a * b) = (mulRight R b).comp (mulRight R a) := by\n  ext\n  simp only [mulRight_apply, comp_apply, mul_assoc]\n#align linear_map.mul_right_mul LinearMap.mulRight_mul\n\nend NonUnital\n\nsection Semiring\n\nvariable (R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]\n\nvariable {R A B} in\n/-- A `LinearMap` preserves multiplication if pre- and post- composition with `LinearMap.mul` are\nequivalent. By converting the statement into an equality of `LinearMap`s, this lemma allows various\nspecialized `ext` lemmas about `→ₗ[R]` to then be applied.\n\nThis is the `LinearMap` version of `AddMonoidHom.map_mul_iff`. -/\ntheorem map_mul_iff (f : A →ₗ[R] B) :\n    (∀ x y, f (x * y) = f x * f y) ↔\n      (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f :=\n  Iff.symm LinearMap.ext_iff₂\n\n/-- The multiplication in an algebra is an algebra homomorphism into the endomorphisms on\nthe algebra.\n\nA weaker version of this for non-unital algebras exists as `NonUnitalAlgHom.mul`. -/\ndef _root_.Algebra.lmul : A →ₐ[R] End R A :=\n  { LinearMap.mul R A with\n    map_one' := by\n      ext a\n      exact one_mul a\n    map_mul' := by\n      intro a b\n      ext c\n      exact mul_assoc a b c\n    map_zero' := by\n      ext a\n      exact zero_mul a\n    commutes' := by\n      intro r\n      ext a\n      exact (Algebra.smul_def r a).symm }\n#align algebra.lmul Algebra.lmul\n\nvariable {R A}\n\n@[simp]\ntheorem _root_.Algebra.coe_lmul_eq_mul : ⇑(Algebra.lmul R A) = mul R A :=\n  rfl\n#align algebra.coe_lmul_eq_mul Algebra.coe_lmul_eq_mul\n\ntheorem _root_.Algebra.lmul_injective : Function.Injective (Algebra.lmul R A) :=\n  fun a₁ a₂ h ↦ by simpa using DFunLike.congr_fun h 1\n\ntheorem _root_.Algebra.lmul_isUnit_iff {x : A} :\n    IsUnit (Algebra.lmul R A x) ↔ IsUnit x := by\n  rw [Module.End_isUnit_iff, Iff.comm]\n  exact IsUnit.isUnit_iff_mulLeft_bijective\n\n@[simp]\ntheorem mulLeft_eq_zero_iff (a : A) : mulLeft R a = 0 ↔ a = 0 := by\n  constructor <;> intro h\n  -- porting note: had to supply `R` explicitly in `@mulLeft_apply` below\n  · rw [← mul_one a, ← @mulLeft_apply R _ _ _ _ _ _ a 1, h, LinearMap.zero_apply]\n  · rw [h]\n    exact mulLeft_zero_eq_zero\n#align linear_map.mul_left_eq_zero_iff LinearMap.mulLeft_eq_zero_iff\n\n@[simp]\ntheorem mulRight_eq_zero_iff (a : A) : mulRight R a = 0 ↔ a = 0 := by\n  constructor <;> intro h\n  -- porting note: had to supply `R` explicitly in `@mulRight_apply` below\n  · rw [← one_mul a, ← @mulRight_apply R _ _ _ _ _ _ a 1, h, LinearMap.zero_apply]\n  · rw [h]\n    exact mulRight_zero_eq_zero\n#align linear_map.mul_right_eq_zero_iff LinearMap.mulRight_eq_zero_iff\n\n@[simp]\ntheorem mulLeft_one : mulLeft R (1 : A) = LinearMap.id := by\n  ext\n  simp only [LinearMap.id_coe, one_mul, id.def, mulLeft_apply]\n#align linear_map.mul_left_one LinearMap.mulLeft_one\n\n@[simp]\ntheorem mulRight_one : mulRight R (1 : A) = LinearMap.id := by\n  ext\n  simp only [LinearMap.id_coe, mul_one, id.def, mulRight_apply]\nend Semiring\n\nend LinearMap"}

uncaught exception: {"message":
 "Could not parse JSON:\noffset 4096: unexpected character in string"}

Is it possible to solve this problem?

kim-em commented 8 months ago

Sorry, I didn't see this. Did you find a solution?

xinhjBrant commented 7 months ago

Sorry, I didn't see this. Did you find a solution?

Yes, I managed to use input redirection to avoid this command-line restriction in Linux.