Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

[wenlong xie]

Hi, Jens
I switched to ocaml 4.05.0, it worked. Thanks!
BTW, someone compiled why3 0.88.3 using ocaml 4.06.1 on macos 10.13.4
successfully. If I updated the os, then I would test it!
Sincerely

2018-04-17 8:58 GMT+08:00 wenlong xie :

> Hi, may it be 4.06.1, thanks for your remind, I check it later!
> Sincerely!
>
> 2018-04-16 21:53 GMT+08:00 Gerlach, Jens  >:
>
>> Hello,
>>
>> I am using why3 0.88.3 without problems on my Mac(s).
>> I remember that there was an issue with ocaml which made it necessary to
>> resort to ocaml version 4.05.0.
>> Which version of ocaml are you using?
>>
>> Regards
>>
>> Jens
>>
>> ___
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>>
>
>
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

[wenlong xie]

Hi, may it be 4.06.1, thanks for your remind, I check it later!
Sincerely!

2018-04-16 21:53 GMT+08:00 Gerlach, Jens :

> Hello,
>
> I am using why3 0.88.3 without problems on my Mac(s).
> I remember that there was an issue with ocaml which made it necessary to
> resort to ocaml version 4.05.0.
> Which version of ocaml are you using?
>
> Regards
>
> Jens
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

[Gerlach, Jens]

Hello,

I am using why3 0.88.3 without problems on my Mac(s).
I remember that there was an issue with ocaml which made it necessary to resort 
to ocaml version 4.05.0.
Which version of ocaml are you using?

Regards

Jens

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

[wenlong xie]

Hi, I have tried both  opam depext conf-pkg-config and  export
PKG_CONFIG_PATH=/usr/local/lib/pkgconfig:/usr/local/opt/
libxml2/lib/pkgconfig:/opt/X11/lib/pkgconfig:$PKG_CONFIG_PATH, but there is
still an error as following:

opam install why3
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-code2
# env-file /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/
why3-base-8811-e7966f.env
# stdout-file  /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/
why3-base-8811-e7966f.out
# stderr-file  /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/
why3-base-8811-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

thanks, sincerely

2018-04-13 15:46 GMT+08:00 Alix TRIEU :

> opam depext conf-pkg-config
>
> may be worth a try too.
>
> Alix
>
> On Fri, Apr 13, 2018 at 8:34 AM Alan Schmitt  org> wrote:
>
>> On 2018-04-12 19:12, Virgile Prevosto  writes:
>>
>> > 2018-04-12 18:36 GMT+02:00 wenlong xie :
>> >>
>> >>
>> >> [conf-gtksourceview: pkg-config gtksourceview-2.0] Command started
>> >> + pkg-config "--short-errors" "--print-errors" "gtksourceview-2.0"
>> >> (CWD=/Users/wenlongxie/.opam/system/build/conf-gtksourceview.2)
>> >> [ERROR] The compilation of conf-gtksourceview failed at "pkg-config
>> >> --short-errors --print-errors gtksourceview-2.0".
>> >>
>> >> #=== ERROR while installing conf-gtksourceview.2
>> ==#
>> >> # opam-version 1.2.2
>> >> # os   darwin
>> >> # command  pkg-config --short-errors --print-errors
>> gtksourceview-2.0
>> >> # path /Users/wenlongxie/.opam/system/build/conf-
>> gtksourceview.2
>> >> # compiler system (4.06.1)
>> >> # exit-code127
>> >
>> > Thanks for the update. As I was suspecting, it seems like pkg-config
>> > is not installed on your machine (under POSIX, 127 is the shell's
>> > error code when it does not find the executable it is asked to
>> > launch). It is quite surprising, as this is a fairly standard command
>> > for any gtk-based library, and I'd have thought that brew would have
>> > installed it together with the rest. Could you check whether there's a
>> > brew package called pkg-config or something similar and if yes,
>> > whether installing it through brew solve your issue? Otherwise, I'm
>> > afraid you'll need help from someone who actually has a Mac on which
>> > they can reproduce the issue.
>>
>> I've had similar issues before, and I have this in my shell profile:
>>
>> export PKG_CONFIG_PATH=/usr/local/lib/pkgconfig:/usr/local/opt/
>> libxml2/lib/pkgconfig:/opt/X11/lib/pkgconfig:$PKG_CONFIG_PATH
>>
>> You could give it a try.
>>
>> Best,
>>
>> Alan
>>
>> --
>> OpenPGP Key ID : 040D0A3B4ED2E5C7
>> Monthly Athmospheric CO₂, Mauna Loa Obs. 2018-03: 409.46, 2017-03: 407.18
>> ___
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

[Alix TRIEU]

opam depext conf-pkg-config

may be worth a try too.

Alix

On Fri, Apr 13, 2018 at 8:34 AM Alan Schmitt 
wrote:

