Tarski Formalization Project: ExtractProofs
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
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.