vscode-lean4 icon indicating copy to clipboard operation
vscode-lean4 copied to clipboard
verified publisher icon leanprover

Infoview spinner keeps spinning on fatal error

Open Kha opened this issue 11 months ago • 0 comments

Description

Image

Context

n/a

Steps to Reproduce

  1. open file with out-of-date deps
  2. observe spinner

Expected behavior: The infoview should alert users on the error Actual behavior: The infoview encourages users to keep waiting, futilely

Versions

Operating system: Linux (release: 6.12.1) CPU architecture: x64 CPU model: 16 x AMD Ryzen 7 7840U w/ Radeon 780M Graphics Available RAM: 32.92 GB

VS Code version: Reasonably up-to-date (version: 1.96.2) Lean 4 extension version: 0.0.194 Curl installed: true Git installed: true Elan: Reasonably up-to-date (version: 3.1.1) Lean: Reasonably up-to-date (version: 4.16.0-nightly-2025-02-02) Project: Valid Lean project (path: /home/sebastian/lean/do-supplement)

Additional Information

n/a

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

Kha avatar Feb 02 '25 11:02 Kha