Verso include lean-code from imported file

Stream: general

[Joseph Tooby-Smith]

In Verso given the name of a definition or theorem, I know that Verso allows you to print the doc-string corresponding to that name. Is there a way to print the Lean code corresponding to that name without having to copy and paste it?

For example I want something like:

import Mathlib
import VersoManual

open Verso.Genre Verso.Genre.Manual


#doc (Manual) "Test" =>

%%%

tag := "Test"

%%%

{docstring Real} -- shows doc-string

{leanCode Real} -- I want something like this to show lean code

[Joachim Breitner]

I doubt it; the docstring is stored as part of the olean, the source is not. Maybe verso could use the declaration range and read the source file, but then it may be hard to elaboate it for all the nice hovers.

It may work if the source file is already annotated by verso. We do that with the blog posts, where the code is processed by a different lean file, and support naming parts of the source file:

%example mergeDef
def merge (xs ys : Array Nat) : Array Nat := go 0 0 #[]
  where go (i j : Nat) (acc : Array Nat) : Array Nat :=
    if _ : i < xs.size then
      if _ : j < ys.size then
        if xs[i] ≤ ys[j] then
          go (i + 1) j (acc.push xs[i])
        else
          go i (j + 1) (acc.push ys[j])
      else
        xs[i:]
    else
      ys[j:]
%end

But this doesn’t work for definitions from normal libraries, I fear.

(Just giving first approximations here, @David Thrane Christiansen is the expert)

[Joseph Tooby-Smith]

Ok, thanks @Joachim Breitner ! This is roughly what I expected. I can probably settle for it without hovers - and I think I know how to do this using the declaration range.

[David Thrane Christiansen]

This is correct. Right now, there 's two ways to get code into Verso:

1. Include it in the document itself. In these cases, the Lean process that's elaborating the document can be used to elaborate the code, saving the result. There's a lot of freedom to control this process as well, like using different scopes or environments for different blocks of code.

2. Extract it from a complete Lean module using the SubVerso library, which is a tool for extracting metadata from Lean source code that's compatible with every Lean release going back to 4.0.0. It generates a JSON format that works in all those versions as well. It supports named examples (as @Joachim Breitner demonstrated) as well as extracting whole modules, but it doesn't have convenient support for saving certain named declarations. That would probably be fairly easy to add - I don't have the bandwidth right now to do it myself, however. You could also implement that as a separate tool built on the SubVerso library.

Basically, to get the nice highlighted code, you need to have an info tree and syntax. This means that the elaborator has to run right before the code is grabbed. But this can be done in lots of ways, and a tool that dumps a JSON object where keys are names, values are their source, and there's a separate table with docstrings would be both very doable and a nice way to implement what you're looking to do here.