RFC: Command-clickable file links in the InfoView

[BoltonBailey]

Proposal

In the InfoView, when I get an error like

error: ././././Foo/Bar.lean:13:37: application type mismatch

or

`/Users/boltonbailey/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lake setup-file /Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/Mathlib/Logic/IsEmpty.lean Init Mathlib.Logic.Function.Basic Mathlib.Logic.Relator` failed:

I would like to be able to click or command-click on the link to go to the file (or even the line) in question, as I would be able to do in the VSCode terminal.

• User Experience: This feature improves the user experience by making it easier to navigate to the source of an error.

• Beneficiaries: The Lean users and projects that benefit most from this feature would be those who work on projects which require frequent switching between files, and which are most likely to experience a build failure in a file that they have closed.

• Maintainability: This will likely not streamline maintainability, but would nevertheless be convenient.

Community Feedback

Here is a Lean Zulip thread. Not a discussion per se, but the concept has gotten some support.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.