Coq Proof Script Visualiser

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).

Project Members

Synopsis

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:

1 Installation

1.1 Dependencies

Coq-psv has the following dependencies

1.2 Preparation

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.

1.3 From our Opam Repository

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

1.4 From source

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

2 Usage

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.

2.1 Command Line Options

The tool supports the usual options as coqtop does. Additionally, we provide the following options:

Output file options:

Output file content options:

General options:

2.2 Extracting Proofs From one Coq File

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).

2.3 Extracting Proofs From Complete Coq Projects

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.

2.4 Using the Output Files

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:

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.

2.5 Example output files

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.

3 Future Work

There are many possible improvements which includes

4 Papers and Technical Reports

4.1 Publications About coq-psv

Nothing yet

5 Developer Information

Nothing yet

6 Special Thanks

I would like to thank