Update to lean v4.15.0

Auto/EvaluateAuto/CommandAnalysis.lean

@@ -1,11 +1,30 @@
 import Lean
 import Auto.EvaluateAuto.EnvAnalysis
+import Auto.EvaluateAuto.ConstAnalysis
 import Auto.EvaluateAuto.Result
 open Lean
 
+register_option auto.evalAuto.ensureAesop : Bool := {
+  defValue := false
+  descr := "Enable/Disable enforcement of importing `aesop`"
+}
+
 namespace EvalAuto
 
 open Elab Frontend
+
+def processHeaderEnsuring (header : Syntax) (opts : Options) (messages : MessageLog)
+    (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (leakEnv := false) (ensuring : Array Import := #[])
+    : IO (Environment × MessageLog) := do
+  try
+    let env ← importModules (leakEnv := leakEnv) (headerToImports header ++ ensuring) opts trustLevel
+    pure (env, messages)
+  catch e =>
+    let env ← mkEmptyEnvironment
+    let spos := header.getPos?.getD 0
+    let pos  := inputCtx.fileMap.toPosition spos
+    pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
+
 def runWithEffectOfCommandsCore
   (cnt? : Option Nat)
   (action : Context → State → State → ConstantInfo → IO (Option α)) : FrontendM (Array α) := do
@@ -38,61 +57,16 @@ def runWithEffectOfCommandsCore
   the procedure is terminated.
 -/
 def runWithEffectOfCommands
-  (input : String) (fileName : String) (opts : Options := {}) (cnt? : Option Nat)
-  (action : Context → State → State → ConstantInfo → IO (Option α)) : IO (Array α) := do
+  (input : String) (fileName : String) (cnt? : Option Nat)
+  (action : Context → State → State → ConstantInfo → IO (Option α)) : CoreM (Array α) := do
   let inputCtx := Parser.mkInputContext input fileName
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
-  let (env, messages) ← processHeader header opts messages inputCtx
-  let commandState := Command.mkState env messages opts
+  let mut ensuring := #[]
+  if auto.evalAuto.ensureAesop.get (← getOptions) then
+    ensuring := ensuring.push { module := `Aesop }
+  let (env, messages) ← processHeaderEnsuring header {} messages inputCtx (ensuring := ensuring)
+  let commandState := Command.mkState env messages {}
   (runWithEffectOfCommandsCore cnt? action { inputCtx }).run'
     { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
 
-open Elab Tactic in
-/--
-  Note: Use `initSrcSearchPath` to get SearchPath of Lean4's builtin source files
--/
-def runTacticAtConstantDeclaration
-  (name : Name) (searchPath : SearchPath)
-  (tactic : ConstantInfo → TacticM Unit) : CoreM Result := do
-  if ← isInitializerExecutionEnabled then
-    throwError "{decl_name%} :: Running this function with execution of `initialize` code enabled is unsafe"
-  let .some modName ← Lean.findModuleOf? name
-    | throwError "{decl_name%} :: Cannot find constant {name}"
-  let .some uri ← Server.documentUriFromModule searchPath modName
-    | throwError "{decl_name%} :: Cannot find module {modName}"
-  let .some path := System.Uri.fileUriToPath? uri
-    | throwError "{decl_name%} :: URI {uri} of {modName} is not a file"
-  let path := path.normalize
-  let inputHandle ← IO.FS.Handle.mk path .read
-  let input ← inputHandle.readToEnd
-  let results ← runWithEffectOfCommands input path.toString {} (.some 1) (fun ctx st₁ st₂ ci =>
-    let metaAction : MetaM (Option Result) := do
-      if ci.name != name then
-        return .none
-      let .mvar mid ← Meta.mkFreshExprMVar ci.type
-        | throwError "{decl_name%} :: Unexpected error"
-      let result : List MVarId ⊕ Exception ←
-        tryCatchRuntimeEx
-          (do let goals ← Term.TermElabM.run' (Tactic.run mid (tactic ci)) {}; return .inl goals)
-          (fun e => return .inr e)
-      match result with
-      | .inl goals =>
-        if goals.length >= 1 then
-          return .some .subGoals
-        let proof ← instantiateMVars (.mvar mid)
-        match Kernel.check (← getEnv) {} proof with
-        | Except.ok autoProofType =>
-          match Kernel.isDefEq (← getEnv) {} autoProofType ci.type with
-          | Except.ok true => return .some .success
-          | _ => return .some .typeUnequal
-        | Except.error _ => return .some .typeCheckFail
-      | .inr e => return .some (.exception e)
-    let coreAction : CoreM (Option Result) := metaAction.run'
-    let ioAction : IO (Option Result × _) := coreAction.toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env }
-    do
-      return (← ioAction).fst)
-  let #[result] := results
-    | throwError "{decl_name%} :: Unexpected error"
-  return result
-
 end EvalAuto

Auto/EvaluateAuto/ConstAnalysis.lean

@@ -11,6 +11,15 @@ def Name.getConstsOfModule (module : Name) : CoreM (Array Name) := do
   let (mod, _) ← readModuleData mFile
   return mod.constNames
 
+def tallyNamesByModule (names : Array Name) : CoreM (Std.HashMap Name (Array Name)) := do
+  let mut ret : Std.HashMap Name (Array Name) := {}
+  for name in names do
+    let .some modName ← Lean.findModuleOf? name
+      | throwError "{decl_name%} :: Cannot find module of {name}"
+    let orig := (ret.get? modName).getD #[]
+    ret := ret.insert modName (orig.push name)
+  return ret
+
 /-- Used as a wrapper in other functions -/
 def Name.getCi (name : Name) (parentFunc : Name) : CoreM ConstantInfo := do
   let .some ci := (← getEnv).find? name

Auto/EvaluateAuto/EnvAnalysis.lean

@@ -1,4 +1,5 @@
 import Lean
+import Auto.EvaluateAuto.NameArr
 
 open Lean
 
@@ -17,6 +18,11 @@ def mathlibModules : CoreM (Array Name) := do
   let u := (← getEnv).header.moduleNames
   return u.filter (fun name => name.components[0]? == .some `Mathlib)
 
+/- Check that all mathlib modules names are ordinary -/
+def allMathlibModuleNamesCanBeFilename : CoreM Bool := do
+  let mms ← mathlibModules
+  return mms.all Name.canBeFilename
+
 /-- Pick `n` elements from array `xs`. Elements may duplicate -/
 def Array.randPick {α} (xs : Array α) (n : Nat) : IO (Array α) := do
   let mut ret := #[]

Auto/EvaluateAuto/NameArr.lean

@@ -4,70 +4,78 @@ open Lean
 namespace EvalAuto
 
 /--
-  Unique string representation of array of names
-  We use `.` to separate fields of a name, and `\n` to separate names.
-  A `.` is appended to the end of each name.
-  A `\n` is further appended to the end of the last name.
-  We use `\` to escape `.` and `\n` occurring in the fields of names, i.e.,
-    `\.` represents literal `.`, `\\n` represents literal `\n`, and
-    `\\` represents literal `\`.
+  Whether a name is a valid filename
+-/
+def Name.canBeFilename (n : Name) : Bool :=
+  n.components.all (fun n =>
+    match n with
+    | .str _ s =>
+      match s.get? 0 with
+      | .some _ => s.all (fun c => c.isAlphanum || c == '_' || c == '\'')
+      | .none => false
+    | _ => false)
+
+/--
+  Unique string representation of names, where it is ensured that `\n` does not occur
+  A `.` is appended to the end of the name
+  We use "\\d" to represent ".", "\\n" to represent "\n", "\\\\" to represent "\\"
   To distinguish `mkStr` and `mkNum`, we prepend `\` to all `mkNum` fields
 -/
-def NameArray.repr (ns : Array Name) : String :=
+def Name.uniqRepr (n : Name) : String :=
   let strRepr (s : String) : String :=
-    ((s.replace "\\" "\\\\").replace "." "\\.").replace "\n" "\\\n"
+    ((s.replace "\\" "\\\\").replace "." "\\d").replace "\n" "\\n"
   let compRepr (c : Name) : String :=
     match c with
     | .anonymous => ""
     | .mkNum _ n => s!"\\{n}"
     | .mkStr _ s => strRepr s
-  let nameRepr (n : Name) : String :=
-    String.join (n.components.map (fun c => compRepr c ++ "."))
-  String.join (ns.map (fun n => nameRepr n ++ "\n")).toList
+  String.join (n.components.map (fun c => compRepr c ++ "."))
 
-/-
-  Parse string representation of array of names
-  We use `.` to separate fields of a name, and `\n` to separate names
-  We use `\` to escape `.` and `\n` occurring in the fields of names, i.e.,
-    `\.` represents literal `.`, `\\n` represents literal `\n`, and
-    `\\` represents literal `\`.
-  To distinguish `mkStr` and `mkNum`, we prepend `\` to all `mkNum` fields
+/--
+  Parsing unique representation of names, see `Name.uniqRepr`
 -/
-def NameArray.parse (repr : String) : Array Name := Id.run <| do
-  let mut curField := ""
-  let mut curFields : Array (String ⊕ Nat) := #[]
-  let mut allNames : Array Name := #[]
-  let mut escape := false
-  let mut num := false
-  for c in repr.data do
-    if !escape && c == '.' then
-      if num then
-        curFields := curFields.push (.inr ((String.toNat? curField).getD 0))
+def Name.parseUniqRepr (n : String) : Name :=
+  let compParse (s : String) : String ⊕ Nat := Id.run <| do
+    let s := s.data
+    if s[0]? == '\\' then
+      if let .some c := s[1]? then
+        if c.isDigit then
+          return .inr ((String.toNat? (String.mk (s.drop 1))).getD 0)
+    let mut ret := ""
+    let mut escape := false
+    for c in s do
+      if !escape then
+        if c != '\\' then
+          ret := ret.push c
+        else
+          escape := true
       else
-        curFields := curFields.push (.inl curField)
-      curField := ""
-      num := false
-      continue
-    if !escape && c == '\n' then
-      let curName := curFields.foldl (fun prev sn =>
-        match sn with
-        | .inl s => Name.mkStr prev s
-        | .inr n => Name.mkNum prev n) .anonymous
-      allNames := allNames.push curName
-      curFields := #[]
-      continue
-    if escape && c.isDigit then
-      num := true
-    if c == '\\' then
-      if escape then
         escape := false
-        curField := curField.push c
-      else
-        escape := true
-    else
-      escape := false
-      curField := curField.push c
-  return allNames
+        match c with
+        | '\\' => ret := ret.push '\\'
+        | 'd' => ret := ret.push '.'
+        | 'n' => ret := ret.push '\n'
+        | _ => ret := ret.push c
+    return .inl ret
+  let components := ((n.splitOn ".").dropLast).map compParse
+  components.foldl (fun prev sn =>
+    match sn with
+    | .inl s => Name.mkStr prev s
+    | .inr n => Name.mkNum prev n) .anonymous
+
+/--
+  Each name in the array is represented using `Name.uniqRepr`
+  Names are separated using `\n`. A `\n` is further appended to the end of the last name.
+-/
+def NameArray.repr (ns : Array Name) : String :=
+  String.join (ns.map (fun n => Name.uniqRepr n ++ "\n")).toList
+
+/-
+  Each name in the array is represented using `Name.uniqRepr`
+  Names are separated using `\n`. A `\n` is further appended to the end of the last name.
+-/
+def NameArray.parse (repr : String) : Array Name :=
+  Array.mk ((repr.splitOn "\n").map Name.parseUniqRepr).dropLast
 
 def NameArray.save (ns : Array Name) (fname : String) : IO Unit := do
   let fd ← IO.FS.Handle.mk fname .write

Auto/EvaluateAuto/OS.lean

@@ -0,0 +1,4 @@
+abbrev EvalProc := IO.Process.Child ⟨.piped, .piped, .piped⟩
+
+def EvalProc.create (path : String) (args : Array String) : IO EvalProc :=
+  IO.Process.spawn {stdin := .piped, stdout := .piped, stderr := .piped, cmd := path, args := args}

Auto/EvaluateAuto/Result.lean

@@ -1,23 +1,33 @@
 import Lean
 open Lean
 
+initialize
+  registerTraceClass `auto.eval.printConfig
+  registerTraceClass `auto.eval.printProblem
+  registerTraceClass `auto.eval.printResult
+
 namespace EvalAuto
 
 inductive Result
   | success
   | nonProp
   | typeCheckFail
   | typeUnequal
+  | nonterminate
   -- `auto` does not produce subgoals, but other tactics we test might (such as `simp`)
   | subGoals
   | exception (e : Exception)
 
+instance : Inhabited Result where
+  default := .success
+
 instance : ToMessageData Result where
   toMessageData : Result → MessageData
   | .success         => "Result.success"
   | .nonProp         => "Result.nonProp"
   | .typeCheckFail   => "Result.typeCheckFail"
   | .typeUnequal     => "Result.typeUnequal"
+  | .nonterminate    => "Result.nonterminate"
   | .subGoals        => "Result.subGoals"
   | .exception e     => m!"Result.exception ::\n{e.toMessageData}"
 
@@ -26,7 +36,41 @@ def Result.concise : Result → String
 | .nonProp => "N"
 | .typeCheckFail => "F"
 | .typeUnequal => "U"
+| .nonterminate => "T"
 | .subGoals => "G"
 | .exception _ => "E"
 
+def Result.ofConcise? : String → Option Result
+| "S" => .some .success
+| "N" => .some .nonProp
+| "F" => .some .typeCheckFail
+| "U" => .some .typeUnequal
+| "T" => .some .nonterminate
+| "G" => .some .subGoals
+| "E" => .some (.exception (.error Syntax.missing "Filled_in_by_Result.ofConcise?"))
+| _   => .none
+
+open Elab Tactic in
+/--
+  Run `tactic` on a metavariable with type `e` and obtain the result
+-/
+def Result.ofTacticOnExpr (e : Expr) (tactic : TacticM Unit) : TermElabM Result := do
+  let .mvar mid ← Meta.mkFreshExprMVar e
+    | throwError "{decl_name%} : Unexpected error"
+  let result : List MVarId ⊕ Exception ← tryCatchRuntimeEx
+    (do let goals ← Term.TermElabM.run' (Tactic.run mid tactic) {}; return .inl goals)
+    (fun e => return .inr e)
+  match result with
+  | .inl goals =>
+    if goals.length >= 1 then
+      return .subGoals
+    let proof ← instantiateMVars (.mvar mid)
+    match Kernel.check (← getEnv) {} proof with
+    | Except.ok autoProofType =>
+      match Kernel.isDefEq (← getEnv) {} autoProofType e with
+      | Except.ok true => return .success
+      | _ => return .typeUnequal
+    | Except.error _ => return .typeCheckFail
+  | .inr e => return (.exception e)
+
 end EvalAuto