The pfnum Program

The pfnum Program

by Leslie Lamport

Last modified 8 August 2012

The Program

The pfnum program is a tool for use with the pf2 LaTeX package.  It rewrites a LaTeX source file so that symbolic proof-step names are replaced with names that are identical to the printed step numbers. The program is run from a command line as

    pfnum   options   file

where file is the name of the LaTeX source file and the possible options are described below.  (The extension .tex can be omitted from file.) The file is rewritten, and a copy of the original is saved with the extension .pfx.


-num   where num is a natural number
Changes the step labels to be the step number, using the long form (e.g., 2.3.5) for proof levels less than num and the short form (e.g., <3>5) for proof levels num and greater.

Puts  %%%{longNum}  immediately after every  \begin{proof}  and  \end{proof} , where  longNum  is the long number of the step for which this  proof  environment is the proof. It deletes everything else on the line following the  \begin{proof}  or  \end{proof} . It also does the analogous operation for  noproof  environments.

Without this option, everything between a  %  and the end of a line is assumed to be a comment, and no changes are made to it. The option causes the input  %%%{lbl}  to be treated as if  lbl  occurred in a  \stepref{lbl}  command.
You cannot use both the  -d  and  -c  options.


Download the version of the pfnum program for your operating system: If you want to compile pfnum yourself or make changes to it, you can download the C code.