Update extract.lean

extract.lean

@@ -10,26 +10,30 @@ open Lean.Elab
 open Lean.Elab.Command
 
 /-
-This file is modified from: https://github.com/semorrison/lean-training-data
+This small file is modified from: https://github.com/semorrison/lean-training-data
+You can refer to the file structure there for more details.
+To run this, there is no need to download another 4GB of Mathlib files.
+Just prepare a Lean project with Mathlib installed. Suppose the project is in the folder LeanProj.
+Your Mathlib files should live in LeanProj/.lake/packages/mathlib.
+My LeanProj/lean-toolchain says I am using version: leanprover/lean4:v4.9.0-rc2
 
-To run this, prepare a Lean project with Mathlib installed. Suppose the project is called LeanProj.
-
-Put this extract.lean in LeanProj/scripts/extract.lean
+Now, put this extract.lean in LeanProj/scripts/extract.lean
 
 In LeanProj/lakefile.lean, below
 @[default_target]
 lean_lib «LeanProj» where
-```,
 
 add this:
 @[default_target]
 lean_exe extract where
   root := `scripts.extract
   supportInterpreter := true
-```
+
+This will make the `lake exe extract` command available,
+and enable the correct `compile_time_search_path%` in the script.
 
 Now in the terminal, run:
-cd LeanProj
+cd path-to-LeanProj
 mkdir data
 lake exe extract > data/theorems.txt
 
@@ -63,7 +67,10 @@ def main : IO Unit := do
   IO.eprintln "\n\n"
   IO.eprintln "importing modules"
   searchPathRef.set compile_time_search_path%
-  CoreM.withImportModules #[`Mathlib] do
+  CoreM.withImportModules #[`Mathlib] (options := {entries := [
+    -- (`maxHeartbeats, .ofNat 0),
+    (`smartUnfolding, .ofBool false),
+  ]}) do
     IO.eprintln s!"simplification timeout: {← getMaxHeartbeats}"
     let env ← getEnv
 
@@ -83,38 +90,38 @@ def main : IO Unit := do
       -- name.toString.startsWith "Nat.add"
     IO.eprintln s!"printing {lst.size} theorems"
     for (name, info) in lst do
-      IO.println "----ast----"
+      IO.println "----thm----"
       -- print module.
       -- eg. "import Mathlib.Data.Real.Basic"
       match (← findModuleOf? name) with
       | .none => IO.println "unknown"
       | .some mod => IO.println s!"import {mod}"
-      IO.println "--ast--"
+      IO.println "--thm--"
 
       -- print kine and decl name
       -- eg. "theorem Nat.add_comm" or "def Nat.add"
       IO.println s!"{info.kind} {name}"
-      IO.println "--ast--"
+      IO.println "--thm--"
 
       -- print decl type.
       -- eg. "∀ (n m : Nat), n + m = m + n"
       -- ppExpr is better than dbgToString
       let ppType := toString (← MetaM.run' do ppExpr info.type)
       truncatePrint ppType
-      IO.println "--ast--"
+      IO.println "--thm--"
 
       -- print doc string if exists.
       -- eg. O(|l| + |r|). Merge two lists using s as a switch.
       match (← findDocString? env name) with
       | .none => IO.println ""
       | .some doc => IO.println doc
-      -- IO.println "--ast--"
+      -- IO.println "--thm--"
 
       -- print decl value. These Lean.Expr are very large.
       -- match info.value? with
       -- | .none => IO.println ""
       -- | .some val => IO.println (toString (← MetaM.run' do ppExpr val))
-      -- IO.println "--ast--"
+      -- IO.println "--thm--"
 
       x := x + 1
       if x % 100 == 0 then