configure.in

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