configure.in

   1 ####################################################################
   2 #                                                                  #
   3 #  The Why3 Verification Platform   /   The Why3 Development Team  #
   4 #  Copyright 2010-2020   --   Inria - CNRS - Paris-Sud University  #
   5 #                                                                  #
   6 #  This software is distributed under the terms of the GNU Lesser  #
   7 #  General Public License version 2.1, with the special exception  #
   8 #  on linking described in file LICENSE.                           #
   9 #                                                                  #
  10 ####################################################################
  11
  12 #
  13 # autoconf input for Objective Caml programs
  14 # Copyright (C) 2001 Jean-Christophe Filliâtre
  15 #   from a first script by Georges Mariano
  16 #
  17 # This library is free software; you can redistribute it and/or
  18 # modify it under the terms of the GNU Library General Public
  19 # License version 2, as published by the Free Software Foundation.
  20 #
  21 # This library is distributed in the hope that it will be useful,
  22 # but WITHOUT ANY WARRANTY; without even the implied warranty of
  23 # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
  24 #
  25 # See the GNU Library General Public License version 2 for more details
  26 # (enclosed in the file LGPL).
  27
  28 AC_INIT([Why3], [1.3.3])
  29
  30 # verbosemake
  31
  32 AC_ARG_ENABLE(verbose-make,
  33     AS_HELP_STRING([--enable-verbose-make], [verbose makefile recipes]),,
  34     enable_verbose_make=no)
  35
  36 # LOCAL_CONF
  37
  38 AC_ARG_ENABLE(local,
  39     AS_HELP_STRING([--enable-local], [use Why3 in the build directory (no installation)]),,
  40     enable_local=no)
  41
  42 # RELOCATABLE INSTALLATION
  43
  44 AC_ARG_ENABLE(relocation,
  45     AS_HELP_STRING([--enable-relocation], [allow for later relocation of Why3 installation]),,
  46     enable_relocation=no)
  47
  48 # NATIVE
  49
  50 AC_ARG_ENABLE(native-code,
  51     AS_HELP_STRING([--disable-native-code], [use only the byte-code compiler]),,
  52     enable_native_code=yes)
  53
  54 # WHY3LIB
  55
  56 AC_ARG_ENABLE(why3-lib,
  57     AS_HELP_STRING([--disable-why3-lib], [use an already installed Why3]),,
  58     enable_why3_lib=yes)
  59
  60 # Zarith
  61
  62 AC_ARG_ENABLE(zarith,
  63     AS_HELP_STRING([--disable-zarith], [use Nums instead of Zarith for computations]),,
  64     enable_zarith=yes)
  65
  66 # ocamlfind
  67
  68 AC_ARG_ENABLE(ocamlfind,
  69     AS_HELP_STRING([--disable-ocamlfind], [do not use Ocamlfind]),,
  70     enable_ocamlfind=yes)
  71
  72 # camlzip
  73
  74 AC_ARG_ENABLE(zip,
  75     AS_HELP_STRING([--disable-zip], [do not use LZ compression to store session files]),,
  76     enable_zip=yes)
  77
  78 # js_of_ocaml
  79
  80 AC_ARG_ENABLE(js_of_ocaml,
  81     AS_HELP_STRING([--disable-js-of-ocaml], [do not use js-of-ocaml]),,
  82     enable_js_of_ocaml=yes)
  83
  84 # re
  85
  86 AC_ARG_ENABLE(re,
  87     AS_HELP_STRING([--disable-re], [use Str instead of Re for regular expressions]),,
  88     enable_re=yes)
  89
  90 # IDE
  91
  92 AC_ARG_ENABLE(ide,
  93     AS_HELP_STRING([--disable-ide], [do not build Why3 IDE]),,
  94     enable_ide=yes)
  95
  96 AC_ARG_ENABLE(web_ide,
  97     AS_HELP_STRING([--disable-web-ide], [do not build Why3 Web IDE]),,
  98     enable_web_ide=yes)
  99
 100 # Coq libraries
 101
 102 AC_ARG_ENABLE(coq-libs,
 103     AS_HELP_STRING([--disable-coq-libs], [do not build Coq realizations]),,
 104     enable_coq_libs=yes)
 105
 106 # PVS libraries
 107
 108 AC_ARG_ENABLE(pvs-libs,
 109     AS_HELP_STRING([--disable-pvs-libs], [do not build PVS realizations]),,
 110     enable_pvs_libs=yes)
 111
 112 # Isabelle libraries
 113
 114 AC_ARG_ENABLE(isabelle-libs,
 115     AS_HELP_STRING([--disable-isabelle-libs], [do not build Isabelle realizations]),,
 116     enable_isabelle_libs=yes)
 117
 118 # hypothesis selection
 119
 120 AC_ARG_ENABLE(hypothesis-selection,
 121     AS_HELP_STRING([--disable-hypothesis-selection], [do not support hypothesis selection]),,
 122     enable_hypothesis_selection=yes)
 123
 124 # documentation
 125
 126 AC_ARG_ENABLE(doc,
 127     AS_HELP_STRING([--disable-doc], [do not build documentation]),,
 128     enable_doc=yes)
 129
 130 AC_ARG_ENABLE(html-pdf,
 131     AS_HELP_STRING([--disable-pdf-doc], [do not build PDF documentation]),,
 132     enable_pdf_doc=yes)
 133
 134 # Experimental Jessie3 Frama-C plugin, disabled by default
 135
 136 AC_ARG_ENABLE(frama-c,
 137     AS_HELP_STRING([--enable-frama-c], [enable Frama-C plugin]),,
 138     [enable_frama_c=no
 139      reason_frama_c=" (disabled by default)"])
 140
 141 # profiling
 142
 143 AC_ARG_ENABLE(profiling,
 144     AS_HELP_STRING([--enable-profiling], [enable profiling]),,
 145     enable_profiling=no)
 146
 147 AC_ARG_ENABLE(statmemprof,
 148     AS_HELP_STRING([--enable-statmemprof], [enable statistical memory profiling]),,
 149     [enable_statmemprof=no
 150      reason_statmemprof=" (disabled by default)"])
 151
 152 # Emacs compilation
 153
 154 AC_ARG_ENABLE(emacs-compilation,
 155     AS_HELP_STRING([--disable-emacs-compilation], [do not compile why3.elc]),,
 156     enable_emacs_compilation=yes)
 157
 158 # either relocation or local, not both
 159 if test "$enable_relocation" = yes ; then
 160 if test "$enable_local" = yes ; then
 161     AC_MSG_ERROR(cannot use --enable-relocation and --enable-local at the same time.)
 162 fi
 163 fi
 164
 165 # Check for arch/OS
 166
 167 AC_MSG_CHECKING(executable suffix)
 168 if uname -s | grep -q CYGWIN ; then
 169   EXE=.exe
 170   STRIP='echo "no strip "'
 171   AC_MSG_RESULT(.exe <Cygwin>)
 172 else
 173 if uname -s | grep -q MINGW ; then
 174   EXE=.exe
 175   STRIP=strip
 176   AC_MSG_RESULT(.exe <MinGW>)
 177 else
 178   EXE=
 179   STRIP=strip
 180   AC_MSG_RESULT(<none>)
 181 fi
 182 fi
 183
 184 AC_PROG_CC
 185 # Add compatibility for C99
 186 AC_PROG_CC_STDC
 187 AC_PROG_MKDIR_P
 188 AC_PROG_INSTALL
 189
 190 AC_DEFUN([AX_VERSION_GE], [AS_VERSION_COMPARE([$1],[$2],[$4],[$3],[$3])])
 191
 192 # Check for Ocaml compilers
 193
 194 # we first look for ocamlc in the path; if not present, we fail
 195 AC_CHECK_PROG(OCAMLC,ocamlc,ocamlc,no)
 196 if test "$OCAMLC" = no ; then
 197         AC_MSG_ERROR(Cannot find ocamlc.)
 198 fi
 199
 200 # we extract Ocaml version number
 201 OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version *\(.*\)$|\1|p'`
 202 echo "ocaml version is $OCAMLVERSION"
 203
 204 AX_VERSION_GE([$OCAMLVERSION], 4.05.0, [],
 205   [AC_MSG_ERROR(You need Objective Caml 4.05.0 or higher.)])
 206
 207 # Ocaml library path
 208 # old way: OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d ' ' | tr -d '\\r'`
 209 OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
 210 echo "ocaml library path is $OCAMLLIB"
 211
 212 # then we look for ocamlopt; if not present, we issue a warning
 213 # if the version is not the same, we also discard it
 214 # we set OCAMLBEST to "opt" or "byte", whether ocamlopt is available or not
 215 AC_CHECK_PROG(OCAMLOPT,ocamlopt,ocamlopt,no)
 216 OCAMLBEST=byte
 217 if test "$OCAMLOPT" = no ; then
 218         AC_MSG_WARN(Cannot find ocamlopt; bytecode compilation only.)
 219 else
 220         AC_MSG_CHECKING(ocamlopt version)
 221         TMPVERSION=`$OCAMLOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p'`
 222         if test "$TMPVERSION" != "$OCAMLVERSION" ; then
 223             AC_MSG_RESULT(differs from ocamlc; ocamlopt discarded.)
 224             OCAMLOPT=no
 225         else
 226             AC_MSG_RESULT(ok)
 227             OCAMLBEST=opt
 228         fi
 229 fi
 230
 231 # checking for native-code
 232 if test "$enable_native_code" != yes || test "$OCAMLBEST" = byte ; then
 233     enable_native_code=no
 234     OCAMLBEST=byte
 235     OCAMLOPT=no
 236 fi
 237
 238 # checking for ocamlc.opt
 239 AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt,no)
 240 if test "$OCAMLCDOTOPT" != no ; then
 241         AC_MSG_CHECKING(ocamlc.opt version)
 242         TMPVERSION=`$OCAMLCDOTOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p'`
 243         if test "$TMPVERSION" != "$OCAMLVERSION" ; then
 244             AC_MSG_RESULT(differs from ocamlc; ocamlc.opt discarded.)
 245         else
 246             AC_MSG_RESULT(ok)
 247             OCAMLC=$OCAMLCDOTOPT
 248         fi
 249 fi
 250
 251 # checking for ocamlopt.opt
 252 if test "$OCAMLOPT" != no ; then
 253     AC_CHECK_PROG(OCAMLOPTDOTOPT,ocamlopt.opt,ocamlopt.opt,no)
 254     if test "$OCAMLOPTDOTOPT" != no ; then
 255         AC_MSG_CHECKING(ocamlc.opt version)
 256         TMPVER=`$OCAMLOPTDOTOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p'`
 257         if test "$TMPVER" != "$OCAMLVERSION" ; then
 258             AC_MSG_RESULT(differs from ocamlc; ocamlopt.opt discarded.)
 259         else
 260             AC_MSG_RESULT(ok)
 261             OCAMLOPT=$OCAMLOPTDOTOPT
 262         fi
 263     fi
 264 fi
 265
 266 # ocamldep, ocamllex and ocamlyacc should also be present in the path
 267 AC_CHECK_PROG(OCAMLDEP,ocamldep,ocamldep,no)
 268 if test "$OCAMLDEP" = no ; then
 269    AC_MSG_ERROR(Cannot find ocamldep.)
 270 else
 271    AC_CHECK_PROG(OCAMLDEPDOTOPT,ocamldep.opt,ocamldep.opt,no)
 272    if test "$OCAMLDEPDOTOPT" != no ; then
 273       OCAMLDEP=$OCAMLDEPDOTOPT
 274    fi
 275 fi
 276
 277 AC_CHECK_PROG(OCAMLLEX,ocamllex,ocamllex,no)
 278 if test "$OCAMLLEX" = no ; then
 279         AC_MSG_ERROR(Cannot find ocamllex.)
 280 else
 281     AC_CHECK_PROG(OCAMLLEXDOTOPT,ocamllex.opt,ocamllex.opt,no)
 282     if test "$OCAMLLEXDOTOPT" != no ; then
 283         OCAMLLEX=$OCAMLLEXDOTOPT
 284     fi
 285 fi
 286
 287 AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no)
 288 if test "$OCAMLYACC" = no ; then
 289         AC_MSG_ERROR(Cannot find ocamlyacc.)
 290 fi
 291
 292 AC_CHECK_PROG(OCAMLDOC,ocamldoc,ocamldoc,true)
 293 if test "$OCAMLDOC" = true ; then
 294     AC_MSG_WARN(Cannot find ocamldoc)
 295 else
 296     AC_CHECK_PROG(OCAMLDOCOPT,ocamldoc.opt,ocamldoc.opt,no)
 297     if test "$OCAMLDOCOPT" != no ; then
 298         OCAMLDOC=$OCAMLDOCOPT
 299     fi
 300 fi
 301
 302 AC_CHECK_PROG(MENHIR,menhir,menhir,no)
 303 if test "$MENHIR" = no ; then
 304         AC_MSG_ERROR(Cannot find menhir.)
 305 fi
 306
 307 MENHIRVERSION=`$MENHIR --version | sed -n -e 's,.*version *\(.*\)$,\1,p'`
 308 AX_VERSION_GE([$MENHIRVERSION], 20151112, [],
 309   [AC_MSG_ERROR(You need Menhir 20151112 or higher.)])
 310
 311 if test "$enable_ocamlfind" != yes; then
 312    OCAMLFIND=no
 313 else
 314    AC_CHECK_PROG(OCAMLFIND,ocamlfind,ocamlfind,no)
 315    if test "$OCAMLFIND" = no; then
 316       enable_ocamlfind=no
 317       reason_ocamlfind=" (not found)"
 318    else
 319       OCAMLFINDLIB=$(ocamlfind printconf stdlib)
 320       if test "$OCAMLFINDLIB" != "$OCAMLLIB"; then
 321          OCAMLFIND=no
 322          enable_ocamlfind=no
 323          reason_ocamlfind=" (incompatible with OCaml)"
 324          echo "but your ocamlfind is not compatible with your ocamlc:"
 325          echo "ocamlfind: $OCAMLFINDLIB, ocamlc: $OCAMLLIB"
 326       fi
 327    fi
 328 fi
 329
 330 #if ocamlfind is used it gives the install path for ocaml library
 331 if test "$enable_ocamlfind" = yes; then
 332    OCAMLINSTALLLIB=$($OCAMLFIND printconf destdir)
 333 else
 334    OCAMLINSTALLLIB=$OCAMLLIB
 335 fi
 336
 337 if test "$enable_why3_lib" = yes ; then
 338    WHY3LIB=
 339 else
 340    AC_MSG_CHECKING([For Why3])
 341    if test "$enable_ocamlfind" = no; then
 342       AC_MSG_RESULT([no])
 343       AC_MSG_ERROR([Cannot use --disable-why3-lib without ocamlfind.])
 344    fi
 345    WHY3LIB=why3
 346    DIR=$($OCAMLFIND query why3)
 347    if test -n "$DIR"; then
 348       AC_MSG_RESULT([$DIR])
 349       WHY3INCLUDE="-I $DIR"
 350    else
 351       AC_MSG_RESULT([no])
 352       AC_MSG_ERROR([Cannot use --disable-why3-lib without an installed Why3.])
 353    fi
 354 fi
 355
 356 if test "$enable_local" = no; then
 357    LOCALDIR=''
 358 else
 359    LOCALDIR="${PWD}"
 360 fi
 361
 362 # ppx
 363 if test "$enable_ocamlfind" = yes; then
 364   COMPILERLIBS=$($OCAMLFIND query compiler-libs)
 365   if test -n "$COMPILERLIBS"; then
 366     echo "ocamlfind found compiler-libs in $COMPILERLIBS"
 367     enable_ppx=yes
 368   else
 369     enable_ppx=no
 370     reason_ppx=" (compiler-libs not found)"
 371   fi
 372 else
 373   enable_ppx=no
 374 fi
 375
 376 # checking for sphinx
 377 if test "$enable_doc" = yes; then
 378    AC_CHECK_PROG(SPHINX,sphinx-build,sphinx-build,no)
 379    if test "$SPHINX" = no; then
 380       enable_doc=no
 381       enable_pdf_doc=no
 382       reason_doc=" (sphinx-build not found)"
 383       AC_MSG_WARN([Cannot find sphinx-build, Documentation disabled.])
 384    fi
 385 else
 386    enable_pdf_doc=no
 387 fi
 388
 389 # checking for rubber or latexmk or pdflatex
 390 if test "$enable_pdf_doc" = yes; then
 391    AC_CHECK_PROGS(LATEX,latexmk rubber pdflatex,no)
 392    if test "$LATEX" = no; then
 393       enable_pdf_doc=no
 394       reason_pdf_doc=" ((rubber|latexmk|pdflatex) not found)"
 395       AC_MSG_WARN([Cannot find any latex compiler, PDF documentation disabled.])
 396    fi
 397 fi
 398
 399 # checking for emacs
 400 if test "$enable_emacs_compilation" = yes ; then
 401    AC_CHECK_PROG(EMACS,emacs,emacs,no)
 402    if test "$EMACS" = no ; then
 403       enable_emacs_compilation=no
 404       AC_MSG_WARN([Cannot find emacs, compilation of why3.elc disabled.])
 405    fi
 406 fi
 407
 408 # checking for Num
 409 # (ocamlfind cannot be trusted here, since the default installation path is $OCAMLLIB)
 410 found_num=no
 411 if test "$enable_ocamlfind" = yes; then
 412    DIR=$($OCAMLFIND query num)
 413    if test -n "$DIR"; then
 414       echo "ocamlfind found num in $DIR"
 415       NUMPKG=num
 416       NUMINCLUDE="-I $DIR"
 417       found_num=yes
 418       AC_CHECK_FILE($DIR/nums.cma,,found_num=no)
 419       AC_CHECK_FILE($DIR/num.cmi,,found_num=no)
 420    else
 421       enable_ocamlfind=no
 422       reason_ocamlfind=" (unable to find num)"
 423    fi
 424 fi
 425 if test "$found_num" = no; then
 426    DIR="$OCAMLLIB"
 427    NUMINCLUDE=
 428    found_num=yes
 429    AC_CHECK_FILE($DIR/nums.cma,,found_num=no)
 430    AC_CHECK_FILE($DIR/num.cmi,,found_num=no)
 431 fi
 432 if test "$found_num" = no; then
 433    AC_MSG_ERROR([Library Num not found.])
 434 fi
 435
 436 # checking for Zarith
 437 if test "$enable_zarith" = yes; then
 438    DIR=
 439    if test "$enable_ocamlfind" = yes; then
 440       DIR=$(ocamlfind query zarith)
 441       if test -n "$DIR"; then
 442          echo "ocamlfind found zarith in $DIR"
 443          BIGINTINCLUDE="-I $DIR"
 444       else
 445          ocamlfind_zarith=no
 446       fi
 447    fi
 448    if test -z "$DIR"; then
 449       BIGINTINCLUDE="-I +zarith"
 450       DIR="$OCAMLLIB/zarith"
 451       AC_CHECK_FILE($DIR/zarith.cma,,enable_zarith=no)
 452    fi
 453    AC_CHECK_FILE($DIR/z.cmi,,enable_zarith=no)
 454    if test "$enable_zarith" = no; then
 455       AC_MSG_WARN([Lib Zarith not found, using Nums instead.])
 456       reason_zarith=" (zarith not found)"
 457    elif test "$ocamlfind_zarith" = no; then
 458       enable_ocamlfind=no
 459       reason_ocamlfind=" (unable to find zarith)"
 460    fi
 461 fi
 462
 463 if test "$enable_zarith" = yes; then
 464    BIGINTLIB=zarith
 465    BIGINTPKG=zarith
 466 else
 467    BIGINTLIB=nums
 468    BIGINTPKG=num
 469    BIGINTINCLUDE="$NUMINCLUDE"
 470 fi
 471
 472 # checking for camlzip
 473 if test "$enable_zip" = yes; then
 474    DIR=
 475    if test "$enable_ocamlfind" = yes; then
 476       DIR=$(ocamlfind query zip)
 477       if test -n "DIR"; then
 478          echo "ocamlfind found camlzip in $DIR"
 479          ZIPINCLUDE="-I $DIR"
 480       else
 481          ocamlfind_zip=no
 482       fi
 483    fi
 484    if test -z "$DIR"; then
 485       ZIPINCLUDE="-I +zip"
 486       DIR="$OCAMLLIB/zip"
 487       AC_CHECK_FILE($DIR/zip.cma,,enable_zip=no)
 488    fi
 489    AC_CHECK_FILE($DIR/zip.cmi,,enable_zip=no)
 490    if test "$enable_zip" = no; then
 491       AC_MSG_WARN([Lib camlzip not found, sessions files will not be compressed.])
 492       reason_zip=" (camlzip not found)"
 493    elif test "$ocamlfind_zip" = no; then
 494       enable_ocamlfind=no
 495       reason_ocamlfind=" (unable to find camlzip)"
 496    fi
 497 fi
 498
 499 if test "$enable_zip" = yes; then
 500    ZIPLIB=zip
 501 else
 502    ZIPLIB=
 503    ZIPINCLUDE=
 504 fi
 505
 506 # checking for menhirlib
 507 found_menhirlib=yes
 508 DIR=
 509 if test "$enable_ocamlfind" = yes; then
 510    DIR=$($OCAMLFIND query menhirLib)
 511    if test -n "$DIR"; then
 512       echo "ocamlfind found menhirLib in $DIR"
 513       MENHIRINCLUDE="-I $DIR"
 514    else
 515       enable_ocamlfind=no
 516       reason_ocamlfind=" (unable to find menhirLib)"
 517    fi
 518 fi
 519 if test -z "$DIR"; then
 520    MENHIRINCLUDE="-I +menhirLib"
 521    DIR="$OCAMLLIB/menhirLib"
 522    AC_CHECK_FILE($DIR/menhirLib.cmx,,found_menhirlib=no)
 523 fi
 524 AC_CHECK_FILE($DIR/menhirLib.cmi,,found_menhirlib=no)
 525 if test "$found_menhirlib" = no; then
 526    AC_MSG_ERROR([Library menhirLib not found.])
 527 fi
 528
 529 # checking for seq
 530 # (ocamlfind cannot be trusted here, since the default installation path is $OCAMLLIB)
 531 found_seq=no
 532 if test "$enable_ocamlfind" = yes; then
 533    DIR=$($OCAMLFIND query seq)
 534    if test -n "$DIR"; then
 535       echo "ocamlfind found seq in $DIR"
 536       SEQINCLUDE="-I $DIR"
 537       SEQLIB=seq
 538       found_seq=yes
 539       AC_CHECK_FILE($DIR/seq.cma,,found_seq=no)
 540       AC_CHECK_FILE($DIR/seq.cmi,,found_seq=no)
 541    fi
 542 fi
 543 if test "$found_seq" = no; then
 544    DIR="$OCAMLLIB"
 545    SEQINCLUDE=
 546    SEQLIB=
 547    found_seq=yes
 548    AC_CHECK_FILE($DIR/stdlib__seq.cmi,,found_seq=no)
 549 fi
 550 if test "$found_seq" = no; then
 551    AC_MSG_WARN([Library seq not found.])
 552    if test "$enable_re" = yes; then
 553       enable_re=no
 554       reason_re=" (seq not found)"
 555    fi
 556 fi
 557
 558 # checking for re
 559 if test "$enable_re" = yes; then
 560    found_re=yes
 561    DIR=
 562    if test "$enable_ocamlfind" = yes; then
 563       DIR=$(ocamlfind query re)
 564       if test -n "$DIR"; then
 565          echo "ocamlfind found re in $DIR"
 566          REINCLUDE="-I $DIR"
 567       else
 568          ocamlfind_re=no
 569       fi
 570    fi
 571    if test -z "$DIR"; then
 572       REINCLUDE="-I +re"
 573       DIR="$OCAMLLIB/re"
 574       AC_CHECK_FILE($DIR/re.cmx,,found_re=no)
 575    fi
 576    AC_CHECK_FILE($DIR/re.cmi,,found_re=no)
 577    if test "$found_re" = no; then
 578       AC_MSG_WARN([Library re not found.])
 579       enable_re=no
 580    elif test "$ocamlfind_re" = no; then
 581       enable_ocamlfind=no
 582       reason_ocamlfind=" (unable to find re)"
 583    fi
 584 fi
 585
 586 if test "$enable_re" = no; then
 587    REINCLUDE=
 588    RELIB=str
 589 else
 590    RELIB=re
 591 fi
 592
 593 # checking for lablgtk3
 594 if test "$enable_ide" != yes ; then
 595    reason_ide=" (disabled by user)"
 596 else
 597    DIR=
 598    if test "$enable_ocamlfind" = yes; then
 599       DIR=$($OCAMLFIND query lablgtk3)
 600       if test -n "$DIR"; then
 601          echo "ocamlfind found lablgtk3 in $DIR"
 602          LABLGTKINCLUDE="-I $DIR -I +threads"
 603       fi
 604    fi
 605    if test -z "$DIR"; then
 606       LABLGTKINCLUDE="-I +lablgtk3 -I +threads"
 607       DIR="$OCAMLLIB/lablgtk3"
 608    fi
 609    AC_CHECK_FILE($DIR/lablgtk.cma,LABLGTKLIB="threads lablgtk",)
 610    AC_CHECK_FILE($DIR/lablgtk3.cma,LABLGTKLIB="threads lablgtk3",)
 611    AC_CHECK_FILE($DIR/gtkButton.cmi,,LABLGTKLIB="")
 612    if test -n "$LABLGTKLIB"; then
 613       GTKVERSION=3
 614       LIB_SOURCEVIEW=lablgtk3_sourceview3
 615       PKG_SOURCEVIEW=lablgtk3-sourceview3
 616       reason_ide=" (gtk3)"
 617    else
 618       AC_MSG_WARN([Lib lablgtk3 not found, trying lablgtk2.])
 619       enable_ide=retry
 620    fi
 621 fi
 622
 623 # checking for lablgtk2
 624 if test "$enable_ide" = retry; then
 625    enable_ide=yes
 626    DIR=
 627    if test "$enable_ocamlfind" = yes; then
 628       DIR=$($OCAMLFIND query lablgtk2)
 629       if test -n "$DIR"; then
 630          echo "ocamlfind found lablgtk2 in $DIR"
 631          LABLGTKINCLUDE="-I $DIR"
 632       fi
 633    fi
 634    if test -z "$DIR"; then
 635       LABLGTKINCLUDE="-I +lablgtk2"
 636       DIR="$OCAMLLIB/lablgtk2"
 637       AC_CHECK_FILE($DIR/lablgtk.cma,,enable_ide=no)
 638    fi
 639    AC_CHECK_FILE($DIR/gtkButton.cmi,,enable_ide=no)
 640    if test "$enable_ide" = yes; then
 641       GTKVERSION=2
 642       LABLGTKLIB=lablgtk
 643       LIB_SOURCEVIEW=lablgtksourceview2
 644       PKG_SOURCEVIEW=lablgtk2.sourceview2
 645       reason_ide=" (gtk2)"
 646    else
 647       AC_MSG_WARN([Lib lablgtk2 not found, IDE disabled.])
 648       reason_ide=" (lablgtk2/3 not found)"
 649    fi
 650 fi
 651
 652 # checking for lablgtksourceview
 653 if test "$enable_ide" = yes ; then
 654    DIR=
 655    if test "$enable_ocamlfind" = yes; then
 656       DIR=$($OCAMLFIND query $PKG_SOURCEVIEW)
 657       if test -z "$DIR"; then
 658          case $GTKVERSION in
 659             2)
 660                 PKG_SOURCEVIEW=lablgtksourceview2
 661                 DIR=$(ocamlfind query $PKG_SOURCEVIEW)
 662                 ;;
 663             3)
 664                 PKG_SOURCEVIEW=lablgtksourceview3
 665                 DIR=$(ocamlfind query $PKG_SOURCEVIEW)
 666                 ;;
 667          esac
 668       fi
 669       if test -n "$DIR";then
 670          echo "ocamlfind found $PKG_SOURCEVIEW in $DIR"
 671       fi
 672    fi
 673    if test -z "$DIR"; then
 674       DIR="$OCAMLLIB/lablgtk$GTKVERSION"
 675       LIB_SOURCEVIEW="lablgtksourceview$GTKVERSION"
 676       AC_CHECK_FILE($DIR/$LIB_SOURCEVIEW.cma,,DIR="")
 677    fi
 678    if test -z "$DIR"; then
 679       DIR="$OCAMLLIB/lablgtk$GTKVERSION-sourceview$GTKVERSION"
 680       LIB_SOURCEVIEW="lablgtk${GTKVERSION}_sourceview$GTKVERSION"
 681       AC_CHECK_FILE($DIR/$LIB_SOURCEVIEW.cma,,enable_ide=no)
 682    fi
 683    AC_CHECK_FILE($DIR/gSourceView$GTKVERSION.cmi,,enable_ide=no)
 684    if test "$enable_ide" = no; then
 685       AC_MSG_WARN([Lib lablgtksourceview not found, IDE disabled.])
 686       reason_ide=" (lablgtksourceview not found)"
 687    else
 688       LABLGTKINCLUDE="$LABLGTKINCLUDE -I $DIR"
 689    fi
 690 fi
 691
 692 if test "$enable_ide" = yes ; then
 693    LABLGTKLIB="$LABLGTKLIB $LIB_SOURCEVIEW"
 694    LABLGTKPKG="lablgtk$GTKVERSION $PKG_SOURCEVIEW"
 695 else
 696    LABLGTKLIB=
 697    LABLGTKPKG=
 698    LABLGTKINCLUDE=
 699 fi
 700
 701 # checking for ocamlgraph
 702 # temporarily disabled until #453 is fixed
 703 if test "$enable_hypothesis_selection" = yes; then
 704    enable_hypothesis_selection=no
 705    reason_hypothesis_selection=" (broken)"
 706 fi
 707
 708 if test "$enable_hypothesis_selection" = yes; then
 709    DIR=
 710    if test "$enable_ocamlfind" = yes; then
 711       DIR=$($OCAMLFIND query ocamlgraph)
 712       if test -n "$DIR"; then
 713          echo "ocamlfind found ocamlgraph in $DIR"
 714          OCAMLGRAPHLIB="$DIR"
 715       else
 716          ocamlfind_ocamlgraph=no
 717       fi
 718    fi
 719    if test -z "$DIR"; then
 720       OCAMLGRAPHLIB="+ocamlgraph"
 721       DIR="$OCAMLLIB/ocamlgraph"
 722       AC_CHECK_FILE($DIR/graph.cma,,enable_hypothesis_selection=no)
 723    fi
 724    AC_CHECK_FILE($DIR/graph.cmi,,enable_hypothesis_selection=no)
 725    if test "$enable_hypothesis_selection" = no; then
 726       reason_hypothesis_selection=" (ocamlgraph not found)"
 727       AC_MSG_WARN([Lib ocamlgraph not found, hypothesis selection disabled.])
 728    elif test "$ocamlfind_ocamlgraph" = no; then
 729       enable_ocamlfind=no
 730       reason_ocamlfind=" (unable to find ocamlgraph)"
 731    fi
 732 fi
 733
 734 if test "$enable_hypothesis_selection" = yes; then
 735    META_OCAMLGRAPH="ocamlgraph"
 736 else
 737    META_OCAMLGRAPH=
 738    OCAMLGRAPHLIB=
 739 fi
 740
 741 # checking for js_of_ocaml
 742 if test "$enable_js_of_ocaml" != yes; then
 743    reason_js_of_ocaml=" (disabled by user)"
 744 elif test "$enable_ocamlfind" != yes; then
 745    enable_js_of_ocaml=no
 746    reason_js_of_ocaml=" (ocamlfind not available)"
 747 else
 748    JSOFOCAML=$($OCAMLFIND query js_of_ocaml)
 749    if test -z "$JSOFOCAML"; then
 750       enable_js_of_ocaml=no
 751       reason_js_of_ocaml=" (js_of_ocaml not found)"
 752    else
 753       JSOFOCAMLPPX=$($OCAMLFIND query js_of_ocaml-ppx)
 754       if test -z "$JSOFOCAMLPPX"; then
 755          enable_js_of_ocaml=no
 756          reason_js_of_ocaml=" (js_of_ocaml-ppx not found)"
 757       else
 758          JSOFOCAMLPKG="js_of_ocaml js_of_ocaml.ppx"
 759       fi
 760    fi
 761 fi
 762
 763 if test "$enable_web_ide" != yes; then
 764    reason_web_ide=" (disabled by user)"
 765 elif test "$enable_js_of_ocaml" != yes; then
 766    enable_web_ide=no
 767    reason_web_ide=" (Javascript support not available)"
 768 fi
 769
 770 # Mlmpfr
 771 MLMPFR_LINK=
 772 if test "$enable_js_of_ocaml" != no; then
 773    found_mlmpfr=no
 774    reason_mlmpfr=" (Cannot allow mlmpfr with js_of_ocaml) "
 775 else
 776    if test "$enable_ocamlfind" = yes; then
 777       DIR=$($OCAMLFIND query mlmpfr)
 778       if test -n "$DIR"; then
 779          echo "ocamlfind found mlmpfr in $DIR"
 780          # Test that mpfr version is higher than 4.0.0 (because of
 781          # Faithful constructor incompatibility).
 782          MPFR_VER=$(grep -q "4.0.0" $DIR/META 2> /dev/null)
 783          EXIT_CODE=$?
 784          if test $EXIT_CODE = 0; then
 785             MLMPFRINCLUDE="-I $DIR"
 786             MLMPFR=mlmpfr
 787             found_mlmpfr=yes
 788             MLMPFR_LINK="-cclib -lmpfr"
 789             AC_CHECK_FILE($DIR/mlmpfr.cma,,found_mlmpfr=yes)
 790          else
 791             reason_mlmpfr=" (Version of mlmpfr is not 4.0.0) "
 792             found_mlmpfr=no
 793          fi
 794       else
 795          reason_mlmpfr=" (mlmpfr not found)"
 796          found_mlmpfr=no
 797       fi
 798    else
 799       reason_mlmpfr=" (ocamlfind not available) "
 800       found_mlmpfr=no
 801    fi
 802 fi
 803 if test "$found_mlmpfr" = no; then
 804    MLMPFRINCLUDE=
 805    MLMPFR=
 806 fi
 807
 808 # checking for statmemprof
 809 if test "$enable_statmemprof" = yes; then
 810    if test "$enable_ocamlfind" != yes; then
 811       enable_statmemprof=no
 812       reason_statmemprof=" (ocamlfind not available)"
 813    else
 814       DIR=$($OCAMLFIND query statmemprof-emacs)
 815       if test -z "$DIR"; then
 816          enable_statmemprof=no
 817          reason_statmemprof=" (statmemprof-emacs not found)"
 818       fi
 819       STATMEMPROFPKG=statmemprof-emacs
 820    fi
 821 fi
 822
 823 # Coq
 824
 825 enable_coq_support=yes
 826 enable_coq_fp_libs=yes
 827
 828 coq_compat_version=
 829
 830 if test "$enable_coq_libs" = no; then
 831    enable_coq_support=no
 832    reason_coq_support=" (disabled by user)"
 833 fi
 834
 835 if test "$enable_coq_support" = yes; then
 836    AC_CHECK_PROG(COQC,coqc,coqc,no)
 837    if test "$COQC" = no ; then
 838       enable_coq_support=no
 839       AC_MSG_WARN(Cannot find coqc.)
 840       reason_coq_support=" (coqc not found)"
 841    fi
 842 fi
 843
 844 if test "$enable_coq_support" = yes; then
 845    COQLIB=`$COQC -where | sed -e 's|\\\|/|g' -e 's| |\\ |g'`
 846    AC_MSG_CHECKING(Coq version)
 847    COQVERSION=[`$COQC -v | sed -n -e 's|.*version *\([^ ]*\) .*$|\1|p'`]
 848    AC_MSG_RESULT($COQVERSION)
 849
 850    case $COQVERSION in
 851       8.6*)
 852          coq_compat_version="COQ86"
 853          ;;
 854       8.7*)
 855          coq_compat_version="COQ87"
 856          ;;
 857       8.8*)
 858          coq_compat_version="COQ88"
 859          ;;
 860       8.9*)
 861          coq_compat_version="COQ89"
 862          ;;
 863       8.10*)
 864          coq_compat_version="COQ810"
 865          ;;
 866       8.11*)
 867          coq_compat_version="COQ811"
 868          ;;
 869       8.12*)
 870          coq_compat_version="COQ812"
 871          ;;
 872       *)
 873          enable_coq_support=no
 874          AC_MSG_WARN(You need Coq 8.6 or later; Coq discarded)
 875          reason_coq_support=" (need version >= 8.6)"
 876          ;;
 877    esac
 878 fi
 879
 880 if test "$enable_coq_support" = yes; then
 881    AC_CHECK_PROG(COQDEP,coqdep,coqdep,no)
 882    if test "$COQDEP" = no; then
 883       enable_coq_support=no
 884       AC_MSG_WARN(Cannot find coqdep.)
 885       reason_coq_support=" (coqdep not found)"
 886    fi
 887 fi
 888
 889 if test "$enable_coq_support" = no; then
 890    enable_coq_libs=no
 891    COQVERSION=
 892 fi
 893
 894 if test "$enable_coq_libs" = yes; then
 895    AC_MSG_CHECKING([for Flocq])
 896    AS_IF(
 897      [ echo "Require Import Flocq.Version BinNat." \
 898             "Goal (30100 <= Flocq_version)%N. easy. Qed." > conftest.v
 899        "$COQC" conftest.v > conftest.err ],
 900      [ AC_MSG_RESULT(yes) ],
 901      [ AC_MSG_RESULT(no)
 902        enable_coq_fp_libs=no
 903        AC_MSG_WARN(Cannot find Flocq.)
 904        reason_coq_fp_libs=" (Flocq >= 3.1 not found)" ])
 905    rm -f conftest.v conftest.vo conftest.err
 906 fi
 907
 908 # PVS
 909
 910 if test "$enable_pvs_libs" = no; then
 911     enable_pvs_support=no
 912     reason_pvs_support=" (disabled by user)"
 913 else
 914     AC_CHECK_PROG(PVS,pvs,pvs,no)
 915     if test "$PVS" = no ; then
 916         enable_pvs_support=no
 917         AC_MSG_WARN(Cannot find pvs.)
 918         reason_pvs_support=" (pvs not found)"
 919     else
 920         PVSLIB=`$PVS -where`
 921         AC_MSG_CHECKING(PVS version)
 922         PVSVERSION=[`$PVS -version | sed -n -e 's|.*Version *\([^ ]*\)$|\1|p'`]
 923
 924         case $PVSVERSION in
 925           6.*)
 926                 enable_pvs_support=yes
 927                 AC_MSG_RESULT($PVSVERSION)
 928                 ;;
 929           *)
 930                 AC_MSG_RESULT($PVSVERSION)
 931                 enable_pvs_support=no
 932                 AC_MSG_WARN(You need PVS 6.0 or higher; PVS discarded)
 933                 reason_pvs_support=" (need version 6.0 or higher)"
 934                 ;;
 935         esac
 936     fi
 937 fi
 938
 939 if test "$enable_pvs_support" = no; then
 940    enable_pvs_libs=no
 941    PVSVERSION=
 942 fi
 943
 944 # Isabelle
 945
 946 # Default version used for generation of realization in the case Isabelle is not
 947 # detected or Why3 is compiled with disable-isabelle.
 948 ISABELLEVERSION=2019
 949
 950 if test "$enable_isabelle_libs" = no; then
 951     enable_isabelle_support=no
 952     reason_isabelle_support=" (disabled by user)"
 953 else
 954     AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
 955     if test "$ISABELLE" = no ; then
 956        enable_isabelle_support=no
 957        AC_MSG_WARN(Cannot find isabelle.)
 958        reason_isabelle_support=" (isabelle not found)"
 959     else
 960         AC_MSG_CHECKING(Isabelle version)
 961         ISABELLEDETECTEDVERSION=[`$ISABELLE version | sed -n -e 's|Isabelle\([^:]*\).*$|\1|p'`]
 962
 963         case $ISABELLEDETECTEDVERSION in
 964           2018*)
 965                 enable_isabelle_support=yes
 966                 ISABELLEVERSION=2018
 967                 AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
 968                 ;;
 969           2019*)
 970                 enable_isabelle_support=yes
 971                 ISABELLEVERSION=2019
 972                 AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
 973                 ;;
 974           *)
 975                 AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
 976                 enable_isabelle_support=no
 977                 AC_MSG_WARN(You need Isabelle 2018 or later; Isabelle discarded)
 978                 reason_isabelle_support=" (need version >= 2018)"
 979                 ;;
 980         esac
 981     fi
 982 fi
 983
 984 if test "$enable_isabelle_support" = no; then
 985    enable_isabelle_libs=no
 986 fi
 987
 988 if test "$enable_pvs_libs" = yes; then
 989    AC_MSG_CHECKING([for NASA PVS library])
 990    enable_pvs_libs=no
 991    reason_pvs_libs=" (no NASA PVS library in PVS_LIBRARY_PATH)"
 992    for dir in  `echo $PVS_LIBRARY_PATH | tr ':' ' '`; do
 993        if test -f $dir/nasalib-version; then
 994           enable_pvs_libs=yes
 995           reason_pvs_libs=""
 996        fi
 997    done
 998    AC_MSG_RESULT($enable_pvs_libs)
 999 fi
