Skip to content

Latest commit

 

History

History
157 lines (102 loc) · 6.95 KB

README.md

File metadata and controls

157 lines (102 loc) · 6.95 KB
Raw

Traf

Traf is a proof tree viewer which cooperates with a proof assistant Coq and is controlled through Proof General (PG). Traf is easy to use; actually all what you have to do to use Traf is just to invoke it. You do not have to pay attention to it while proving lemmas by using PG. Traf automatically draws a proof tree corresponding to what you have done while you are interacting with Coq through PG. The trees drawn by Traf are informative and will be of great help.

Traf is an extention to a proof tree viewer named Prooftree. Traf version 0.1 is based on Prooftree-0.13.

Traf version 0.1 has been developed by Hideyuki Kawabata and Yuta Tanaka, with Yuuki Sasaki and Mai Kimura, at Hiroshima City University [1].

This is version 0.1.2 of Traf.

[1] Hideyuki Kawabata, Yuta Tanaka, Mai Kimura and Tetsuo Hironaka, Traf: a Graphical Proof Tree Viewer Cooperating with Coq through Proof General, 16th Asian Symposium on Programming Languages and Systems (APLAS 2018), LNCS 11275, pp.157--165, 2018. DOI: 10.1007/978-3-030-02768-1_9

News

A New version of Traf is comming soon!

  • GTK3 based, utilizing lablgtk3 and cairo2
  • Supports Fitch style-like proof tree drawing

Requirement

Following programs are required to build and run Traf. Numbers indicate tested versions of corresponding software.

  • Coq 8.10.2, 8.9.1, 8.8.2, 8.7.2, 8.6.1
  • Proof General 4.5 (Coq 8.6), 4.4, 4.4.1pre (modification required for Coq 8.7 or later)
  • GTK+ 2.24
  • Lablgtk 2.18.11, 2.18.10, 2.18.5 (opam install lablgtk)
  • OCaml 4.11.1, 4.10.0, 4.05.0

If you use Coq 8.6, Proof General 4.4 and 4.5 can be used without any modification. If you want to use Coq 8.7, 8.8, 8.9, or 8.10, Proof General 4.4 (with slight modification) can only be used. Coq 8.11 or later is not currently supported.

When you use Proof Gneral 4.4, you might want to add the following line to .emacs.

(load-library "cl-extra")

Note that Proof General 4.4 is the latest version available at stable.melpa.org. The version of Coq used with Traf can be changed easily by modifying a single line of .emacs. Settings for Traf wont bother you while you are using higher versions of Coq through Proof General unless you try to open Traf's window by pushing "prooftree icon" on the menubar of Emacs.

Checked environments:

  • macOS Big Sur 11.1 (M1), Catalina 10.15.7, Mojave 10.14.6, Sierra 10.12.6
  • ubuntu 16.04 LTS

Note: a bug ?

On macOS Mojave (10.14.*), Traf does not seem to work smoothly; it may not update what is displayed in its window while it is running background. You seem to be required to give a focus on the window to update the tree shown by Traf.

Known workaround: when you use Split View to show Traf and Emacs on a screen simultaneously, no problem seems to occur.

Note: for users of Coq 8.7 or later

Proof General requires slight modification. Please apply the patch file in misc and rebuild PG.

$ cd pg_top_dir
$ patch -p0 < traf_top_dir/misc/pg44.patch
$ make

Note 0: If you use PG 4.4.1pre, use pg.patch instead of pg44.patch.

Note 1: This modification of PG is also recommended for Coq 8.6 users because of a slight (preferable, maybe) change of behavior.

Note 2: When you install PG by using MELPA, you might have to modify files in a directory named like ~/.emacs.d/elpa/proof-general-20181226.2300/. Be sure that you might have to byte-compile .el files into .elc files.

Building Traf

Run misc/quick_build.sh at the Traf's top directory, and you will get the executable traf in newly created directory build. You can copy traf anywhere you want.

$ cd traf_top_dir
$ sh misc/quick_build.sh

FYI: What is done by misc/quick_build.sh:

  1. Obtain prooftree-0.13.tar.gz. See https://askra.de/software/prooftree/ for details of Prooftree. Just for convenience, we have the tarball in the directory misc.

    $ cd traf_top_dir
$ tar zxfv ./misc/prooftree-0.13.tar.gz

    The above command creates a directory named prooftree-0.13. Let's rename it build.

    $ mv prooftree-0.13 build

  2. Put additional files and a patch file in src into build.

    $ cp ./src/* ./build/

  3. Apply the patch for Traf.

    $ cd build
$ patch -p1 < prooftree-to-traf.patch

  4. Build.

    $ ./configure
$ make

    You will have traf in the current directory, i.e., build. If you want, type make install to install traf in a public area.

Settings

Put following lines in .emacs (the 2nd line only is related to Traf):

(setq coq-prog-name "/home/where/my/thoughts/escaping/coqtop")
(setq proof-tree-program "/home/where/my/musics/playing/traf")
(load "/home/where/my/love/lies/waiting/generic/proof-site")

  • The third line may not be required if you have been already using PG, or you have installed PG by using MELPA.

  • Note that you can modify exec-path to make the values of coq-prog-name and proof-tree-program short.

  • Note that you can not share coq library if your machine has multiple versions of coqtop. Since PG is not smart enough to detect the place where the corresponding version of the library for each coqtop is installed (default lib dir: /usr/local/lib/coq), we advise that coq-prog-name is not a symbolic link to coqtop. For example, if you are using Homebrew, we recommend you write

    (setq coq-prog-name "/usr/local/Cellar/coq/8.6.1_1/bin/coqtop")

    instead of /usr/local/bin/coqtop, which is a symbolic link to the above, in order to avoid troubles in advance.

Usage

  • While proving a theorem by using Proof General, you can invoke Traf by clicking the "prooftree icon", or equivalently, type C-c C-d (proof-tree-external-display-toggle). Note that if you are using company-coq C-c C-d might be assigned to a different function.
  • You can perform anything while proving with PG; e.g., C-c RET (proof-goto-point), C-c C-u (proof-undo-last-successful-command), etc. The proof tree shown in the Traf window changes synchronously.
  • Once a proof of a theorem (Theorem, Lemma, Example, whatever) is finished, i.e., the vernacular command Qed is given to Coq, the connection between PG and Traf is closed (but the Traf window remains on the screen and you can manipulate it). When you start proving another theorem, you are required to invoke Traf again (by clicking the "prooftree icon").