installing Frama-C 22 beta on Ubuntu 20.04 fails

Thank you for submitting an issue to the Frama-C team. We propose the following template to ease the process. Please directly edit it inline to provide the required information.

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 BTS;
• you installed Frama-C as prescribed in the instructions.

Contextual information

• Frama-C installation mode: Opam
• Frama-C version: Frama-C version (as reported by frama-c -version) https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz
• Plug-in used: Plug-in used
• OS name: Xubuntu
• OS version: 20.04

Please add specific information deemed relevant with regard to this issue.

When installing Frama-C 22 (beta) I received the following error message

[ERROR] The compilation of frama-c failed at "/home/jens/.opam/opam-init/hooks/sandbox.sh build
        make -j7".

#=== ERROR while compiling frama-c.22.0-beta ==================================#
# context     2.0.5 | linux/x86_64 | ocaml-base-compiler.4.09.1 | pinned(https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz)
# path        ~/.opam/4.09.1/.opam-switch/build/frama-c.22.0-beta
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code   2
# env-file    ~/.opam/log/frama-c-1555-de8c6b.env
# output-file ~/.opam/log/frama-c-1555-de8c6b.out
### output ###
# [...]
# Ocamlopt     src/kernel_services/ast_data/alarms.cmx
# Ocamlopt     src/kernel_services/ast_data/statuses_by_call.cmx
# Ocamlopt     src/plugins/gui/gui_printers.cmx
# Ocamlopt     src/plugins/e-acsl/tests/print.cmx
# File "./src/plugins/wp/share/coqwp/Vlist.v", line 403, characters 8-11:
# Error:
# In nested Ltac calls to "lia" and "xlia (tactic)", last call failed.
# Tactic failure:  Cannot find witness.
# 
# Coqc         src/plugins/wp/share/coqwp/ArcTrigo.v
# make: *** [src/plugins/wp/share/Makefile.coqwp:39: src/plugins/wp/share/coqwp/Vlist.vo] Error 1
# make: *** Waiting for unfinished jobs....

Steps to reproduce the issue

Please indicate here steps to follow to get a minimal, complete, and verifiable example which reproduces the issue.

Here are my installation steps:

• opam init --yes --comp=4.09.1
• opam install --yes depext
• opam depext --yes frama-c
• opam install --yes alt-ergo why3
• opam install --yes why3-coq
• opam pin add --yes https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz

The final step failed with the message shown above

Thanks for the feedback. Could you in addition indicate which Coq version is installed on your side? If I recall correctly WP is now targeting Coq 8.12, and your report might indicate that the ./configure script should be more strict in checking this point.

It's 8.9.1. Sorry, I forgot to mention that I had pinned coq to 8.9.1 (which was necessary so far.)

opam pin add --yes coqide 8.9.1

I will try installing it with Coq 8.12. !

Now I have run into another issue

opam init
opam install --yes depext
opam depext --yes frama-c
opam install --yes alt-ergo why3 why3-coq coqide

I have encountered a failure after the last step. However, fortunately there was a message suggesting

The packages you requested declare the following system dependencies. Please make sure they are
installed before retrying:
    libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev

After I had manually installed them through apt (I wonder whether this couldn't be done by depext...), I was able to continue with

time opam install --yes frama-c

Configuring why3 also worked. But I haven't tested it yet.

Probably these dependencies were required by coqide for which you didn't ask for a depext. In fact, contrarily to Frama-C, whose GUI can use either lablgtk2 or lablgtk3 (but with some restrictions related to OCamlGraph), coqide is only lablgtk3-compliant. I guess that opam depext frama-c decided to install lablgtk2-related packages (I'm not sure there's a way to tell opam's solver to prefer a given path when there's an or-constraint where both sides are satisfiable).

Thanks for the update anyway. We'll update our configure script to check more thoroughly the coq version which is installed.

I figured out that when I proceed as follows, then Frama-C is apparently built using lablgtk3. The key seems to be run opam depext with both frama-c and coqide as arguments.

opam init
opam install --yes depext
opam depext --yes frama-c coqide
opam install --yes alt-ergo why3 why3-coq coqide
opam pin add --yes https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz

Thanks Jens for this feedback. I understand that there is an issue when using WP with Coq version 8.9, right? We need to fix it in the configuration.

For the dependencies on coqide, however, I don't see how we can improve the situation... do you?

We need to fix it in the configuration.

I'll test from 8.10 to 8.12 to set the minimal one.

Ok, 8.12 seems to be the minimal one. It is a bit sad since using only the Why3 backend we would probably be compatible with older versions.

A solution could be to deactivate the compilation of share/coqwp since I think it is not used for the why3 backend and only for the native-coq, deprecated output.

Maybe we could deactivate the compilation of the native backend when Coq is < 8.12, but in this case we should also display a message in Opam. I'll have a look at it.

I am not particular attached to coq 8.9.1 It is just the highest version I could use (install) with Scandium.

By the way, has native-coq already been disabled?

No, it benefits from a last suspension of sentence in this release. Native alt-ergo and coq support will be removed on next release in favor of the much more robust Why3 backend.

I think that for the lablgtk3 issue, we cannot do much more as it is just due to the way dependencies are managed by Opam. The message is moreover precise enough to fix the problem when it happens.

closed

marked this issue as related to #2548 (closed)

reopened