Commit f5ba4315 authored by Heiko Becker's avatar Heiko Becker

Add explanation on how to run certificate checking to README

parent dd9ced38
......@@ -58,6 +58,35 @@ You can then run Daisy on an input file as follows:
$ ./daisy testcases/rosa/Doppler.scala
```
If you want to produce certificates to check them in either of the supported backends,
you have to call Daisy as with
```bash
$ ./daisy file --certificate=coq
```
or
```bash
$ ./daisy file --certificate=hol
```
The certificate can then be found in the folder `coq/output` or `hol/output`.
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.
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
```bash
$ ./configure_hol.sh
$ ocaml output/CERTIFICATE_FILE.hl
```
## Additional Software
Some features of Daisy require additional software to be installed.
......@@ -69,6 +98,13 @@ Currently, this is
* MPFR: Daisy uses a [Java binding](https://github.com/kframework/mpfr-java).
(TODO: figure out whether we used the static or dynamic binding)
* 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
......@@ -82,5 +118,3 @@ directly taken from the Leon project (see the LEON_LICENSE).
Especially the files in frontend, lang, solvers and utils bear more than
a passing resemblance to Leon's code.
Leon version used: 978a08cab28d3aa6414a47997dde5d64b942cd3e
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