Copyright 2019-2020 Mario Frank mario.frank@uni-potsdam.de
This tool is distributed under the terms of the LGPL 2.1 license (see LICENSE for details).
This tool provides the functionality to visualise Coq proof scripts in a form that is understandable without using Coq.
It currently should be seen as a proof-of-concept and is in an early beta phase (version number 0.5).
So, errors may occur. If you have technical difficulties or just want to give feedback, do not hesitate
to contact me.
If you stumble over an exception that states that you should report the error to the Coq bug tracker,
please report it to me as the error will probably be on my side and not on the Coq side.
The error messages are generated by Coq functionality and thus point to the Coq resources.
I will hopefully get that corrected, soon.
Status of Coq support:
Supported output Formats are:
-t latex-table
)-t latex
)-t pdf
)Coq-psv has the following dependencies
In order to install coq-psv, you need the current version of coq, i.e. coq 8.10.
You can install coq with
opam install coq.8.10.0
Those who wish to work with coqide, have to install it with
opam install coqide.8.10.0
Nevertheless, coq-psv does not need nor use coqide.
After the installation of coq is finished, you can go on to the installation of coq-psv.
If you want to have it as easy as possible, add our opam repository on the command line with
opam repo add up_cs_thi_soft https://www.cs.uni-potsdam.de/~mafrank/public/opam/
and install coq-psv with
opam install coq-psv
If you want to install this plugin from source, you first have to compile it. The source code will be published in the near future but is already provided when the tool is installed from the opam repository.
For the compilation, you have to make sure that dune is installed. If it is not, call
opam install dune
on the command line.
Then, you can compile coq-psv being in the root directory of the package with
dune build
and install it with
dune install
After successful installation, the program coq_psv
is available. And you can use both the tool and its output.
First, we will describe the supported command line options and then, the way, you can use the tool and its output.
The tool supports the usual options as coqtop
does. Additionally, we provide the following options:
Output file options:
-t <fmt>
: Defines the output file format.
latex-table
: Only the LaTeX table is generated.
This option is useful if you want to include the generated file
into an existing document.latex
: A complete standalone LaTeX document is generated (default). pdf
: A complete standalone LaTeX document and the respective PDF are generated. -out-fmt <fmt>
: (idem)-generate-stub-files
: Defines that for every input file, an output file should be generated,
even if it does not contain proofs. The default behaviour is to ignore files without proofs.-one-file-per-proof
: If this flag is set, a separate output file File_proof_name.tex
will be generated for each proof in the file File.v
Output file content options:
-psit-style <style>
: Sets the proof situation (hyps and goal(s)) column
coq
: The proof situation as is shown as frac as in Coq. (default) Invariant hypotheses are hidden by default. sequent
: The proof situation is shown as in sequent calculus style. Invariant hypotheses are shown by default.-hide-inv-hyps [yes|no]
: Defines whether invariant hypotheses shall be hidden in output.-hide-branch-psits
: If this flag is set, the proof situations resulting from a tactic are not printed in the step of a
tactic if they are handled by bullets later on. However, Each bullet has it’s proof situation in it’s proof situation column.-show-all-sequence-psits
: Defines that, if a tactic is applied in a situation with multiple proof situations
(Sequence node), all proof situations should be shown. The default is to show only the first and note, how many exist additionally.General options:
-v
: Print the coq_psv version and exit --version
: (idem) -print-version
: Print coq_psv version in easy to parse format and exit.
The format is psv-version Coq-version Ocaml-version. -h
: Print this list of options -help
: (idem) --help
: (idem)To extract all proofs from file numbers.v
, you can for example call
coq_psv -l numbers.v
which will generate the file numbers.tex
Note that this mode currently only works if the numbers.v
only imports modules from the Coq library or already compiled. In other cases, the project extraction mode should be used (as described in the following subsection).
To enable coq-psv to process complete Coq projects, you currently have to add the following lines to the CoqMakefile.in
template provided by Coq. This file can be found in your opam directory, which is usually in your home directory. The usual location of the template is
~/.opam/default/lib/coq/tools/CoqMakefile.in
You have to add
COQPSV ?= "$(COQBIN)coq_psv"
to the section annotated with
# Coq binaries
Also, you have to replace the lines
$(VOFILES): %.vo: %.v
$(SHOW)COQC $<
$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
with
$(VOFILES): %.vo: %.v
$(SHOW)COQPSV $<
$(HIDE)$(TIMER) $(COQPSV) $(COQFLAGS) $(COQLIBS) $(COQPSVOPTS) -l $<
$(SHOW)COQC $<
$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
Furthermore, you need a _CoqProject
file for your project. You then first have to generate the Makefile for processing your project with
coq_makefile -o CoqMakefile _CoqProject
You also should clean your project with
make -f CoqMakefile clean
After that, you can start the processing of your project with
make -f CoqMakefile COQPSVOPTS="-hide-branch-psits -one-file-per-proof"
which will generate the proof table files in the directories where the referenced Coq files are located. For other options, please refer to the command line options.
To include the generated LaTeX files, make sure that you define at least
\usepackage{tabularx} % general table support
\usepackage[mathletters]{ucs} % UTF8 symbol support
\usepackage[utf8x]{inputenc} % UTF8 symbol support
\usepackage{unicode} % UTF8 symbol support
\usepackage{multirow} % support of multirows in tables
\usepackage{longtable, array} % Support for multipage-tables
If you generated the file numbers_my_proof.tex
, you can input this file in your own LaTeX document with
\input{numbers_my_proof.tex}
In your document, you can reference the proof with
\ref{Proofs:numbers:Theorem:my-theorem-name}
Please note that the name of the input file and theorem are not allowed to have underscores in the label. Thus, underscores are replaced by minus symbols.
All generated LaTeX files use default table and cell spaces.
You can override the following commands for spacing and widths:
\stepcolwidth
The width of the justification/Coq step column (default is set to 20 % of the table width)\rulewidth
The width of the rule in frac/default style (default is set to 100% of the cell text width)\rulethickness
The thickness of the rule in frac/default style (default is set to 0.2 mm)To override these default values, you can define the commands according to your wished values with \newcommand
or \renewcommand
before loading the generated file with \input
or \include
and the default values will be ignored happily.
We provide some example output files for a non-trivial proof in Coq as PDF files. The layout is far from being perfect and a small calculation bug currently leads to the command in Coq not always being centered.
The provided example files visualise the proof of the theorem: for all two lists of naturals L and K: If both lists are strictly ordered and both are "subsets" of each other, then they are identical.
There are many possible improvements which includes
Nothing yet
Nothing yet
I would like to thank
Chris Dams
for providing a standalone Coq file as test case for proof information extraction.