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