Documentation formatting in tactic.localized

Stream: general

[Gihan Marasingha]

Sorry not sure how to submit a bug report, but I think there's a little issue in the documentation for tactic.localized. The source uses 'triple backquote lean' for inline code, which actually inserts the word 'lean' in the HTML version of the documentation: https://leanprover-community.github.io/mathlib_docs/tactic/localized.html

[Floris van Doorn]

Ah, from other occurrences of ```lean it seems like the syntax needs a newline before (and after?) the code snippet for it to work.

[Floris van Doorn]

No, scratch that. The problem seems to be that the code blocks are indented?

[Floris van Doorn]

There is definitely something weird going on. The documentation of docs#simps_get_raw_projections contains code snippets that start with lean, even though the doc-string source doesn't contain ```lean.

[Floris van Doorn]

@Rob Lewis any ideas?

[Bryan Gin-ge Chen]

If I remember correctly something in doc-gen converts ``` to ```lean .

[Bryan Gin-ge Chen]

Gabriel mentioned it in this issue comment.

[Floris van Doorn]

This is definitely a fine place to report bugs like this. I also opened doc-gen#93 so we don't forget.

[Rob Lewis]

I think that's preprocessing in Lean, not in doc-gen.

[Bryan Gin-ge Chen]

Oh, right. I forgot about that.

[Rob Lewis]

import tactic.simps

open tactic

run_cmd tactic.doc_string `simps_get_raw_projections >>= trace

[Rob Lewis]

This seems like a bug in the markdown processing. The indented fenced code block is getting processed as inline code.

[Rob Lewis]

Weren't we talking about switching from markdown2 to a different package? Or was it the opposite, did we switch the website to markdown2?

[Rob Lewis]

Yeah, looks like a markdown2 bug.

import markdown2
import mistletoe

s = """
* Here is a list
  ```python
  def s = 2
  ```
"""

print(markdown2.markdown(s))

print(mistletoe.markdown(s))

<ul>
<li>Here is a list
<code>python
def s = 2
</code></li>
</ul>

<ul>
<li>Here is a list
<pre><code class="language-python">def s = 2
</code></pre>
</li>
</ul>

[Floris van Doorn]

Is this related? https://github.com/trentm/python-markdown2/issues/263#issuecomment-313176533

[Floris van Doorn]

i.e. does markdown2.markdown(s, extras=["fenced-code-blocks"]) work?

[Rob Lewis]

Good point -- that was missing in my test, but we use fenced-code-blocks in doc-gen. Doesn't fix it.

import markdown2
import mistletoe

s = """
  ```python
  def s = 2
  ```
"""

print(markdown2.markdown(s, extras=['fenced-code-blocks']))

print(mistletoe.markdown(s))

<p><code>python
  def s = 2
</code></p>

<pre><code class="language-python">def s = 2
</code></pre>

[Rob Lewis]

#4842 for now. mistletoe isn't a drop in replacement for markdown2.

[Floris van Doorn]

So is it the indentation? I thought I saw an indented code snippet somewhere else where the generated doc was fine.

[Rob Lewis]

A quick local test shows that markdown2 with the fenced-code-blocks extra properly handles

```python
def foo():
  return 1
```

but not

 ```python
 def foo():
   return 1
 ```

[Kevin Buzzard]

I thought for a while that they were the same picture -- I just noticed the indentation!

[Bryan Gin-ge Chen]

@Rob Lewis Would migrating doc-gen from mistletoe to markdown2 require a huge refactor?

[Rob Lewis]

More just tedium figuring out how to replicate every markdown2 feature we're using.

[Rob Lewis]

In particular the linkifiers need some attention.

[Julian Berman]

Possibly also worth considering pandoc... I was super lazy recently for my doc generating and just passed all the lean docstrings through pandoc

[Kevin Lacker]

is that actually valid markdown with the triple-ticks plus indentation? i don't think I would expect that to work

[Kevin Lacker]

I think once it's indented, then it isn't a code block, it's just inline code

[Julian Berman]

I mean there's like 4 markdown specs at least so "valid markdown" is itself a fun concept

[Julian Berman]

But pandoc agrees with what it looks like mistletoe thinks

[Julian Berman]

And produces...

⊙  pandoc --from markdown --to html <<<'                                                                                                                                                        julian@Air ●
  ```python
  def s = 2
  ```'
<div class="sourceCode" id="cb1"><pre class="sourceCode python"><code class="sourceCode python"><span id="cb1-1"><a href="#cb1-1" aria-hidden="true"></a><span class="kw">def</span> s <span class="op">=</span> <span class="dv">2</span></span></code></pre></div>

[Kevin Lacker]

let's just unindent the markdown in src/tactic/localized.lean

[Kevin Lacker]

rather than migrating markdown processors

[Julian Berman]

The PR did that looks like, so all this was some longer term thing.

[Bryan Gin-ge Chen]

It'd be good to have consistent markdown processing on the community website (which uses mistletoe) and the API docs in the long term.

[Rob Lewis]

In principle there's a semantic difference. The code blocks appeared in a list. markdown2 seems to forbid this, you have to break the list indentation to insert a code block.

[Rob Lewis]

That said, I have no attachment to any particular markdown flavor or processor as long as it supports the features we want. And as Bryan says it would be a big plus if the website and doc-gen used the same one.

[Rob Lewis]

Well, it gets trickier. This example seems to be handled correctly: https://github.com/leanprover-community/mathlib/blob/cc7f06b/src/algebra/group/to_additive.lean#L260

[Rob Lewis]

https://leanprover-community.github.io/mathlib_docs/algebra/group/to_additive.html#to_additive.attr

[Floris van Doorn]

Yes, that was one example where I found that the code was indented and the markdown happened correctly. Another example is in the module doc string of https://leanprover-community.github.io/mathlib_docs/tactic/unfold_cases.html

Maybe it's related to a newline after the doc string?