Merge remote-tracking branch 'upstream/master' into opaquerepr

Author: Komyyy

Diff for: RELEASES.md

@@ -10,6 +10,12 @@ Please check the [releases](https://github.com/leanprover/lean4/releases) page f
 v4.3.0 (development in progress)
 ---------
 
+* **Lake:** Changed `postUpdate?` configuration option to a `post_update` declaration. See the `post_update` syntax docstring for more information on the new syntax.
+
+* [Lake: A manifest is automatically created on workspace load if one does not exists.](https://github.com/leanprover/lean4/pull/2680).
+
+* **Lake:** The `:=` syntax for configuration declarations (i.e., `package`, `lean_lib`, and `lean_exe`) has been deprecated. For example, `package foo := {...}` is deprecated.
+
 v4.2.0
 ---------
 

Diff for: src/Init/Data/Fin/Basic.lean

@@ -45,19 +45,19 @@ protected def sub : Fin n → Fin n → Fin n
   | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
 
 /-!
-Remark: mod/div/modn/land/lor can be defined without using (% n), but
+Remark: land/lor can be defined without using (% n), but
 we are trying to minimize the number of Nat theorems
 needed to bootstrap Lean.
 -/
 
 protected def mod : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a % b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b,  Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 protected def div : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a / b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
 
 def modn : Fin n → Nat → Fin n
-  | ⟨a, h⟩, m => ⟨(a % m) % n, mlt h⟩
+  | ⟨a, h⟩, m => ⟨a % m, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 def land : Fin n → Fin n → Fin n
   | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, mlt h⟩
@@ -110,7 +110,7 @@ theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
   fun h' => absurd (eq_of_val_eq h') h
 
 theorem modn_lt : ∀ {m : Nat} (i : Fin n), m > 0 → (modn i m).val < m
-  | _, ⟨_, _⟩, hp =>  Nat.lt_of_le_of_lt (mod_le _ _) (mod_lt _ hp)
+  | _, ⟨_, _⟩, hp =>  by simp [modn]; apply Nat.mod_lt; assumption
 
 theorem val_lt_of_le (i : Fin b) (h : b ≤ n) : i.val < n :=
   Nat.lt_of_lt_of_le i.isLt h

Diff for: src/Init/Meta.lean

@@ -1261,6 +1261,10 @@ structure Config where
   /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will fail if they do not make progress. -/
   failIfUnchanged   : Bool := true
+  /-- If `ground := true`, then ground terms are reduced. A term is ground when
+  it does not contain free or meta variables. Reduction is interrupted at a function application `f ...`
+  if `f` is marked to not be unfolded. -/
+  ground            : Bool := false
   deriving Inhabited, BEq, Repr
 
 -- Configuration object for `simp_all`
@@ -1276,6 +1280,7 @@ def neutralConfig : Simp.Config := {
   decide            := false
   arith             := false
   autoUnfold        := false
+  ground            := false
 }
 
 end Simp

Diff for: src/Lean/Meta/Tactic/Simp.lean

@@ -17,6 +17,7 @@ builtin_initialize registerTraceClass `Meta.Tactic.simp.congr (inherited := true
 builtin_initialize registerTraceClass `Meta.Tactic.simp.discharge (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.rewrite (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.unify (inherited := true)
+builtin_initialize registerTraceClass `Meta.Tactic.simp.ground (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.numSteps
 builtin_initialize registerTraceClass `Meta.Tactic.simp.heads
 builtin_initialize registerTraceClass `Debug.Meta.Tactic.simp

Diff for: src/Lean/Meta/Tactic/Simp/Main.lean

@@ -7,6 +7,7 @@ import Lean.Meta.Transform
 import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Rewrite
+import Lean.Meta.Match.Value
 
 namespace Lean.Meta
 namespace Simp
@@ -145,15 +146,59 @@ where
       let f := e.getAppFn
       f.isConst && isMatcherCore env f.constName!
 
+/--
+Auxiliary function for implementing `ctx.config.ground`: evaluate ground terms eagerly.
+We currently use `whnf` to implement this feature, but we want to stop ground evaluation at symbols marked with the `-` modifier.
+For example, `simp (config := { ground := true }) [-f]` should not unfold `f` even if the goal contains a ground term such as `f 2`.
+-/
+private def canUnfoldAtSimpGround (erased : SimpTheoremsArray) (_ : Meta.Config) (info : ConstantInfo) : CoreM Bool := do
+  return !erased.isErased (.decl info.name)
+
+/--
+Try to unfold `e`.
+-/
 private def unfold? (e : Expr) : SimpM (Option Expr) := do
   let f := e.getAppFn
   if !f.isConst then
     return none
   let fName := f.constName!
-  if (← isProjectionFn fName) then
-    return none -- should be reduced by `reduceProjFn?`
   let ctx ← read
-  if ctx.config.autoUnfold then
+  -- TODO: remove `rec` after we switch to new code generator
+  let rec unfoldGround? : SimpM (Option Expr) := do
+      unless ctx.config.ground do return none
+      -- We are assuming that assigned metavariables are going to be instantiated by the main simp loop.
+      if e.hasExprMVar || e.hasFVar then return none
+      if ctx.simpTheorems.isErased (.decl fName) then return none
+      -- TODO: check whether we need more filters
+      if (← isType e) then return none -- we don't unfold types
+      if (← isProof e) then return none -- we don't unfold proofs
+      if (← isInstance fName) then return none -- we don't unfold instances
+      -- TODO: we must have a notion of `simp` value, or more general solution for Lean
+      if Meta.isMatchValue e || isOfNatNatLit e then return none
+      if e.isConst then
+        -- We don't unfold constants that take arguments
+        -- TODO: add support for skipping partial applications too.
+        if let .forallE .. ← whnfD (← inferType e) then
+          return none
+      /-
+      We are currently using `whnf` with a custom `canUnfold?` predicate to reduce ground terms.
+      This can be inefficient, and produce proofs that are too expensive to type check in the Kernel. Some reasons:
+      - Functions defined by Well-founded recursion are expensive to reduce here and in the kernel.
+      - The kernel does not know we may have controlled reduction using `canUnfold?`.
+
+      It would be great to reduce the ground term using a to-be-implemented `cbv` tactic which produces a
+      proof that can be efficiently checked by the kernel.
+      -/
+      let eNew ← withDefault <|
+        withTheReader Meta.Context (fun c => { c with canUnfold? := canUnfoldAtSimpGround ctx.simpTheorems }) <| whnf e
+      if eNew == e then return none
+      trace[Meta.Tactic.simp.ground] "{e}\n---->\n{eNew}"
+      return some eNew
+  if let some eNew ← unfoldGround? then
+    return some eNew
+  else if (← isProjectionFn fName) then
+    return none -- should be reduced by `reduceProjFn?`
+  else if ctx.config.autoUnfold then
     if ctx.simpTheorems.isErased (.decl fName) then
       return none
     else if hasSmartUnfoldingDecl (← getEnv) fName then

Diff for: src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -109,8 +109,9 @@ mutual
         else if proof.isAppOfArity ``Eq.symm 4 then
           -- `Eq.symm` of rfl theorem is a rfl theorem
           isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
-        else if proof.isApp && proof.getAppFn.isConst then
+        else if proof.getAppFn.isConst then
           -- The application of a `rfl` theorem is a `rfl` theorem
+          -- A constant which is a `rfl` theorem is a `rfl` theorem
           isRflTheorem proof.getAppFn.constName!
         else
           return false

Diff for: src/Lean/Meta/Tactic/Subst.lean

@@ -52,9 +52,9 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
           if clearH then
             let mvarId ← mvarId.clear hFVarId
             let mvarId ← mvarId.clear aFVarId
-            pure ({}, mvarId)
+            pure (fvarSubst, mvarId)
           else
-            pure ({}, mvarId)
+            pure (fvarSubst, mvarId)
         else
           mvarId.withContext do
             let mvarDecl   ← mvarId.getDecl

Diff for: src/Lean/Meta/Tactic/UnifyEq.lean

@@ -53,8 +53,13 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
         /- Remark: we use `let rec` here because otherwise the compiler would generate an insane amount of code.
           We can remove the `rec` after we fix the eagerly inlining issue in the compiler. -/
         let rec substEq (symm : Bool) := do
-          /- Remark: `substCore` fails if the equation is of the form `x = x` -/
-          if let some (subst, mvarId) ← observing? (substCore mvarId eqFVarId symm subst) then
+          /-
+          Remark: `substCore` fails if the equation is of the form `x = x`
+          We use `(tryToSkip := true)` to ensure we avoid unnecessary `Eq.rec`s in user code.
+          Recall that `Eq.rec`s can negatively affect term reduction performance in the kernel and elaborator.
+          See issue https://github.com/leanprover/lean4/issues/2552 for an example.
+          -/
+          if let some (subst, mvarId) ← observing? (substCore mvarId eqFVarId symm subst (tryToSkip := true)) then
             return some { mvarId, subst }
           else if (← isDefEq a b) then
             /- Skip equality -/

Diff for: src/lake/Lake/Build/Index.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Build.Targets
 import Lake.Build.Executable
 import Lake.Build.Topological
 
@@ -104,5 +105,8 @@ export BuildInfo (build)
 @[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) :=
   self.exe.build
 
+@[inline] protected def LeanExeConfig.build (self : LeanExeConfig) : BuildM (BuildJob FilePath) := do
+  (← self.get).build
+
 @[inline] protected def LeanExe.fetch (self : LeanExe) : IndexBuildM (BuildJob FilePath) :=
   self.exe.fetch

Diff for: src/lake/Lake/Config/Package.lean

@@ -90,32 +90,6 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   /-- An `Array` of target names to build whenever the package is used. -/
   extraDepTargets : Array Name := #[]
 
-  /--
-  A post-`lake update` hook. The monadic action is run after a successful
-  `lake update` execution on this package or one of its downstream dependents.
-  Defaults to `none`.
-
-  As an example, Mathlib can use this feature to synchronize the Lean toolchain
-  and run `cache get`:
-
-  ```
-  package mathlib where
-    postUpdate? := some do
-      let some pkg ← findPackage? `mathlib
-        | error "mathlib is missing from workspace"
-      let wsToolchainFile := (← getRootPackage).dir / "lean-toolchain"
-      let mathlibToolchain ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
-      IO.FS.writeFile wsToolchainFile mathlibToolchain
-      let some exe := pkg.findLeanExe? `cache
-        | error s!"{pkg.name}: cache is missing from the package"
-      let exeFile ← runBuild (exe.build >>= (·.await))
-      let exitCode ← env exeFile.toString #["get"]
-      if exitCode ≠ 0 then
-        error s!"{pkg.name}: failed to fetch cache"
-  ```
-  -/
-  postUpdate? : Option (LakeT LogIO PUnit) := none
-
   /--
   Whether to compile each of the package's module into a native shared library
   that is loaded whenever the module is imported. This speeds up evaluation of
@@ -197,6 +171,9 @@ deriving Inhabited
 /-! # Package -/
 --------------------------------------------------------------------------------
 
+
+declare_opaque_type OpaquePostUpdateHook (pkg : Name)
+
 /-- A Lake package -- its location plus its configuration. -/
 structure Package where
   /-- The path to the package's directory. -/
@@ -231,6 +208,8 @@ structure Package where
   (i.e., on a bare `lake run` of the package).
   -/
   defaultScripts : Array Script := #[]
+  /-- Post-`lake update` hooks for the package. -/
+  postUpdateHooks : Array (OpaquePostUpdateHook config.name) := #[]
 
 instance : Nonempty Package :=
   have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance
@@ -263,6 +242,22 @@ instance : CoeDep Package pkg (NPackage pkg.name) := ⟨⟨pkg, rfl⟩⟩
 /-- The package's name. -/
 abbrev NPackage.name (_ : NPackage n) := n
 
+/--
+The type of a post-update hooks monad.
+`IO` equipped with logging ability and information about the Lake configuration.
+-/
+abbrev PostUpdateFn (pkgName : Name) := NPackage pkgName → LakeT LogIO PUnit
+
+structure PostUpdateHook (pkgName : Name) where
+  fn : PostUpdateFn pkgName
+  deriving Inhabited
+
+hydrate_opaque_type OpaquePostUpdateHook PostUpdateHook name
+
+structure PostUpdateHookDecl where
+  pkg : Name
+  fn : PostUpdateFn pkg
+
 namespace Package
 
 /-- The package's direct dependencies. -/
@@ -289,10 +284,6 @@ namespace Package
 @[inline] def extraDepTargets (self : Package) : Array Name :=
   self.config.extraDepTargets
 
-/-- The package's `postUpdate?` configuration. -/
-@[inline] def postUpdate? (self : Package) :=
-  self.config.postUpdate?
-
 /-- The package's `releaseRepo?` configuration. -/
 @[inline] def releaseRepo? (self : Package) : Option String :=
   self.config.releaseRepo?

Diff for: src/lake/Lake/DSL/Attributes.lean

@@ -14,6 +14,9 @@ initialize packageAttr : OrderedTagAttribute ←
 initialize packageDepAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency"
 
+initialize postUpdateAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook"
+
 initialize scriptAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `script "mark a definition as a Lake script"
 

Diff for: src/lake/Lake/DSL/DeclUtil.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.DSL.Config
 import Lake.Util.Binder
 import Lean.Parser.Command
 
@@ -24,15 +25,21 @@ def expandAttrs (attrs? : Option Attributes) : Array AttrInstance :=
   else
     #[]
 
+syntax declField :=
+  ident ":=" term
+
 syntax structVal :=
-  "{" manyIndent(group(Term.structInstField ", "?)) "}"
+  "{" manyIndent(group(declField ", "?)) "}"
 
 syntax declValDo :=
   ppSpace Term.do (Term.whereDecls)?
 
 syntax declValStruct :=
   ppSpace structVal (Term.whereDecls)?
 
+syntax declValWhere :=
+  " where " sepByIndentSemicolon(declField) (Term.whereDecls)?
+
 syntax declValTyped :=
   Term.typeSpec declValSimple
 
@@ -43,7 +50,7 @@ syntax simpleDeclSig :=
   ident Term.typeSpec declValSimple
 
 syntax structDeclSig :=
-  ident (Command.whereStructInst <|> declValOptTyped <|> declValStruct)?
+  ident (declValWhere <|> declValOptTyped <|> declValStruct)?
 
 syntax bracketedSimpleBinder :=
   "(" ident (" : " term)? ")"
@@ -69,18 +76,25 @@ def fixName (id : Ident) : Option Name → Ident
 | some n => mkIdentFrom id n
 | none => id
 
-def mkConfigStructDecl (name? : Option Name)
+def expandDeclField : TSyntax ``declField → MacroM (TSyntax ``Term.structInstField)
+| `(declField| $id :=%$tk $val) => `(Term.structInstField| $id:ident :=%$tk $val)
+| x => Macro.throwErrorAt x "ill-formed field declaration"
+
+def mkConfigDecl (name? : Option Name)
 (doc? : Option DocComment) (attrs : Array AttrInstance) (ty : Term)
 : (spec : Syntax) → MacroM Syntax.Command
 | `(structDeclSig| $id:ident) =>
   `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty :=
     {name := $(quote id.getId)})
-| `(structDeclSig| $id:ident where $ds;* $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty where
-      name := $(quote id.getId); $ds;* $[$wds?]?)
-| `(structDeclSig| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $(ty?.getD ty) := $defn $[$wds?]?)
+| `(structDeclSig| $id:ident where $fs;* $[$wds?]?) => do
+  let fields ← fs.getElems.mapM expandDeclField
+  let defn ← `({ name := $(quote id.getId), $fields,* })
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
+| `(structDeclSig| $id:ident $[: $ty?]? :=%$defTk $defn $[$wds?]?) => do
+  let notice ← withRef defTk `(#eval IO.eprintln s!" warning: {__dir__}: `:=` syntax for configurations has been deprecated")
+  `($notice $[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
 | `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
-  let defn ← `({ name := $(quote id.getId), $fs,* })
+  let fields ← fs.mapM expandDeclField
+  let defn ← `({ name := $(quote id.getId), $fields,* })
   `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
 | stx => Macro.throwErrorAt stx "ill-formed configuration syntax"