Sledgehammering without ATPs

Content of this Archive This archive contains the following directories. (In Zenodo, they are ZIP archives.) scripts: This directory contains the scripts that automate the experiment. build-container.sh: This shell script builds a container image containing Isabelle/HOL and the Archive of Formal Proofs. Containerfile: This file describe the container to build. proof_methods: This subdirectory contains the scripts that automate evaluating the proof methods. sledgehammer: This subdirectory contains the scripts that automate evaluating Sledgehammer. test_proof_methods: This directory contains the evaluation results for the proof methods. It consists of many subdirectories that each contain one Mirabelle log file. These log files can be analyzed to extract success-rate and timing results. test_sledgehammer: This directory contains the evaluation results for Sledgehammer. It consists of many subdirectories that each contain one Mirabelle log file. These log files can be analyzed to extract success-rate and timing results. Perform the Experiment The experiment can be performed by following these steps. Step 1: Build the Container To run the experiment, we first download, install, and configure specific versions of Isabelle/HOL and the Archive of Formal Proofs in a podman container. The container image can be built using the following command: $ sh ./scripts/build-container.sh Building the container image takes approximately 38 minutes on a laptop with an AMD Ryzen AI 7 PRO 360 processor and 64 GiB of random-access memory. Step 2: Test Sledgehammer Sledgehammer can be tested using the following commands: $ mkdir test_sledgehammer $ cd test_sledgehammer $ sh ../scripts/sledgehammer/run.sh This evaluates Sledgehammer with the MePo and MeSh fact filters on multiple Isabelle sessions.It creates one subdirectory per tested configuration.Each subdirectory follows this naming pattern: <fact-filter>__<isabelle-session>. Running this can take several days to a few weeks. Step 3: Test the Proof Methods The proof methods can be tested using the following commands: $ mkdir test_proof_methods $ cd test_proof_methods $ sh ../scripts/proof_methods/run.sh This evaluates several proof methods with varying number of facts on multiple Isabelle sessions.It creates one subdirectory per tested configuration.Each subdirectory follows this naming pattern: <proof-method>__<number-of-facts>facts__<isabelle-session>. Running this can take several weeks. Step 4: Compile Results Success Rate Run the following commands to compute the success rate of Sledgehammer: $ cd test_sledgehammer $ sh ../scripts/sledgehammer/compute-stats.sh This outputs percentages that can be copy-pasted into the paper. Run the following commands to compute the success rate of the proof methods: $ cd test_proof_methods $ sh ../scripts/proof_methods/compute-stats.sh This outputs a partial LaTeX table that can be copy-pasted into Table 1 of the paper. Fine-Grain Statistics More fine-grain statistics require us to compute the sets of solved goals for each configuration: $ cd test_sledgehammer $ sh ../scripts/sledgehammer/compute-solved-sets.sh This generates the files solved-goals-mepo.txt and solved-goals-mesh.txt, which store the sets of goals solved by Sledgehammer when using the MePo and MeSh fact filters respectively.The sets contain on element per line. $ cd test_proof_methods $ sh ../scripts/proof_methods/compute-solved-sets.sh This prints, for each proof method, the success rate each tested configurations and the success rate of their union.It also prints the success rate of the union of all proof methods' configurations.This information can be used to fill the missing column "Union" of Table 1. In addition, this creates the subdirectory solved-goals that contains one file per proof-method configuration.Each file contains the set of goals solved by that configuration. This also creates the file solved-goals-all.txt, which contains the union of all goals solved by all configurations, and the file solved-goals-try0.txt, which contains the union of goals solved by all proof methods without any fact. These files can be used to compute the portfolios. Portfolios The standard portfolio can be computed using the following commands: $ cd test_proof_methods $ sh ../scripts/proof_methods/ComputePortfolio solved-goals/*__??facts The try0-subsuming portfolio can be computed using the following commands: $ cd test_proof_methods $ SUBSUME_TRY0=1 sh ../scripts/proof_methods/ComputePortfolio solved-goals/*__??facts These can be used to fill out Table 3 of the paper. Timing Statistics Run the following commands to compute Sledgehammer's timing: $ cd test_sledgehammer $ sh ../scripts/sledgehammer/compute-stats.sh This generates the files solving-time-mepo.txt and solving-time-mesh.txt, which store the sets solving time for goals solved by Sledgehammer when using the MePo and MeSh fact filters respectively.The percentiles can be computed with the st command-line tool. $ cd test_sledgehammer $ for P in 25 50 75 90 95 99; do st-console --percentile=${P} solving-time-mesh.txt; done Run the following commands to compute the success rate of the proof methods: $ cd test_proof_methods $ sh ../scripts/proof_methods/compute-solving-time.sh This outputs a partial LaTeX table that can be copy-pasted into Table 2 of the paper.