jump to module on output of #find_home

Stream: general

[Johan Commelin]

#find_home is super useful. It prints a list of modules in the infoview where I should move little helper lemmas and such. But navigating to those modules is somewhat nontrivial, because I can't Ctrl-click on the output. Does someone know how to fix this?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

One could use the new widget message functionality to emit a clickable link instead of a plain string in the #find_home message. The one annoying part seems to be that EnvironmentHeader.moduleData doesn't keep track of which URIs it loaded the modules from, so one might have to query the server for this.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I wrote a simple implementation in leanprover-community/import-graph#17.

[Kim Morrison]

@Damiano Testa, would you like to exercise your new powers at import-graph by testing this one out and merging?

[Kim Morrison]

(In an ideal world Mathlib would then automatically upgrade the dependency, but that part of our automation remains very flaky!)

[Damiano Testa]

Ah, yes!

[Damiano Testa]

I can see the Merge button... let me try to push it! :smile:

[Damiano Testa]

The merge seems to have worked! (I tested it locally a bit before merging.)

[Damiano Testa]

@Wojciech Nawrocki thanks!

I like the clickable links! My (very very slight) concern might be that it could become trickier to copy from the infoview without triggering the opening of the module. However, whether that is a serious issue or not is probably best left to using it and seeing how it works in practice.