diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-03-15 13:27:56 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-03-15 13:27:56 +0100 |
commit | 7da3a3dc751adb2829c29b0b1500913636ba1f41 (patch) | |
tree | d13a2f91df51bda2132a110298e17d4885afe9dd /INSTALL.md | |
parent | ae455fa3aa29c872c9c5b2736fff861afebcd051 (diff) | |
download | smtcoq-7da3a3dc751adb2829c29b0b1500913636ba1f41.tar.gz smtcoq-7da3a3dc751adb2829c29b0b1500913636ba1f41.zip |
Explain LFSCSIGS in the installation instructions for CVC4
Diffstat (limited to 'INSTALL.md')
-rw-r--r-- | INSTALL.md | 38 |
1 files changed, 17 insertions, 21 deletions
@@ -186,6 +186,23 @@ the latest version available). The `cvc4` binary must be present in your PATH to use it through SMTCoq. +In your `.bashrc` (or `.bash_profile`, or any other initialization file read by +your shell), export the following environment variable to make it point at the +`signatures` directory distributed with SMTCoq. + +> Don't use `~` in the path but rather `$HOME`. + +```bash +export LFSCSIGS="$HOME/path/to/smtcoq/src/lfsc/tests/signatures/" +``` + +If you don't want SMTCoq to spit the translated proof in your proof environment +window, add the following optional definition (in the same file). + +```bash +export DONTSHOWVERIT="yes" +``` + ### veriT @@ -219,27 +236,6 @@ The `zchaff` binary must be present in your PATH to use it through SMTCoq. ## Setting up environment for SMTCoq - -To use the latest features of SMTCoq, you need to make these configuration -changes: - -In your `.bashrc` (or `.bash_profile`, or any other initialization file read by -your shell), export the following environment variable to make it point at the -`signatures` directory distributed with SMTCoq. - -> Don't use `~` in the path but rather `$HOME`. - -```bash -export LFSCSIGS="$HOME/path/to/smtcoq/src/lfsc/tests/signatures/" -``` - -If you don't want SMTCoq to spit the translated proof in your proof environment -window, add the following optional definition (in the same file). - -```bash -export DONTSHOWVERIT="yes" -``` - ### Using SMTCoq without installing If you want to use SMTCoq without installing it your Coq installation, you can |