Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove z3 dependency more #637

Merged
merged 2 commits into from
Oct 18, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 3 additions & 5 deletions backend/cn/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,12 @@ Below are the installation instructions for installing Cerberus, CN,
and their dependencies.


1. Install a recent version of OCaml (we are using 5.0.0) and the opam
1. Install a recent version of OCaml (we are using 5.0.0 -- 5.2.0) and the opam
package manager for OCaml, following the instructions at
<https://ocaml.org/docs/install.html>. (Remember to initialise opam
via `opam init` after the installation of opam.)

2. Install the GMP and MPFR libraries, and Python (a dependency of
Z3). On a Ubuntu system this is done via `sudo apt install libgmp-dev libmpfr-dev python2.7` .
2. Install the GMP and MPFR libraries, and Z3. On a Ubuntu system this is done via `sudo apt install libgmp-dev libmpfr-dev z3` .

3. Install the `dune` OCaml build system and Lem via

Expand All @@ -31,8 +30,7 @@ via `opam init` after the installation of opam.)
```

5. In the downloaded `cerberus` directory run the following opam
command to install CN's opam-package dependencies, including
Z3. (Installation of Z3 usually takes relatively long.)
command to install CN's opam-package dependencies.

```
opam install --deps-only ./cerberus-lib.opam ./cn.opam
Expand Down
3 changes: 1 addition & 2 deletions backend/cn/bin/dune
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,7 @@
ocamlgraph
result
str
unix
z3))
unix))

; There is already a Version in Cerb_frontend, but if new commits only require
; rebuilding the CN backend that module will be out of date.
Expand Down
Loading