Commit 93095593 authored by Heiko Becker's avatar Heiko Becker

Add flocq version to README

parent c3036aae
...@@ -40,6 +40,13 @@ $ make ...@@ -40,6 +40,13 @@ $ make
``` ```
This will compile all coq files and then in the end the certificate in the output directory. This will compile all coq files and then in the end the certificate in the output directory.
To compile the file `IEEE_connection.v` showing the relation to IEEE754 semantics, it is necessary to install
the Flocq library via opam:
```bash
$ opam install coq-flocq.2.6.1
```
Note that due to some incompatibilities, FloVer currently does not support flocq 3.0.
The coq binary is build in the directory `coq/binary` and you can compile it by The coq binary is build in the directory `coq/binary` and you can compile it by
running `make native` in the directory. running `make native` in the directory.
......
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