--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2020 ---
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