search

leanprover / vscode-lean4

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

A small bug report: potential conflict with Harmonic Lean 4 #538

Closed Rustastra closed 1 month ago

Rustastra commented 1 month ago

Description

I was getting this error

Internal error (while activating Lean 4 extension): Error: command 'lean4.troubleshooting.showOutput' already exists

Error: command 'lean4.troubleshooting.showOutput' already exists
    at T0.registerCommand (file:///private/var/folders/t4/9l3c8mzj129fr0dgbkjzk_j80000gn/T/AppTranslocation/73E1F5EA-9956-4060-89E4-608532D0FCF8/d/Visual%20Studio%20Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:114:31536)
    at Object.registerCommand (file:///private/var/folders/t4/9l3c8mzj129fr0dgbkjzk_j80000gn/T/AppTranslocation/73E1F5EA-9956-4060-89E4-608532D0FCF8/d/Visual%20Studio%20Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:156:36293)
    at /Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:193192
    at /Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:194373
    at Generator.next (<anonymous>)
    at /Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:192044
    at new Promise (<anonymous>)
    at s (/Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:191789)
    at /Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:192259
    at /Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:280566
    at Generator.next (<anonymous>)
    at /Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:280407
    at new Promise (<anonymous>)
    at i (/Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:280152)
    at t.displayInternalErrorsIn (/Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:280515)
    at /Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:192223
    at Generator.next (<anonymous>)
    at s (/Users/olga/.vscode/extensions/leanprover.lean4-0.0.183/dist/extension.js:1:191846)

Context

I needed to re-set up Lean + VS Code + Mathlib today, and I started hitting this error. I am not yet 100% sure, but I believe this is due to Harmonic Lean 4 extension (which I experimentally enabled).

Steps to Reproduce

  1. Install Lean 4 VS Code extension
  2. Install Harmonic Lean 4 extension
  3. Restart VS Code
  4. Open mathematics in lean project

Expected behavior: No errors

Actual behavior: When I open VS Code, I get a dialog window with the error and a suggestion to report it.

Versions

[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)] 0.0.183 [Output of lean --version in the folder that the issue occured in]
[OS version] Sonoma 14.6

Additional Information

The error seems to go away when I disable Harmonic Lean 4

Impact

Low impact

mhuisi commented 1 month ago

Since the Harmonic extension appears to be a fork of this one, I don't think it was intended to be enabled together with this extension. Looking at the marketplace page, it appears to also have been last released on 2024-03-01, so it is a very out-of-date fork.