diff options
| -rw-r--r-- | .gitignore | 7 | ||||
| -rw-r--r-- | BUILDING.md | 14 | ||||
| -rw-r--r-- | lib/coq/.gitignore | 1 | ||||
| -rw-r--r-- | test/mono/.gitignore | 1 |
4 files changed, 19 insertions, 4 deletions
@@ -33,6 +33,7 @@ lib/hol/sail-heap *.glob .*.aux /lib/coq/.nia.cache +/lib/coq/deps # Isabelle @@ -60,16 +61,22 @@ lib/hol/sail-heap /test/smt/*.out /test/smt/*.smt2 /test/c/*.c +/test/c/*.h /test/c/*.result /test/c/*.iresult /test/c/*.oresult /test/c/*.bin /test/c/*_ocaml /test/c/_sbuild* +/test/coq/.lia.cache +/test/coq/.nia.cache +/test/coq/out.v +/test/coq/out_types.v /test/mono/Out_lemmas.thy /test/mono/log /test/mono/test.cmi /test/mono/test.cmo +/test/mono/test-output /language/*.pdf /language/*.uo diff --git a/BUILDING.md b/BUILDING.md index 8df08e0b..7e63de0c 100644 --- a/BUILDING.md +++ b/BUILDING.md @@ -127,11 +127,21 @@ To build Sail with interactive support we need two more commands opam install linenoise make isail ``` -To test Sail is installed correctly, execute the following from the +To test if Sail behaves correctly, execute the following from the root directory of the sail repository. You may also need to set $LEM_DIR to the root of the lem repository for the lem tests. Some of -the C backend tests will fail if valgrind isn't installed. +the C backend tests will fail if valgrind isn't installed. Some tests will +fail if cvc4 isn’t installed. ``` export SAIL_DIR=$PWD test/run_tests.sh ``` + +To install Sail using OPAM from the git repo, use `opam pin` as follows. +``` +opam pin add sail /path/to/local/sail/repo +``` +This way, you can make the most recent changes to Sail easily available to programs +that use it. To rebuild this installation of Sail, use `opam upgrade` as usual. +If you want to do more complicated things, `opam pin --help` might be of +interest. diff --git a/lib/coq/.gitignore b/lib/coq/.gitignore deleted file mode 100644 index 1aa62803..00000000 --- a/lib/coq/.gitignore +++ /dev/null @@ -1 +0,0 @@ -deps
\ No newline at end of file diff --git a/test/mono/.gitignore b/test/mono/.gitignore deleted file mode 100644 index bb7f92e1..00000000 --- a/test/mono/.gitignore +++ /dev/null @@ -1 +0,0 @@ -test-output
\ No newline at end of file |