AstraVer Toolset » Deductive Verification Tools for Linux Kernel

Jessie2 throws an error during the installation process if the system already has the coq,coqide installed from opam.

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of jessie2 failed at "make -j 1".

#=== ERROR while installing jessie2.alpha2 ====================================#
# opam-version 1.2.2
# os           linux
# command      make -j 1
# path         /home/user/.opam/4.03.0/build/jessie2.alpha2
# compiler     4.03.0
# exit-code    2
# env-file     /home/user/.opam/4.03.0/build/jessie2.alpha2/jessie2-4867-6d07ae.env
# stdout-file  /home/user/.opam/4.03.0/build/jessie2.alpha2/jessie2-4867-6d07ae.out
# stderr-file  /home/user/.opam/4.03.0/build/jessie2.alpha2/jessie2-4867-6d07ae.err
### stdout ###
# [...]
# rm -f jc.cm*
# touch _build/src/jc/jc.cmxa
# if [ -f jc_main.native ]; then mv jc_main.native bin/jessie.opt; fi
# touch bin/jessie.opt
# make -C lib/coq
# make[1]: Entering directory '/home/user/.opam/4.03.0/build/jessie2.alpha2/lib/coq'
# coqc -R /home/user/.opam/4.03.0/lib/why3/coq Why3 -R . Jessie Jessie_pointer.v
# Makefile:7: recipe for target 'Jessie_pointer.vo' failed
# make[1]: Leaving directory '/home/user/.opam/4.03.0/build/jessie2.alpha2/lib/coq'
# Makefile:330: recipe for target 'lib/coq/Jessie_pointer.vo' failed
### stderr ###
# Warning: Cannot open /home/user/.opam/4.03.0/lib/why3/coq
# [cannot-open-path,filesystem]
# File "./Jessie_pointer.v", line 3, characters 15-22:
# Error: Unable to locate library BuiltIn.
# make[1]: *** [Jessie_pointer.vo] Error 1
# make: *** [lib/coq/Jessie_pointer.vo] Error 2