Merge branch 'master' of https://github.com/leanprover/lean4 into joachim/issue10821

Author: nomeata

.github/workflows/ci.yml

@@ -116,6 +116,7 @@ jobs:
         # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
         run: |
           check_level=0
+          fast=false
 
           if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=2
@@ -128,9 +129,13 @@ jobs:
             elif echo "$labels" | grep -q "merge-ci"; then
               check_level=1
             fi
+            if echo "$labels" | grep -q "fast-ci"; then
+              fast=true
+            fi
           fi
 
           echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
+          echo "fast=$fast" >> "$GITHUB_OUTPUT"
         env:
           GH_TOKEN: ${{ github.token }}
 
@@ -140,7 +145,8 @@ jobs:
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
-            console.log(`level: ${level}`);
+            const fast = ${{ steps.set-level.outputs.fast }};
+            console.log(`level: ${level}, fast: ${fast}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
@@ -165,7 +171,8 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                "os": "ubuntu-latest",
+                // usually not a bottleneck so make exclusive to `fast-ci`
+                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
                 // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
@@ -230,22 +237,22 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && level >= 1 ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
+                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
-                "test": true,
                 "shell": "bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
                 // See "Linux release" for release job levels; Grove is not a concern here
                 "enabled": isPr || level != 1,
+                "test": level >= 1,
                 "secondary": level == 0,
               },
               {
                 "name": "Windows",
-                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
                 "enabled": level >= 2,
                 "test": true,

src/Lean/Elab/App.lean

@@ -1252,8 +1252,11 @@ inductive LValResolution where
   The `baseName` is the base name of the type to search for in the parameter list. -/
   | localRec (baseName : Name) (fvar : Expr)
 
+private def mkLValError (e : Expr) (eType : Expr) (msg : MessageData) : MessageData :=
+  m!"{msg}{indentExpr e}\nhas type{indentExpr eType}"
+
 private def throwLValErrorAt (ref : Syntax) (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
-  throwErrorAt ref "{msg}{indentExpr e}\nhas type{indentExpr eType}"
+  throwErrorAt ref (mkLValError e eType msg)
 
 private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α := do
   throwLValErrorAt (← getRef) e eType msg
@@ -1322,9 +1325,19 @@ where
     | some (_, p2) => prodArity p2 + 1
 
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
-  let throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name) : TermElabM α := do
-    throwLValErrorAt ref e eType <| ← mkUnknownIdentifierMessage (declHint := fullName)
-      m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`"
+  let throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name)
+      (declHint := Name.anonymous) : TermElabM α := do
+    let msg ←
+      -- ordering: put decl hint, if any, last
+      mkUnknownIdentifierMessage (declHint := declHint)
+        (mkLValError e eType
+          m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`")
+    -- HACK: Simulate previous embedding of tagged `mkUnknownIdentifierMessage`.
+    -- The "import unknown identifier" code action requires the tag to be present somewhere in the
+    -- message. But if it is at the root, the tag will also be shown to the user even though the
+    -- current help page does not address field notation, which should likely get its own help page
+    -- (if any).
+    throwErrorAt ref m!"{msg}{.nil}"
   if eType.isForall then
     match lval with
     | LVal.fieldName ref fieldName suffix? _fullRef =>
@@ -1390,6 +1403,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
       return LValResolution.const baseStructName structName fullName
     throwInvalidFieldAt ref fieldName fullName
+      -- Suggest a potential unreachable private name as hint. This does not cover structure
+      -- inheritance, nor `import all`.
+      (declHint := (mkPrivateName env structName).mkStr fieldName)
   | none, LVal.fieldName ref _ (some suffix) _fullRef =>
     -- This may be a function constant whose implicit arguments have already been filled in:
     let c := e.getAppFn

src/Lean/Elab/Term/TermElabM.lean

@@ -1971,7 +1971,7 @@ where
     let env ← getEnv
     -- check for scope errors before trying auto implicits
     if env.isExporting then
-      if let [(npriv, _)] ← withEnv (env.setExporting false) <| resolveGlobalName (enableLog := false) n then
+      if let [(npriv, _)] ← withoutExporting <| resolveGlobalName (enableLog := false) n then
         throwUnknownIdentifierAt (declHint := npriv) stx m!"Unknown identifier `{.ofConstName n}`"
     if (← read).autoBoundImplicit &&
           !(← read).autoBoundImplicitForbidden n &&

src/Lean/Exception.lean

@@ -105,17 +105,8 @@ function directly.
 protected def «throwNamedErrorAt» [Monad m] [MonadError m] (ref : Syntax) (name : Name) (msg : MessageData) : m α :=
   withRef ref <| Lean.throwNamedError name msg
 
-/--
-Creates a `MessageData` that is tagged with `unknownIdentifierMessageTag`.
-This tag is used by the 'import unknown identifier' code action to detect messages that should
-prompt the code action.
-The end position of the range of an unknown identifier message should always point at the end of the
-unknown identifier.
-
-If `declHint` is specified, a corresponding hint is added to the message in case the name refers to
-a private declaration that is not accessible in the current context.
--/
-def mkUnknownIdentifierMessage [Monad m] [MonadEnv m] [MonadError m] (msg : MessageData)
+/-- Like `mkUnknownIdentifierMessage`, but does not tag the message. -/
+def mkUnknownIdentifierMessageCore [Monad m] [MonadEnv m] [MonadError m] (msg : MessageData)
     (declHint := Name.anonymous) : m MessageData := do
   let mut msg := msg
   let env ← getEnv
@@ -131,6 +122,21 @@ def mkUnknownIdentifierMessage [Monad m] [MonadEnv m] [MonadError m] (msg : Mess
           msg ++ .note m!"A private declaration `{c}` (from `{mod}`) exists but would need to be public to access here."
         else
           msg ++ .note m!"A public declaration `{c}` exists but is imported privately; consider adding `public import {mod}`."
+  return msg
+
+/--
+Creates a `MessageData` that is tagged with `unknownIdentifierMessageTag`.
+This tag is used by the 'import unknown identifier' code action to detect messages that should
+prompt the code action.
+The end position of the range of an unknown identifier message should always point at the end of the
+unknown identifier.
+
+If `declHint` is specified, a corresponding hint is added to the message in case the name refers to
+a private declaration that is not accessible in the current context.
+-/
+def mkUnknownIdentifierMessage [Monad m] [MonadEnv m] [MonadError m] (msg : MessageData)
+    (declHint := Name.anonymous) : m MessageData := do
+  let msg ← mkUnknownIdentifierMessageCore msg declHint
   return MessageData.tagged unknownIdentifierMessageTag msg
 
 /--

src/Std/Internal/Async/Signal.lean

@@ -238,23 +238,26 @@ def stop (s : Signal.Waiter) : IO Unit :=
   s.native.stop
 
 /--
-Create a `Selector` that resolves once `s` has received the signal. Note that calling this function starts `s`
-if it hasn't already started.
+Create a `Selector` that resolves once `s` has received the signal. Note that calling this function
+does not start the signal waiter.
 -/
-def selector (s : Signal.Waiter) : IO (Selector Unit) := do
-  let signalWaiter ← s.wait
-  return {
+def selector (s : Signal.Waiter) : Selector Unit :=
+  {
     tryFn := do
+      let signalWaiter : AsyncTask _ ← async s.wait
       if ← IO.hasFinished signalWaiter then
         return some ()
       else
+        s.native.cancel
         return none
 
     registerFn waiter := do
+      let signalWaiter ← s.wait
       discard <| AsyncTask.mapIO (x := signalWaiter) fun _ => do
         let lose := return ()
         let win promise := promise.resolve (.ok ())
         waiter.race lose win
 
-    unregisterFn := s.stop
+    unregisterFn := s.native.cancel
+
   }

src/Std/Internal/Async/TCP.lean

@@ -69,6 +69,44 @@ def accept (s : Server) : Async Client := do
   |> Async.ofPromise
   |>.map Client.ofNative
 
+/--
+Tries to accept an incoming connection.
+-/
+@[inline]
+def tryAccept (s : Server) : IO (Option Client) := do
+  let res ← s.native.tryAccept
+  let socket ← IO.ofExcept res
+  return Client.ofNative <$> socket
+
+/--
+Creates a `Selector` that resolves once `s` has a connection available. Calling this function
+does not start the connection wait, so it must not be called in parallel with `accept`.
+-/
+def acceptSelector (s : TCP.Socket.Server) : Selector Client :=
+  {
+    tryFn :=
+      s.tryAccept
+
+    registerFn waiter := do
+      let task ← s.native.accept
+
+      -- If we get cancelled the promise will be dropped so prepare for that
+      IO.chainTask (t := task.result?) fun res => do
+        match res with
+        | none => return ()
+        | some res =>
+          let lose := return ()
+          let win promise := do
+            try
+              let result ← IO.ofExcept res
+              promise.resolve (.ok (Client.ofNative result))
+            catch e =>
+              promise.resolve (.error e)
+          waiter.race lose win
+
+    unregisterFn := s.native.cancelAccept
+  }
+
 /--
 Gets the local address of the server socket.
 -/
@@ -143,20 +181,25 @@ def recv? (s : Client) (size : UInt64) : Async (Option ByteArray) :=
 
 /--
 Creates a `Selector` that resolves once `s` has data available, up to at most `size` bytes,
-and provides that data. Calling this function starts the data wait, so it must not be called
+and provides that data. Calling this function does not starts the data wait, so it must not be called
 in parallel with `recv?`.
 -/
-def recvSelector (s : TCP.Socket.Client) (size : UInt64) : Async (Selector (Option ByteArray)) := do
-  let readableWaiter ← s.native.waitReadable
-  return {
+def recvSelector (s : TCP.Socket.Client) (size : UInt64) : Selector (Option ByteArray) :=
+  {
     tryFn := do
+      let readableWaiter ← s.native.waitReadable
+
       if ← readableWaiter.isResolved then
         -- We know that this read should not block
         let res ← (s.recv? size).block
         return some res
       else
+        s.native.cancelRecv
         return none
+
     registerFn waiter := do
+      let readableWaiter ← s.native.waitReadable
+
       -- If we get cancelled the promise will be dropped so prepare for that
       discard <| IO.mapTask (t := readableWaiter.result?) fun res => do
         match res with
@@ -172,6 +215,7 @@ def recvSelector (s : TCP.Socket.Client) (size : UInt64) : Async (Selector (Opti
             catch e =>
               promise.resolve (.error e)
           waiter.race lose win
+
     unregisterFn := s.native.cancelRecv
   }
 

src/Std/Internal/Async/Timer.lean

@@ -69,17 +69,18 @@ def stop (s : Sleep) : IO Unit :=
   s.native.stop
 
 /--
-Create a `Selector` that resolves once `s` has finished. Note that calling this function starts `s`
-if it hasn't already started.
+Create a `Selector` that resolves once `s` has finished. `s` only starts when it runs inside of a Selectable.
 -/
-def selector (s : Sleep) : Async (Selector Unit) := do
-  return {
+def selector (s : Sleep) : Selector Unit :=
+  {
     tryFn := do
       let sleepWaiter ← s.native.next
       if ← sleepWaiter.isResolved then
         return some ()
       else
+        s.native.cancel
         return none
+
     registerFn waiter := do
       let sleepWaiter ← s.native.next
       BaseIO.chainTask sleepWaiter.result? fun
@@ -107,7 +108,7 @@ Return a `Selector` that completes after `duration`.
 -/
 def Selector.sleep (duration : Std.Time.Millisecond.Offset) : Async (Selector Unit) := do
   let sleeper ← Sleep.mk duration
-  sleeper.selector
+  return sleeper.selector
 
 /--
 `Interval` can be used to repeatedly wait for some duration like a clock.

src/Std/Internal/Async/UDP.lean

@@ -91,20 +91,24 @@ def recv (s : Socket) (size : UInt64) : Async (ByteArray × Option SocketAddress
 Creates a `Selector` that resolves once `s` has data available, up to at most `size` bytes,
 and provides that data. If the socket has not been previously bound with `bind`, it is
 automatically bound to `0.0.0.0` (all interfaces) with a random port.
-Calling this function starts the data wait, so it must not be called in parallel with `recv`.
+Calling this function does starts the data wait, only when it's used with `Selectable.one` or `combine`.
+It must not be called in parallel with `recv`.
 -/
-def recvSelector (s : Socket) (size : UInt64) :
-    Async (Selector (ByteArray × Option SocketAddress)) := do
-  let readableWaiter ← s.native.waitReadable
-  return {
+def recvSelector (s : Socket) (size : UInt64) : Selector (ByteArray × Option SocketAddress) :=
+ {
     tryFn := do
+      let readableWaiter ← s.native.waitReadable
+
       if ← readableWaiter.isResolved then
         -- We know that this read should not block
         let res ← (s.recv size).block
         return some res
       else
+        s.native.cancelRecv
         return none
     registerFn waiter := do
+      let readableWaiter ← s.native.waitReadable
+
       -- If we get cancelled the promise will be dropped so prepare for that
       discard <| IO.mapTask (t := readableWaiter.result?) fun res => do
         match res with
@@ -120,6 +124,7 @@ def recvSelector (s : Socket) (size : UInt64) :
             catch e =>
               promise.resolve (.error e)
           waiter.race lose win
+
     unregisterFn := s.native.cancelRecv
   }
 

src/Std/Internal/UV/Signal.lean

@@ -77,6 +77,15 @@ This function has different behavior depending on the state of the `Signal`:
 @[extern "lean_uv_signal_stop"]
 opaque stop (signal : @& Signal) : IO Unit
 
+/--
+This function has different behavior depending on the state of the `Signal`:
+- If it is initial or finished this is a no-op.
+- If it's running then it drops the accept promise and if it's not repeatable it sets
+  the signal handler to the initial state.
+-/
+@[extern "lean_uv_signal_cancel"]
+opaque cancel (signal : @& Signal) : IO Unit
+
 end Signal
 
 end UV

src/Std/Internal/UV/TCP.lean

@@ -95,6 +95,18 @@ Accepts an incoming connection on a listening TCP socket.
 @[extern "lean_uv_tcp_accept"]
 opaque accept (socket : @& Socket) : IO (IO.Promise (Except IO.Error Socket))
 
+/--
+Tries to accept an incoming connection on a listening TCP socket.
+-/
+@[extern "lean_uv_tcp_try_accept"]
+opaque tryAccept (socket : @& Socket) : IO (Except IO.Error (Option Socket))
+
+/--
+Cancels the accept request of a socket.
+-/
+@[extern "lean_uv_tcp_cancel_accept"]
+opaque cancelAccept (socket : @& Socket) : IO Unit
+
 /--
 Shuts down an incoming connection on a listening TCP socket.
 -/