Why3 0.81 is broken - Githubissues

protz commented 11 years ago

I recently uploaded a why3-0.80 package which compiled fine, but the 0.81 version doesn't work anymore.

=-=-= Installing why3.0.81 =-=-=
Downloading http://opam.ocamlpro.com/archives/why3.0.81+opam.tar.gz.
Extracting /home/jonathan/.opam/archives/why3.0.81+opam.tar.gz.
Applying configure.patch.
Building why3.0.81:
  ./configure --prefix /home/nas/gallium/protzenk/.opam/4.00.1 --sbindir=/home/nas/gallium/protzenk/.opam/4.00.1/lib/why3/sbin --libexecdir=/home/nas/gallium/protzenk/.opam/4.00.1/lib/why3/libexec --sysconfdir=/home/nas/gallium/protzenk/.opam/4.00.1/lib/why3/etc --sharedstatedir=/home/nas/gallium/protzenk/.opam/4.00.1/lib/why3/com --localstatedir=/home/nas/gallium/protzenk/.opam/4.00.1/lib/why3/var --libdir=/home/nas/gallium/protzenk/.opam/4.00.1/lib/why3/lib --includedir=/home/nas/gallium/protzenk/.opam/4.00.1/lib/why3/include --datarootdir=/home/nas/gallium/protzenk/.opam/4.00.1/lib/why3/share --disable-bench
  make opt byte
  make install install-lib
The compilation of why3.0.81 failed.
Uninstalling why3.0.81.

