Internal error

Stream: new members

[Kevin Sullivan]

Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.152'.

This error is produced by the following code. Lean nightly from 8/30. Haven't tried most recent build. Class started with this version in fall and has stuck with it.

import Mathlib.Data.Set.Basic

example (α : Type) (r s t : Set α) : (r ∩ (s ∪ t)) = ((r ∩ s) ∪ (r ∩ t)) := by
    apply Set.ext   -- replaces = with logical ↔
    intro x
    apply Iff.intro
    intro h
    cases h with
    | intro hl hr =>
      _

[Kyle Miller]

In a recent mathlib, I'm not seeing anything but the "unsolved goals" error. Where is it being reported for you?

[Kevin Sullivan]

Kyle Miller said:

In a recent mathlib, I'm not seeing anything but the "unsolved goals" error. Where is it being reported for you?

Let me pull the most recent and I'll get back. Thank you.

[Kevin Sullivan]

Kevin Sullivan said:

Kyle Miller said:

In a recent mathlib, I'm not seeing anything but the "unsolved goals" error. Where is it being reported for you?

Let me pull the most recent and I'll get back. Thank you.

All good with most recent.

[Kaixin Wang]

I think I have downloaded Lean 4 and elan on vscode, but I am 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 d.registerCommand (/Applications/Visual Studio Code-3.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:154:205087)
at Object.registerCommand (/Applications/Visual Studio Code-3.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:164:22263)
at /Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:196120
at /Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:197301
at Generator.next (<anonymous>)
at /Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:193375
at new Promise (<anonymous>)
at s (/Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:193120)
at /Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:195272
at /Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:278665
at Generator.next (<anonymous>)
at /Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:278447
at new Promise (<anonymous>)
at i (/Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:278192)
at t.displayInternalErrorsIn (/Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:278614)
at /Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:195236
at Generator.next (<anonymous>)
at s (/Users/kaiwang/.vscode/extensions/leanprover.lean4-0.0.176/dist/extension.js:1:193177)

[Kaixin Wang]

Do you have any advice how to fix this? Thank you!

[Marc Huisinga]

@Kaixin Wang Are you still encountering this issue?

[Kaixin Wang]

Marc Huisinga said:

Kaixin Wang Are you still encountering this issue?

Yes, I am still encountering this issue. I reinstall and uninstalled this many times, but the problem still persists.

[Kaixin Wang]

I am no longer running into this issue as of now.