Error: Unbound value Why3.Whyconf.load_default_config_if_needed

Before submitting the issue, please confirm (by adding a X in the [ ]):

• the issue has not yet been reported on Gitlab;
• the issue has not yet been reported on our old BTS (note: the old BTS is deprecated); (Can't tell; getting a database connection error)
• you installed Frama-C as prescribed in the instructions. (Not exactly; I'm building from source within a Dockerfile)

Contextual information

• Frama-C installation mode: from source
• Frama-C version: c4d10fb9
• Plug-in used: WP
• OS name: Debian Buster
• OS version: 20210326 (10.8)

Steps to reproduce the issue

Dockerfile:

FROM debian:buster-20210326 AS base

RUN apt update -y
RUN apt install -y gnupg2 wget apt-transport-https ca-certificates
RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add -
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN cat /etc/apt/sources.list
RUN apt update -y
RUN apt install -y clang-12 lld-12 grub-common ninja-build git libssl-dev libgmp-dev pkg-config make m4 unzip tar bzip2 gcc g++ autoconf zlib1g-dev time

RUN cc --version
RUN c++ --version

WORKDIR /opam
RUN wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
RUN echo "/opam" | sh install.sh --no-backup
ENV PATH="/opam:/opam/bin:${PATH}"
RUN opam --version
RUN time opam init -y --disable-sandboxing --jobs=1
RUN time opam install -y depext ocamlfind ocamlgraph zarith yojson why3.1.4.0 alt-ergo.2.4.0
ENV PATH="/root/.opam/default/bin:${PATH}"
RUN why3 --version
RUN why3 config detect

ARG FRAMAC_REF=c4d10fb975d443e3c40289843fae89c424b54e63
WORKDIR /framac
RUN git init .
RUN git remote add origin https://git.frama-c.com/pub/frama-c.git
RUN git fetch origin ${FRAMAC_REF}
RUN git checkout ${FRAMAC_REF}
RUN autoconf
RUN ./configure
RUN make -j4
RUN make install
RUN frama-c --version; echo

Expected behaviour

Should build to completion.

Actual behaviour

File "src/plugins/wp/Why3Provers.ml", line 31, characters 19-61:
31 |       let config = Why3.Whyconf.load_default_config_if_needed config in
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Whyconf.load_default_config_if_needed
make: *** [share/Makefile.generic:78: src/plugins/wp/Why3Provers.cmo] Error 2
make: *** Waiting for unfinished jobs....
The command '/bin/sh -c make -j4' returned a non-zero code: 2

---

Some context: Trying to verify a new toy OS and having a bunch of issues since I can't use the standard C library that ships with Frama-C (as there is no C library available in this environment) so I've ended up copying the axiomatic clauses from the __fc_xxx.h headers directly.

I saw on StackOverflow that a few bugs that seemed to be affecting me were recently patched on master but not yet released, so I spun up a Dockerfile in order to try to see if any of the verification could be fixed by trying it with the latest head.

However, it doesn't seem to be working - much less getting even simple programs to verify correctly :/ Hence why I'm trying to update everything to latest to see if I can't get any verification to work.

Anyway this is the latest issue I've hit trying to get everything up to date.

Note that there is a lot of stuff in there that isn't directly related to this bug - this is a stripped down Dockerfile, and there is a bunch of extra stuff that comes after this step that I removed to keep things small.

changed the description

added confirmed wp labels

Frama-C is indeed not compatible with Why3 1.4.0 as of now. You should stick to why3.1.3.3 and alt-ergo.2.2.0 in the opam install of your Dockerfile (or use frama-c/frama-c on Dockerhub, where the tag dev should give you the latest commit on master here).

For future information, the frama-c opam package description contains some constraints which might provide hints, for instance, it currently contains:

"why3" { >= "1.3.3" & < "1.4~" }

Which indicates that, actually, Why3 1.3.3 is the only version compatible with the current development version (1.4 should be made compatible soon).

Also, looking at your Dockerfile, I have some minor recommendations:

1. Adding rsync to the list of installed Debian packages; it is used by opam and, as far as I know, very small (< 1 MB);

2. You could try doing opam pin to locally add frama-c as a package, so that you can at least run opam install --deps-only frama-c. This asks opam to compute the required dependencies, including any version constraints. It should help minimize issues. Also, another useful command might be opam depext frama-c, which will help identify useful Debian packages.

For instance, I tried the following with your Dockerfile (after installing rsync):

RUN git checkout ${FRAMAC_REF}
RUN opam pin add frama-c . -k path --no-action # locally configure a 'frama-c' package using the checked out version
RUN opam install --deps-only frama-c -y # ask opam to compute dependencies for OCaml packages and install them
RUN opam depext -y frama-c # ask opam to compute and install Debian dependencies

The opam install line will prompt for downgrading the why3 package:

The following actions will be performed:
  - downgrade why3               1.4.0 to 1.3.3

This can help debug other issues if you find them later. It is not foolproof, but may help.

Regarding the Frama-C libc issues with WP, you may consider trying to discuss it on our Mattermost (https://mattermost.frama-c.com/frama-c/channels/town-square). You can login via Gitlab. There's not much traffic there currently, but it offers a way to ask questions and get feedback.

marked this issue as related to #40 (closed)