vscode-lean4 icon indicating copy to clipboard operation
vscode-lean4 copied to clipboard

InfoView not working Xubuntu 22.04

Open solmersa opened this issue 6 months ago • 1 comments

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)

solmersa avatar Aug 13 '24 11:08 solmersa