Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feature request: in VSCode, open downstream files with errors #397

Open
kim-em opened this issue Feb 15, 2024 · 0 comments
Open

feature request: in VSCode, open downstream files with errors #397

kim-em opened this issue Feb 15, 2024 · 0 comments
Labels
RFC Request for comments

Comments

@kim-em
Copy link
Contributor

kim-em commented Feb 15, 2024

I would like a user interaction in VSCode that

  • starts a lake build
  • as errors occur, opens the relevant files in VSCode, but without changing the currently focussed tab

(I think I would also want this to check if there was an existing lake build running, and terminate that.)

Currently to achieve this one has to scroll up and down through the lake build log (which sometimes gets very slow), identifying file names and clicking on them.)

@kim-em kim-em added the RFC Request for comments label Feb 15, 2024
@kim-em kim-em changed the title feature request: open downstream files with errors feature request: in VSCode, open downstream files with errors Feb 15, 2024
@kim-em kim-em transferred this issue from leanprover/lean4 Feb 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
RFC Request for comments
Projects
None yet
Development

No branches or pull requests

1 participant