Merge remote-tracking branch 'origin/master' into releases/v4.2.0

src/Lean/CoreM.lean

@@ -199,11 +199,6 @@ instance [MetaEval α] : MetaEval (CoreM α) where
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 
-@[inline] def checkInterrupted : CoreM Unit := do
-  if (← IO.checkCanceled) then
-    -- should never be visible to users!
-    throw <| Exception.error .missing "elaboration interrupted"
-
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
   let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
@@ -217,11 +212,6 @@ def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat)
 def checkMaxHeartbeats (moduleName : String) : CoreM Unit := do
   checkMaxHeartbeatsCore moduleName `maxHeartbeats (← read).maxHeartbeats
 
-def checkSystem (moduleName : String) : CoreM Unit := do
-  -- TODO: bring back more checks from the C++ implementation
-  checkInterrupted
-  checkMaxHeartbeats moduleName
-
 private def withCurrHeartbeatsImp (x : CoreM α) : CoreM α := do
   let heartbeats ← IO.getNumHeartbeats
   withReader (fun ctx => { ctx with initHeartbeats := heartbeats }) x
@@ -250,7 +240,7 @@ instance : MonadLog CoreM where
 
 end Core
 
-export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
+export Core (CoreM mkFreshUserName checkMaxHeartbeats withCurrHeartbeats)
 
 @[inline] def withAtLeastMaxRecDepth [MonadFunctorT CoreM m] (max : Nat) : m α → m α :=
   monadMap (m := CoreM) <| withReader (fun ctx => { ctx with maxRecDepth := Nat.max max ctx.maxRecDepth })

src/Lean/Elab/Do.lean

@@ -1595,7 +1595,7 @@ mutual
   partial def doSeqToCode : List Syntax → M CodeBlock
     | [] => do liftMacroM mkPureUnitAction
     | doElem::doElems => withIncRecDepth <| withRef doElem do
-      checkSystem "`do`-expander"
+      checkMaxHeartbeats "`do`-expander"
       match (← liftMacroM <| expandMacro? doElem) with
       | some doElem => doSeqToCode (doElem::doElems)
       | none =>

src/Lean/Elab/Term.lean

@@ -1354,7 +1354,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
   | .missing => mkSyntheticSorryFor expectedType?
   | stx => withFreshMacroScope <| withIncRecDepth do
     withTraceNode `Elab.step (fun _ => return m!"expected type: {expectedType?}, term\n{stx}") do
-    checkSystem "elaborator"
+    checkMaxHeartbeats "elaborator"
     let env ← getEnv
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew?) =>

src/Lean/Environment.lean

@@ -230,7 +230,6 @@ inductive KernelException where
   | deterministicTimeout
   | excessiveMemory
   | deepRecursion
-  | interrupted
 
 namespace Environment
 
@@ -255,20 +254,20 @@ structure EnvExtensionInterface where
   ext          : Type → Type
   inhabitedExt : Inhabited σ → Inhabited (ext σ)
   registerExt  (mkInitial : IO σ) : IO (ext σ)
-  setState     (e : ext σ) (env : Environment) : σ → Environment
-  modifyState  (e : ext σ) (env : Environment) : (σ → σ) → Environment
-  getState     [Inhabited σ] (e : ext σ) (env : Environment) : σ
+  setState     (e : ext σ) (exts : Array EnvExtensionState) : σ → Array EnvExtensionState
+  modifyState  (e : ext σ) (exts : Array EnvExtensionState) : (σ → σ) → Array EnvExtensionState
+  getState     [Inhabited σ] (e : ext σ) (exts : Array EnvExtensionState) : σ
   mkInitialExtStates : IO (Array EnvExtensionState)
-  ensureExtensionsSize : Environment → IO Environment
+  ensureExtensionsSize : Array EnvExtensionState → IO (Array EnvExtensionState)
 
 instance : Inhabited EnvExtensionInterface where
   default := {
     ext                  := id
     inhabitedExt         := id
-    ensureExtensionsSize := fun env => pure env
+    ensureExtensionsSize := fun exts => pure exts
     registerExt          := fun mk => mk
-    setState             := fun _ env _ => env
-    modifyState          := fun _ env _ => env
+    setState             := fun _ exts _ => exts
+    modifyState          := fun _ exts _ => exts
     getState             := fun ext _ => ext
     mkInitialExtStates   := pure #[]
   }
@@ -290,41 +289,40 @@ private builtin_initialize envExtensionsRef : IO.Ref (Array (Ext EnvExtensionSta
   user-defined environment extensions. When this happens, we must adjust the size of the `env.extensions`.
   This method is invoked when processing `import`s.
 -/
-partial def ensureExtensionsArraySize (env : Environment) : IO Environment := do
-  loop env.extensions.size env
+partial def ensureExtensionsArraySize (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do
+  loop exts.size exts
 where
-  loop (i : Nat) (env : Environment) : IO Environment := do
+  loop (i : Nat) (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do
     let envExtensions ← envExtensionsRef.get
     if i < envExtensions.size then
       let s ← envExtensions[i]!.mkInitial
-      let env := { env with extensions := env.extensions.push s }
-      loop (i + 1) env
+      let exts := exts.push s
+      loop (i + 1) exts
     else
-      return env
+      return exts
 
 private def invalidExtMsg := "invalid environment extension has been accessed"
 
-unsafe def setState {σ} (ext : Ext σ) (env : Environment) (s : σ) : Environment :=
-  if h : ext.idx < env.extensions.size then
-    { env with extensions := env.extensions.set ⟨ext.idx, h⟩ (unsafeCast s) }
+unsafe def setState {σ} (ext : Ext σ) (exts : Array EnvExtensionState) (s : σ) : Array EnvExtensionState :=
+  if h : ext.idx < exts.size then
+    exts.set ⟨ext.idx, h⟩ (unsafeCast s)
   else
-    have : Inhabited Environment := ⟨env⟩
+    have : Inhabited (Array EnvExtensionState) := ⟨exts⟩
     panic! invalidExtMsg
 
-@[inline] unsafe def modifyState {σ : Type} (ext : Ext σ) (env : Environment) (f : σ → σ) : Environment :=
-  if ext.idx < env.extensions.size then
-    { env with
-      extensions := env.extensions.modify ext.idx fun s =>
-        let s : σ := unsafeCast s
-        let s : σ := f s
-        unsafeCast s }
+@[inline] unsafe def modifyState {σ : Type} (ext : Ext σ) (exts : Array EnvExtensionState) (f : σ → σ) : Array EnvExtensionState :=
+  if ext.idx < exts.size then
+    exts.modify ext.idx fun s =>
+      let s : σ := unsafeCast s
+      let s : σ := f s
+      unsafeCast s
   else
-    have : Inhabited Environment := ⟨env⟩
+    have : Inhabited (Array EnvExtensionState) := ⟨exts⟩
     panic! invalidExtMsg
 
-unsafe def getState {σ} [Inhabited σ] (ext : Ext σ) (env : Environment) : σ :=
-  if h : ext.idx < env.extensions.size then
-    let s : EnvExtensionState := env.extensions.get ⟨ext.idx, h⟩
+unsafe def getState {σ} [Inhabited σ] (ext : Ext σ) (exts : Array EnvExtensionState) : σ :=
+  if h : ext.idx < exts.size then
+    let s : EnvExtensionState := exts.get ⟨ext.idx, h⟩
     unsafeCast s
   else
     panic! invalidExtMsg
@@ -363,14 +361,22 @@ opaque EnvExtensionInterfaceImp : EnvExtensionInterface
 
 def EnvExtension (σ : Type) : Type := EnvExtensionInterfaceImp.ext σ
 
-private def ensureExtensionsArraySize (env : Environment) : IO Environment :=
-  EnvExtensionInterfaceImp.ensureExtensionsSize env
+private def ensureExtensionsArraySize (env : Environment) : IO Environment := do
+  let exts ← EnvExtensionInterfaceImp.ensureExtensionsSize env.extensions
+  return { env with extensions := exts }
 
 namespace EnvExtension
 instance {σ} [s : Inhabited σ] : Inhabited (EnvExtension σ) := EnvExtensionInterfaceImp.inhabitedExt s
-def setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := EnvExtensionInterfaceImp.setState ext env s
-def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := EnvExtensionInterfaceImp.modifyState ext env f
-def getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) : σ := EnvExtensionInterfaceImp.getState ext env
+
+def setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment :=
+  { env with extensions := EnvExtensionInterfaceImp.setState ext env.extensions s }
+
+def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment :=
+  { env with extensions := EnvExtensionInterfaceImp.modifyState ext env.extensions f }
+
+def getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) : σ :=
+  EnvExtensionInterfaceImp.getState ext env.extensions
+
 end EnvExtension
 
 /-- Environment extensions can only be registered during initialization.

src/Lean/Message.lean

@@ -370,7 +370,6 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
   | deterministicTimeout                => "(kernel) deterministic timeout"
   | excessiveMemory                     => "(kernel) excessive memory consumption detected"
   | deepRecursion                       => "(kernel) deep recursion detected"
-  | interrupted                         => "(kernel) interrupted"
 
 end KernelException
 end Lean

src/Lean/Meta/ExprDefEq.lean

@@ -1851,7 +1851,7 @@ private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Un
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (return m!"{t} =?= {s}") do
-  checkSystem "isDefEq"
+  checkMaxHeartbeats "isDefEq"
   whenUndefDo (isDefEqQuick t s) do
   whenUndefDo (isDefEqProofIrrel t s) do
   /-

src/Lean/Meta/SynthInstance.lean

@@ -175,8 +175,7 @@ structure State where
 
 abbrev SynthM := ReaderT Context $ StateRefT State MetaM
 
-def checkSystem : SynthM Unit := do
-  Core.checkInterrupted
+def checkMaxHeartbeats : SynthM Unit := do
   Core.checkMaxHeartbeatsCore "typeclass" `synthInstance.maxHeartbeats (← read).maxHeartbeats
 
 @[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
@@ -553,7 +552,7 @@ def resume : SynthM Unit := do
       consume { key := cNode.key, mvar := cNode.mvar, subgoals := rest, mctx, size := cNode.size + answer.size }
 
 def step : SynthM Bool := do
-  checkSystem
+  checkMaxHeartbeats
   let s ← get
   if !s.resumeStack.isEmpty then
     resume

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -268,7 +268,7 @@ where
       e
 
 partial def simp (e : Expr) : M Result := withIncRecDepth do
-  checkSystem "simp"
+  checkMaxHeartbeats "simp"
   let cfg ← getConfig
   if (← isProof e) then
     return { expr := e }

src/Lean/Meta/WHNF.lean

@@ -863,7 +863,7 @@ private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
 @[export lean_whnf]
 partial def whnfImp (e : Expr) : MetaM Expr :=
   withIncRecDepth <| whnfEasyCases e fun e => do
-    checkSystem "whnf"
+    checkMaxHeartbeats "whnf"
     let useCache ← useWHNFCache e
     match (← cached? useCache e) with
     | some e' => pure e'

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -240,7 +240,7 @@ partial def delabFor : Name → Delab
     <|> if k.isAtomic then failure else delabFor k.getRoot
 
 partial def delab : Delab := do
-  checkSystem "delab"
+  checkMaxHeartbeats "delab"
   let e ← getExpr
 
   -- no need to hide atomic proofs

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -351,7 +351,7 @@ abbrev AnalyzeAppM := ReaderT App.Context (StateT App.State AnalyzeM)
 mutual
 
   partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do
-    checkSystem "Delaborator.topDownAnalyze"
+    checkMaxHeartbeats "Delaborator.topDownAnalyze"
     trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel}"
     let e ← getExpr
     let opts ← getOptions

src/Lean/Server/AsyncList.lean

@@ -112,20 +112,6 @@ partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε
 def waitHead? (as : AsyncList ε α) : Task (Except ε (Option α)) :=
   as.waitFind? fun _ => true
 
-/-- Cancels all tasks in the list. -/
-partial def cancel : AsyncList ε α → BaseIO Unit
-  | cons _ tl => tl.cancel
-  | nil => pure ()
-  | delayed tl => do
-    -- mind the order: if we asked the task whether it is still running
-    -- *before* cancelling it, it could be the case that it finished
-    -- just in between and has enqueued a dependent task that we would
-    -- miss (recall that cancellation is inherited by dependent tasks)
-    IO.cancel tl
-    if (← hasFinished tl) then
-      if let .ok t := tl.get then
-        t.cancel
-
 end AsyncList
 
 end IO

src/Lean/Server/FileWorker.lean

@@ -300,7 +300,6 @@ section Updates
       let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
       -- Ignore exceptions, we are only interested in the successful snapshots
       let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
-      oldDoc.cmdSnaps.cancel
       -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
       -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
       let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
@@ -466,7 +465,6 @@ section MainLoop
     | Message.notification "exit" none =>
       let doc := st.doc
       doc.cancelTk.set
-      doc.cmdSnaps.cancel
       return ()
     | Message.notification method (some params) =>
       handleNotification method (toJson params)

src/kernel/expr_eq_fn.cpp

@@ -60,9 +60,7 @@ template<bool CompareBinderInfo>
 class expr_eq_fn {
     eq_cache & m_cache;
 
-    static void check_system() {
-        ::lean::check_system("expression equality test");
-    }
+    static void check_system() { ::lean::check_system("expression equality test"); }
 
     bool apply(expr const & a, expr const & b) {
         if (is_eqp(a, b))          return true;

src/kernel/kernel_exception.h

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 #include "kernel/local_ctx.h"
-#include "runtime/interrupt.h"
 
 namespace lean {
 /** \brief Base class for all kernel exceptions. */
@@ -146,6 +145,21 @@ an `kernel_exception` or `exception`. Then, convert result into `Except KernelEx
 where `T` is the type of the lean objected represented by `A`.
 We use the constructor `KernelException.other <msg>` to handle C++ `exception` objects which
 are not `kernel_exception`.
+```
+inductive KernelException
+0  | unknownConstant  (env : Environment) (name : Name)
+1  | alreadyDeclared  (env : Environment) (name : Name)
+2  | declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr)
+3  | declHasMVars     (env : Environment) (name : Name) (expr : Expr)
+4  | declHasFVars     (env : Environment) (name : Name) (expr : Expr)
+5  | funExpected      (env : Environment) (lctx : LocalContext) (expr : Expr)
+6  | typeExpected     (env : Environment) (lctx : LocalContext) (expr : Expr)
+7  | letTypeMismatch  (env : Environment) (lctx : LocalContext) (name : Name) (givenType : Expr) (expectedType : Expr)
+8  | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
+9  | appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
+10 | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
+11 | other            (msg : String)
+```
 */
 template<typename A>
 object * catch_kernel_exceptions(std::function<A()> const & f) {
@@ -197,9 +211,6 @@ object * catch_kernel_exceptions(std::function<A()> const & f) {
     } catch (stack_space_exception & ex) {
         // 14 | deepRecursion
         return mk_cnstr(0, box(14)).steal();
-    } catch (interrupted & ex) {
-        // 15 | interrupted
-        return mk_cnstr(0, box(15)).steal();
     }
 }
 }

src/kernel/type_checker.cpp

@@ -287,7 +287,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
         throw kernel_exception(env(), "type checker does not support loose bound variables, replace them with free variables before invoking it");
 
     lean_assert(!has_loose_bvars(e));
-    check_system("type checker", /* do_check_interrupted */ true);
+    check_system("type checker");
 
     auto it = m_st->m_infer_type[infer_only].find(e);
     if (it != m_st->m_infer_type[infer_only].end())
@@ -410,7 +410,7 @@ static bool is_let_fvar(local_ctx const & lctx, expr const & e) {
     If `cheap == true`, then we don't perform delta-reduction when reducing major premise of recursors and projections.
     We also do not cache results. */
 expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) {
-    check_system("type checker: whnf", /* do_check_interrupted */ true);
+    check_system("type checker: whnf");
 
     // handle easy cases
     switch (e.kind()) {
@@ -1002,7 +1002,7 @@ bool type_checker::is_def_eq_unit_like(expr const & t, expr const & s) {
 }
 
 bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
-    check_system("is_definitionally_equal", /* do_check_interrupted */ true);
+    check_system("is_definitionally_equal");
     bool use_hash = true;
     lbool r = quick_is_def_eq(t, s, use_hash);
     if (r != l_undef) return r == l_true;

src/lake/examples/scripts/.gitignore

@@ -1 +1,2 @@
 lakefile.olean
+lake-manifest.json

src/lake/tests/clone/test.sh

@@ -11,9 +11,12 @@ fi
 
 ./clean.sh
 
+# Test Lake's management of a single Git-cloned dependency.
+
 mkdir hello
 pushd hello
 $LAKE init hello
+git checkout -b master
 git config user.name test
 git config user.email [email protected]
 git add --all

src/lake/tests/manifest/test.sh → src/lake/tests/depTree/test.sh

@@ -11,7 +11,8 @@ fi
 
 ./clean.sh
 
-# tests issues:
+# Test the functionality of Lake's dependency resolution
+# in many edge cases with a full tree of dependencies.
 # https://github.com/leanprover/lake/issues/70
 # https://github.com/leanprover/lake/issues/84
 # https://github.com/leanprover/lake/issues/85