Skip to content

Commit

Permalink
Auto-Update {userman, adaptingman}
Browse files Browse the repository at this point in the history 
href: ProofGeneral/PG@cb23709
  • Loading branch information
@proofbot
proofbot committed May 13, 2024
1 parent 8fe7fec commit 0fc143b
Show file tree
Hide file tree
Showing 49 changed files with 153 additions and 81 deletions.
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Beginning-with-a-New-Prover.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -258,7 +258,7 @@ <h2 class="section">1.3 Major modes used by Proof General</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Concept-Index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ <h1 class="unnumbered">Concept Index</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Configuring-Editing-Syntax.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ <h1 class="chapter">9. Configuring Editing Syntax</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Configuring-Font-Lock.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ <h1 class="chapter">10. Configuring Font Lock</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -455,7 +455,7 @@ <h3 class="subsection">12.4.2 Prooftree Adaption</h3>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Configuring-Tokens.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ <h1 class="chapter">11. Configuring Tokens</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Demonstration-Instantiations.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -261,7 +261,7 @@ <h2 class="section">B.2 demoisa.el</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Function-Index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ <h1 class="unnumbered">Function and Command Index</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Global-Constants.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ <h1 class="chapter">7. Global Constants</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Goals-Buffer-Settings.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ <h1 class="chapter">5. Goals Buffer Settings</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Handling-Multiple-Files.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ <h1 class="chapter">8. Handling Multiple Files</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Internals-of-Proof-General.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1256,7 +1256,7 @@ <h2 class="section">14.7 Debugging</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Introduction.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ <h2 class="unnumberedsec">Credits</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ <h2 class="section">2.3 Toolbar configuration</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
4 changes: 2 additions & 2 deletions doc/master/adaptingman/PG-adapting_abt.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
</div>
<h1>About This Document</h1>
<p>
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</p>
<p>
The buttons in the navigation panels have the following meaning:
Expand Down Expand Up @@ -124,7 +124,7 @@ <h1>About This Document</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/PG-adapting_toc.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ <h1>Table of Contents</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Plans-and-Ideas.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ <h2 class="section">A.3 Browser mode for script files and theories</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
25 changes: 13 additions & 12 deletions doc/master/adaptingman/Proof-Script-Settings.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -686,17 +686,18 @@ <h2 class="section">3.6 Omitting proofs for speed</h2>
<a class="anchor" id="Proof-status-statistic-1"></a>
<h2 class="section">3.7 Proof status statistic</h2>

<p>The command <code>proof-check-proofs</code> builds on the omit-proofs
feature. Using its machinery, it splits the current buffer into opaque
proofs and all other material. The other material is asserted in the
usual way and <code>proof-check-proofs</code> aborts if it detects an error
in there. For opaque proofs the command first tries to assert them in
the usual way too. If this succeeds the proof is considered valid.
Otherwise the proof is replaced with
<code>proof-script-proof-admit-command</code> and the proof is considered
invalid. To associate theorem names with opaque proofs, the function
<code>proof-get-proof-info-fn</code> is called, which is identical to
<code>proof-tree-get-proof-info</code>, See section <a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#Proof-Tree-Elisp-configuration">Proof Tree Elisp configuration</a>.
<p>The commands <code>proof-check-report</code> and <code>proof-check-annotate</code>
build on the omit-proofs feature. Using its machinery,
<code>proof-check-proofs</code>, the inner working horse of both commands,
splits the current buffer into opaque proofs and all other material.
The other material is asserted in the usual way and
<code>proof-check-proofs</code> aborts if it detects an error in there. For
opaque proofs it first tries to assert them in the usual way too. If
this succeeds the proof is considered valid. Otherwise the proof is
replaced with <code>proof-script-proof-admit-command</code> and the proof is
considered invalid. To associate theorem names with opaque proofs, the
function <code>proof-get-proof-info-fn</code> is called, which is identical
to <code>proof-tree-get-proof-info</code>, See section <a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#Proof-Tree-Elisp-configuration">Proof Tree Elisp configuration</a>.
</p>
<p>To enable proof status statistics, the omit-proofs feature must be
configured, See section <a href="#Omitting-proofs-for-speed">Omitting proofs for speed</a>. Additionally, the
Expand Down Expand Up @@ -898,7 +899,7 @@ <h2 class="section">3.12 Completions</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Proof-Shell-Settings.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -748,7 +748,7 @@ <h2 class="section">4.5 Hooks and other settings</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Splash-Screen-Settings.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ <h1 class="chapter">6. Splash Screen Settings</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Variable-Index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -235,7 +235,7 @@ <h1 class="unnumbered">Variable and User Option Index</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/Writing-More-Lisp-Code.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -248,7 +248,7 @@ <h2 class="section">13.4 Useful functions and macros</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
2 changes: 1 addition & 1 deletion doc/master/adaptingman/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ <h1 class="settitle">Proof General</h1>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
93 changes: 77 additions & 16 deletions doc/master/userman/Advanced-Script-Management-and-Editing.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -389,18 +389,27 @@ <h2 class="section">3.7 Asserting across files</h2>
<h2 class="section">3.8 Proof status statistic</h2>
<a class="anchor" id="index-Proof-status-statistic"></a>

