Skip to content

rocdoc directive inserts an extra blank line in doc, doesn't look right #20679

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
jfehrle opened this issue May 25, 2025 · 2 comments · May be fixed by #20710
Open

rocdoc directive inserts an extra blank line in doc, doesn't look right #20679

jfehrle opened this issue May 25, 2025 · 2 comments · May be fixed by #20710
Assignees
@Villetaneuse
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: documentation Additions or improvement to documentation.

Comments

@jfehrle
Copy link
Member

jfehrle commented May 25, 2025 •
edited
Loading

Description of the problem

.. rocdoc:: always inserts an extra blank line, which doesn't look right. (Note the doc uses :n: heavily, which can create doc hyperlinks for non-terminals but doesn't provide the coloring you get from rocdoc. :n: can also be used in-line rather than becoming a new paragraph.)

   For instance, suppose that we define the following.

   .. rocqdoc::

      Ltac2 Notation foo := fun x => x ().

   Then we have the following expansion at internalization time.

is rendered as

Image

Version of Rocq / Coq where this bug occurs

9.0
@jfehrle jfehrle added kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. kind: documentation Additions or improvement to documentation. labels May 25, 2025
@jfehrle jfehrle mentioned this issue May 25, 2025
Merged
@Villetaneuse
Copy link
Contributor

So, it's a problem of whitespace : pre in css, together with sphinx generating code like this:

<div class="coqdoc literal-block docutils container">
<span><span class="coqdoc-keyword">Ltac2</span><span> </span><span class="coqdoc-keyword">Notation</span><span> </span><span class="coqdoc-var">foo</span><span> := </span><span class="coqdoc-keyword">fun</span><span> </span><span class="coqdoc-var">x</span><span> =&gt; </span><span class="coqdoc-var">x</span><span> ().</span><span>
</span></span></div>

The spurious line-break is the one after <div class=...>.
Struggling to find out how to have sphinx generate this without the line-break.

@Villetaneuse Villetaneuse removed the needs: triage The validity of this issue needs to be checked, or the issue itself updated. label Jun 4, 2025
@Villetaneuse Villetaneuse self-assigned this Jun 4, 2025
@Zimmi48
Copy link
Member

Zimmi48 commented Jun 4, 2025

Fixing the HTML generation sounded complicated to me. I compared the HTML generated for rocqdoc and rocqtop:

rocqdoc:

<div class="coqdoc literal-block docutils container">
<span><span></span><span class="coqdoc-keyword">let</span><span> </span><span class="coqdoc-var">x</span><span> := '0 </span><span class="coqdoc-tactic">in</span><span> </span><span class="coqdoc-keyword">constr</span><span>:(1 + </span><span class="coqdoc-var">ltac2</span><span>:(</span><span class="coqdoc-tactic">exact</span><span> $</span><span class="coqdoc-var">x</span><span>))</span></span></div>

rocqtop:

<div class="coqtop literal-block docutils container">
<span></span><dl class="simple">
<dt><span></span><span class="coqdoc-keyword">Ltac</span><span>2 </span><span class="coqdoc-var">myconstr</span><span> () := </span><span class="coqdoc-keyword">constr</span><span>:(</span><span class="coqdoc-var">nat</span><span> -&gt; 0).</span><span>
</span></dt></dl>
</div>

In both case, there is the first div with a newline after.

The difference however is in how the CSS is applied:

.coqdoc, .coqtop dt, .coqtop dd, pre { /* pre added because of production lists */
    font-family: Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace !important; /* Copied from RTD theme */
    font-size: 12px !important; /* Copied from RTD theme */
    line-height: 1.5 !important; /* Copied from RTD theme */
    white-space: pre;
}

The difference is that in the case of coqdoc, the whitespace: pre property applies as soon as we are in the div block, whereas in the case of coqtop, the whitespace: pre applies in children elements of the div (dt and dd). It seems that there is an equivalent of the dl which is a span in the case of a rocqdoc block, so we can replace the .coqdoc selector with a .coqdoc > span one. I'll open a PR with a fix.

Zimmi48 added a commit to Zimmi48/coq that referenced this issue Jun 4, 2025
@Zimmi48
Fix rocq-prover#20679: avoid spurious newline in rocqdoc blocks.
1a7a153 
Adjust the CSS selectors of rocqdoc to be closer to the ones of rocqtop.
@Zimmi48 Zimmi48 linked a pull request Jun 4, 2025 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Villetaneuse Villetaneuse

Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: documentation Additions or improvement to documentation.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix #20679: avoid spurious newline in rocqdoc blocks. Zimmi48/coq
3 participants
@Zimmi48 @jfehrle @Villetaneuse