==== ERROR [while installing why3.0.81] ====
# opam-version    1.0.0 (1.0.0)
# os              linux
# command         make opt byte
# path            /home/jonathan/.opam/4.00.1/build/why3.0.81
# exit-code       2
# env-file        /home/jonathan/.opam/4.00.1/build/why3.0.81/why3-c743ac.env
# stdout-file     /home/jonathan/.opam/4.00.1/build/why3.0.81/why3-c743ac.out
# stderr-file     /home/jonathan/.opam/4.00.1/build/why3.0.81/why3-c743ac.err
### stdout ###
...[truncated]
3236 additional bytes used for bindings
Ocamlyacc plugins/tptp/tptp_parser.mly
Ocamldep plugins/tptp/tptp_printer.ml
Ocamldep plugins/tptp/tptp_lexer.ml
Ocamldep plugins/tptp/tptp_typing.ml
Ocamldep plugins/tptp/tptp_parser.ml
Ocamldep plugins/tptp/tptp_ast.ml
Ocamldep plugins/transform/hypothesis_selection.ml
Ocamldep plugins/parser/genequlin.ml
autoconf
### stderr ###
...[truncated]
configure.in:662:AC_SUBST(FRAMAC_SHARE)
configure.in:663:AC_SUBST(FRAMAC_LIBDIR)
configure.in:676:AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
configure.in:677:AC_CONFIG_FILES(share/provers-detection-data.conf lib/why3/META)
configure.in:678:AC_CONFIG_FILES(src/jessie/Makefile)
configure.in:679:AC_CONFIG_COMMANDS([chmod],
configure.in:726:   echo "    Version             : $FRAMAC_VERSION"
configure.in:727:   echo "    Share path          : $FRAMAC_SHARE"
configure.in:728:   echo "    Library path        : $FRAMAC_LIBDIR"
make: *** [configure] Error 1

'opam install why3' failed.

CC @bobot @claudemarche

protz commented 11 years ago

The log files are available here http://pauillac.inria.fr/~protzenk/opam/

Thanks,

jonathan

bobot commented 11 years ago

Hi,

Thank you for the 0.80 package. For the 0.81 package, I added the installation of the why3 library. For that I needed to patch the configure.in. That seems to be the problem: Is it correct that you are cross compiling? Is it correct that your version of autoconf doesn't like the macro of the why3 configure.in? I should have patched the configure file instead of the configure.in. I will correct that.

ps: It seems that the bug reports for particular opam package should be created in the opam-repository issue tracker instead of the opam one.

Thanks again,

François

protz commented 11 years ago

Hi,

As far as I know, I am not cross-compiling. I don't know why autoconf generated such a warning. I have the ocaml-android package installed, but all the binaries are prefixed in ~/.opam/4.00.1/arm-android-eabi-blah... so that should not interfere at all.
My version of autoconf is 2.13 which is, as far as I know, the default on my Debian box. Is there anything I can do to confirm that there's a clash between configure.in and autoconf? I just re-ran autoconf in the why3 directory and I get:

configure.in:338: warning: Cannot check for file existence when cross compiling
configure.in:357: warning: Cannot check for file existence when cross compiling
configure.in:391: warning: Cannot check for file existence when cross compiling
configure.in:449: warning: Cannot check for file existence when cross compiling
configure.in:546: warning: Cannot check for file existence when cross compiling
autoconf: Undefined macros:
configure.in:142:  AC_MSG_RESULT(.exe <Cygwin>)
configure.in:148:  AC_MSG_RESULT(.exe <MinGW>)
configure.in:153:  AC_MSG_RESULT(<none>)
configure.in:187:   AC_MSG_WARN(Cannot find ocamlopt; bytecode compilation only.)
configure.in:192:       AC_MSG_RESULT(differs from ocamlc; ocamlopt discarded.)
configure.in:195:       AC_MSG_RESULT(ok)
configure.in:213:       AC_MSG_RESULT(differs from ocamlc; ocamlc.opt discarded.)
configure.in:215:       AC_MSG_RESULT(ok)
configure.in:227:       AC_MSG_RESULT(differs from ocamlc; ocamlopt.opt discarded.)
configure.in:229:       AC_MSG_RESULT(ok)
configure.in:263:    AC_MSG_WARN(Cannot find ocamldoc)
configure.in:303:      AC_MSG_WARN([Cannot find rubber, documentation disabled.])
configure.in:315:      AC_MSG_WARN([Cannot find hevea, HTML documentation disabled.])
configure.in:325:      AC_MSG_WARN([Cannot find hacha, HTML documentation disabled.])
configure.in:340:         AC_MSG_WARN([Lib lablgtk2 not found, IDE disabled.])
configure.in:359:         AC_MSG_WARN([Lib lablgtksourceview2 not found, IDE disabled.])
configure.in:376:dnl         AC_MSG_WARN(Lib sqlite3 not found, IDE disabled.)
configure.in:393:        AC_MSG_WARN([Lib sqlite3 not found, why3bench disabled.])
configure.in:410:    AC_MSG_WARN(coq support disabled)
configure.in:416:        AC_MSG_WARN(Cannot find coqc.)
configure.in:427:                AC_MSG_RESULT($COQVERSION)
configure.in:432:                AC_MSG_RESULT($COQVERSION)
configure.in:436:           AC_MSG_WARN(You need Coq 8.3 or later; Coq discarded)
configure.in:468:      AC_MSG_WARN(Cannot find coqc.)
configure.in:479:     [ AC_MSG_RESULT(yes) ],
configure.in:480:     [ AC_MSG_RESULT(no)
configure.in:482:       AC_MSG_WARN(Cannot find Flocq.)
configure.in:491:    AC_MSG_WARN(PVS support disabled)
configure.in:497:        AC_MSG_WARN(Cannot find pvs.)
configure.in:507:                AC_MSG_RESULT($PVSVERSION)
configure.in:510:                AC_MSG_RESULT($PVSVERSION)
configure.in:512:           AC_MSG_WARN(You need PVS 6.0 or higher; PVS discarded)
configure.in:533:   AC_MSG_RESULT($enable_pvs_nasa_libs)
configure.in:548:       AC_MSG_WARN([Lib ocamlgraph not found, hypothesis selection disabled.])
configure.in:557:        AC_MSG_WARN(Cannot find Frama-C.)
configure.in:562:      FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|Version: *\(.*\)$|\1|p'`
configure.in:563:      AC_MSG_RESULT($FRAMAC_VERSION)
configure.in:564:      case $FRAMAC_VERSION in
configure.in:566:         *) AC_MSG_WARN(Version Oxygen-20120901 required.)
configure.in:571:      FRAMAC_SHARE=`$FRAMAC -print-path`
configure.in:572:      FRAMAC_LIBDIR=`$FRAMAC -print-libpath`
configure.in:661:AC_SUBST(FRAMAC_VERSION)
configure.in:662:AC_SUBST(FRAMAC_SHARE)
configure.in:663:AC_SUBST(FRAMAC_LIBDIR)
configure.in:676:AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
configure.in:677:AC_CONFIG_FILES(share/provers-detection-data.conf lib/why3/META)
configure.in:678:AC_CONFIG_FILES(src/jessie/Makefile)
configure.in:679:AC_CONFIG_COMMANDS([chmod],
configure.in:726:   echo "    Version             : $FRAMAC_VERSION"
configure.in:727:   echo "    Share path          : $FRAMAC_SHARE"
configure.in:728:   echo "    Library path        : $FRAMAC_LIBDIR"

I'll make sure I create the bug report in the opam-repository next time.

Thanks for the quick report, and let me know if you want me to test further changes to configure.in, I still have a build directory ready to try any further patches.

jonathan

PS: if you tell me which version of autoconf you need, I can try running it. For instance, running 'autoconf 2.50' gives me the empty output, i.e. autoconf seems happy :)

bobot commented 11 years ago

I'm using autoconf 2.69 (stable debian version is 2.67). But the why3 opam package shouldn't depend on autoconf.

Can you add temporarily my repository and test the new why3 package? opam remote add bobot git://github.com/bobot/opam-repository.git

PS: GitHub is great just by writing in the commit message OCamlPro/opam#577 an hyperlink is created to this issue and conversely!!! (if the issue was in the opam-repository #Num would have been sufficient ;) )

protz commented 11 years ago

The new package works just fine, many thanks!

ocaml / opam

Why3 0.81 is broken #577