1000
1001 #check frama-c
1002 FRAMAC_SUPPORTED=Sulfur
1003 if test "$enable_frama_c" = yes ; then
1004    AC_CHECK_PROG(FRAMAC,frama-c,frama-c,no)
1005    if test "$FRAMAC" = no ; then
1006         AC_MSG_WARN(Cannot find Frama-C.)
1007         enable_frama_c="no"
1008         reason_frama_c=" (frama-c not found)"
1009    else
1010       AC_MSG_CHECKING(Frama-C version)
1011       FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|\(Version: \)\?\(.*\)$|\2|p'`
1012       AC_MSG_RESULT($FRAMAC_VERSION)
1013       case $FRAMAC_VERSION in
1014          $FRAMAC_SUPPORTED-*) ;;
1015          *) AC_MSG_WARN(Version $FRAMAC_SUPPORTED required.)
1016             enable_frama_c=no
1017             reason_frama_c=" (version $FRAMAC_SUPPORTED required)"
1018             ;;
1019       esac
1020    fi
1021 fi
1022
1023 if test "$enable_frama_c" = yes; then
1024    FRAMAC_SHARE=`$FRAMAC -print-path`
1025    FRAMAC_LIBDIR=`$FRAMAC -print-libpath`
1026    FRAMAC_INCLUDE="-I $FRAMAC_LIBDIR"
1027 fi
1028
1029 VERSION=$PACKAGE_VERSION
1030
1031 # substitutions to perform
1032 AC_SUBST(VERSION)
1033
1034 AC_SUBST(enable_verbose_make)
1035
1036 AC_SUBST(EXE)
1037 AC_SUBST(STRIP)
1038
1039 AC_SUBST(OCAMLC)
1040 AC_SUBST(OCAMLOPT)
1041 AC_SUBST(OCAMLDEP)
1042 AC_SUBST(OCAMLLEX)
1043 AC_SUBST(OCAMLYACC)
1044 AC_SUBST(OCAMLDOC)
1045 AC_SUBST(OCAMLBEST)
1046 AC_SUBST(OCAMLVERSION)
1047 AC_SUBST(OCAMLLIB)
1048 AC_SUBST(OCAMLINSTALLLIB)
1049 AC_SUBST(OCAMLGRAPHLIB)
1050 AC_SUBST(MENHIR)
1051
1052 AC_SUBST(enable_ocamlfind)
1053 AC_SUBST(OCAMLFIND)
1054
1055 AC_SUBST(enable_profiling)
1056
1057 AC_SUBST(enable_statmemprof)
1058 AC_SUBST(STATMEMPROFPKG)
1059
1060 AC_SUBST(enable_ide)
1061 AC_SUBST(LABLGTKLIB)
1062 AC_SUBST(LABLGTKPKG)
1063 AC_SUBST(LABLGTKINCLUDE)
1064 AC_SUBST(GTKVERSION)
1065
1066 AC_SUBST(enable_web_ide)
1067 AC_SUBST(enable_js_of_ocaml)
1068 AC_SUBST(JSOFOCAMLPKG)
1069
1070 AC_SUBST(META_OCAMLGRAPH)
1071
1072 AC_SUBST(enable_ppx)
1073
1074 AC_SUBST(NUMINCLUDE)
1075 AC_SUBST(MLMPFRINCLUDE)
1076 AC_SUBST(MLMPFR)
1077 AC_SUBST(MLMPFR_LINK)
1078 AC_SUBST(found_mlmpfr)
1079
1080 AC_SUBST(enable_zarith)
1081 AC_SUBST(BIGINTINCLUDE)
1082 AC_SUBST(BIGINTLIB)
1083 AC_SUBST(BIGINTPKG)
1084
1085 AC_SUBST(enable_zip)
1086 AC_SUBST(ZIPINCLUDE)
1087 AC_SUBST(ZIPLIB)
1088
1089 AC_SUBST(MENHIRINCLUDE)
1090
1091 AC_SUBST(SEQINCLUDE)
1092 AC_SUBST(SEQLIB)
1093
1094 AC_SUBST(enable_re)
1095 AC_SUBST(REINCLUDE)
1096 AC_SUBST(RELIB)
1097
1098 AC_SUBST(enable_coq_libs)
1099 AC_SUBST(enable_coq_fp_libs)
1100 AC_SUBST(coq_compat_version)
1101
1102 AC_SUBST(COQC)
1103 AC_SUBST(COQDEP)
1104 AC_SUBST(COQLIB)
1105 AC_SUBST(COQVERSION)
1106
1107 AC_SUBST(enable_pvs_libs)
1108 AC_SUBST(PVS)
1109 AC_SUBST(PVSVERSION)
1110
1111 AC_SUBST(enable_isabelle_libs)
1112 AC_SUBST(ISABELLE)
1113 AC_SUBST(ISABELLEVERSION)
1114
1115 AC_SUBST(enable_hypothesis_selection)
1116
1117 AC_SUBST(enable_doc)
1118 AC_SUBST(enable_pdf_doc)
1119
1120 AC_SUBST(LATEX)
1121 AC_SUBST(SPHINX)
1122
1123 AC_SUBST(enable_emacs_compilation)
1124 AC_SUBST(EMACS)
1125
1126 AC_SUBST(enable_frama_c)
1127
1128 AC_SUBST(FRAMAC)
1129 AC_SUBST(FRAMAC_VERSION)
1130 AC_SUBST(FRAMAC_SHARE)
1131 AC_SUBST(FRAMAC_LIBDIR)
1132 AC_SUBST(FRAMAC_INCLUDE)
1133
1134 AC_SUBST(enable_local)
1135 AC_SUBST(LOCALDIR)
1136
1137 AC_SUBST(enable_why3_lib)
1138 AC_SUBST(WHY3LIB)
1139 AC_SUBST(WHY3INCLUDE)
1140
1141 AC_SUBST(enable_relocation)
1142
1143 # Finally create the Makefile from Makefile.in
1144 AC_CONFIG_FILES(Makefile)
1145 AC_CONFIG_FILES(src/config.sh)
1146 AC_CONFIG_FILES(lib/why3/META)
1147 AC_CONFIG_FILES(.merlin)
1148 AC_CONFIG_FILES(src/jessie/Makefile)
1149 AC_CONFIG_FILES(src/jessie/.merlin)
1150 AC_CONFIG_FILES(lib/coq/version lib/pvs/version)
1151 AC_CONFIG_COMMANDS([chmod],
1152 chmod a-w Makefile src/jessie/Makefile;
1153 chmod a-w src/config.sh;
1154 chmod a-w lib/why3/META;
1155 chmod a-w .merlin;
1156 chmod a-w src/jessie/Makefile;
1157 chmod a-w src/jessie/.merlin;
1158 chmod a-w lib/coq/version lib/pvs/version;
1159 chmod u+x src/config.sh)
1160
1161 AC_OUTPUT
1162
1163
1164 # Summary
1165
1166 echo
1167 echo "                 Summary"
1168 echo "-----------------------------------------"
1169 echo "Verbose make                : $enable_verbose_make"
1170 echo "OCaml compiler              : yes"
1171 echo "    Version                 : $OCAMLVERSION"
1172 echo "    Library path            : $OCAMLLIB"
1173 echo "    Ocamlfind               : $enable_ocamlfind$reason_ocamlfind"
1174 echo "    Native compilation      : $enable_native_code"
1175 echo "    Profiling               : $enable_profiling"
1176 echo "    Memory profiling        : $enable_statmemprof$reason_statmemprof"
1177 echo "    PPX                     : $enable_ppx$reason_ppx"
1178 echo "    Javascript support      : $enable_js_of_ocaml$reason_js_of_ocaml"
1179 echo "    Mpfr support            : $found_mlmpfr$reason_mlmpfr"
1180 echo "    Re support              : $enable_re$reason_re"
1181 echo "Components"
1182 echo "    Why3 library            : $enable_why3_lib"
1183 echo "    GTK IDE                 : $enable_ide$reason_ide"
1184 echo "    Web IDE                 : $enable_web_ide$reason_web_ide"
1185 echo "    GMP arithmetic          : $enable_zarith$reason_zarith"
1186 echo "    Compressed sessions     : $enable_zip$reason_zip"
1187 echo "    Hypothesis selection    : $enable_hypothesis_selection$reason_hypothesis_selection"
1188 echo "    Frama-C support         : $enable_frama_c$reason_frama_c"
1189 if test "$enable_frama_c" = yes ; then
1190    echo "        Version             : $FRAMAC_VERSION"
1191    echo "        Share path          : $FRAMAC_SHARE"
1192    echo "        Library path        : $FRAMAC_LIBDIR"
1193 fi
1194 echo "Documentation               : $enable_doc$reason_doc"
1195 if test "$enable_doc" = yes ; then
1196    echo "    HTML                    : yes"
1197    echo "    PDF                     : $enable_pdf_doc$reason_pdf_doc"
1198 fi
1199 echo "Support for interactive proof assistants"
1200 echo "    Coq                     : $enable_coq_support$reason_coq_support"
1201 if test "$enable_coq_support" = yes ; then
1202    echo "        Version             : $COQVERSION"
1203    echo "        Library path        : $COQLIB"
1204    echo "        Realization support : $enable_coq_libs$reason_coq_libs"
1205    if test "$enable_coq_libs" = yes ; then
1206       echo "            FP arithmetic   : $enable_coq_fp_libs$reason_coq_fp_libs"
1207    fi
1208 fi
1209 echo "    PVS                     : $enable_pvs_support$reason_pvs_support"
1210 if test "$enable_pvs_support" = yes ; then
1211    echo "        Version             : $PVSVERSION"
1212    echo "        Library path        : $PVSLIB"
1213    echo "        Realization support : $enable_pvs_libs$reason_pvs_libs"
1214 fi
1215 echo "    Isabelle                : $enable_isabelle_support$reason_isabelle_support"
1216 if test "$enable_isabelle_support" = yes ; then
1217    echo "        Version             : $ISABELLEVERSION ($ISABELLEDETECTEDVERSION)"
1218    echo "        Realization support : $enable_isabelle_libs$reason_isabelle_libs"
1219 fi
1220 if test "$enable_local" = yes ; then
1221    echo "Installable                 : no"
1222    echo "    OCaml library path      : $OCAMLINSTALLLIB/why3"
1223 else
1224    echo "Installable                 : yes"
1225    echo "    Binary path             : $bindir"
1226    echo "    Library path            : $libdir/why3"
1227    echo "    Data path               : $datarootdir/why3"
1228    echo "    OCaml library path      : $OCAMLINSTALLLIB/why3"
1229    echo "    Relocatable             : $enable_relocation"
1230 fi