Commit 46952ce5 authored by Heiko Becker's avatar Heiko Becker

Update README

parent 65ca46a4
......@@ -58,7 +58,7 @@ You can then run Daisy on an input file as follows:
$ ./daisy testcases/rosa/Doppler.scala
```
## Checking Interval Arithmetic Certificates
## Generating Error Bound Certificates
If you want to produce certificates to check them in either of the supported backends,
you have to call Daisy as with
......@@ -67,26 +67,74 @@ $ ./daisy file --certificate=coq
```
or
```bash
$ ./daisy file --certificate=hol
$ ./daisy file --certificate=hol4
```
or for one of the binaries
```bash
$ ./daisy file --certificate=binary
```
The certificate can then be found in the folder `coq/output`, `hol4/output` or `output` for binary certificates.
The certificate can then be found in the folder `coq/output` or `hol/output`.
## Checking Coq certificates
To check the Coq certificate, you need to enter the coq directory and then run
To check the Coq certificate, you need to enter the `coq` directory and then run
```bash
$ ./configure_coq.sh
$ make
```
This will compile all coq files and then in the end the certificate in the output directory.
The coq binaries are build in the directory `coq/binary` and you can compile them by running
either `make native` or make byte` in the directory.
If an additional certificate should be checked later on, it suffices to call the Coq compiler:
```bash
$ coqc -R ./ Daisy output/CERTIFICATE_FILE.v
```
To check the HOL-Light certificates, you need to enter the hol directory and then run
The generated binaries can be run with `coq_checker_{native/byte} CERTIFICATE_FILE`.
## Checking HOL4 certificates
If you haven't updated your HOL4 installation in a while, update it first:
```bash
$ cd path/to/HOL
$ bin/build cleanAll
$ poly < tools/smart-configure.sml
$ bin/build
```
Then, back in the Daisy home directory, if you haven't done so before:
```bash
$ git submodule init
```
(If successfull, you should see a message like ```Submodule 'hol4/cakeml' (https://github.com/CakeML/cakeml.git) registered for path 'hol4/cakeml'```)
Then, initialize the CakeML submodule and start compilation:
```bash
$ ./configure_hol.sh
$ ocaml output/CERTIFICATE_FILE.hl
$ git submodule update --recursive --remote
$ cd hol4/
$ Holmake
```
Note that this may take some time, since it also builds all files from CakeML on which the binary code extraction depends.
If you don't want to wait for so long, you can cheat the compilation:
```bash
$ Holmake --fast
```
To check the HOL4 certificates, enter the `hol4/output` directory and run
```bash
$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}
```
The HOL4 binary is build by entering the directory `hol4/binary`. Then one needs to run
```bash
$ Holmake checkerBinaryTheory.sig
$ Holmake
```
The generated file `cake_checker` is the binary.
It can be run by
```bash
$ ./cake_checker < CERTIFICATE_FILE
```
## Additional Software
......@@ -102,12 +150,6 @@ Currently, this is
* Coq: Version 8.5pl2 if you want to extract certificates for it, [install it](https://coq.inria.fr/download)
* HOL-Light: Git checkout (no later than 1.08.2016) if you want to extract certificates for it, [downloadit](https://github.com/jrh13/hol-light/)
Afterwards configure the environment variable HOLLIGHT_HOME to point to the directory you downloaded HOL-Light into with
```
$ export HOLLIGHT_HOME=path_to_hol_light_git
```
## Documentation
## Intellij Idea Setup
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment