fix: work around go-to-definition limitation in language server

leanprover / verso

Lean documentation authoring tool

Apache License 2.0

120 stars 14 forks source link

fix: work around go-to-definition limitation in language server #148

Closed david-christiansen closed 2 months ago

david-christiansen commented 2 months ago

The language server presently assumes that each module path has a unique source directory corresponding to it. This rearranges Verso's internals so that this is the case.

Imports of Verso.Genre.Manual should now be VersoManual, and Verso.Genre.Blog should now be VersoBlog.

david-christiansen commented 2 months ago

This is a workaround for https://github.com/leanprover/lean4/issues/4962