<p>The command <code>proof-check-proofs</code> (menu <code>Proof-General -&gt;
<p>The command <code>proof-check-report</code> (menu <code>Proof-General -&gt;
Check Opaque Proofs</code>) generates the proof status of all opaque proofs
in the current buffer, i.e., it generates an overview that shows which
of the opaque proofs in the current buffer are currently valid and
which are failing. When used interactively, the proof status is shown
in the buffer <code>*proof-check-report*</code> (as long as
<code>proof-check-report-buffer</code> is not changed).
</p>
<p>Currently <code>proof-check-proofs</code> does only work for Coq.
<p>The command <code>proof-check-annotate</code> (menu <code>Proof-General -&gt;
Annotate Failing Proofs</code>) modifies the current buffer and places
comments containing <code>FAIL</code> on all failing opaque proofs. With
prefix argument also the passing proofs are annotated with
<code>PASS</code>. For configuring the position of these comments, see
<code>proof-check-annotate-position</code> and
<code>proof-check-annotate-right-margin</code>.
</p>
<p>Currently <code>proof-check-report</code> and <code>proof-check-annotate</code>
only work for Coq.
</p>
<dl>
<dt><a class="anchor" id="index-proof_002dcheck_002dproofs"></a><u>Command:</u> <b>proof-check-proofs</b><i> tap &amp;optional batch</i></dt>
<dt><a class="anchor" id="index-proof_002dcheck_002dreport"></a><u>Command:</u> <b>proof-check-report</b><i> tap &amp;optional batch</i></dt>
<dd><p>Generate an overview about valid and invalid proofs.<br>
This command completely processes the current buffer and
generates an overview about all the opaque proofs in it and
Expand All @@ -418,45 +427,97 @@ <h2 class="section">3.8 Proof status statistic</h2>
protocol (<var>tap</var>). Argument <var>batch</var> controls where the overview goes
to. If nil, or in an interactive call, the overview appears in
&lsquo;<samp><code>proof-check-report-buffer</code></samp>&rsquo;. If <var>batch</var> is a string, it should be a
filename and the overview is appended there. Otherwise the
overview is output via &lsquo;<samp>message</samp>&rsquo; such that it appears on stdout
when this command runs in batch mode.
filename to write the overview to. Otherwise the overview is
output via &lsquo;<samp>message</samp>&rsquo; such that it appears on stdout when this
command runs in batch mode.
</p>
<p>In the same way as the omit-proofs feature, this command only
tolerates errors inside scripts of opaque proofs. Any other error
is reported to the user without generating an overview. The
overview only contains those names of theorems whose proofs
overview only contains those names of theorems whose proof
scripts are classified as opaque by the omit-proofs feature. For
Coq for instance, among others, proof scripts terminated with
<code>'Defined'</code> are not opaque and do not appear in the generated
overview.
</p>
<p>Note that this command does not (re-)compile required files.
Files must be required before running this commands, for instance
by asserting all require commands beforehand.
Dependencies must be compiled before running this commands, for
instance by asserting all require commands beforehand.
</p></dd></dl>

<dl>
<dt><a class="anchor" id="index-proof_002dcheck_002dannotate"></a><u>Command:</u> <b>proof-check-annotate</b><i> annotate-passing &amp;optional save-buffer</i></dt>
<dd><p>Annotate failing proofs in current buffer with a &quot;<var>fail</var>&quot; comment.<br>
This function modifies the current buffer in place. Use with
care!
</p>
<p>Similarly to &lsquo;<samp><code>proof-check-report</code></samp>&rsquo;, check all opaque proofs in the
current buffer. Instead of generating a report, failing proofs
are annotated with &quot;<var>fail</var>&quot; in a comment. Existing &quot;<var>pass</var>&quot; or
&quot;<var>fail</var>&quot; comments (e.g., from a previous run) are deleted
together with the surrounding white space. With prefix argument
(or when <var>annotate-passing</var> is non-nil) also passing proofs are
annotated with a &quot;<var>pass</var>&quot; comment. Pass and fail comments can be
placed at the last or second last statement before the opaque
proof. For Coq this corresponds to the proof using and the
theorem statement, respectively. In both cases the comment is
placed at the right margin of the first line, see
&lsquo;<samp><code>proof-check-annotate-position</code></samp>&rsquo; and
&lsquo;<samp><code>proof-check-annotate-right-margin</code></samp>&rsquo;.
</p>
<p>Interactively, this command does not save the current buffer
after placing the annotations. With <var>save-buffer</var> non-nil, the
current buffer is saved if it has been modified.
</p></dd></dl>

<dl>
<dt><a class="anchor" id="index-proof_002dcheck_002dannotate_002dposition"></a><u>Variable:</u> <b>proof-check-annotate-position</b></dt>
<dd><p>Line for annotating proofs with &quot;<var>pass</var>&quot; or &quot;<var>fail</var>&quot; comments.<br>
This option determines the line where &lsquo;<samp><code>proof-check-annotate</code></samp>&rsquo; puts
comments with &quot;<var>pass</var>&quot; and &quot;<var>fail</var>&quot;. Value &lsquo;&rsquo;theoren&rsquo; uses the
first line of the second last statement before the start of the
opaque proof, which corresponds to the line containing a Theorem
keyword for Coq. Value &lsquo;&rsquo;proof-using&rsquo; uses the first line of the
last statement before the opaque proof, which corresponds to the
Proof using line for Coq.
</p></dd></dl>

<dl>
<dt><a class="anchor" id="index-proof_002dcheck_002dannotate_002dright_002dmargin"></a><u>Variable:</u> <b>proof-check-annotate-right-margin</b></dt>
<dd><p>Right margin for &quot;<var>pass</var>&quot; and &quot;<var>fail</var>&quot; comments.<br>
This option determines the right margin to which
&lsquo;<samp><code>proof-check-annotate</code></samp>&rsquo; right-aligns the comments with &quot;<var>pass</var>&quot;
and &quot;<var>fail</var>&quot;. If nil, the value of &lsquo;<samp><code>fill-column</code></samp>&rsquo; is used.
</p></dd></dl>


<p>See section <a href="/doc/master/userman/Coq-Proof-General#Quick-and-inconsistent-compilation">Quick and inconsistent compilation</a> for enabling vos compilation
inside Proof General and see See section <a href="/doc/master/userman/Coq-Proof-General#Omitting-proofs-for-speed">Omitting proofs for speed</a> for the
omit-proofs feature.
</p>
<p>The interactive use of this commands is limited because it only works
on the current buffer. However, this commands can also be run in batch
mode in a script, for instance in a continuous integration
environment. To run this command on a file in batch mode, use
<p>The interactive use of <code>proof-check-report</code> and
<code>proof-check-annotate</code> is limited because they only work on the
current buffer. However, these commands can also be run in batch mode
in a script, for instance in a continuous integration environment. To
run <code>proof-check-report</code> on a file in batch mode, use
</p>
<pre class="verbatim">emacs -batch -l &lt;your-pg-dir&gt;/generic/proof-site.el &lt;file&gt; \
--eval '(proof-check-proofs &lt;tap&gt; &lt;output&gt;)'
--eval '(proof-check-report &lt;tap&gt; &lt;output&gt;)'
</pre>
<p>where <code>&lt;tap&gt;</code> should be <code>nil</code> for human readable output and
<code>t</code> for test anything protocol. If <code>&lt;output&gt;</code> is <code>t</code>
the proof status appears in the standard output of the Emacs process.
Otherwise <code>&lt;output&gt;</code> should be a filename as string in double
quotes. Then the proof status is appended to this file. (If
quotes. Then the proof status is written to this file. (If
<code>output</code> is <code>nil</code> or omitted, the proof status is only put
into the <code>*proof-check-report*</code> buffer, which does not make much
sense in a batch command as the one above.)
</p>
<p>Using a similar command also <code>proof-check-annotate</code> can run in
batch mode in a continuous integration environment, for instance for
checking that all failing proofs are annotated with <code>FAIL</code>
via <code>git diff --exit-code</code>.
</p>

<hr size="6">
<a class="anchor" id="Automatic-multiple-file-handling"></a>
Expand Down Expand Up @@ -627,7 +688,7 @@ <h2 class="section">3.11 Editing features</h2>
</div>
<p>
<font size="-1">
This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>

Expand Down
Loading

0 comments on commit 0fc143b

Please sign in to comment.