Can some inline code blocks stay unprocessed in Verso?

Stream: general

[Dan Abramov]

@Terence Tao's Analysis Lean companion is using Verso to generate the website. The source of truth are these sheets with definitions and exercise which the reader can work through in a local VS Code checkout. It's nice to be able to generate the site from them directly, but there is also a minor issue.

The issue is that Verso parses the docstring and tries to interpret everything inside backticks as something resolvable. For example, consider this intro text from this file:

/-!
# Analysis I, Section 3.4: Images and inverse images

Main constructions and results of this section:

- Images and inverse images of (Mathlib) functions, within the framework of Section 3.1 set
  theory. (The Section 3.3 functions are now deprecated and will not be used further.)
- Connection with Mathlib's image `f '' S` and preimage `f ⁻¹' S` notions.
-/

In the generated Verso page, f and S appear kind of broken:

Screenshot 2025-08-01 at 19.48.33.png

It is technically possible to placate verso by literally defining them as variables:

variable (X : Type) (S : _root_.Set X) (f : X → X)

However, they would serve no purpose for the rest of the section and pollute the tactic state scope in every theorem (which is why I removed them). Another alternative I considered was wrapping that variable and the docstring into its own section, but this would look a bit noisy in the Verso page and probably not much less confusing. Yet another option is to rephrase such terms to avoid specific variables, e.g. write Set.image and Set.preimage instead. However, that is sometimes inconvenient. And of course one could omit the backticks altogether, but this would look worse in VS Code. This looks nice and readable:

Screenshot 2025-08-01 at 19.52.29.png

Is there a nice way to get around this? What would be the idiomatic suggestion from someone familiar with how Verso is intended to be used?

Thanks!

[Bhavik Mehta]

I believe

{lit}`f '' S`

should do what you want here. That said, I haven't tested this in the analysis project, but if not then I think it shouldn't be too hard to write a role expander for this

[Pim Otte]

I think what we want is a similar option like logInlines from one of the existing genres. As I understand it, it would do a best effort elaboration and just not show the errors.

This is nice, because it will then still link constants, but not complain if stuff is not fully typed.

I've been a bit busy with other projects, so feel free to remove the sections and/or apply Bhaviks suggestion in the mean time.

(As a side note, maybe this thread would be better suited in the Analysis book stream.)

[Li Xuanji]

I couldn't get {lit} working in the analysis project (maybe it has the wrong genre?) but I put up a PR to at least disable the wavy underline. (The hovers don't seem to be configurable via CSS)

[David Thrane Christiansen]

I just saw this thread - sorry for not seeing it before. The right short-term solution here is to have Verso's heuristic attempt to interpret Markdown just give up in these cases, rather than rendering an error message, like @Pim Otte is suggesting.

I'm working on bringing Verso syntax to docstrings, and that will solve the problem - fundamentally, the issue here is that Markdown provides no way to say which code elements are intended to be references, and which aren't. Then something like @Bhavik Mehta's suggestion will work.

[Dan Abramov]

Thanks! I’m not sure if {lit} is a bit heavy-handed syntax wise. Part of the point is to make reading in the editor intuitive, and unusual syntax may raise more questions. Not that I have a better suggestion.

[David Thrane Christiansen]

That syntax won't be necessary. It's used in the various Verso books because there's a linter that attempts to suggest various things that a backticked element could be (e.g. variable, tactic name, keyword) and suggests annotating it as such, and {lit} silences the linter and says "no, this is really just plain monospace text". It would work equally well to disable that linter.