Skip to content

[Bug] [Lean] Clicking into the file quickly breaks the proof view #374

Description

@pimotte

How can we reproduce this issue?

Example:

  1. Start the extension with a Lean file open
  2. Immediately click a proof area.
  3. Observe the infoview being stuck at Waiting for Lean server to start...

What was supposed to happen?

It should update to show the goals.

(Probably some sort of race condition)

Metadata

Metadata

Assignees

Labels

bugSomething isn't working

Type

No type
No fields configured for issues without a type.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions