Tables in verso

Stream: general

[Peter Pfaffelhuber]

Upcoming semester, I am teaching a Lean course, and I would like to use verso for this. Is there a way to make a (simple) table? The usual Markdown syntax does not seem to work.

[Henrik Böving]

CC @David Thrane Christiansen

[Markus Himmel]

There is a table at https://lean-lang.org/doc/reference/latest/Basic-Types/Tuples/#tuples, the source of which is at https://github.com/leanprover/reference-manual/blob/4854c14961cf421aa5d8c4b91e1a2241afe0e39d/Manual/BasicTypes/Products.lean#L31

[David Thrane Christiansen]

Verso doesn't have a built-in table syntax, but rather relies on the extensibility mechanism to let users define them as a library. @Markus Himmel linked to an example of that - is it enough to help you get done what you need?

[Peter Pfaffelhuber]

Thanks for the answers and the hint! I will try to make this work using the ref.

[David Thrane Christiansen]

Please feel free to ping me any time if you get stuck - there's not yet enough guidance on how to use this thing.

[Peter Pfaffelhuber]

David Thrane Christiansen schrieb:

Please feel free to ping me any time if you get stuck - there's not yet enough guidance on how to use this thing.

Now my tables work, thanks for pointing me in the right direction... A quick follow-up question: Is there a way to force a newline (<br>) within a cell in a table?

[David Thrane Christiansen]

Great to hear it!

The markup language doesn't include an equivalent of <br> by default, but you can implement one. Assuming you're in the manual genre, you can make something like {br}[] work.

Try sticking this at the start of the file:

def Inline.br : Manual.Inline where
  name := `My.Namespace.br

def My.Namespace.br (_ : Array (Verso.Doc.Inline Manual)) : Verso.Doc.Inline Manual :=
  .other Inline.br #[]

open Verso.Output.Html in
@[inline_extension My.Namespace.br]
def My.Namespace.br.descr : InlineDescr where
  traverse _ _ _ := pure none
  toHtml := some fun _ _ _ _ =>
    pure {{<br/>}}
  toTeX := none

open My.Namespace

Then you can write Here's some text{br}[]with a new line.

[David Thrane Christiansen]

(adjust namespaces and place in imported module as you see fit)

[Peter Pfaffelhuber]

Wow, it works! Marvelous, many thanks!!

[David Thrane Christiansen]

Thanks for being patient and figuring out how this all works :)

[Peter Pfaffelhuber]

@David Thrane Christiansen My project leancourse is progressing well. However, I discovered the following unintuitive behavior: When I run lake exe leancourse --output _out --verbose, the content of _out/html-single is almost identical to _out/html-multi, i.e. html-multi is not what I thought it would be since it is a single page. It works well when I run lake exe leancourse --output _out --verbose --depth 2, i.e. when adding the --depth 2. Not sure if this is intended.

[David Thrane Christiansen]

It is intended, but it may not be what is best - the default HTML splitting depth should probably be 2, rather than 0. I'll change it - thanks!