Support non-Lean code blocks in the mdbook

[Vtec234]

Description

When adding a tutorial for user widgets in #1407, we tried to embed a JavaScript code block in a module docstring within a literate Lean file. Unfortunately the block seems to be misprocessed and to produce invalid output, also making mdbook tests fail.

Steps to Reproduce

Expected behavior: It is possible to use code blocks in module docstrings in literate Lean files.

Actual behavior: They are miscompiled.

Reproduces how often: 100%

[EdAyers]

Mwe:

1.in doc/examples/ make a pair of files test.lean and test.lean.md
2. add - [test](examples/test.lean.md) to doc/SUMMARY.md
2. in test.lean.md put the following thing:

(this chapter is rendered by Alectryon in the CI)

```lean
{{#include test.lean}}
```

4. In test.lean put:

#check "hello world"
/-!
This is a comment
```
this is a code block
```
-/

#check "hello world again"

5. cd doc, mdbook build see manual
6. look at main block of doc/out/examples/test.lean.html:

                    <main>
                        <p>(this chapter is rendered by Alectryon in the CI)</p>
<pre><code class="language-lean">#check &quot;hello world&quot;
/-!
This is a comment
</code></pre>
<p>this is a code block</p>
<pre><code>-/

#check &quot;hello world again&quot;
</code></pre>

                    </main>

If I've understood the pipeline correctly, the expected output needs to be something like

<main>
    <pre><code class="language-lean">#check &quot;hello world&quot;</code></pre>
    <p>This is a comment</p>
    <pre><code>this is a code block</code></pre>
    <pre><code>#check &quot;hello world again&quot;</code></pre>
</main>

[Kha]

This works fine using (note the number of backticks)

````lean
{{#include palindromes.lean}}
````

right? It's only mdbook test that still fails (without ,ignore).

[EdAyers]

Increasing backticks gives

                    <main>
                        <p>(this chapter is rendered by Alectryon in the CI)</p>
<pre><code class="language-lean">#check &quot;hello world&quot;
/-!
This is a comment
```lean
this is a code block
```
-/

#check &quot;hello world again&quot;
</code></pre>

                    </main>

is that the correct output? It's equivariant under changing lean in '''lean to any other string.

[Kha]

Ah yes, this is the expected output when LeanInk is not involved! It should look correct after going through the entire CI pipeline.

[EdAyers]

What's the nix incantation to get this output?

[Kha]

It's

lean4/.github/workflows/nix-ci.yml

Line 88 in 0ec56c3

nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc

(ignore the NIX_BUILD_ARGS).

(this will get much easier with edolstra/nix@8a0a55f)

[EdAyers]

hmmm ok I think this is working then. Still getting

/build/mdbook-d0xfKR/widgets.lean.md_3.lean:130:0: error: unterminated comment

if I build the widget-doc branch with the following code block:

```lean,ignore
#check "hello"
```

[Kha]

Do you have a full example on a branch? I assume that's not you entire file.

[EdAyers]

MWE branch: https://github.com/Vtec234/lean4/tree/doc-codeblock-bug (relevant file)

then I run

nix-shell -A nix
 nix build -v --print-build-logs --fallback --update-input lean --no-write-lock-file ./doc#test -

And get error:

lean-doc-test> 2022-08-08 10:45:26 [INFO] (mdbook::book): Testing chapter 'test': "/build/source/doc/./examples/test.lean.md"
lean-doc-test> 2022-08-08 10:45:26 [INFO] (mdbook::book):   testing snippet on line: 3
lean-doc-test> 2022-08-08 10:45:27 [ERROR] (mdbook::book): lean returned an error:
lean-doc-test> --- stdout
lean-doc-test> "hello world" : String
lean-doc-test> /build/mdbook-Yk6tZ1/test.lean.md_3.lean:4:0: error: unterminated comment
lean-doc-test> --- stderr

[Kha]

Ah, I misunderstood you then. It works if you use ,ignore on the outer block in test.lean.md, and only use blocks for languages other than lean inside it. For anything else, we need a proper fix of mdbook test.

@lovettchris Specifically, the problem is that our mdbook test code does not properly handle nesting. That is, in

````lean
a
```js
b
```
c
````

It will send just a to Lean instead of the entire code block.

[lovettchris]

@Kha - this should fix it: leanprover/mdBook#10