-
Notifications
You must be signed in to change notification settings - Fork 414
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
Delaboration of re-exported names #2524
Comments
@tydeu Let's just turn these into |
@Kha Printing it always as |
This replaces `export Lean (Name NameMap)` and `export System (SearchPath FilePath)` with the relevant `open` commands. This fixes docgen output so that it can refer to, for example, `Lean.Name` instead of `Lake.Name`. The reason for these `export`s was convenience: by doing `open Lake` you could get these aliases for free. However, aliases affect pretty printing, and the Lake aliases took precedence. We don't want to disable pretty printing re-exported names because this can be a valid pattern (names could incrementally get re-exported from namespace to parent namespace). In the future we might implement a feature to be able to `scope export` some names. Closes leanprover#2524
…n-API" `export`s Heuristic: an "API" `export` is one that exports a declaration to a parent namespace. This PR makes it so that aliases created by `export` from exporting a name into some parallel namespace are not considered. This is motivated by Lake's use of `export` to make some declarations like `Lean.Name` permanently available in the `Lake` namespace. A consequence to this is that in docgen, we see `Lean.Name` pretty printed as `Lake.Name`. Another solution would be to create a `scoped open` command that auto-opens some names whenever a namespace is activated. If that is ever implemented, it would be easy to revert the changes in this PR. Closes leanprover#2524
I have two competing solutions to this problem:
I'd prefer option 1 if @tydeu would be ok with it (and if it wouldn't cause problems for lakefiles), but otherwise I'll leave it to @Kha and the triage team to decide which of these two solutions (if either) might be acceptable. There's a third option, which is to implement a |
@kmill I am fine with a temporary stop-gap measure, but I would very much want this fixed in the future. Having to manually |
This replaces `export Lean (Name NameMap)` and `export System (SearchPath FilePath)` with the relevant `open` commands. This fixes docgen output so that it can refer to, for example, `Lean.Name` instead of `Lake.Name`. The reason for these `export`s was convenience: by doing `open Lake` you could get these aliases for free. However, aliases affect pretty printing, and the Lake aliases took precedence. We don't want to disable pretty printing re-exported names because this can be a valid pattern (names could incrementally get re-exported from namespace to parent namespace). In the future we might implement a feature to be able to `scope export` some names. Closes leanprover#2524
This replaces `export Lean (Name NameMap)` and `export System (SearchPath FilePath)` with the relevant `open` commands. This fixes docgen output so that it can refer to, for example, `Lean.Name` instead of `Lake.Name`. The reason for these `export`s was convenience: by doing `open Lake` you could get these aliases for free. However, aliases affect pretty printing, and the Lake aliases took precedence. We don't want to disable pretty printing re-exported names because this can be a valid pattern (names could incrementally get re-exported from namespace to parent namespace). In the future we might implement a feature to be able to `scoped open` some names. Breaking change: Lakefiles that refer to `FilePath` may need to change this to `System.FilePath` or otherwise add `open System (FilePath)`. Closes #2524
…rover#5688) This replaces `export Lean (Name NameMap)` and `export System (SearchPath FilePath)` with the relevant `open` commands. This fixes docgen output so that it can refer to, for example, `Lean.Name` instead of `Lake.Name`. The reason for these `export`s was convenience: by doing `open Lake` you could get these aliases for free. However, aliases affect pretty printing, and the Lake aliases took precedence. We don't want to disable pretty printing re-exported names because this can be a valid pattern (names could incrementally get re-exported from namespace to parent namespace). In the future we might implement a feature to be able to `scoped open` some names. Breaking change: Lakefiles that refer to `FilePath` may need to change this to `System.FilePath` or otherwise add `open System (FilePath)`. Closes leanprover#2524
Description
Delaborating things that contain names of re-exported types can chose the wrong name for the type.
This most notably causes incorrect doc-gen4 renders: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Confusing.20delaboration.20in.20.20doc-gen/near/388158478
Steps to Reproduce
Delaboration of
Lake.Name
:Further minified:
Expected behavior: We get
Lean.Name
Actual behavior: We get
Lake.Name
Reproduces how often: Always
The text was updated successfully, but these errors were encountered: