docutils: Add a new .. massert:: directive to test Coq's output

Closes GH-63.
cpitclaudel · Aug 31, 2021 · bc2d8a4 · bc2d8a4
1 parent f52489e
commit bc2d8a4
Show file tree

Hide file tree

Showing 4 changed files with 135 additions and 10 deletions.
diff --git a/alectryon/docutils.py b/alectryon/docutils.py
@@ -519,10 +519,15 @@ def replace_one_mref(self, node, ios, last_io):
             repl = self.format_one_ref(target, node)
         elif kind == "quote":
             repl = self.format_one_quote(target, node)
+        elif kind == "assert":
+            repl = None
         else:
             assert False
 
-        node.replace_self(repl)
+        if repl:
+            node.replace_self(repl)
+        else:
+            node.parent.remove(node)
 
     def _apply(self, **_kwargs):
         ios = {id: node
@@ -636,7 +641,14 @@ def recompute_contents(directive, real_indentation):
     contents = "\n".join(ln[body_indentation:] for ln in body_lines)
     return body_indentation, contents
 
-class CoqDirective(Directive):
+class AlectryonDirective(Directive): # pylint: disable=abstract-method
+    def _error(self, msg):
+        msg = 'Error in "{}" directive:\n{}'.format(self.name, msg)
+        literal = nodes.literal_block(self.block_text, self.block_text)
+        err = self.state_machine.reporter.error(msg, literal, line=self.lineno)
+        return [err]
+
+class CoqDirective(AlectryonDirective):
     """Highlight and annotate a Coq snippet."""
     name = "coq"
 
@@ -653,12 +665,6 @@ class CoqDirective(Directive):
     def header(self):
         return "`{}`".format(self.block_text.partition('\n')[0])
 
-    def _error(self, msg):
-        msg = 'Error in "{}" directive:\n{}'.format(self.name, msg)
-        literal = nodes.literal_block(self.block_text, self.block_text)
-        err = self.state_machine.reporter.error(msg, literal, line=self.lineno)
-        return [err]
-
     def _annots_of_arguments(self):
         try:
             return transforms.read_all_io_flags(" ".join(self.arguments)), []
@@ -708,7 +714,7 @@ def run(self):
         return [pending]
 
 # This is just a small example
-class ExperimentalExerciseDirective(Sidebar):
+class ExperimentalExerciseDirective(Sidebar, AlectryonDirective):
     """Introduce an exercise."""
     name = "exercise"
 
@@ -986,7 +992,7 @@ def _opt_mquote_lexer(arg):
     'language': _opt_mquote_lexer,
 }
 
-class MQuoteDirective(Directive):
+class MQuoteDirective(AlectryonDirective):
     has_content = False
     required_arguments = 1
     optional_arguments = 0
@@ -1007,6 +1013,27 @@ def run(self):
         except ValueError as e:
             return self._error(str(e))
 
+class MAssertDirective(Directive):
+    has_content = True
+    required_arguments = 0
+    optional_arguments = 1
+    final_argument_whitespace = True
+
+    name = "massert"
+    option_spec: Dict[str, Any] = {}
+
+    def run(self):
+        prefix = markers.parse_path(self.arguments[0] if self.arguments else "")
+        sm = self.state_machine
+        options = {**self.options, "kind": "assert", "prefix": prefix}
+        try:
+            start = self.content_offset + 1
+            return [_marker_ref("assertion `{}`".format(ref), ref,
+                                linum, sm.document, sm, {**options})
+                    for linum, ref in enumerate(self.content, start=start) if ref]
+        except ValueError as e:
+            return self._error(str(e))
+
 # Error printer
 # -------------
 
@@ -1349,6 +1376,7 @@ def get_pipeline(frontend, backend, dialect):
 DIRECTIVES = [CoqDirective,
               AlectryonToggleDirective,
               MQuoteDirective,
+              MAssertDirective,
               ExperimentalExerciseDirective,
               DirectiveDirective]
 ROLES = [alectryon_bubble,

diff --git a/recipes/_output/references.html b/recipes/_output/references.html
@@ -199,6 +199,23 @@ <h1>Customizing proof rendering (<strong>experimental</strong>)</h1>
 </span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kp">all</span>: <span class="nb">simpl</span> <span class="kr">in</span> *; <span class="bp">tauto</span>.</span><span class="alectryon-wsp">
 </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Qed</span>.</span></span></pre></blockquote>
 </div>
+<div class="section" id="asserting-properties-of-the-output">
+<h1>Asserting properties of the output</h1>
+<p>A constant concern when displaying proof states to readers is that what is displayed to the user may go stale.  Alectryon mitigates the issue by automatically collecting proof states, but simply recording the prover's output doesn't fully solve the issue.  That is because the output of a command may change in an unexpected way, without raising an error.  For example, we may have written, with an early version of Coq:</p>
+<blockquote>
+<pre class="alectryon-io highlight" id="plus"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="references-rst-chk1b" style="display: none" type="checkbox"><label class="alectryon-input" for="references-rst-chk1b"><span class="kn">Print</span> plus.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message"><span class="kn">Notation</span> <span class="nf">plus</span> := Nat.add</blockquote></div></div></small></span></pre></blockquote>
+<p>To show the recursive definition of addition.   But as Coq's standard library got reorganized, the definition of <code class="highlight coq"><span class="n">plus</span></code> changed to being an alias for <code class="highlight coq"><span class="n">Nat</span><span class="o">.</span><span class="n">add</span></code>, making the output of <code class="highlight coq"><span class="kn">Print</span> <span class="n">plus</span></code> uninteresting.  In general, the recommended way to prevent this issue is by recording and versioning the prover's output using Alectryon caching facility (<tt class="docutils literal"><span class="pre">--cache-directory</span></tt>).  For small checks, however, Alectryon provides the <tt class="docutils literal">massert</tt> directive, which checks that all references in its body resolve to a part of Coq's output.  For example, the following checks that <code class="highlight coq"><span class="n">plus</span></code> is indeed an alias and <code class="highlight coq"><span class="n">Nat</span><span class="o">.</span><span class="n">add</span></code> a <code class="highlight coq"><span class="kn">Fixpoint</span></code>.</p>
+<blockquote>
+<pre class="alectryon-io highlight"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="references-rst-chk1c" style="display: none" type="checkbox"><label class="alectryon-input" for="references-rst-chk1c"><span class="kn">Print</span> Nat.add.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">Nat.add = 
+<span class="kr">fix</span> add (n m : nat) {<span class="kr">struct</span> n} : nat :=
+  <span class="kr">match</span> n <span class="kr">with</span>
+  | <span class="mi">0</span> =&gt; m
+  | S p =&gt; S (add p m)
+  <span class="kr">end</span>
+     : nat -&gt; nat -&gt; nat
+
+<span class="kn">Arguments</span> Nat.add (_ _)%nat_scope</blockquote></div></div></small></span></pre></blockquote>
+</div>
 </div>
 </div></body>
 </html>
diff --git a/recipes/_output/references.xe.tex b/recipes/_output/references.xe.tex
@@ -924,4 +924,63 @@ \section{Customizing proof rendering (\textbf{experimental})%
 \end{alectryon}
 \end{quote}
 
+
+\section{Asserting properties of the output%
+  \label{asserting-properties-of-the-output}%
+}
+
+A constant concern when displaying proof states to readers is that what is displayed to the user may go stale.  Alectryon mitigates the issue by automatically collecting proof states, but simply recording the prover's output doesn't fully solve the issue.  That is because the output of a command may change in an unexpected way, without raising an error.  For example, we may have written, with an early version of Coq:
+
+\begin{quote}
+\begin{alectryon}
+  \anchor{plus}
+  \sep
+  % Generator: Alectryon
+  \sep
+  \begin{sentence}
+    \begin{input}
+      \PY{k+kn}{Print}~\PY{n}{plus}\PY{o}{.}
+    \end{input}
+    \sep
+    \begin{output}
+      \begin{messages}
+        \begin{message}
+          \PY{k+kn}{Notation}~\PY{n+nf}{plus}~\PY{o}{:=}~\PY{n}{Nat}\PY{o}{.}\PY{n}{add}
+        \end{message}
+      \end{messages}
+    \end{output}
+  \end{sentence}
+\end{alectryon}
+\end{quote}
+
+To show the recursive definition of addition.   But as Coq's standard library got reorganized, the definition of \texttt{\DUrole{code}{\DUrole{highlight}{\DUrole{coq}{\DUrole{n}{plus}}}}} changed to being an alias for \texttt{\DUrole{code}{\DUrole{highlight}{\DUrole{coq}{\DUrole{n}{Nat}\DUrole{o}{.}\DUrole{n}{add}}}}}, making the output of \texttt{\DUrole{code}{\DUrole{highlight}{\DUrole{coq}{\DUrole{kn}{Print} \DUrole{n}{plus}}}}} uninteresting.  In general, the recommended way to prevent this issue is by recording and versioning the prover's output using Alectryon caching facility (\texttt{--cache-directory}).  For small checks, however, Alectryon provides the \texttt{massert} directive, which checks that all references in its body resolve to a part of Coq's output.  For example, the following checks that \texttt{\DUrole{code}{\DUrole{highlight}{\DUrole{coq}{\DUrole{n}{plus}}}}} is indeed an alias and \texttt{\DUrole{code}{\DUrole{highlight}{\DUrole{coq}{\DUrole{n}{Nat}\DUrole{o}{.}\DUrole{n}{add}}}}} a \texttt{\DUrole{code}{\DUrole{highlight}{\DUrole{coq}{\DUrole{kn}{Fixpoint}}}}}.
+
+\begin{quote}
+\begin{alectryon}
+  % Generator: Alectryon
+  \sep
+  \begin{sentence}
+    \begin{input}
+      \PY{k+kn}{Print}~\PY{n}{Nat}\PY{o}{.}\PY{n}{add}\PY{o}{.}
+    \end{input}
+    \sep
+    \begin{output}
+      \begin{messages}
+        \begin{message}
+          \PY{n}{Nat}\PY{o}{.}\PY{n}{add}~\PY{o}{=}~\nl
+          \PY{k+kr}{fix}~\PY{n}{add}~\PY{o}{(}\PY{n}{n}~\PY{n}{m}~\PY{o}{:}~\PY{n}{nat}\PY{o}{)}~\PY{o}{\PYZob{}}\PY{k+kr}{struct}~\PY{n}{n}\PY{o}{\PYZcb{}}~\PY{o}{:}~\PY{n}{nat}~\PY{o}{:=}\nl
+          ~~\PY{k+kr}{match}~\PY{n}{n}~\PY{k+kr}{with}\nl
+          ~~\PY{o}{|}~\PY{l+m+mi}{0}~\PY{o}{=\PYZgt{}}~\PY{n}{m}\nl
+          ~~\PY{o}{|}~\PY{n}{S}~\PY{n}{p}~\PY{o}{=\PYZgt{}}~\PY{n}{S}~\PY{o}{(}\PY{n}{add}~\PY{n}{p}~\PY{n}{m}\PY{o}{)}\nl
+          ~~\PY{k+kr}{end}\nl
+          ~~~~~\PY{o}{:}~\PY{n}{nat}~\PY{o}{\PYZhy{}\PYZgt{}}~\PY{n}{nat}~\PY{o}{\PYZhy{}\PYZgt{}}~\PY{n}{nat}\nl
+          \nl
+          \PY{k+kn}{Arguments}~\PY{n}{Nat}\PY{o}{.}\PY{n}{add}~\PY{o}{(}\PY{n}{\PYZus{}}~\PY{n}{\PYZus{}}\PY{o}{)\PYZpc{}}\PY{n}{nat\PYZus{}scope}
+        \end{message}
+      \end{messages}
+    \end{output}
+  \end{sentence}
+\end{alectryon}
+\end{quote}
+
 \end{document}
diff --git a/recipes/references.rst b/recipes/references.rst
@@ -188,3 +188,24 @@ References can also be used to customize the display of goals and hypotheses.  I
            (* .unfold -.g#* .g#2 .g#4 .g#4.h{list A} *)
          all: simpl in *; tauto.
        Qed.
+
+Asserting properties of the output
+==================================
+
+A constant concern when displaying proof states to readers is that what is displayed to the user may go stale.  Alectryon mitigates the issue by automatically collecting proof states, but simply recording the prover's output doesn't fully solve the issue.  That is because the output of a command may change in an unexpected way, without raising an error.  For example, we may have written, with an early version of Coq:
+
+    .. coq::
+       :name: plus
+
+       Print plus.
+
+To show the recursive definition of addition.   But as Coq's standard library got reorganized, the definition of `plus` changed to being an alias for `Nat.add`, making the output of `Print plus` uninteresting.  In general, the recommended way to prevent this issue is by recording and versioning the prover's output using Alectryon caching facility (``--cache-directory``).  For small checks, however, Alectryon provides the ``massert`` directive, which checks that all references in its body resolve to a part of Coq's output.  For example, the following checks that `plus` is indeed an alias and `Nat.add` a `Fixpoint`.
+
+    .. coq::
+
+       Print Nat.add.
+
+    .. massert::
+
+       .io#plus.s(Print).msg{*Notation*}
+       .s(Print).msg{*Nat.add*=*fix add*}