diff --git a/INSTALL.md b/INSTALL.md index 98a063f8c016b787e8b4d853e65d9d8df245887e..b4f5c160edcb2817c9144e4ac395196d92105a94 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -89,22 +89,10 @@ Why3 must be configured to make them available for Frama-C/WP: why3 config --detect ``` -### Known working configuration - -The following set of packages is known to be a working configuration for -Frama-C 21 (Scandium): - -- OCaml 4.07.1 -- ocamlfind.1.8.0 -- apron.v0.9.12 (optional) -- lablgtk.2.18.10 | lablgtk3.3.0.beta6 + lablgtk3-sourceview3.3.0.beta6 -- mlgmpidl.1.2.12 (optional) -- ocamlgraph.1.8.8 -- why3.1.2.1 -- alt-ergo.2.0.0 (for wp, optional) -- yojson.1.7.0 -- zarith.1.9.1 -- zmq.5.1.3 (for server, optional) +### Reference configuration + +See file [reference-configuration.md](reference-configuration.md) +for a set of packages that is known to work with Frama-C 21 (Scandium). ### Installing Custom Versions of Frama-C diff --git a/bin/check-reference-configuration.sh b/bin/check-reference-configuration.sh new file mode 100755 index 0000000000000000000000000000000000000000..2e18397b47adcaf77edd010754e5fbae320695f8 --- /dev/null +++ b/bin/check-reference-configuration.sh @@ -0,0 +1,80 @@ +#!/bin/bash -eu + +# Displays the current working configuration of OCaml dependencies of Frama-C, +# comparing them with the one in `reference-configuration.md`. + +if ! type "opam" > /dev/null; then + opam="NOT" +else + opam="$(opam --version)" +fi + +if ! type "ocaml" > /dev/null; then + ocaml="NOT" +else + ocaml=$(ocaml -vnum) +fi + +version_via_opam() { + v=$(opam info -f installed-version "$1" 2>/dev/null) + if [ "$v" = "" -o "$v" = "--" ]; then + echo "NOT" + else + echo $v + fi +} + +version_via_ocamlfind() { + v=$(ocamlfind query -format "$1" 2>/dev/null) + if [ "$v" = "" ]; then + echo "NOT" + else + echo $v + fi +} + +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" +refconf="$SCRIPT_DIR/../reference-configuration.md" + +packages=$(grep '^- [^ ]*\.' "$refconf" | sed 's/^- //' | sed 's/ .*//') + +bold=$(tput bold) +normal=$(tput sgr0) + +has_any_diffs=0 +# Check OCaml version separately (not same syntax as the packages) +working_ocaml=$(grep "\- OCaml " "$refconf" | sed 's/.*OCaml //') +if [ "$working_ocaml" != "$ocaml" ]; then + echo -n "warning: OCaml ${bold}${ocaml}${normal} installed, " + echo "expected ${bold}${working_ocaml}${normal}" + has_any_diffs=1 +fi + +all_packages="" +for package in $packages; do + name=${package%%.*} + all_packages+=" $package" + working_version=$(echo $package | sed 's/^[^.]*\.//') + if [ "$opam" != "NOT" ]; then + actual_version=$(version_via_opam $name) + elif [ "$ocamlfind" != "NOT" ]; then + actual_version=$(version_via_ocamlfind $name) + else + echo "error: neither opam nor ocamlfind found." + exit 1 + fi + if [ "$working_version" != "$actual_version" ]; then + has_any_diffs=1 + echo -n "warning: $name ${bold}${actual_version}${normal} installed, " + echo "expected ${bold}${working_version}${normal}" + fi +done + +echo "All packages checked." +if [ $has_any_diffs -ne 0 ]; then + echo "Useful commands:" + echo " opam switch create ${working_ocaml}" + echo " opam install depext" + echo " opam depext --install$all_packages" + echo " rm -f ~/.why3.conf && why3 config --full-config" +fi diff --git a/reference-configuration.md b/reference-configuration.md new file mode 100644 index 0000000000000000000000000000000000000000..4924e5ebc07ff2fce10e9a8b86ceedf958fdee05 --- /dev/null +++ b/reference-configuration.md @@ -0,0 +1,20 @@ +The following set of packages is known to be a working configuration for +compiling Frama-C 21 (Scandium), on a machine with gcc <= 9[^gcc-10] + +- OCaml 4.07.1 +- ocamlfind.1.8.0 +- apron.v0.9.12 (optional) +- lablgtk.2.18.10 | lablgtk3.3.0.beta6 + lablgtk3-sourceview3.3.0.beta6 +- mlgmpidl.1.2.12 (optional) +- ocamlgraph.1.8.8 +- why3.1.3.1 +- alt-ergo.2.0.0 (for wp, optional) +- yojson.1.7.0 +- zarith.1.9.1 +- zmq.5.1.3 (for server, optional) + +[^gcc-10]: As mentioned in this [OCaml PR](https://github.com/ocaml/ocaml/issues/9144) +gcc 10 changed its default linking conventions to make them more stringent, +resulting in various linking issues. In particular, only OCaml 4.10 can be +linked against gcc-10. With respect to the list above, this also means using +ocamlfind.1.8.1 and the development version of lablgtk (https://github.com/garrigue/lablgtk) \ No newline at end of file