Frama-C-discuss mailing list archives

Claude.Marche at inria.fr (Claude Marché) · Tue, 22 Aug 2017 09:52:52 +0200

Hi to all,

I forward this message from the Why list to the Frama-C list, in case
one has an answer.

It seems that the compilation of the Jessie plugin fails because some
strange interaction with the PathCrawler plugin. The log says:

# make -C frama-c-plugin depend
# make[1]: Entering directory
'/home/park11/.opam/4.03.0/build/why.2.38/frama-c-plugin'
# make[1]: Leaving directory
'/home/park11/.opam/4.03.0/build/why.2.38/frama-c-plugin'
# Makefile:684: recipe for target '.depend' failed
### stderr ###
# 1 shift/reduce conflict.
# Makefile:117: /home/park11/PathCrawler/Makefile.dynamic: No such file
or directory
# make[1]: *** No rule to make target
'/home/park11/PathCrawler/Makefile.dynamic'.  Stop.
# make: *** [.depend] Error 2

Any thought ?

A poor suggestion: deactivate/suppress the PathCrawler plugin to compile
Jessie, then reactivate/reinstall it afterwards

- Claude

Le 14/08/2017 Ã  22:45, Junkil Park a Ã©crit :
> Hi,
> 
> As I posted in my previous email, I had a problem with installing Jessie
> (why.2.38) on my Mac through opam. I still didn't resolve it. If anyone
> can help, I would appreciate it.
> 
> This time, I try to install why 2.38 through opam (Ocaml v 4.03.0) on my
> Ubuntu machine (16.04). But, it failed with the following error message:
> 
> The following actions will be performed:
>   âˆ—  install why 2.38
> 
> =-=- Gathering sources
> =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
> [why] Archive in cache
> 
> =-=- Processing actions
> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
> [ERROR] The compilation of why failed at "make".
> Processing  1/1: [why: rm]
> #=== ERROR while installing why.2.38
> ==========================================#
> # opam-version 1.2.2
> # os           linux
> # command      make
> # path         /home/park11/.opam/4.03.0/build/why.2.38
> # compiler     4.03.0
> # exit-code    2
> # env-file     /home/park11/.opam/4.03.0/build/why.2.38/why-32328-d2c37b.env
> # stdout-file  /home/park11/.opam/4.03.0/build/why.2.38/why-32328-d2c37b.out
> # stderr-file  /home/park11/.opam/4.03.0/build/why.2.38/why-32328-d2c37b.err
> ### stdout ###
> # [...]
> # printf "option=\"-R /home/park11/.opam/4.03.0/lib/why/coq Why\"\n" >>
> lib/why3/why3.conf
> # printf "\n"  >> lib/why3/why3.conf
> # printf "[editor_modifiers proofgeneral-coq]\n" >> lib/why3/why3.conf
> # printf "option=\"--eval \\\\\"(setq coq-load-path (cons
> '(\\\\\\\\\\\\\"/home/park11/.opam/4.03.0/lib/why/coq\\\\\\\\\\\\\"
> \\\\\\\\\\\\\"Why\\\\\\\\\\\\\") coq-load-path))\\\\\"\"\n"  >>
> lib/why3/why3.conf
> # rm -f .depend
> # ocamldep.opt -slash -I src -I jc -I java -I mix -I tools src/*.ml
> src/*.mli jc/*.mli jc/*.ml java/*.mli java/*.ml mix/*.mli mix/*.ml  >
> .depend
> # make -C frama-c-plugin depend
> # make[1]: Entering directory
> '/home/park11/.opam/4.03.0/build/why.2.38/frama-c-plugin'
> # make[1]: Leaving directory
> '/home/park11/.opam/4.03.0/build/why.2.38/frama-c-plugin'
> # Makefile:684: recipe for target '.depend' failed
> ### stderr ###
> # 1 shift/reduce conflict.
> # Makefile:117: /home/park11/PathCrawler/Makefile.dynamic: No such file
> or directory
> # make[1]: *** No rule to make target
> '/home/park11/PathCrawler/Makefile.dynamic'.  Stop.
> # make: *** [.depend] Error 2
> 
> 
> 
> =-=- Error report
> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
> The following actions failed
>   âˆ—  install why 2.38
> No changes have been performed
> 
> 
> Thanks,
> Junkil
> 
> 
>> On Aug 14, 2017, at 4:45 PM, Junkil Park <park11 at seas.upenn.edu
>> <mailto:park11 at seas.upenn.edu>> wrote:
>>
>> Hi,
>>
>> Thank you for your answer, Claude.
>>
>> First of all, the installation completed without error:
>> =-=- Processing actions
>> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  ðŸ«
>> âˆ—  installed why3-base.0.87.3
>> âˆ—  installed why3.0.87.3
>> âˆ—  installed frama-c-base.20161101
>> âˆ—  installed frama-c.20161101
>> âˆ—  installed why.2.38
>> Done.
>>
>>
>> Secondly, it seems that frama-c has options neither '-plugin-path' or
>> '-kernel-debug'. Instead, the 'plugins' option of frama-c shows the
>> list of plugins, which does not include Jessie. These are the only
>> files which name contain the keyword 'Jessie' in my opam system:
>> ~/.opam/4.05.0/bin/jessie
>> ~/.opam/4.05.0/bin/jessie.log
>> ~/.opam/4.05.0/lib/why/why3/jessie_why3.mlw
>> ~/.opam/4.05.0/lib/why/why3/jessie_why3theories.why
>>
>>
>> Lastly, I downloaded and unzip the source code of Why
>> from http://why.lri.fr/download/why-2.38.tar.gz, which contains the
>> folder 'frama-c-plugin'. However, I cannot find the 'frama-c-plugin'
>> folder and its files in my opam installation. Can this be a problem?
>>
>> BTW, I am doing this on my Mac.
>>
>> Thanks,
>> Junkil
>>
>>> On Aug 3, 2017, at 3:12 AM, Claude MarchÃ© <Claude.Marche at inria.fr
>>> <mailto:Claude.Marche at inria.fr>> wrote:
>>>
>>>
>>> Hi,
>>>
>>> Indeed 'opam install why' should do everything fine in one shot. You're
>>> not missing anything, so you should check whether installation went
>>> without error.
>>>
>>> To investigate the problem,  you should check whether the plugin code is
>>> at the right place, that is some Jessie.cmxs present in the `frama-c
>>> -plugin-path` Also option -kernel-debug might help.
>>>
>>> You should also consider asking for help on the Frama-C discuss list
>>>
>>> - Claude
>>>
>>>
>>>
>>> Le 31/07/2017 Ã  20:48, Junkil Park a Ã©crit :
>>>> Hi,
>>>>
>>>> To use the Jessie plugin of Frama-C, I installed
>>>> Frama-C(Silicon-20161101), Why(2.38), Why3(0.87.3) through opam
>>>> (ocaml v. 4.05.0).
>>>>
>>>> However, Frama-C cannot find the Jessie plugin, saying
>>>>
>>>>  [kernel] user error: option `-jessie' is unknown.
>>>>
>>>> How can I enable the Jessie plugin? Am I missing something?
>>>>
>>>> Thanks,
>>>> Junkil
>>>> _______________________________________________
>>>> Why-discuss mailing list
>>>> Why-discuss at lists.gforge.inria.fr
>>>> <mailto:Why-discuss at lists.gforge.inria.fr>
>>>> https://lists.gforge.inria.fr/mailman/listinfo/why-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/
>>> <http://www.lri.fr/%7Emarche/>
>>> F-91405 ORSAY Cedex                    |
>>> _______________________________________________
>>> Why-discuss mailing list
>>> Why-discuss at lists.gforge.inria.fr
>>> <mailto:Why-discuss at lists.gforge.inria.fr>
>>> https://lists.gforge.inria.fr/mailman/listinfo/why-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 archives

[Frama-c-discuss] [Why-discuss] Installing Jessie