-
Notifications
You must be signed in to change notification settings - Fork 11
Standardize on using dune to build CodeHawk #196
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
Merged
Databean
merged 4 commits into
static-analysis-engineering:master
from
brk:standardize-on-dune
May 31, 2025
Merged
Changes from all commits
Commits
Show all changes
4 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,173 +1,62 @@ | ||
| # Building with make | ||
| # Install Dependencies | ||
|
|
||
| ## System Requirements | ||
|
|
||
| Building codehawk requires the following applications and libraries: | ||
|
|
||
| - Objective Caml (version 4.09 or higher) | ||
| - The Findlib / ocamlfind library manager | ||
| - The Zlib C library, version 1.1.3 or up | ||
| - The Zarith library | ||
|
|
||
| The CodeHawk Tool Suite contains three analyzers that can all be built | ||
| individually. All three analyzers have an optional gui that can be built | ||
| separately (and that requires additional dependencies to be installed). | ||
|
|
||
|
|
||
| ### Install dependencies: Ubuntu 16.04 or later (without gui) | ||
|
|
||
| ``` | ||
| sudo apt update -y | ||
| sudo apt install software-properties-common pkg-config m4 zlib1g-dev libgmp-dev -y | ||
| sudo add-apt-repository ppa:avsm/ppa -y | ||
| sudo apt update -y | ||
| sudo apt install opam | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| opam init --bare --no-setup --disable-sandboxing | ||
| opam switch create codehawk-4.12.1 4.12.1 --no-switch | ||
| eval $(opam env --switch=codehawk-4.12.1 --set-switch) | ||
| opam install ocamlfind zarith camlzip extlib goblint-cil | ||
| cd codehawk/CodeHawk | ||
| ``` | ||
|
|
||
| Depending on which analyzer you want to build: | ||
| - **Binary:** `./make_binary_analyzer.sh` | ||
| - analyzer binary: CHB/bchcmdline/chx86_analyze | ||
| - **C:** `./make_c_analyzer.sh` | ||
| - parser binary: CHC/cchcil/parseFile | ||
| - analyzer binary: CHC/cchcmdline/canalyzer | ||
| - **Java:** `./make_java_analyzer.sh` | ||
| - analyzer binary: CHJ/jchstac/chj_initialize | ||
| - **all:** `./full_make_no_gui.sh` | ||
| - analyzer/parser binaries: all of the above | ||
|
|
||
|
|
||
| ### Install dependencies and build: Ubuntu 16.04 or later (including gui) | ||
| <details> | ||
| <summary>Ubuntu 22.04+ and Debian 11+</summary> | ||
|
|
||
| ``` | ||
| sudo apt update -y | ||
| sudo apt install software-properties-common pkg-config m4 zlib1g-dev libgmp-dev liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev -y | ||
| sudo add-apt-repository ppa:avsm/ppa -y | ||
| sudo apt update -y | ||
| sudo apt install opam | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| opam init --bare --no-setup --disable-sandboxing | ||
| opam switch create codehawk-4.12.1 4.12.1 --no-switch | ||
| eval $(opam env --switch=codehawk-4.12.1 --set-switch) | ||
| opam install ocamlfind zarith camlzip extlib lablgtk lablgtk-extras goblint-cil | ||
| cd codehawk/CodeHawk | ||
| ./full_make.sh | ||
| sudo apt install --no-install-recommends \ | ||
| git ca-certificates \ | ||
| build-essential opam unzip default-jdk \ | ||
| pkg-config m4 zlib1g-dev libgmp-dev bubblewrap -y | ||
| ``` | ||
| </details> | ||
|
|
||
| # Building with shake | ||
|
|
||
| ### High-level process: | ||
|
|
||
| 1. Install dependencies | ||
| 2. Install the shake build system | ||
| 3. Install ocaml | ||
| 4. Build CodeHawk | ||
|
|
||
| The top-level dependencies needed to build CodeHawk are zlib for compression, the shake build | ||
| system, and the ocaml package manager (opam). In addition to the commands below, use the `opam` | ||
| setup above to get the dependencies. | ||
|
|
||
| ### Generic Unix | ||
|
|
||
| Other dependencies: `pkg-config`, `m4` | ||
| <details> | ||
| <summary>Fedora</summary> | ||
|
|
||
| ``` | ||
| sudo apt update -y | ||
| sudo apt install curl -y | ||
| curl -sSL https://get.haskellstack.org/ | sh | ||
| sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) | ||
| stack install shake | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| cd codehawk/CodeHawk | ||
| stack runghc Shakefile.hs | ||
| sudo yum install awk diffutils git gmp-devel opam \ | ||
| perl-ExtUtils-MakeMaker perl-FindBin perl-Pod-Html zlib-devel -y | ||
| ``` | ||
| </details> | ||
|
|
||
| ### Arch Linux | ||
|
|
||
| ``` | ||
| sudo pacman -Syu opam haskell-shake lablgtk2 | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| cd codehawk/CodeHawk | ||
| shake | ||
| ``` | ||
|
|
||
| ### Fedora | ||
| <details> | ||
| <summary>Arch Linux</summary> | ||
|
|
||
| ``` | ||
| sudo yum install opam shake ghc-compiler ghc-shake-devel diffutils zlib-devel ocaml-lablgtk-devel -y | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| cd codehawk/CodeHawk | ||
| shake | ||
| sudo pacman -Syu base-devel git opam | ||
| ``` | ||
| </details> | ||
|
|
||
| ### Homebrew | ||
| <details> | ||
| <summary>macOS</summary> | ||
|
|
||
| ``` | ||
| brew install opam | ||
| brew install cabal-install | ||
| brew install lablgtk | ||
| cabal update | ||
| cabal install --lib shake | ||
| cabal install --lib unordered-containers | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| cd codehawk/CodeHawk | ||
| ~/.cabal/bin/shake | ||
| ``` | ||
| </details> | ||
|
|
||
| ### MacPorts | ||
|
|
||
| ``` | ||
| sudo port install opam | ||
| sudo port install hs-cabal-install | ||
| sudo port install lablgtk2 | ||
| cabal update | ||
| cabal install --lib shake | ||
| cabal install --lib unordered-containers | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| cd codehawk/CodeHawk | ||
| ~/.cabal/bin/shake | ||
| ``` | ||
| # Build CodeHawk | ||
|
|
||
| ### Ubuntu 19.04 or later, Debian Buster or later | ||
| Note that on Ubuntu 24.04 you must also pass `--disable-sandboxing` to `opam init`, | ||
| or create an AppArmor profile with `userns` permissions. This is also required | ||
| if you are running in `docker` without `--privileged`. | ||
| [Yes, this is a mess!](https://github.com/containers/bubblewrap/issues/505#issuecomment-2093203129) | ||
|
|
||
| ``` | ||
| sudo apt update -y | ||
| sudo apt install cabal-install pkg-config m4 zlib1g-dev opam liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev -y | ||
| cabal update | ||
| cabal install shake | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| cd codehawk/CodeHawk | ||
| ~/.cabal/bin/shake | ||
| ``` | ||
|
|
||
| ### Ubuntu 16.04 or later | ||
| opam init --bare | ||
|
|
||
| ``` | ||
| sudo apt update -y | ||
| sudo apt install software-properties-common cabal-install pkg-config m4 zlib1g-dev liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev -y | ||
| sudo add-apt-repository ppa:avsm/ppa -y | ||
| sudo apt update -y | ||
| sudo apt install opam | ||
| cabal update | ||
| cabal install shake | ||
| git clone https://github.com/static-analysis-engineering/codehawk.git | ||
| cd codehawk/CodeHawk | ||
| ~/.cabal/bin/shake | ||
| ``` | ||
| opam switch create . 5.2.0 | ||
| eval $(opam env) | ||
| opam install dune ocamlfind zarith camlzip extlib goblint-cil.2.0.6 | ||
|
|
||
| ### Manually configured opam | ||
| dune build @install | ||
| ``` | ||
|
|
||
| Before the final "shake" command in one of the above instructions: | ||
| The Makefiles in the repository are to help CodeHawk's developers | ||
| debug circular module dependencies, they are not intended for users. | ||
|
|
||
| ``` | ||
| opam init --bare --no-setup --disable-sandboxing | ||
| opam switch create codehawk-4.12.1 4.09.0 --no-switch | ||
| eval $(opam env --switch=codehawk-4.12.1 --set-switch) | ||
| opam install ocamlfind zarith camlzip extlib lablgtk lablgtk-extras | ||
| /path/to/shake | ||
| ``` | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What makes it necessary to pin
goblint-cilat a specific version while leaving the others at arbitrary versions?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
goblint-cilhas released API-incompatible changes in point version bumps... I think three times in the last two years?CodeHawk's other dependencies have remained API-stable, so there is no particular reason to pin them.