Did Sulfur support ocaml 4.06.1 on mac os x

[aogrcs]

Hi, my os x version is 10.13.3, opam is 1.2.2 and ocaml is 4.06.1. Following the instructions, there was an error:

The following actions will be performed:
  ∗  install why3-base 0.88.3                 [required by why3]
  ∗  install why3      0.88.3
       Coq realizations of Why3 theories are only available if Coq is installed
===== ∗  2 =====
Do you want to continue ? [Y/n] y

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[why3-base] Archive in cache

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[ERROR] The compilation of why3-base failed at "make -j4 all opt byte".
Processing  1/2: [why3-base: rm]
#=== ERROR while installing why3-base.0.88.3 ==================================#
# opam-version 1.2.2
# os           darwin
# command      make -j4 all opt byte
# path         /Users/wenlongxie/.opam/system/build/why3-base.0.88.3
# compiler     system (4.06.1)
# exit-code    2
# env-file     /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/why3-base-7673-e7966f.env
# stdout-file  /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/why3-base-7673-e7966f.out
# stderr-file  /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/why3-base-7673-e7966f.err
### stdout ###
# [...]
# Ocamlc   src/printer/simplify.mli
# Ocamlc   src/printer/gappa.mli
# Ocamlc   src/printer/cvc3.mli
# Ocamlc   src/whyml/mlw_main.mli
# Ocamlc   src/session/compress.mli
# Ocamlc   src/session/xml.mli
# Ocamlc   src/util/bigInt.ml
# Ocamlc   src/util/util.ml
# Ocamlc   src/util/opt.ml
# Ocamlc   src/util/lists.ml
### stderr ###
# [...]
# Warning: you are using the standard library and/or the %inline keyword. We
# recommend switching on --infer in order to avoid obscure type error messages.
# Warning: you are using the standard library and/or the %inline keyword. We
# recommend switching on --infer in order to avoid obscure type error messages.
# Warning: you are using the standard library and/or the %inline keyword. We
# recommend switching on --infer in order to avoid obscure type error messages.
# File "src/util/bigInt.ml", line 12, characters 5-12:
# Error: Unbound module Big_int
# make: *** [src/util/bigInt.cmo] Error 2
# make: *** Waiting for unfinished jobs....

=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
The following actions were aborted
  ∗  install why3 0.88.3
The following actions failed
  ∗  install why3-base 0.88.3
No changes have been performed

Has anyone tested for mac? Thanks! Sincerely

[maroneze]

(I edited your comment to put the terminal output inside a code block, to make it easier to read.)

There are regular tests performed on Mac, so in the worst case it should always be possible to compile Frama-C from source. When dependencies evolve, it is possible that opam will not be able to compile everything, but they are usually sorted quickly.

From your opam output, the issue is with why3 and not Frama-C itself, so you should probably seek for information over there.

If you don't intend to use the WP plug-in and do not need why3 at all, compiling Frama-C from source will work (only the why3 features will be disabled).

[vprevosto]

If you don't intend to use the WP plug-in and do not need why3 at all, compiling Frama-C from source will work (only the why3 features will be disabled).

As a matter of fact, Why3 is an optional dependency of Frama-C's opam package, which means that you can install Frama-C through opam without Why3, i.e. doing

opam install frama-c

should work regardless of whether Why3's package has been installed or not. Note however that in this case, as mentioned by @maroneze the only prover available to WP will be Alt-Ergo, for which WP has a native output.

[tantignac]

I just tried and I have not been able to reproduce the bug under macOS 10.13.4. Compilation of Why3 0.88.3 worked fine for me with spam 1.2.2 switched to OCaml 4.06.1.

[aogrcs]

I switched to ocaml 4.05, it worked! Thanks