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.
- There are no command definitions within the proof.
- There is at most one \begin{proof},
\end{proof}, \step, or \qedstep
command per line. None of these commands may be commented
out or be used in any strange way outside of the proof (e.g.,
in an verbatim).
- No text precedes a \begin{proof} or follows an
\end{proof} on the same line.
- There is no space between the \begin or
\end and the {proof}, or between
the \step and the following {.
- The proof contains no \nostep command or
noproof environment.
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:
-
- hyperpf.c
samplepf.tex
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