Try yet again to fix the import/build bug without introducing flakiness.

Author: Julian

lua/lean/infoview.lua

@@ -1653,12 +1653,15 @@ end
 
 ---@private
 ---Called by the $/lean/fileProgress handler.
----Only updates pins whose processing state at their position has changed.
+---Skips updates only when the pin's position is not being processed
+---and was already not being processed on the last notification.
+---During processing, every notification may carry new diagnostics
+---(e.g. lake build output) worth re-rendering.
 function infoview.__on_file_progress(uri)
   for _, each in pairs(infoview._by_tabpage) do
     for _, pin in pairs(each:pins_for(uri)) do
-      local current = progress.at_or_file(pin.__position_params)
-      if current ~= pin.__last_processing then
+      local current = progress.at(pin.__position_params)
+      if current ~= nil or pin.__last_processing ~= nil then
         pin.__last_processing = current
         pin:request_update()
       end

lua/lean/progress.lua

@@ -46,42 +46,6 @@ function M.at(params)
   return info and (info.kind or M.Kind.processing)
 end
 
----Like `at`, but also returns processing if the file has processing
----ranges that haven't reached the given position yet.
----This is needed when e.g. imports are building and the cursor is on a
----later line that hasn't been reached yet.
----@param params lsp.TextDocumentPositionParams
----@return LeanFileProgressKind? kind
-function M.at_or_file(params)
-  local infos = M.proc_infos[params.textDocument.uri]
-  if not infos then
-    return M.Kind.processing
-  end
-  if #infos == 0 then
-    return
-  end
-
-  local line = params.position.line
-  ---@type LeanFileProgressProcessingInfo?
-  local info = vim.iter(infos):find(function(each)
-    return (line >= each.range.start.line) and (line <= each.range['end'].line)
-  end)
-  if info then
-    return info.kind or M.Kind.processing
-  end
-
-  -- Cursor is not in any processing range. If processing hasn't reached
-  -- the cursor yet (cursor is past all ranges), treat as processing.
-  -- Lean processes top-to-bottom, so this means the cursor's line is
-  -- waiting for earlier lines (e.g. imports) to finish.
-  local max_end = vim.iter(infos):fold(-1, function(acc, each)
-    return math.max(acc, each.range['end'].line)
-  end)
-  if line > max_end then
-    return M.Kind.processing
-  end
-end
-
 ---Calculate the percentage of a buffer which finished processing.
 ---@param bufnr? number the buffer number, defaulting to 0
 ---@return number the percentage of *finished* lines as a number from 0 to 100

spec/infoview/contents_spec.lua

@@ -520,12 +520,11 @@ describe('interactive infoview', function()
   )
 
   describe(
-    'file progress updates when cursor is not on a processing line',
-    helpers.clean_buffer('#eval IO.sleep 5000\n\n#check (37 : Nat)', function()
-      helpers.move_cursor { to = { 3, 0 } }
-      helpers.wait:for_file_processing()
-
+    'file progress updates',
+    helpers.clean_buffer('#check (37 : Nat)', function()
       it('does not trigger redundant updates for unchanged progress', function()
+        helpers.wait:for_processing()
+
         local uri = vim.uri_from_bufnr(0)
         local pin = infoview.get_current_infoview().pin
 
@@ -543,7 +542,11 @@ describe('interactive infoview', function()
         assert.are.equal(0, update_count)
 
         -- But a genuine state change does trigger an update.
-        require('lean.progress').proc_infos[uri] = {}
+        require('lean.progress').proc_infos[uri] = {
+          {
+            range = { start = { line = 0, character = 0 }, ['end'] = { line = 0, character = 0 } },
+          },
+        }
         infoview.__on_file_progress(uri)
         assert.are.equal(1, update_count)