Mario Carneiro

> Part 2 can be moved into a separate PR, no? As I indicated in the PR, I'm not sure how the protocol for this works. Do I open two...

It does, did you want me to put `(part 2)`?

this PR was meant to be merged immediately after part 1, but I guess it wasn't and now presumably it has rotted

The FIXMEs are fine to merge as is. The issue is that while it would be nice to have docs for these bits of syntax, they appear far too often...

Yes, you see the issue now. There is a difference between documentation useful for people reading the parser or hovering references in a `syntax` declaration, and documentation useful for people...

> > I think the best way to address this in the near term is to selectively avoid `@[builtin_doc]` > > Hmm, but that only helps users on a bare...

Yes, that is correct. The fact that `import Lean` is needed for several not obviously related features to work, like go to definition and hovers for core syntax, is a...

> Refactors in a file may change the statements of theorems in another file without breaking anything Note that this is also a problem for proof parallelism, as it is...

I was aware of this issue in the original implementation. The problem is that because `inherit_doc` is an attribute, it runs after the `def bar := 2` main part of...

Your two examples are not the same. Did you try attempting to complete the proof using `exact hp; exact hq` in the REPL? It is expected that calling `apply test`...