Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Installing Frama-c from https://git.frama-c.com/pub/frama-c.git

Hello,

Le 01/05/2020 à 11:31, Gerlach, Jens a écrit :
> Feeling somewhat adventurous I tried to install Frama-C from the public git repository.
> 
> I used the following steps for a clean install under xubuntu-19.10 after removing .opam
> 
> opam init --yes --comp=4.06.1
> opam install --yes depext
> opam depext frama-c
> opam pin add frama-c https://git.frama-c.com/pub/frama-c.git
>   
> Unfortunately, I received the error message below.
> What should I do to be able to install Frama-C from this source?

Reading the error log below, the issue lies most likely, in the fact that 
opam did install the recently released why3 1.3, while Frama-C is still 
relying on why3 1.2 (and sadly the opam file was not updated at the time of 
Why3 new release to reflect that). opam pin add why3 1.2.1 shoud take care 
of that.

> A followup question is: What is the relationship between Frama-C 20.0 (released in December 2019) and this git version?
> Is it closer to Frama-C 21 or Frama-C 20?
> 

The git version is pulled each day from the master branch of the internal 
Frama-C repository. It is thus much closer to Frama-C 21 than to Frama-C 20.

> 
> #=== ERROR while compiling frama-c.20.0 =======================================#
> # context     2.0.5 | linux/x86_64 | ocaml-base-compiler.4.06.1 | pinned(git+https://git.frama-c.com/pub/frama-c.git#92419510)
> # path        ~/.opam/4.06.1/.opam-switch/build/frama-c.20.0
> # command     ~/.opam/opam-init/hooks/sandbox.sh build make -j7
> # exit-code   2
> # env-file    ~/.opam/log/frama-c-14780-e4db2f.env
> # output-file ~/.opam/log/frama-c-14780-e4db2f.out
> ### output ###
> # [...]
> # Ocamlc       src/plugins/wp/cfgWP.cmi
> # Ocamlopt     src/kernel_internals/parsing/logic_lexer.cmx
> # Ocamlc       src/plugins/wp/TacSplit.cmo
> # Ocamlc       src/plugins/wp/TacChoice.cmo
> # Ocamlc       src/plugins/wp/TacRange.cmo
> # Ocamlc       src/plugins/wp/TacArray.cmo
> # Ocamlc       src/plugins/wp/TacCompound.cmo
> # Ocamlc       src/plugins/wp/TacUnfold.cmo
> # File "src/plugins/wp/ProverWhy3.ml", line 259, characters 31-47:
> # Error: Unbound value const_of_big_int
> # make: *** [share/Makefile.generic:78: src/plugins/wp/ProverWhy3.cmo] Error 2
> # make: *** Waiting for unfinished jobs....


Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile