Benchmarks used for ITP 2023 submission

Benchmarked code for Candle, HOL4, and HOL Light

Files

The following archive contains code that may be used to reproduce the benchmarks in the paper: benchmarks.tar.gz.

It contains the following benchmarks:

• compute_examples.ml: Candle benchmarks
• eval_examples.ml: HOL Light benchmarks
• hol4testScript.sml: HOL4 benchmarks

• gospers.rle: The Game of Life (GOL) state used in the benchmarks
• readerScript.sml: Code for generating a HOL term of the GOL state

Instructions

Instructions for building and installing Candle is shown below. For instructions on how to build and run HOL4 and HOL Light, please refer to respective projects instructions on Github:

• HOL4
• HOL Light

Building Candle

Candle currently runs on Linux x86-64 and requires a C compiler. Below is a script which downloads and builds Candle:

#!/bin/sh

# Clone and move to the Candle Github repository:
git clone https://github.com/CakeML/candle.git
cd candle

# Get the following CakeML compiler release that has a C FFI that has been
# modified to perform timings for the benchmarks:
curl -OL http://www.cakeml.org/itp2023/cake-x64-64.tar.gz
tar xvzf cake-x64-64.tar.gz

# Build the compiler binary
cd cake-x64-64 && make && cd ..

# Copy the compiler binary and the exported compiler state into this directory:
cp cake-x64-64/cake cake-x64-64/config_enc_str.txt .

# You should now be able to start Candle by writing:
#   ./cake --candle
# or:
#   ./candle
# from the shell.

Benchmarks

First, unpack the files from benchmarks.tar.gz somewhere.

Benchmarks: Candle

From the directory where you installed Candle, do the following:

1. Start the Candle REPL by writing: ./candle.
2. Load the HOL Light basis theories from the REPL by writing: #use "hol.ml";;.
3. (Wait for some time)
4. Execute the benchmarks from the REPL by writing: #use "/path/to/benchmarks/compute_examples.ml";;

Benchmarks: HOL Light

From the directory where you installed HOL Light, do the following:

1. Start the OCaml REPL by writing: ocaml -I $(camlp5 -where).
2. Load the HOL Light basis theories from the REPL by writing: #use "hol.ml";;.
3. (Wait for some time)
4. Execute the benchmarks from the REPL by writing: #use "/path/to/benchmarks/eval_examples.ml";;

N.B. The HOL Light examples take several hours to execute on a fast machine.

Benchmarks: HOL4

From the directory where you unpacked the benchmarks, do the following:

1. Build the HOL4 theory by writing: Holmake -j1 hol4testTheory.

(If you need to re-run the benchmarks, first remove the theory with Holmake clean)