Bump Lean version to 4.14.0

Verbose/English/Calc.lean

@@ -1,7 +1,6 @@
 import Verbose.Tactics.Calc
 import Verbose.English.Common
 
-
 namespace Lean.Elab.Tactic
 open Meta Verbose English
 
@@ -55,13 +54,12 @@ elab_rules : tactic
   let some calcRange := (← getFileMap).rangeOfStx? calcstx | unreachable!
   let indent := calcRange.start.character
   let mut isFirst := true
-  for step in ← Lean.Elab.Term.getCalcSteps steps do
-    let some replaceRange := (← getFileMap).rangeOfStx? step | unreachable!
-    let `(calcStep| $(_) := $proofTerm) := step | unreachable!
+  for step in ← Lean.Elab.Term.mkCalcStepViews  steps do
+    let some replaceRange := (← getFileMap).rangeOfStx? step.ref | unreachable!
     let json := json% {"replaceRange": $(replaceRange),
                        "isFirst": $(isFirst),
                        "indent": $(indent)}
-    Lean.Widget.savePanelWidgetInfo CalcPanel.javascriptHash (pure json) proofTerm
+    Lean.Widget.savePanelWidgetInfo CalcPanel.javascriptHash (pure json) step.proof
     isFirst := false
   evalCalc (← `(tactic|calc%$calcstx $steps))
 

Verbose/English/Since.lean

@@ -34,6 +34,8 @@ pure s!"Could not prove:\n {goal}"
 implement_endpoint (lang := en) failedProofUsing (goal : Format) : CoreM String :=
 pure s!"Failed to prove this using the provided facts.\n{goal}"
 
+set_option linter.unusedVariables false
+
 example (n : Nat) (h : ∃ k, n = 2*k) : True := by
   Since ∃ k, n = 2*k we get k such that H : n = 2*k
   trivial

Verbose/French/Calc.lean

@@ -54,13 +54,12 @@ elab_rules : tactic
   let some calcRange := (← getFileMap).rangeOfStx? calcstx | unreachable!
   let indent := calcRange.start.character
   let mut isFirst := true
-  for step in ← Lean.Elab.Term.getCalcSteps steps do
-    let some replaceRange := (← getFileMap).rangeOfStx? step | unreachable!
-    let `(calcStep| $(_) := $proofTerm) := step | unreachable!
+  for step in ← Lean.Elab.Term.mkCalcStepViews steps do
+    let some replaceRange := (← getFileMap).rangeOfStx? step.ref | unreachable!
     let json := json% {"replaceRange": $(replaceRange),
                        "isFirst": $(isFirst),
                        "indent": $(indent)}
-    Lean.Widget.savePanelWidgetInfo CalcPanel.javascriptHash (pure json) proofTerm
+    Lean.Widget.savePanelWidgetInfo CalcPanel.javascriptHash (pure json) step.proof
     isFirst := false
   evalCalc (← `(tactic|calc%$calcstx $steps))
 

Verbose/French/Since.lean

@@ -38,6 +38,8 @@ pure s!"La justification en utilisant les faits fournis a échoué :\n{goal}"
 
 setLang fr
 
+set_option linter.unusedVariables false
+
 example (n : Nat) (h : ∃ k, n = 2*k) : True := by
   Comme ∃ k, n = 2*k on obtient k tel que H : n = 2*k
   trivial

Verbose/Infrastructure/DeclListExtension.lean

@@ -41,7 +41,7 @@ macro "registerDeclListExtension" name:ident : command =>
 `(initialize $name : DeclListExtension ←
   registerSimplePersistentEnvExtension {
     addEntryFn := fun map ⟨key, val⟩ ↦ map.insert key val
-    addImportedFn := fun as ↦ .fromArray (as.concatMap id) Name.quickCmp
+    addImportedFn := fun as ↦ .fromArray (as.flatMap id) Name.quickCmp
   })
 
 def  DeclListExtension.printDeclList (ext : DeclListExtension) : CommandElabM Unit :=

Verbose/Infrastructure/Extension.lean

@@ -12,7 +12,8 @@ It includes a number of extensions that tracks lists of declaration names, as we
 configuration extension `verboseConfigurationExt`.
 -/
 
-open Lean Elab Command Term Meta
+open Lean hiding HashMap
+open Std Elab Command Term Meta
 open Lean.Parser.Command (docComment)
 
 /-! ## Help provider lists extension
@@ -153,11 +154,11 @@ def Verbose.getDataProviders : MetaM (HashMap Expr (Array DataProvider)) := do
   return result
 
 declare_syntax_cat providersDescr
-syntax providersField := term ": [" ident,* "]"
+syntax providersField := term " : " "[" ident,* "]"
 syntax "{" providersField,* "}" : providersDescr
 
 def elabProvidersField : TSyntax `providersField → Term × Array Ident
