hyperpf - A HyperTeXt Structured Proof Reader

Last modified 20 February 1998

What is hyperpf?

Hyperpf is a C program that provides a hypertext reader for a structured proof. It works by producing--on command--a file containing just the part of the proof you want to look at, running the file through LaTeX, and causing xdvi (or another dvi previewer) to redisplay the result. On a 230 MHz Alpha, the new view appears within about 3 to 5 seconds of when you issue the command.

The current version of hyperpf runs on Unix. It should be easy to get it to run on another operating system, such as Windows. I haven't used any dvi previewers for Windows that can be made to redisplay a dvi file that has been changed, but I'm told that dviwin, which is available from the Gutenberg Project, does it.

The hyperpf program is new and untested. C and I don't get along well together, so there are probably many system dependencies in the code, as well as the usual number of bugs in an untested program.

How to use hyperpf

Assuming hyperpf is already installed, just prepare the input file as described below and type
 hyperpf file_name
It is self-documenting. Try it out on the sample file samplepf.tex. For information on additional options, run the hyperpf command with no arguments.

Preparing the input file

The input must be a LaTeX source file that contains a single proof written with the pf package. Click here to obtain the pf package. The input file must satisfy the following requirements. It's a good idea to put a \batchmode command near the beginning of the file.

How to install hyperpf

You will have to compile the hyperpf program using a command such as
  cc -lcurses -o hyper hyperpf.c
The switches and perhaps the compiler may be different at your site. The file hyperpf.c contains an explanation of how to

The files can be obtained here:

You may have to customize hyperpf.c to get it to work right at your site. The file contains simple instructions for doing this. You can probably make most of the necessary changes even if you know nothing about C.

Web search unique id: uidlamporthyperpf