search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
155 stars 47 forks source link

InfoView not working Xubuntu 22.04 #517

Open solmersa opened 1 month ago

solmersa commented 1 month ago

The infoview always displays "No Info found", All messages is always (0).

Also after a Lean4: Project Build Project

The infoview always displays "Error updating: Error fetching goals: Client is not running."

Here is my setup:

Operating system: Linux (release: 6.5.0-28-generic) CPU architecture: x64 CPU model: 1 x Intel(R) Core(TM) i5-3570K CPU @ 3.40GHz Available RAM: 5.11 GB

VS Code version: Reasonably up-to-date (version: 1.81.1) Lean 4 extension version: 0.0.176 Curl installed: true Git installed: true Elan: Reasonably up-to-date (version: 3.1.1) Lean: Reasonably up-to-date (version: 4.10.0) Project: Valid Lean project (path: /home/sdavila/lean3)

Elan toolchains: 

leanprover/lean4:stable (overridden by '/home/sdavila/lean3/lean-toolchain')

Lean (version 4.10.0, x86_64-unknown-linux-gnu, commit c375e19f6b65, Release)
mhuisi commented 2 weeks ago

Does the extension display any other errors? (E.g. as a notification in the bottom right or in the Troubleshooting: Show Output menu)