2021-03-03 04:06 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002331Frama-CKernel > Makefilepublic2017-12-06 09:10
Reporterseberoon 
Assigned Tobobot 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformmacOSmac osOS Version10.11.6
Product VersionFrama-C 15-Phosphorus 
Target VersionFixed in VersionFrama-C 16-Sulfur 
Summary0002331: opam installation of frama-c-base fails
DescriptionFollowing opam installation instructions at https://frama-c.com/install-phosphorus-20170501.html#installing-frama-c-on-mac-os-x.

All ok up until opam install frama-c-base, which fails:

# File "src/plugins/wp/qed/src/numbers.mll", line 131, characters 18-19:
# Error: This expression has type string but an expression was expected of type
# bytes

This is using a fresh installation of homebrew and opam.
Additional InformationMac OS 10.11.6
Xcode 8.2.1
TagsNo tags attached.
Attached Files
  • txt file icon frama-c_install_fail.txt (2,270 bytes) 2017-11-07 19:12 -
    pflap845085:~ seb$ opam install frama-c-base
    The following actions will be performed:
      ∗  install frama-c-base 20170501
           Why3 can be used by the WP plug-in for running additional automatic solvers
           Coq can be used with the WP plug-in for proving interactively proof obligations
    
    =-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
    [frama-c-base] Archive in cache
    
    =-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
    [ERROR] The compilation of frama-c-base failed at "make -j4".
    Processing  1/1: [frama-c-base: rm]
    #=== ERROR while installing frama-c-base.20170501 =============================#
    # opam-version 1.2.2
    # os           darwin
    # command      make -j4
    # path         /Users/seb/.opam/system/build/frama-c-base.20170501
    # compiler     system (4.06.0)
    # exit-code    2
    # env-file     /Users/seb/.opam/system/build/frama-c-base.20170501/frama-c-base-54084-c61e7b.env
    # stdout-file  /Users/seb/.opam/system/build/frama-c-base.20170501/frama-c-base-54084-c61e7b.out
    # stderr-file  /Users/seb/.opam/system/build/frama-c-base.20170501/frama-c-base-54084-c61e7b.err
    ### stdout ###
    # [...]
    # Ocamlc       src/libraries/stdlib/transitioning.cmo
    # Ocamlc       src/libraries/stdlib/FCSet.cmo
    # Ocamlc       src/libraries/stdlib/FCMap.cmo
    # Ocamlc       src/libraries/stdlib/FCBuffer.cmi
    # Ocamlc       src/libraries/stdlib/FCHashtbl.cmo
    # Ocamlc       src/libraries/stdlib/extlib.cmo
    # Ocamlc       src/libraries/datatype/unmarshal.cmo
    # Ocamlc       src/libraries/datatype/unmarshal_z.cmi
    # Ocamlc       src/libraries/utils/pretty_utils.cmo
    # Ocamlc       src/libraries/utils/hook.cmo
    ### stderr ###
    # 4 shift/reduce conflicts.
    # 7 shift/reduce conflicts.
    # File "src/plugins/wp/qed/src/numbers.mll", line 131, characters 18-19:
    # Error: This expression has type string but an expression was expected of type
    #          bytes
    # make[1]: *** [numbers.cmo] Error 2
    # make[1]: *** Waiting for unfinished jobs....
    # make: *** [src/plugins/wp/qed/bin/Qed.cmo] Error 2
    # make: *** Waiting for unfinished jobs....
    
    
    
    =-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
    The following actions failed
      ∗  install frama-c-base 20170501
    No changes have been performed
    
    txt file icon frama-c_install_fail.txt (2,270 bytes) 2017-11-07 19:12 +

-Relationships
+Relationships

-Notes

~0006470

virgile (developer)

You're presumably using opam switch 4.06.0 (i.e. the recently released OCaml version). The current Frama-C Phosphorus is indeed not compatible with this switch, and the opam package has just been updated to reflect that. Frama-C Sulfur will be, but it is not officially released yet. If everything goes according to plan, this should be done by the end of the month.

If you do not want to wait until then, there are two possibilities:

- you can try the beta version at https://github.com/Frama-C/Frama-C-snapshot/wiki/Frama-C-Sulfur-20171101-beta (note that you'll need to install opam base-num package that was provided directly within the compiler until 4.06.0 in order to have Frama-C compile)

- or you can use the 4.05.0 switch of opam. 4.05.0 was the latest release by the time Phosphorus came out.
+Notes

-Issue History
Date Modified Username Field Change
2017-11-07 19:12 seberoon New Issue
2017-11-07 19:12 seberoon Status new => assigned
2017-11-07 19:12 seberoon Assigned To => bobot
2017-11-07 19:12 seberoon File Added: frama-c_install_fail.txt
2017-11-08 09:00 virgile Note Added: 0006470
2017-11-08 09:00 virgile Status assigned => resolved
2017-11-08 09:00 virgile Resolution open => fixed
2017-12-06 09:09 signoles Fixed in Version => Frama-C 16-Sulfur
2017-12-06 09:10 signoles Status resolved => closed
+Issue History