Errors with new doc.verso

Stream: lean4

[Thomas Zhu]

I have two separate issues regarding the new verso-style docstrings. Currently (v4.24.0-rc1), the following raises an enigmatic error:

set_option doc.verso true

/--
```
some code
```
-/
def a := 0  -- internal exception #2

My second issue is more a feature request. Doc-gen4 supports citations using the Markdown reference style by referencing a citation in docs/references.bib. However, currently the following raise errors if doc.verso is true (as expected):

set_option doc.verso true

/--
doc-gen4 style citation: [wiles1995]
-/
def b := 0

/--
doc-gen4 style named citation: [text][wiles1995]
-/
def c := 0

Is there any plan to make this ignore errors, or even directly support citations in verso docstrings?

[Jason Reed]

I looked into your first issue a little and I think I see some (but not all) of why it's happening. Filed https://github.com/leanprover/verso/issues/538 which contains a little explanation.

[Jason Reed]

Not sure about our plans for citations yet, but it seems like a reasonable ask in general. It might be that a different concrete syntax would fit better into the way verso expresses hyperlinks.

[David Thrane Christiansen]

Thanks for checking this out!

This option is still at the "here there be dragons" stage - this code works fine on the latest nightly. I'll make an announcement when it's more ready for use and broader testing.

As far as references go, the subset of Verso that's in Lean docstrings is arbitrarily extensible by users. There will be documentation on how to do this once it's ready, but here's a little taste.

[David Thrane Christiansen]

That's just a little sketch of a citation command, but it could be made to do things like parse BibTeX, give better error messages, support all the various natbib options, and so forth, and this can be a library developed outside of core. We may eventually have one in core as well, but just as Lean's extensibility means you don't have to wait for us to do something, Verso's means that you are also able to mold the tool to your needs.

[Thomas Zhu]

Thank you for the explanation! I didn't know about the extension mechanism, it seems like exactly what I wanted.

[Jason Reed]

Oh, great! Closed the issue, then. Thought my toolchain was set to nightly on my local machine, but it wasn't.

[David Thrane Christiansen]

Once it's been put a bit more through it's paces, I'll get some documentation into your hands. I'm using it myself for a fair bit of docs work right now, on the theory that it's better for me to encounter the annoying parts and fix them before anyone else starts to rely on it.