IMPORTANT: This code is not actively maintained anymore
The Case Studies for the CPP 2021 paper can be found in the folder examples.
Please make sure to install the dependencies and follow the setup guide below if
you intend to run them on your machine.
To run Lassie you need to have a working HOL4 installation. For this please refer to [https://github.com/HOL-Theorem-Prover/HOL].
To compile and run SEMPRE you need to have a working ruby installation.
The java jar command should also be available either from OpenJDK or Oracle Java.
Running the following command should on Debian based systems set up the dependencies correctly:
apt-get install ant ruby2.7
To run Lassie you need to first configure some environment variables. Assuming you are in the directory to which the Lassie repository was cloned, run
export LASSIEDIR=`pwd`
echo "export LASSIEDIR=$LASSIEDIR" >> ~/.bash_profile
Now you can set up SEMPRE and build the Lassie support library
cd $LASSIEDIR/sempre/
./pull-dependencies core interactive
ant core interactive
cd $LASSIEDIR/src
$HOLDIR/bin/Holmake
The examples folder comes with an already preconfigured Holmake file. We
suggest to put new files in that directory to experiment with Lassie.
To use Lassie in a HOL4 script, add the following line after other included libraries
open LassieLib;
Running this command loads the functions from the Lassie library and starts a SEMPRE instance. Note that we currently support only one instance of SEMPRE being run.
Now you can use nltac as a drop-in replacement for any HOL4 tactic, sending
tactic descriptions to SEMPRE.
We recommend running the examples from the examples directory (files
arithTactics.sml and realTactics.sml) to get some predefined descriptions.
Also see the script files in that directory for examples how to use nltac.
Funtion nlexplain can be run similarly.
It must be put before starting the actual proof script:
nlexplain()
<Lassie tactics>
After sending nlexplain() to the HOL4 REPL, Lassie tactics can be send just
like normal HOL4 commands to the REPL.
If you want to use Holmake, you have to explicitly enforce no parallelism, using
Holmake -j 1.
In case there are any issues with Holmake please look at the [[Known Bugs]].
If you only want to test SEMPRE's grammar for Lassie, this can be done by running
the run script:
$LASSIEDIR/sempre/interactive/run @mode=lassie
This will give you an interactive SEMPRE session where commands can be send to SEMPRE and their parse according to the grammar is printed.
The case studies for our CPP 2021 paper can be found in the directory examples.
File caseStudy<N> is the n-th case study from section 5 of the paper.
The file gaussScript.sml contains the prove of the closed formula for the sum
of the first n numbers, used as an example in our HOL4 tutorial.
The files arithTacticsLib.sml, logicTacticsLib.sml and realTacticsLib.sml
contain the calls to def setting up the Lassie tactics for the case studies
and the tutorial.
The directory src contains the main SML development of Lassie, connecting HOL4
to the semantic parser SEMPRE.
The directory sempre contains the version of SEMPRE that we have based the
development of Lassie on.
It is mostly based GitHub version (https://github.com/percyliang/sempre) of the paper
Berant, J., Chou, A., Frostig, R., and Liang, P. Semantic parsing on
Freebase from question-answer pairs. In Empirical Methods in Natural
Language Processing (EMNLP) (2013)/.
There is a known bug with HOL4, in that sometimes HOL4 will get hung up on
reading the SEMPRE output, especially when not running with Holmake -j1.
This can be seen by Holmake printing something along the lines of invalid command: ....
If this happens please interrupt the process with Ctrl-c and restart Holmake.