feat: add test suite depending on mathlib

test.sh

@@ -34,3 +34,6 @@ for infile in $IN_DIR/*.in; do
     # Remove the temporary file
     rm "$tmpfile"
 done
+
+# Run the Mathlib tests
+cd test/Mathlib/ && ./test.sh

test/Mathlib/.gitignore

@@ -0,0 +1,5 @@
+/build
+/lake-packages/*
+/lakefile.olean
+/test/*.olean
+/test/*.olean.tmp

test/Mathlib/ReplMathlibTests/20231025.lean

@@ -0,0 +1,10 @@
+import Mathlib.Data.Real.Basic
+
+open Real
+
+variable (x y : ℝ)
+variable (f : ℝ → ℝ)
+
+theorem problem (h0 : f 5 = 3) (h1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))) :
+    ∃ (k : ℝ), f 2015 = k := by
+  sorry

test/Mathlib/lake-manifest.json

@@ -0,0 +1,52 @@
+{"version": 6,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/leanprover-community/mathlib4",
+    "subDir?": null,
+    "rev": "1a79f4b2854dea6dc7a133543f0a140d4138cc58",
+    "opts": {},
+    "name": "mathlib",
+    "inputRev?": "master",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "fb56324020c8e4f3d451e8901b290dea82c072ae",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/quote4",
+    "subDir?": null,
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "opts": {},
+    "name": "Qq",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "9dc4a1097a690216eaa7cf2d2290efd447e60d7a",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/lean4-cli",
+    "subDir?": null,
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
+    "subDir?": null,
+    "rev": "5382e38eca1e2537d75d4c4705a9e744424b0037",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.19",
+    "inherited": true}}],
+ "name": "«repl-mathlib-tests»"}

test/Mathlib/lakefile.lean

@@ -0,0 +1,9 @@
+import Lake
+open Lake DSL
+
+package «repl-mathlib-tests» where
+  -- add package configuration options here
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
+
+lean_lib «ReplMathlibTests» where
+  -- add library configuration options here

test/Mathlib/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.2.0-rc4

test/Mathlib/test.sh

@@ -0,0 +1,38 @@
+#!/bin/bash
+
+# Define the paths
+IN_DIR="test"
+EXPECTED_DIR="test"
+
+lake exe cache get > /dev/null
+lake build
+
+# Iterate over each .in file in the test directory
+for infile in $IN_DIR/*.in; do
+    # Extract the base filename without the extension
+    base=$(basename "$infile" .in)
+
+    # Define the path for the expected output file
+    expectedfile="$EXPECTED_DIR/$base.expected.out"
+
+    # Check if the expected output file exists
+    if [[ ! -f $expectedfile ]]; then
+        echo "Expected output file $expectedfile does not exist. Skipping $infile."
+        continue
+    fi
+
+    # Run the command and store its output in a temporary file
+    tmpfile=$(mktemp)
+    lake env ../../build/bin/repl < "$infile" > "$tmpfile" 2>&1
+
+    # Compare the output with the expected output
+    if diff "$tmpfile" "$expectedfile"; then
+        echo "$base: PASSED"
+    else
+        echo "$base: FAILED"
+    fi
+
+    # Remove the temporary file
+    rm "$tmpfile"
+done
+

test/Mathlib/test/H20231020.expected.out

@@ -0,0 +1,8 @@
+{"env": 0}
+
+{"env": 1}
+
+{"env": 2}
+
+{"env": 3}
+

test/Mathlib/test/H20231020.in

@@ -0,0 +1,8 @@
+{"cmd": "import Mathlib.Algebra.BigOperators.Basic\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.Complex.Basic\nimport Mathlib.Data.Nat.Log\nimport Mathlib.Data.Complex.Exponential\nimport Mathlib.NumberTheory.Divisors\nimport Mathlib.Data.ZMod.Defs\nimport Mathlib.Data.ZMod.Basic\nimport Mathlib.Topology.Basic\nimport Mathlib.Data.Nat.Digits\nopen BigOperators\nopen Real\nopen Nat\nopen Topology"}
+
+{"cmd": "theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num", "env": 0}
+
+{"cmd": "theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp", "env": 0}
+
+{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw [h₀]", "env": 0}
+