Stream: Coq devs & plugin devs

Topic: Display of `.. coqtop::` with coqdoc

Kenji Maillard (May 12 2020 at 10:48):

Hello! Would there be a way to make the display of the coqtop instruction a bit better in these examples ? The code I used is

   .. example:: Dynamic nature of mutable cells

      .. coqtop:: all

         Ltac2 mutable x := true.
         Ltac2 y := x.
         Ltac2 Eval y.
         Ltac2 Set x := false.
         Ltac2 Eval y.

and the non Eval lines produce empty lines that do not look good...

Théo Zimmermann (May 12 2020 at 11:57):

@Kenji Maillard A bug was recently introduced in a PR attempting to improve the output. Cf. https://github.com/coq/coq/pull/12272#issuecomment-626387244. This should hopefully be solved soon, and in any case before the release.

Kenji Maillard (May 12 2020 at 13:43):

putting a double line as you indicate in the issue helps a bit, but it still displays the empty lines: nothing we can do about them ?

Théo Zimmermann (May 12 2020 at 16:58):

Please comment in the issue so that the other people involved are aware.

Last updated: Oct 08 2024 at 14:01 UTC