Commit e525d16d by Eva Darulova

Update README.md

parent 8d9eac85
......@@ -71,7 +71,7 @@ You can then run Daisy on an input file as follows:
$ ./daisy testcases/rosa/Doppler.scala
```
## Checking Error Bound 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
......@@ -88,7 +88,7 @@ $ ./daisy file --certificate=binary
```
The certificate can then be found in the folder `coq/output`, `hol4/output` or `output` for binary certificates.
## Compiling the formal developments
## Checking Coq certificates
To check the Coq certificate, you need to enter the `coq` directory and then run
```bash
......@@ -107,16 +107,35 @@ $ coqc -R ./ Daisy output/CERTIFICATE_FILE.v
The generated binaries can be run with `coq_checker_{native/byte} CERTIFICATE_FILE`.
To check the HOL4 certificate, you need to enter the `hol4` directory and then run
## 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
$ git submodule update --recursive --remote
$ cd hol4/
$ Holmake
```
to initialize the CakeML submodule and then start compilation.
Note that this may take a lot of time, since it also builds all files from CakeML on which the extraction depends.
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, you need to enter the `hol4/output` directory and then run
To check the HOL4 certificates, enter the `hol4/output` directory and run
```bash
$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}
```
......
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