doc: add documentation for builtin attributes #8173
Conversation
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
I'm going to need some help for the |
|
Not sure if anyone with that knowledge will be around soon, so maybe split into one PR per (set of related) attributes, for quicker merging of easy ones? |
|
I guess I'll just postpone |
leanprover-community-bot
added
the
builds-mathlib
|
I guess this would fix #8432 well enough. |
|
@david-christiansen, could you take a look at the documentation? I'm sure there some parts that could be improved |
src/Lean/Compiler/ExportAttr.lean
Outdated
| This feature can be used in combination with `@[extern]` to allow for cyclic references | ||
| between files: | ||
| ``` | ||
| -- File1.lean | ||
| @[extern "my_foo_function"] | ||
| opaque fooFn : Nat → Nat | ||
| def bar (x : Nat) : Nat := ... -- can use `foo` indirectly as `fooFn` | ||
| -- File2.lean | ||
| import File1 | ||
| @[export my_foo_function] | ||
| def foo (x : Nat) : Nat := ... -- can use `bar` | ||
| ``` | ||
| Note however that this only works in compiled code. |
There was a problem hiding this comment.
Is this something that we want to advertise in the docstring? I've always understood it to be more of a necessary kludge than something we really want to be encouraging the use of. Perhaps this should be an in-source comment instead of the docstring?
There was a problem hiding this comment.
I want to answer the question "why is @[export] here" for everyone who sees it in the Lean source code. Should I maybe refer to it as a "hack" then and remove the example?
There was a problem hiding this comment.
I'd really prefer that we not advertise this to everyone who sees @[export] in any Lean code anywhere in the world and scrubs the mouse over it. Users of Lean are a more important audience than people working on Lean itself, and I think this is more likely to make their lives worse, rather than better.
A comment next to the attribute would let any Lean developer who does "go to def" see this, resolving their curiosity, as would comments next to instances of the trick.
There was a problem hiding this comment.
Note that this trick actually doesn't work in user code, it's a lean core exclusive. It needs to be compiled as a builtin or something; I never managed to get the lake invocation to make it work, if one exists.
There was a problem hiding this comment.
Yeah I changed the documentation to instead mention an FFI example
src/Lean/BuiltinDocAttr.lean
Outdated
| Makes the documentation and location of a declaration available as a builtin. | ||
| This allows the documentation of core Lean features to be visible without importing the file they | ||
| are defined in. This is only possible because of bootstrapping and should not be used outside of |
There was a problem hiding this comment.
| are defined in. This is only possible because of bootstrapping and should not be used outside of | |
| are defined in. This is only needed because of bootstrapping and should not be used outside of |
There was a problem hiding this comment.
The thing I wanted to say here is "you can only have documentation visible without importing the file it's in if you have a bootstrapping step"
| with `Formatter` in the parameter types." | ||
| @[builtin_init mkCombinatorFormatterAttribute] opaque combinatorFormatterAttribute : ParserCompiler.CombinatorAttribute | ||
| "Register a formatter for a parser combinator" | ||
| `Lean.PrettyPrinter.mkCombinatorFormatterAttribute -- TODO (bootstrapping): remove if possible |
There was a problem hiding this comment.
What does this comment mean here? Does this meant here should be a stage0 update, after which this could then be removed?
There was a problem hiding this comment.
If this would be removed, the attribute would correctly have a ref to combinatorFormatterAttribute, where the documentation is. But, the environment extension would also be renamed, causing existing .olean data to be ignored (I think that's how it works?). Which is to say there would probably need to be a separate PR for removing this line and doing a stage0 update (the usual stage0 update probably wouldn't work because test failures).
|
OK, I found a couple tiny detail things, and one substantive question. Otherwise, we're good to go - thanks! I see that the |
After a stage0 update, yeah. So there needs to be a follow-up PR (maybe also with |
Co-authored-by: David Thrane Christiansen <[email protected]>
…to attribute-docs
OK. In the morning, I'll just give it a quick local test to make sure things work as we expect after the Thanks! |
|
Thanks for the contribution and the reviewing! |
This PR un-does the temporary changes made in #8173 for bootstrapping purposes.
This PR adds documentation to builtin attributes like `@[refl]` or `@[implemented_by]`. Closes leanprover#8432 --------- Co-authored-by: David Thrane Christiansen <[email protected]> Co-authored-by: David Thrane Christiansen <[email protected]>
This PR un-does the temporary changes made in leanprover#8173 for bootstrapping purposes.
This PR un-does the temporary changes made in leanprover#8173 for bootstrapping purposes.
8 participants
This PR adds documentation to builtin attributes like
@[refl]or@[implemented_by].Closes #8432