PISA (Portal to ISAbelle)

PISA supports automated proof search with the interactive theorem prover Isabelle.

PISA can also be used to extract proof corpus. We extracted the datasets in our AITP 2021 paper LISA: Language models of ISAbelle proofs with it.

Installation

1. Scala configuration

   Install SDKMAN

   curl -s "https://get.sdkman.io" | bash
   source .bashrc

   Try

   sdk help

   to makes ure sdk is properly installed.

   Install JAVA 11 and sbt

   sdk install java 11.0.11-open
   sdk install sbt

2. Clone project and make sure it compiles

   git clone https://github.com/albertqjiang/Portal-to-ISAbelle.git
   cd Portal-to-ISAbelle

   Then compile the project:

   sbt compile

3. Configure Isabelle

   Go back to home directory first and download isabelle2021

   cd ~
   wget https://isabelle.in.tum.de/dist/Isabelle2022_linux.tar.gz
   tar -xzf Isabelle2022_linux.tar.gz
   alias isabelle=~/Isabelle2022/bin/isabelle

4. Build Isabelle HOL

   To build with 20 parallel processes:

   isabelle build -b -D Isabelle2022/src/HOL/ -j 20

   This takes ~8 hours of CPU time. The actual time depends on the number of CPUs you have. On a 96-core TPU VM it takes about 15 minutes.

5. Download and build afp

   To build with 10 parallel processes:

   wget https://www.isa-afp.org/release/afp-current.tar.gz
   tar -xzf afp-current.tar.gz
   export AFP=afp-{$AFP_DATE}/thys
   isabelle build -b -D $AFP -j 20

   This takes ~150 hours of CPU time. On a 96-core TPU VM it takes ~5 wall-clock hours. We can extract ~93% of all afp theory files.

   We built the heap images for two options:

   1. Isabelle2021 with afp-2021-10-22 for linux machines (ubuntu). You can download it at: https://archive.org/download/isabelle_heaps.tar/isabelle_heaps.tar.gz and decompress it as ~/.isabelle.
   2. Isabelle2022 with afp-2022-12-06 for linux machines (ubuntu). You can download it at: https://archive.org/download/isabelle2022_afp20221206_heaps/isabelle2022heaps.tar.gz and decompress it as ~/.isabelle.

   Note: this does not always work on different operating systems.

6. Extract the test theorems The universal test theorems contains 3000 theorems with their file paths and names. The first 600 of them are packaged as "quick" theorems if you have no patience testing all 3000 out.

   tar -xzf universal_test_theorems.tar.gz

Evaluation setup (if you want to have N (N>50) PISA servers running on your machine)

1. Create some PISA jars

   For a single process, sbt is good enough. But for multiple processes, to have native JAVA processes running is a better idea. We first use sbt-assembly to create a fat jar (a jar where all the java code is compiled into and can be run independently).

   sbt assembly

   The assembly process should take less than 5 minutes. The compiled jar file is in the target/scala-2.13/ directory as PISA-assembly-0.1.jar. You can then copy the PISA jar for N times if you want the jars to be truly independent and separated by calling the following script:

   python eval_setup/copy_pisa_jars.py --pisa-jar-path target/scala-2.13/PISA-assembly-0.1.jar --number-of-jars $N --output-path $OUTPUT_PATH

2. Create some Isabelle copies

   This step is to create multiple copies of the Isabelle software as well as the built heap images to avoid IO errors which can occur when many processes are run at the same time. We use $ISABELLE to denote where your Isabelle software lives and $ISABELLE_USER to denote where your built heap images live, which is usually at $USER/.isabelle

   Note that one copy of the Isabelle software plus all the heaps needed for the Archive of Formal Proofs amount to 35GB of disk space. So create copies with care. Alternatively, you can start by trimming the heaps so only the ones you need are kept.

   Use the following script to create the copies:

   python eval_setup/copy_isabelle.py --isabelle $ISABELLE --isabelle-user $ISABELLE_USER --number-of-copies $N --output-path $OUTPUT_PATH

Extract PISA dataset

Archive of formal proofs

Generate commands for extracting proofs. Edit line 9 of command_generation/generate_commands_afp.py so that it uses your actually home directory. Run the following command:

python command_generation/generate_commands_afp.py

and follow the instructions. At the first step it asks you which ports you want to use. We current support ports 8000-8200, 9000, 10000, 11000, 12000. You can also add your favourites by editing src/scala/server/PisaOneStageServers.scala. This dictates how many processes for extraction you wish to run at the same time.

It should say "A total of X files are due to be generated" with X > 5000. And you should see files called afp_extract_script_${port_number}.sh in the directory.

To extract the files, run the following commands to install necessary libraries and execute the commands:

pip install grpc
pip install func_timeout
bash afp_extract_script_${port_number_1}.sh &
bash afp_extract_script_${port_number_2}.sh &
bash afp_extract_script_${port_number_3}.sh &
...
bash afp_extract_script_${port_number_n}.sh &

With a single process, the extraction takes ~5 days. This will extract files to the directory afp_extractions. We have also extracted this dataset, available for download at https://archive.org/download/afp_extractions.tar/afp_extractions.tar.gz.

To extract state-only source-to-target pairs, run the following command:

python3 src/main/python/prepare_episodic_transitions.py -efd afp_extractions -sd data/state_only --state

To extract proof-only source-to-target pairs, run the following command:

python3 src/main/python/prepare_episodic_transitions.py -efd afp_extractions -sd data/proof_only --proof

To extract proof-and-state source-to-target pairs, run the following command:

python3 src/main/python/prepare_episodic_transitions.py -efd afp_extractions -sd data/proof_and_state --proof --state

Note that extraction involving proofs will take pretty long and will result in large files. State-only files amount to 8.1G. With proof steps it's even much larger.

Acknowledgement

This library is heavily based on scala-isabelle, the work of Dominique Unruh. We are very grateful to Dominique for his kind help and guidance.

Citation

If you use this directory, or our code, please cite the paper we published at AITP 2021.

@article{jiang2021lisa,
  title={LISA: Language models of ISAbelle proofs},
  author={Jiang, Albert Q. and Li, Wenda and Han, Jesse Michael and Wu, Yuhuai},
  year={2021},
  journal={6th Conference on Artificial Intelligence and Theorem Proving},
}