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] [PROVENANCE INTERNET] Re: [Why-discuss] Installing Jessie

It seems that something has been changed.

~/D/why-2.38 ❯❯❯ autoconf
~/D/why-2.38 ❯❯❯ ./configure
checking for ocamlc... ocamlc
ocaml version is 4.03.0
ocaml library path is /Users/david/.opam/4.03.0/lib/ocaml
checking for ocamlfind... yes
checking OS dependent settings... Unix
checking for ocamlopt... ocamlopt
checking ocamlopt version... ok
checking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version... ok
checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version... ok
checking for ocamldep... ocamldep
checking for ocamldep.opt... ocamldep.opt
checking for ocamllex... ocamllex
checking for ocamllex.opt... ocamllex.opt
checking for ocamlyacc... ocamlyacc
checking for ocamldoc... ocamldoc
checking for ocamldoc.opt... ocamldoc.opt
ocamlfind found ocamlgraph in /Users/david/.opam/4.03.0/lib/ocamlgraph
checking for ocamlweb... true
checking for frama-c... /Users/david/.opam/4.03.0/bin/frama-c
checking Frama-c version... Silicon-20161101
checking for why3... /Users/david/.opam/4.03.0/bin/why3
checking Why3 version...
configure: WARNING: unknown version , hope this works
checking for coqc... no
configure: WARNING: Cannot find coqc.
checking for pvs... no
configure: WARNING: Cannot find PVS.
configure: creating ./config.status
config.status: creating Makefile

                 Summary
-----------------------------------------
OCaml version            : 4.03.0
OCaml library path       : /Users/david/.opam/4.03.0/lib/ocaml
OcamlGraph lib           : found by ocamlfind
Verbose make             : no
Inference of annotations : no
Why3 support             : yes
    Binary               : /Users/david/.opam/4.03.0/bin/why3
    Version              :
    unknown version , hope this works
Frama-C plugin           : yes
    Binary               : /Users/david/.opam/4.03.0/bin/frama-c
    Version              : Silicon-20161101
Coq support (via Why3)   : no
    command 'coqc' not found
PVS support (via Why3)   : no
    command 'pvs' not found
Other provers support    : (via Why3)

Thanks,
Junkil

> On Aug 22, 2017, at 5:23 AM, Claude Marché <Claude.Marche at inria.fr> wrote:
> 
> 
> I see, I guess the 'sed' command used to parse the answer does not work
> on Mac, maybe because now there is no newline anymore at the end,
> something like that
> 
> So a possible workaround : edit the configure.in file, find the first
> occurence of Silicon in it, then replace the line above
> 
> FRAMACVERSION=`$FRAMAC -version | sed -n -e 's|\(Version:
> \)\?\(.*\)$|\2|p' `
> 
> by
> 
> FRAMACVERSION=`$FRAMAC -version`
> 
> then
> 
> autoconf
> ./configure
> 
> 
> If autoconf does not work for you, then you should do the modification
> directly in the file 'configure' instead
> 
> - Claude
> 
> 
> 
> 
> Le 22/08/2017 à 11:14, Junkil “David” Park a écrit :
>> ❯❯ frama-c --version
>> Silicon-20161101%
>> 
>> Thanks,
>> Junkil
>> 
>>> On Aug 22, 2017, at 5:13 AM, Claude Marché <Claude.Marche at inria.fr> wrote:
>>> 
>>> 
>>> 
>>> Le 22/08/2017 à 10:53, Junkil “David” Park a écrit :
>>>> checking Frama-c version...
>>>> configure: WARNING: bad Frama-c version "", you need version Silicon
>>> 
>>> there's a bug here... what is the answer of
>>> 
>>> frama-c --version
>>> 
>>> ?
>>> 
>>> -- 
>>> Claude Marché                          | tel: +33 1 69 15 66 08
>>> INRIA Saclay - ÃŽle-de-France           |
>>> Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
>>> F-91405 ORSAY Cedex                    |
>>> _______________________________________________
>>> Frama-c-discuss mailing list
>>> Frama-c-discuss at lists.gforge.inria.fr
>>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>> 
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>> 
> 
> -- 
> Claude Marché                          | tel: +33 1 69 15 66 08
> INRIA Saclay - ÃŽle-de-France           |
> Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex                    |
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss