Michael Beeson's Research

Tarski Formalization Project: ExtractProofs

The script ExtractProofs permits one to extract the proofs from the output files, a chapter at a time, and dump them in a specified directory. The actual extraction is performed by WriteProofFile, which is in file GenerateInputFiles.php.

For reasons of security, since it is often used on web servers to serve dynamic web pages, PHP is not allowed to open files in arbitrary locations. Therefore, you must dump the proofs into a subdirectory of the directory where ExtractProofs.php is located. That is not a serious limitation, because after than you can copy them to a desired location, even one that you could not open from within PHP.