> On 2018-04-12 19:12, Virgile Prevosto  writes:
>
> > 2018-04-12 18:36 GMT+02:00 wenlong xie :
> >>
> >>
> >> [conf-gtksourceview: pkg-config gtksourceview-2.0] Command started
> >> + pkg-config "--short-errors" "--print-errors" "gtksourceview-2.0"
> >> (CWD=/Users/wenlongxie/.opam/system/build/conf-gtksourceview.2)
> >> [ERROR] The compilation of conf-gtksourceview failed at "pkg-config
> >> --short-errors --print-errors gtksourceview-2.0".
> >>
> >> #=== ERROR while installing conf-gtksourceview.2
> ==#
> >> # opam-version 1.2.2
> >> # os   darwin
> >> # command  pkg-config --short-errors --print-errors
> gtksourceview-2.0
> >> # path /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2
> >> # compiler system (4.06.1)
> >> # exit-code127
> >
> > Thanks for the update. As I was suspecting, it seems like pkg-config
> > is not installed on your machine (under POSIX, 127 is the shell's
> > error code when it does not find the executable it is asked to
> > launch). It is quite surprising, as this is a fairly standard command
> > for any gtk-based library, and I'd have thought that brew would have
> > installed it together with the rest. Could you check whether there's a
> > brew package called pkg-config or something similar and if yes,
> > whether installing it through brew solve your issue? Otherwise, I'm
> > afraid you'll need help from someone who actually has a Mac on which
> > they can reproduce the issue.
>
> I've had similar issues before, and I have this in my shell profile:
>
> export
> PKG_CONFIG_PATH=/usr/local/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/opt/X11/lib/pkgconfig:$PKG_CONFIG_PATH
>
> You could give it a try.
>
> Best,
>
> Alan
>
> --
> OpenPGP Key ID : 040D0A3B4ED2E5C7
> Monthly Athmospheric CO₂, Mauna Loa Obs. 2018-03: 409.46, 2017-03: 407.18
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

[Alan Schmitt]

On 2018-04-12 19:12, Virgile Prevosto  writes:

> 2018-04-12 18:36 GMT+02:00 wenlong xie :
>>
>>
>> [conf-gtksourceview: pkg-config gtksourceview-2.0] Command started
>> + pkg-config "--short-errors" "--print-errors" "gtksourceview-2.0"
>> (CWD=/Users/wenlongxie/.opam/system/build/conf-gtksourceview.2)
>> [ERROR] The compilation of conf-gtksourceview failed at "pkg-config
>> --short-errors --print-errors gtksourceview-2.0".
>>
>> #=== ERROR while installing conf-gtksourceview.2 
>> ==#
>> # opam-version 1.2.2
>> # os   darwin
>> # command  pkg-config --short-errors --print-errors gtksourceview-2.0
>> # path /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2
>> # compiler system (4.06.1)
>> # exit-code127
>
> Thanks for the update. As I was suspecting, it seems like pkg-config
> is not installed on your machine (under POSIX, 127 is the shell's
> error code when it does not find the executable it is asked to
> launch). It is quite surprising, as this is a fairly standard command
> for any gtk-based library, and I'd have thought that brew would have
> installed it together with the rest. Could you check whether there's a
> brew package called pkg-config or something similar and if yes,
> whether installing it through brew solve your issue? Otherwise, I'm
> afraid you'll need help from someone who actually has a Mac on which
> they can reproduce the issue.

I've had similar issues before, and I have this in my shell profile:

export 
PKG_CONFIG_PATH=/usr/local/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/opt/X11/lib/pkgconfig:$PKG_CONFIG_PATH

You could give it a try.

Best,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2018-03: 409.46, 2017-03: 407.18


signature.asc
Description: PGP signature
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

[Virgile Prevosto]

2018-04-12 18:36 GMT+02:00 wenlong xie :
>
>
> [conf-gtksourceview: pkg-config gtksourceview-2.0] Command started
> + pkg-config "--short-errors" "--print-errors" "gtksourceview-2.0" 
> (CWD=/Users/wenlongxie/.opam/system/build/conf-gtksourceview.2)
> [ERROR] The compilation of conf-gtksourceview failed at "pkg-config 
> --short-errors --print-errors gtksourceview-2.0".
>
> #=== ERROR while installing conf-gtksourceview.2 
> ==#
> # opam-version 1.2.2
> # os   darwin
> # command  pkg-config --short-errors --print-errors gtksourceview-2.0
> # path /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2
> # compiler system (4.06.1)
> # exit-code127

Thanks for the update. As I was suspecting, it seems like pkg-config
is not installed on your machine (under POSIX, 127 is the shell's
error code when it does not find the executable it is asked to
launch). It is quite surprising, as this is a fairly standard command
for any gtk-based library, and I'd have thought that brew would have
installed it together with the rest. Could you check whether there's a
brew package called pkg-config or something similar and if yes,
whether installing it through brew solve your issue? Otherwise, I'm
afraid you'll need help from someone who actually has a Mac on which
they can reproduce the issue.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

[Virgile Prevosto]

Hello,

As I asked on the issue you opened on Frama-C's bts yesterday (
https://bts.frama-c.com/view.php?id=2373) for the exact same problem: did
you try the suggestion offered by opam, i.e.
launching opam depext conf-gtksourceview.2? There is apparently an issue
with the way gtksourceview was installed on your system (which should have
been done by the line
brew install gmp gtk+ gtksourceview libgnomecanvas according to the
installation you link to). Note that this implies that you have install
depext with opam install depext before.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club