Numbering lines within `.. coq::` blocks

[jhaag]

In some of our documentation we dissect each line in a given snippet of Coq code individually. Oftentimes we refer to 'line 2' or 'line 7', but unfortunately Alectryon doesn't (seem to) have support for numbering the snippets in .. coq:: blocks. It would be a nice quality-of-life improvement if line-numbering (similar to how it's done for regular code blocks) was incorporated.

[cpitclaudel]

Quite reasonable; we just need to find a clean way to implement it. At the moment Alectryon's code blocks are plain HTML (we don't go through the CodeBlock code because the HTML that we generate is more complex than what it can produce. I'll check if we can reuse that code.

[cpitclaudel]

Sphinx uses pygments linenos option directly (it runs pygments on the whole code block). We run pygments on individual sentences, so that won't work.

[cpitclaudel]

Besides, their implementation just puts a second div next to the first one with the line numbers:

$ cat test.v
Definition foo := unit.
Notation bar := foo.
Lemma FooBar: foo = bar.
$ pygmentize -f html -P linenos=true ./test.v 
<table class="highlighttable"><tr><td class="linenos"><div class="linenodiv"><pre>1
2
3</pre></div></td><td class="code"><div class="highlight"><pre><span></span><span class="n">Definition</span> <span class="n">foo</span> <span class="o">:=</span> <span class="n">unit</span><span class="p">.</span>
<span class="n">Notation</span> <span class="n">bar</span> <span class="o">:=</span> <span class="n">foo</span><span class="p">.</span>
<span class="n">Lemma</span> <span class="nl">FooBar:</span> <span class="n">foo</span> <span class="o">=</span> <span class="n">bar</span><span class="p">.</span>
</pre></div>
</td></tr></table>

That breaks if you can expand part of a line to show goals. The proper solution is probably to insert a line marker at the beginning of each line instead, and style it so that it isn't selectable.

[jhaag]

That makes sense. Again, this is a QoL improvement and not something that is blocking our progress with using Alectryon, so feel free to table it for the time being if the solution is involved.

[cpitclaudel]

Actually, how about numbering sentences instead of lines?

.alectryon-io {
    counter-reset: sentences;
}

.alectryon-input {
    counter-increment: sentences;
}

.alectryon-io .alectryon-input:after,
.alectryon-io label.alectryon-input:after,
.alectryon-io label.alectryon-input:after,
.alectryon-io label.alectryon-input:hover:after {
    content: counter(sentences);
    /* Prettier display: */
    display: inline-block !important;
    border: thin solid #2e3436 !important;
    border-radius: 0;
    min-width: 1.35em;
    min-height: 1.35em;
    padding: 0.05em;
    text-align: center;
    background: #555753 !important;
    color: white;
    font-weight: 900;
    font-size: 75%;
    margin: 0 0 0 0.25em;
    vertical-align: middle;
    box-sizing: content-box;
}

Rendered:

[cpitclaudel]

Or for PL-minded folks, content: counter(sentences, lower-greek);:

[cpitclaudel]

(Of course, JS would also work for this),

It would also be nice to add a role in Alectryon for this; you'd write this:

.. coq::

  Check nat.
  Definition a : nat.
    apply Nat.add.
    exact 1.
    exact 1.
  Defined.

Pay particular attention to :coqref:`Check nat.` and :coqref:`exact 1 <2>`.

and it would render as this:

Check nat. [1]
Definition a : nat.
  apply Nat.add.
  exact 1.
  exact 1. [2]
Defined.

Pay particular attention to [1] and [2].

And it would check for you that the things you are referring to are actually in the code.

[jhaag]

These changes seem like they would certainly fit the bill! Thanks for looking into this in more earnest :~)

[cpitclaudel]

OK, I've implemented something which I think fits the bill; see the :mref: entry in https://github.com/cpitclaudel/alectryon#extra-roles-and-directives and the examples at https://github.com/cpitclaudel/alectryon/blob/master/recipes/references.rst . The idea is that you refer to a sentence or a goal or a hypothesis by its contents, and Alectryon adds the corresponding markers in the right spots.

Here's the HTML:

And the PDF:

[jhaag]

This looks great! I will test this out next week and get back to you regarding how well this fits our use-case :~)

[cpitclaudel]

Perfect, thanks

[jhaag]

While we're not going to update our existing documentation en masse with this new feature, it is indeed a good fit for the sort of documentation which I'm writing! I look forward to slowly integrating it more as we update and extend our documentation.

[cpitclaudel]

Perfect, excellent news (and yes, massive updates don't sound good!) There may be a few tweaks to the syntax as we move forward, let me know if you run into corner cases or missing features!