-| `(providersField|$x:term : [$[$idents],*]) => (x, idents)
+| `(providersField|$x:term :[$[$idents],*]) => (x, idents)
 | _  => default
 
 def elabProvidersDescr : TSyntax `providersDescr → CommandElabM (HashMap Expr (Array Name))

Verbose/Infrastructure/HelpInfrastructure.lean

@@ -42,16 +42,43 @@ def Lean.Expr.relSymb : Expr → Option String
 | .const ``HasSubset.Subset _ => pure " ⊆ "
 | _ => none
 
-
+/-- Given an expression which is either describing an inequality or subset or membership,
+return a string decribing the relation and the LHS and RHS. -/
 partial def Lean.Expr.relInfo? : Expr → MetaM (Option (String × Expr × Expr))
 | .mvar m => do Lean.Expr.relInfo? (← m.getType'')
 | e@(_) =>  if e.getAppNumArgs < 2 then
     return none
   else
     return match relSymb e.getAppFn with
+           | some " ∈ " => some (" ∈ ", e.appArg!, e.appFn!.appArg!)
            | some s => some (s , e.appFn!.appArg!, e.appArg!)
            | none => none
 
+/-- For testing purposes -/
+elab "#relInfo" t:term: command =>
+  Command.runTermElabM fun _ ↦ do
+  let t ← Term.elabTerm t none
+  let t ← instantiateMVars t
+  let Option.some x ← t.relInfo? | failure
+  let (rel, l, r) := x
+  logInfo m!"Expression: {t}:\n{← ppExpr l} {rel} {← ppExpr r}"
+
+variable (x : ℕ) (A : Set ℕ)
+
+/--
+info: Expression: x > 0:
+x  >  0
+-/
+#guard_msgs in
+#relInfo x > 0
+
+/--
+info: Expression: x ∈ A:
+x  ∈  A
+-/
+#guard_msgs in
+#relInfo x ∈ A
+
 namespace Verbose
 open Lean
 
@@ -370,7 +397,7 @@ initialize hypHelpExt : PersistentEnvExtension HypHelpEntry (HypHelpEntry × Hyp
   }
 
 /-- Attribute for identifying `hypHelp` extensions. -/
-syntax (name := Verbose.hypHelp) "hypHelp " term,+ : attr
+syntax (name := hypHelp) "hypHelp " term,+ : attr
 
 initialize registerBuiltinAttribute {
   name := `hypHelp
@@ -431,7 +458,7 @@ initialize goalHelpExt : PersistentEnvExtension GoalHelpEntry (GoalHelpEntry ×
   }
 
 /-- Attribute for identifying `goalHelp` extensions. -/
-syntax (name := Verbose.goalHelp) "goalHelp " term,+ : attr
+syntax (name := goalHelp) "goalHelp " term,+ : attr
 
 initialize registerBuiltinAttribute {
   name := `goalHelp

Verbose/Tactics/Fix.lean

@@ -106,7 +106,7 @@ def Fix1 : introduced → TacticM Unit
                     | intro_rel.gt => mkAppM ``GT.gt #[n_expr, E]
                     | intro_rel.le => mkAppM ``LE.le #[n_expr, E]
                     | intro_rel.ge => mkAppM ``GE.ge #[n_expr, E]
-                    | intro_rel.mem => mkAppM ``Membership.mem #[n_expr, E]
+                    | intro_rel.mem => mkAppM ``Membership.mem #[E, n_expr]
 
       let (hyp_fvar, newer_goal) ← new_goal.intro hyp_name
       newer_goal.withContext do

Verbose/Tactics/Notations.lean

@@ -1,5 +1,4 @@
 import Mathlib.Util.Delaborators
-import Mathlib.Mathport.Notation
 import Mathlib.Tactic.SuppressCompilation
 
 /-! # Notations

Verbose/Tactics/Widget.lean

@@ -33,7 +33,7 @@ macro "dataProvider " name:ident args:ident* " := " q:term : command => do
     else
       return none
   let q' ← `(`($q))
-  let args' := args.mapIdx fun i arg => (i.val, arg)
+  let args' := args.mapIdx fun i arg => (i, arg)
   let t := mkIdent `terms
   let body ← args'.foldrM (init := q') fun (i, arg) body => `(let $arg := $t[$(quote i)]; $body)
   `(def $name ($t : Array Term) : MetaM Term :=
@@ -73,7 +73,7 @@ def SelectionInfo.mkBasicData (si : SelectionInfo) (typ : Expr) : MetaM (Array E
   let data ← decls.mapM (PrettyPrinter.delab ∘ LocalDecl.toExpr)
   let mut res : Array Expr := #[]
   let providers ← Verbose.getDataProviders
-  for maker in providers.findD typ #[] do
+  for maker in providers.getD typ #[] do
     try
       res := res.push (← (Lean.Elab.Term.elabTerm (← maker data) typ).run')
     catch _ => continue

lake-manifest.json

@@ -1,75 +1,95 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.14.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f27beb10b53350d6c1257ba3a8899df369135cc3",
-   "name": "batteries",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
-   "name": "Qq",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
-   "name": "aesop",
+   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.47",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.14.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
-   "name": "importGraph",
+   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "23c87df3dc33f21c40279c894022a37b71ffa918",
-   "name": "mathlib",
+   "scope": "leanprover",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "verbose",
  "lakeDir": ".lake"}

lakefile.toml

@@ -9,7 +9,8 @@ pp.proofs.withType = false
 
 [[require]]
 name = "mathlib"
-git = "https://github.com/leanprover-community/mathlib4.git"
+git = "https://github.com/leanprover-community/mathlib4.git" 
+rev = "v4.14.0"
 
 [[lean_lib]]
 name = "Verbose"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.14.0