#! /bin/sh # Guess values for system-dependent variables and create Makefiles. # Generated by GNU Autoconf 2.72 for Why3 1.8.2+git. # # # Copyright (C) 1992-1996, 1998-2017, 2020-2023 Free Software Foundation, # Inc. # # # This configure script is free software; the Free Software Foundation # gives unlimited permission to copy, distribute and modify it. ## -------------------- ## ## M4sh Initialization. ## ## -------------------- ## # Be more Bourne compatible DUALCASE=1; export DUALCASE # for MKS sh if test ${ZSH_VERSION+y} && (emulate sh) >/dev/null 2>&1 then : emulate sh NULLCMD=: # Pre-4.2 versions of Zsh do word splitting on ${1+"$@"}, which # is contrary to our usage. Disable this feature. alias -g '${1+"$@"}'='"$@"' setopt NO_GLOB_SUBST else case e in #( e) case `(set -o) 2>/dev/null` in #( *posix*) : set -o posix ;; #( *) : ;; esac ;; esac fi # Reset variables that may have inherited troublesome values from # the environment. # IFS needs to be set, to space, tab, and newline, in precisely that order. # (If _AS_PATH_WALK were called with IFS unset, it would have the # side effect of setting IFS to empty, thus disabling word splitting.) # Quoting is to prevent editors from complaining about space-tab. as_nl=' ' export as_nl IFS=" "" $as_nl" PS1='$ ' PS2='> ' PS4='+ ' # Ensure predictable behavior from utilities with locale-dependent output. LC_ALL=C export LC_ALL LANGUAGE=C export LANGUAGE # We cannot yet rely on "unset" to work, but we need these variables # to be unset--not just set to an empty or harmless value--now, to # avoid bugs in old shells (e.g. pre-3.0 UWIN ksh). This construct # also avoids known problems related to "unset" and subshell syntax # in other old shells (e.g. bash 2.01 and pdksh 5.2.14). for as_var in BASH_ENV ENV MAIL MAILPATH CDPATH do eval test \${$as_var+y} \ && ( (unset $as_var) || exit 1) >/dev/null 2>&1 && unset $as_var || : done # Ensure that fds 0, 1, and 2 are open. if (exec 3>&0) 2>/dev/null; then :; else exec 0&1) 2>/dev/null; then :; else exec 1>/dev/null; fi if (exec 3>&2) ; then :; else exec 2>/dev/null; fi # The user is always right. if ${PATH_SEPARATOR+false} :; then PATH_SEPARATOR=: (PATH='/bin;/bin'; FPATH=$PATH; sh -c :) >/dev/null 2>&1 && { (PATH='/bin:/bin'; FPATH=$PATH; sh -c :) >/dev/null 2>&1 || PATH_SEPARATOR=';' } fi # Find who we are. Look in the path if we contain no directory separator. as_myself= case $0 in #(( *[\\/]* ) as_myself=$0 ;; *) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac test -r "$as_dir$0" && as_myself=$as_dir$0 && break done IFS=$as_save_IFS ;; esac # We did not find ourselves, most probably we were run as 'sh COMMAND' # in which case we are not to be found in the path. if test "x$as_myself" = x; then as_myself=$0 fi if test ! -f "$as_myself"; then printf "%s\n" "$as_myself: error: cannot find myself; rerun with an absolute file name" >&2 exit 1 fi # Use a proper internal environment variable to ensure we don't fall # into an infinite loop, continuously re-executing ourselves. if test x"${_as_can_reexec}" != xno && test "x$CONFIG_SHELL" != x; then _as_can_reexec=no; export _as_can_reexec; # We cannot yet assume a decent shell, so we have to provide a # neutralization value for shells without unset; and this also # works around shells that cannot unset nonexistent variables. # Preserve -v and -x to the replacement shell. BASH_ENV=/dev/null ENV=/dev/null (unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV case $- in # (((( *v*x* | *x*v* ) as_opts=-vx ;; *v* ) as_opts=-v ;; *x* ) as_opts=-x ;; * ) as_opts= ;; esac exec $CONFIG_SHELL $as_opts "$as_myself" ${1+"$@"} # Admittedly, this is quite paranoid, since all the known shells bail # out after a failed 'exec'. printf "%s\n" "$0: could not re-execute with $CONFIG_SHELL" >&2 exit 255 fi # We don't want this to propagate to other subprocesses. { _as_can_reexec=; unset _as_can_reexec;} if test "x$CONFIG_SHELL" = x; then as_bourne_compatible="if test \${ZSH_VERSION+y} && (emulate sh) >/dev/null 2>&1 then : emulate sh NULLCMD=: # Pre-4.2 versions of Zsh do word splitting on \${1+\"\$@\"}, which # is contrary to our usage. Disable this feature. alias -g '\${1+\"\$@\"}'='\"\$@\"' setopt NO_GLOB_SUBST else case e in #( e) case \`(set -o) 2>/dev/null\` in #( *posix*) : set -o posix ;; #( *) : ;; esac ;; esac fi " as_required="as_fn_return () { (exit \$1); } as_fn_success () { as_fn_return 0; } as_fn_failure () { as_fn_return 1; } as_fn_ret_success () { return 0; } as_fn_ret_failure () { return 1; } exitcode=0 as_fn_success || { exitcode=1; echo as_fn_success failed.; } as_fn_failure && { exitcode=1; echo as_fn_failure succeeded.; } as_fn_ret_success || { exitcode=1; echo as_fn_ret_success failed.; } as_fn_ret_failure && { exitcode=1; echo as_fn_ret_failure succeeded.; } if ( set x; as_fn_ret_success y && test x = \"\$1\" ) then : else case e in #( e) exitcode=1; echo positional parameters were not saved. ;; esac fi test x\$exitcode = x0 || exit 1 blah=\$(echo \$(echo blah)) test x\"\$blah\" = xblah || exit 1 test -x / || exit 1" as_suggested=" as_lineno_1=";as_suggested=$as_suggested$LINENO;as_suggested=$as_suggested" as_lineno_1a=\$LINENO as_lineno_2=";as_suggested=$as_suggested$LINENO;as_suggested=$as_suggested" as_lineno_2a=\$LINENO eval 'test \"x\$as_lineno_1'\$as_run'\" != \"x\$as_lineno_2'\$as_run'\" && test \"x\`expr \$as_lineno_1'\$as_run' + 1\`\" = \"x\$as_lineno_2'\$as_run'\"' || exit 1" if (eval "$as_required") 2>/dev/null then : as_have_required=yes else case e in #( e) as_have_required=no ;; esac fi if test x$as_have_required = xyes && (eval "$as_suggested") 2>/dev/null then : else case e in #( e) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR as_found=false for as_dir in /bin$PATH_SEPARATOR/usr/bin$PATH_SEPARATOR$PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac as_found=: case $as_dir in #( /*) for as_base in sh bash ksh sh5; do # Try only shells that exist, to save several forks. as_shell=$as_dir$as_base if { test -f "$as_shell" || test -f "$as_shell.exe"; } && as_run=a "$as_shell" -c "$as_bourne_compatible""$as_required" 2>/dev/null then : CONFIG_SHELL=$as_shell as_have_required=yes if as_run=a "$as_shell" -c "$as_bourne_compatible""$as_suggested" 2>/dev/null then : break 2 fi fi done;; esac as_found=false done IFS=$as_save_IFS if $as_found then : else case e in #( e) if { test -f "$SHELL" || test -f "$SHELL.exe"; } && as_run=a "$SHELL" -c "$as_bourne_compatible""$as_required" 2>/dev/null then : CONFIG_SHELL=$SHELL as_have_required=yes fi ;; esac fi if test "x$CONFIG_SHELL" != x then : export CONFIG_SHELL # We cannot yet assume a decent shell, so we have to provide a # neutralization value for shells without unset; and this also # works around shells that cannot unset nonexistent variables. # Preserve -v and -x to the replacement shell. BASH_ENV=/dev/null ENV=/dev/null (unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV case $- in # (((( *v*x* | *x*v* ) as_opts=-vx ;; *v* ) as_opts=-v ;; *x* ) as_opts=-x ;; * ) as_opts= ;; esac exec $CONFIG_SHELL $as_opts "$as_myself" ${1+"$@"} # Admittedly, this is quite paranoid, since all the known shells bail # out after a failed 'exec'. printf "%s\n" "$0: could not re-execute with $CONFIG_SHELL" >&2 exit 255 fi if test x$as_have_required = xno then : printf "%s\n" "$0: This script requires a shell more modern than all" printf "%s\n" "$0: the shells that I found on your system." if test ${ZSH_VERSION+y} ; then printf "%s\n" "$0: In particular, zsh $ZSH_VERSION has bugs and should" printf "%s\n" "$0: be upgraded to zsh 4.3.4 or later." else printf "%s\n" "$0: Please tell bug-autoconf@gnu.org about your system, $0: including any error possibly output before this $0: message. Then install a modern shell, or manually run $0: the script under such a shell if you do have one." fi exit 1 fi ;; esac fi fi SHELL=${CONFIG_SHELL-/bin/sh} export SHELL # Unset more variables known to interfere with behavior of common tools. CLICOLOR_FORCE= GREP_OPTIONS= unset CLICOLOR_FORCE GREP_OPTIONS ## --------------------- ## ## M4sh Shell Functions. ## ## --------------------- ## # as_fn_unset VAR # --------------- # Portably unset VAR. as_fn_unset () { { eval $1=; unset $1;} } as_unset=as_fn_unset # as_fn_set_status STATUS # ----------------------- # Set $? to STATUS, without forking. as_fn_set_status () { return $1 } # as_fn_set_status # as_fn_exit STATUS # ----------------- # Exit the shell with STATUS, even in a "trap 0" or "set -e" context. as_fn_exit () { set +e as_fn_set_status $1 exit $1 } # as_fn_exit # as_fn_mkdir_p # ------------- # Create "$as_dir" as a directory, including parents if necessary. as_fn_mkdir_p () { case $as_dir in #( -*) as_dir=./$as_dir;; esac test -d "$as_dir" || eval $as_mkdir_p || { as_dirs= while :; do case $as_dir in #( *\'*) as_qdir=`printf "%s\n" "$as_dir" | sed "s/'/'\\\\\\\\''/g"`;; #'( *) as_qdir=$as_dir;; esac as_dirs="'$as_qdir' $as_dirs" as_dir=`$as_dirname -- "$as_dir" || $as_expr X"$as_dir" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ X"$as_dir" : 'X\(//\)[^/]' \| \ X"$as_dir" : 'X\(//\)$' \| \ X"$as_dir" : 'X\(/\)' \| . 2>/dev/null || printf "%s\n" X"$as_dir" | sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ s//\1/ q } /^X\(\/\/\)[^/].*/{ s//\1/ q } /^X\(\/\/\)$/{ s//\1/ q } /^X\(\/\).*/{ s//\1/ q } s/.*/./; q'` test -d "$as_dir" && break done test -z "$as_dirs" || eval "mkdir $as_dirs" } || test -d "$as_dir" || as_fn_error $? "cannot create directory $as_dir" } # as_fn_mkdir_p # as_fn_executable_p FILE # ----------------------- # Test if FILE is an executable regular file. as_fn_executable_p () { test -f "$1" && test -x "$1" } # as_fn_executable_p # as_fn_append VAR VALUE # ---------------------- # Append the text in VALUE to the end of the definition contained in VAR. Take # advantage of any shell optimizations that allow amortized linear growth over # repeated appends, instead of the typical quadratic growth present in naive # implementations. if (eval "as_var=1; as_var+=2; test x\$as_var = x12") 2>/dev/null then : eval 'as_fn_append () { eval $1+=\$2 }' else case e in #( e) as_fn_append () { eval $1=\$$1\$2 } ;; esac fi # as_fn_append # as_fn_arith ARG... # ------------------ # Perform arithmetic evaluation on the ARGs, and store the result in the # global $as_val. Take advantage of shells that can avoid forks. The arguments # must be portable across $(()) and expr. if (eval "test \$(( 1 + 1 )) = 2") 2>/dev/null then : eval 'as_fn_arith () { as_val=$(( $* )) }' else case e in #( e) as_fn_arith () { as_val=`expr "$@" || test $? -eq 1` } ;; esac fi # as_fn_arith # as_fn_error STATUS ERROR [LINENO LOG_FD] # ---------------------------------------- # Output "`basename $0`: error: ERROR" to stderr. If LINENO and LOG_FD are # provided, also output the error to LOG_FD, referencing LINENO. Then exit the # script with STATUS, using 1 if that was 0. as_fn_error () { as_status=$1; test $as_status -eq 0 && as_status=1 if test "$4"; then as_lineno=${as_lineno-"$3"} as_lineno_stack=as_lineno_stack=$as_lineno_stack printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: $2" >&$4 fi printf "%s\n" "$as_me: error: $2" >&2 as_fn_exit $as_status } # as_fn_error if expr a : '\(a\)' >/dev/null 2>&1 && test "X`expr 00001 : '.*\(...\)'`" = X001; then as_expr=expr else as_expr=false fi if (basename -- /) >/dev/null 2>&1 && test "X`basename -- / 2>&1`" = "X/"; then as_basename=basename else as_basename=false fi if (as_dir=`dirname -- /` && test "X$as_dir" = X/) >/dev/null 2>&1; then as_dirname=dirname else as_dirname=false fi as_me=`$as_basename -- "$0" || $as_expr X/"$0" : '.*/\([^/][^/]*\)/*$' \| \ X"$0" : 'X\(//\)$' \| \ X"$0" : 'X\(/\)' \| . 2>/dev/null || printf "%s\n" X/"$0" | sed '/^.*\/\([^/][^/]*\)\/*$/{ s//\1/ q } /^X\/\(\/\/\)$/{ s//\1/ q } /^X\/\(\/\).*/{ s//\1/ q } s/.*/./; q'` # Avoid depending upon Character Ranges. as_cr_letters='abcdefghijklmnopqrstuvwxyz' as_cr_LETTERS='ABCDEFGHIJKLMNOPQRSTUVWXYZ' as_cr_Letters=$as_cr_letters$as_cr_LETTERS as_cr_digits='0123456789' as_cr_alnum=$as_cr_Letters$as_cr_digits as_lineno_1=$LINENO as_lineno_1a=$LINENO as_lineno_2=$LINENO as_lineno_2a=$LINENO eval 'test "x$as_lineno_1'$as_run'" != "x$as_lineno_2'$as_run'" && test "x`expr $as_lineno_1'$as_run' + 1`" = "x$as_lineno_2'$as_run'"' || { # Blame Lee E. McMahon (1931-1989) for sed's syntax. :-) sed -n ' p /[$]LINENO/= ' <$as_myself | sed ' t clear :clear s/[$]LINENO.*/&-/ t lineno b :lineno N :loop s/[$]LINENO\([^'$as_cr_alnum'_].*\n\)\(.*\)/\2\1\2/ t loop s/-\n.*// ' >$as_me.lineno && chmod +x "$as_me.lineno" || { printf "%s\n" "$as_me: error: cannot create $as_me.lineno; rerun with a POSIX shell" >&2; as_fn_exit 1; } # If we had to re-execute with $CONFIG_SHELL, we're ensured to have # already done that, so ensure we don't try to do so again and fall # in an infinite loop. This has already happened in practice. _as_can_reexec=no; export _as_can_reexec # Don't try to exec as it changes $[0], causing all sort of problems # (the dirname of $[0] is not the place where we might find the # original and so on. Autoconf is especially sensitive to this). . "./$as_me.lineno" # Exit status is that of the last command. exit } # Determine whether it's possible to make 'echo' print without a newline. # These variables are no longer used directly by Autoconf, but are AC_SUBSTed # for compatibility with existing Makefiles. ECHO_C= ECHO_N= ECHO_T= case `echo -n x` in #((((( -n*) case `echo 'xy\c'` in *c*) ECHO_T=' ';; # ECHO_T is single tab character. xy) ECHO_C='\c';; *) echo `echo ksh88 bug on AIX 6.1` > /dev/null ECHO_T=' ';; esac;; *) ECHO_N='-n';; esac # For backward compatibility with old third-party macros, we provide # the shell variables $as_echo and $as_echo_n. New code should use # AS_ECHO(["message"]) and AS_ECHO_N(["message"]), respectively. as_echo='printf %s\n' as_echo_n='printf %s' rm -f conf$$ conf$$.exe conf$$.file if test -d conf$$.dir; then rm -f conf$$.dir/conf$$.file else rm -f conf$$.dir mkdir conf$$.dir 2>/dev/null fi if (echo >conf$$.file) 2>/dev/null; then if ln -s conf$$.file conf$$ 2>/dev/null; then as_ln_s='ln -s' # ... but there are two gotchas: # 1) On MSYS, both 'ln -s file dir' and 'ln file dir' fail. # 2) DJGPP < 2.04 has no symlinks; 'ln -s' creates a wrapper executable. # In both cases, we have to default to 'cp -pR'. ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe || as_ln_s='cp -pR' elif ln conf$$.file conf$$ 2>/dev/null; then as_ln_s=ln else as_ln_s='cp -pR' fi else as_ln_s='cp -pR' fi rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file rmdir conf$$.dir 2>/dev/null if mkdir -p . 2>/dev/null; then as_mkdir_p='mkdir -p "$as_dir"' else test -d ./-p && rmdir ./-p as_mkdir_p=false fi as_test_x='test -x' as_executable_p=as_fn_executable_p # Sed expression to map a string onto a valid CPP name. as_sed_cpp="y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g" as_tr_cpp="eval sed '$as_sed_cpp'" # deprecated # Sed expression to map a string onto a valid variable name. as_sed_sh="y%*+%pp%;s%[^_$as_cr_alnum]%_%g" as_tr_sh="eval sed '$as_sed_sh'" # deprecated as_awk_strverscmp=' # Use only awk features that work with 7th edition Unix awk (1978). # My, what an old awk you have, Mr. Solaris! END { while (length(v1) && length(v2)) { # Set d1 to be the next thing to compare from v1, and likewise for d2. # Normally this is a single character, but if v1 and v2 contain digits, # compare them as integers and fractions as strverscmp does. if (v1 ~ /^[0-9]/ && v2 ~ /^[0-9]/) { # Split v1 and v2 into their leading digit string components d1 and d2, # and advance v1 and v2 past the leading digit strings. for (len1 = 1; substr(v1, len1 + 1) ~ /^[0-9]/; len1++) continue for (len2 = 1; substr(v2, len2 + 1) ~ /^[0-9]/; len2++) continue d1 = substr(v1, 1, len1); v1 = substr(v1, len1 + 1) d2 = substr(v2, 1, len2); v2 = substr(v2, len2 + 1) if (d1 ~ /^0/) { if (d2 ~ /^0/) { # Compare two fractions. while (d1 ~ /^0/ && d2 ~ /^0/) { d1 = substr(d1, 2); len1-- d2 = substr(d2, 2); len2-- } if (len1 != len2 && ! (len1 && len2 && substr(d1, 1, 1) == substr(d2, 1, 1))) { # The two components differ in length, and the common prefix # contains only leading zeros. Consider the longer to be less. d1 = -len1 d2 = -len2 } else { # Otherwise, compare as strings. d1 = "x" d1 d2 = "x" d2 } } else { # A fraction is less than an integer. exit 1 } } else { if (d2 ~ /^0/) { # An integer is greater than a fraction. exit 2 } else { # Compare two integers. d1 += 0 d2 += 0 } } } else { # The normal case, without worrying about digits. d1 = substr(v1, 1, 1); v1 = substr(v1, 2) d2 = substr(v2, 1, 1); v2 = substr(v2, 2) } if (d1 < d2) exit 1 if (d1 > d2) exit 2 } # Beware Solaris /usr/xgp4/bin/awk (at least through Solaris 10), # which mishandles some comparisons of empty strings to integers. if (length(v2)) exit 1 if (length(v1)) exit 2 } ' test -n "$DJDIR" || exec 7<&0 &1 # Name of the host. # hostname on some systems (SVR3.2, old GNU/Linux) returns a bogus exit status, # so uname gets run too. ac_hostname=`(hostname || uname -n) 2>/dev/null | sed 1q` # # Initializations. # ac_default_prefix=/usr/local ac_clean_files= ac_config_libobj_dir=. LIBOBJS= cross_compiling=no subdirs= MFLAGS= MAKEFLAGS= # Identity of this package. PACKAGE_NAME='Why3' PACKAGE_TARNAME='why3' PACKAGE_VERSION='1.8.2+git' PACKAGE_STRING='Why3 1.8.2+git' PACKAGE_BUGREPORT='' PACKAGE_URL='' ac_subst_vars='LTLIBOBJS LIBOBJS enable_relocation WHY3INCLUDE WHY3LIB enable_why3_lib LOCALDIR enable_local FRAMAC_INCLUDE FRAMAC_LIBDIR FRAMAC_SHARE FRAMAC_VERSION enable_frama_c enable_emacs_compilation enable_pdf_doc enable_doc enable_stackify enable_hypothesis_selection ISABELLEVERSION enable_isabelle_libs PVSVERSION enable_pvs_libs COQFLAGS COQVERSION COQLIB coq_compat_version enable_coq_fp_libs enable_coq_libs RELIB REINCLUDE enable_re MENHIRINCLUDE ZIPLIB ZIPINCLUDE enable_zip INFERPKG INFERLIB INFERINCLUDE enable_bddinfer enable_infer BIGINTINCLUDE old_mpfr enable_mpfr MLMPFR SEXPLIBPPX SEXPLIB enable_sexp enable_ppx META_OCAMLGRAPH JSOFOCAMLPKG enable_js_of_ocaml enable_web_ide GTKVERSION LABLGTKPKG enable_ide STATMEMPROFPKG enable_statmemprof enable_ocamlfind OCAMLGRAPHLIB OCAMLINSTALLLIB OCAMLLIB OCAMLVERSION OCAMLBEST OCAML_OS_TYPE BUILD_ENV_TYPE STRIP EXE enable_verbose_make VERSION JAVA JAVAC FRAMAC ISABELLE PVS COQDEP COQC menhirlib_cmo EMACS LATEX SPHINX OCAMLFIND MENHIR OCAMLDOCOPT OCAMLDOC OCAMLYACC OCAMLLEXDOTOPT OCAMLLEX OCAMLDEPDOTOPT OCAMLDEP OCAMLOPTDOTOPT OCAMLCDOTOPT OCAMLOPT INSTALL_DATA INSTALL_SCRIPT INSTALL_PROGRAM MKDIR_P OBJEXT EXEEXT ac_ct_CC CPPFLAGS LDFLAGS CFLAGS CC OCAMLC EDITOR target_alias host_alias build_alias LIBS ECHO_T ECHO_N ECHO_C DEFS mandir localedir libdir psdir pdfdir dvidir htmldir infodir docdir oldincludedir includedir runstatedir localstatedir sharedstatedir sysconfdir datadir datarootdir libexecdir sbindir bindir program_transform_name prefix exec_prefix PACKAGE_URL PACKAGE_BUGREPORT PACKAGE_STRING PACKAGE_VERSION PACKAGE_TARNAME PACKAGE_NAME PATH_SEPARATOR SHELL' ac_subst_files='' ac_user_opts=' enable_option_checking enable_verbose_make enable_local enable_relocation enable_native_code enable_why3_lib enable_ocamlfind enable_zip enable_infer enable_bddinfer enable_js_of_ocaml enable_re enable_sexp enable_ide enable_web_ide enable_coq_libs enable_pvs_libs enable_isabelle_libs enable_mpfr enable_hypothesis_selection enable_stackify enable_doc enable_html_pdf enable_frama_c enable_statmemprof enable_emacs_compilation enable_java ' ac_precious_vars='build_alias host_alias target_alias EDITOR CC CFLAGS LDFLAGS LIBS CPPFLAGS' # Initialize some variables set by options. ac_init_help= ac_init_version=false ac_unrecognized_opts= ac_unrecognized_sep= # The variables have the same names as the options, with # dashes changed to underlines. cache_file=/dev/null exec_prefix=NONE no_create= no_recursion= prefix=NONE program_prefix=NONE program_suffix=NONE program_transform_name=s,x,x, silent= site= srcdir= verbose= x_includes=NONE x_libraries=NONE # Installation directory options. # These are left unexpanded so users can "make install exec_prefix=/foo" # and all the variables that are supposed to be based on exec_prefix # by default will actually change. # Use braces instead of parens because sh, perl, etc. also accept them. # (The list follows the same order as the GNU Coding Standards.) bindir='${exec_prefix}/bin' sbindir='${exec_prefix}/sbin' libexecdir='${exec_prefix}/libexec' datarootdir='${prefix}/share' datadir='${datarootdir}' sysconfdir='${prefix}/etc' sharedstatedir='${prefix}/com' localstatedir='${prefix}/var' runstatedir='${localstatedir}/run' includedir='${prefix}/include' oldincludedir='/usr/include' docdir='${datarootdir}/doc/${PACKAGE_TARNAME}' infodir='${datarootdir}/info' htmldir='${docdir}' dvidir='${docdir}' pdfdir='${docdir}' psdir='${docdir}' libdir='${exec_prefix}/lib' localedir='${datarootdir}/locale' mandir='${datarootdir}/man' ac_prev= ac_dashdash= for ac_option do # If the previous option needs an argument, assign it. if test -n "$ac_prev"; then eval $ac_prev=\$ac_option ac_prev= continue fi case $ac_option in *=?*) ac_optarg=`expr "X$ac_option" : '[^=]*=\(.*\)'` ;; *=) ac_optarg= ;; *) ac_optarg=yes ;; esac case $ac_dashdash$ac_option in --) ac_dashdash=yes ;; -bindir | --bindir | --bindi | --bind | --bin | --bi) ac_prev=bindir ;; -bindir=* | --bindir=* | --bindi=* | --bind=* | --bin=* | --bi=*) bindir=$ac_optarg ;; -build | --build | --buil | --bui | --bu) ac_prev=build_alias ;; -build=* | --build=* | --buil=* | --bui=* | --bu=*) build_alias=$ac_optarg ;; -cache-file | --cache-file | --cache-fil | --cache-fi \ | --cache-f | --cache- | --cache | --cach | --cac | --ca | --c) ac_prev=cache_file ;; -cache-file=* | --cache-file=* | --cache-fil=* | --cache-fi=* \ | --cache-f=* | --cache-=* | --cache=* | --cach=* | --cac=* | --ca=* | --c=*) cache_file=$ac_optarg ;; --config-cache | -C) cache_file=config.cache ;; -datadir | --datadir | --datadi | --datad) ac_prev=datadir ;; -datadir=* | --datadir=* | --datadi=* | --datad=*) datadir=$ac_optarg ;; -datarootdir | --datarootdir | --datarootdi | --datarootd | --dataroot \ | --dataroo | --dataro | --datar) ac_prev=datarootdir ;; -datarootdir=* | --datarootdir=* | --datarootdi=* | --datarootd=* \ | --dataroot=* | --dataroo=* | --dataro=* | --datar=*) datarootdir=$ac_optarg ;; -disable-* | --disable-*) ac_useropt=`expr "x$ac_option" : 'x-*disable-\(.*\)'` # Reject names that are not valid shell variable names. expr "x$ac_useropt" : ".*[^-+._$as_cr_alnum]" >/dev/null && as_fn_error $? "invalid feature name: '$ac_useropt'" ac_useropt_orig=$ac_useropt ac_useropt=`printf "%s\n" "$ac_useropt" | sed 's/[-+.]/_/g'` case $ac_user_opts in *" "enable_$ac_useropt" "*) ;; *) ac_unrecognized_opts="$ac_unrecognized_opts$ac_unrecognized_sep--disable-$ac_useropt_orig" ac_unrecognized_sep=', ';; esac eval enable_$ac_useropt=no ;; -docdir | --docdir | --docdi | --doc | --do) ac_prev=docdir ;; -docdir=* | --docdir=* | --docdi=* | --doc=* | --do=*) docdir=$ac_optarg ;; -dvidir | --dvidir | --dvidi | --dvid | --dvi | --dv) ac_prev=dvidir ;; -dvidir=* | --dvidir=* | --dvidi=* | --dvid=* | --dvi=* | --dv=*) dvidir=$ac_optarg ;; -enable-* | --enable-*) ac_useropt=`expr "x$ac_option" : 'x-*enable-\([^=]*\)'` # Reject names that are not valid shell variable names. expr "x$ac_useropt" : ".*[^-+._$as_cr_alnum]" >/dev/null && as_fn_error $? "invalid feature name: '$ac_useropt'" ac_useropt_orig=$ac_useropt ac_useropt=`printf "%s\n" "$ac_useropt" | sed 's/[-+.]/_/g'` case $ac_user_opts in *" "enable_$ac_useropt" "*) ;; *) ac_unrecognized_opts="$ac_unrecognized_opts$ac_unrecognized_sep--enable-$ac_useropt_orig" ac_unrecognized_sep=', ';; esac eval enable_$ac_useropt=\$ac_optarg ;; -exec-prefix | --exec_prefix | --exec-prefix | --exec-prefi \ | --exec-pref | --exec-pre | --exec-pr | --exec-p | --exec- \ | --exec | --exe | --ex) ac_prev=exec_prefix ;; -exec-prefix=* | --exec_prefix=* | --exec-prefix=* | --exec-prefi=* \ | --exec-pref=* | --exec-pre=* | --exec-pr=* | --exec-p=* | --exec-=* \ | --exec=* | --exe=* | --ex=*) exec_prefix=$ac_optarg ;; -gas | --gas | --ga | --g) # Obsolete; use --with-gas. with_gas=yes ;; -help | --help | --hel | --he | -h) ac_init_help=long ;; -help=r* | --help=r* | --hel=r* | --he=r* | -hr*) ac_init_help=recursive ;; -help=s* | --help=s* | --hel=s* | --he=s* | -hs*) ac_init_help=short ;; -host | --host | --hos | --ho) ac_prev=host_alias ;; -host=* | --host=* | --hos=* | --ho=*) host_alias=$ac_optarg ;; -htmldir | --htmldir | --htmldi | --htmld | --html | --htm | --ht) ac_prev=htmldir ;; -htmldir=* | --htmldir=* | --htmldi=* | --htmld=* | --html=* | --htm=* \ | --ht=*) htmldir=$ac_optarg ;; -includedir | --includedir | --includedi | --included | --include \ | --includ | --inclu | --incl | --inc) ac_prev=includedir ;; -includedir=* | --includedir=* | --includedi=* | --included=* | --include=* \ | --includ=* | --inclu=* | --incl=* | --inc=*) includedir=$ac_optarg ;; -infodir | --infodir | --infodi | --infod | --info | --inf) ac_prev=infodir ;; -infodir=* | --infodir=* | --infodi=* | --infod=* | --info=* | --inf=*) infodir=$ac_optarg ;; -libdir | --libdir | --libdi | --libd) ac_prev=libdir ;; -libdir=* | --libdir=* | --libdi=* | --libd=*) libdir=$ac_optarg ;; -libexecdir | --libexecdir | --libexecdi | --libexecd | --libexec \ | --libexe | --libex | --libe) ac_prev=libexecdir ;; -libexecdir=* | --libexecdir=* | --libexecdi=* | --libexecd=* | --libexec=* \ | --libexe=* | --libex=* | --libe=*) libexecdir=$ac_optarg ;; -localedir | --localedir | --localedi | --localed | --locale) ac_prev=localedir ;; -localedir=* | --localedir=* | --localedi=* | --localed=* | --locale=*) localedir=$ac_optarg ;; -localstatedir | --localstatedir | --localstatedi | --localstated \ | --localstate | --localstat | --localsta | --localst | --locals) ac_prev=localstatedir ;; -localstatedir=* | --localstatedir=* | --localstatedi=* | --localstated=* \ | --localstate=* | --localstat=* | --localsta=* | --localst=* | --locals=*) localstatedir=$ac_optarg ;; -mandir | --mandir | --mandi | --mand | --man | --ma | --m) ac_prev=mandir ;; -mandir=* | --mandir=* | --mandi=* | --mand=* | --man=* | --ma=* | --m=*) mandir=$ac_optarg ;; -nfp | --nfp | --nf) # Obsolete; use --without-fp. with_fp=no ;; -no-create | --no-create | --no-creat | --no-crea | --no-cre \ | --no-cr | --no-c | -n) no_create=yes ;; -no-recursion | --no-recursion | --no-recursio | --no-recursi \ | --no-recurs | --no-recur | --no-recu | --no-rec | --no-re | --no-r) no_recursion=yes ;; -oldincludedir | --oldincludedir | --oldincludedi | --oldincluded \ | --oldinclude | --oldinclud | --oldinclu | --oldincl | --oldinc \ | --oldin | --oldi | --old | --ol | --o) ac_prev=oldincludedir ;; -oldincludedir=* | --oldincludedir=* | --oldincludedi=* | --oldincluded=* \ | --oldinclude=* | --oldinclud=* | --oldinclu=* | --oldincl=* | --oldinc=* \ | --oldin=* | --oldi=* | --old=* | --ol=* | --o=*) oldincludedir=$ac_optarg ;; -prefix | --prefix | --prefi | --pref | --pre | --pr | --p) ac_prev=prefix ;; -prefix=* | --prefix=* | --prefi=* | --pref=* | --pre=* | --pr=* | --p=*) prefix=$ac_optarg ;; -program-prefix | --program-prefix | --program-prefi | --program-pref \ | --program-pre | --program-pr | --program-p) ac_prev=program_prefix ;; -program-prefix=* | --program-prefix=* | --program-prefi=* \ | --program-pref=* | --program-pre=* | --program-pr=* | --program-p=*) program_prefix=$ac_optarg ;; -program-suffix | --program-suffix | --program-suffi | --program-suff \ | --program-suf | --program-su | --program-s) ac_prev=program_suffix ;; -program-suffix=* | --program-suffix=* | --program-suffi=* \ | --program-suff=* | --program-suf=* | --program-su=* | --program-s=*) program_suffix=$ac_optarg ;; -program-transform-name | --program-transform-name \ | --program-transform-nam | --program-transform-na \ | --program-transform-n | --program-transform- \ | --program-transform | --program-transfor \ | --program-transfo | --program-transf \ | --program-trans | --program-tran \ | --progr-tra | --program-tr | --program-t) ac_prev=program_transform_name ;; -program-transform-name=* | --program-transform-name=* \ | --program-transform-nam=* | --program-transform-na=* \ | --program-transform-n=* | --program-transform-=* \ | --program-transform=* | --program-transfor=* \ | --program-transfo=* | --program-transf=* \ | --program-trans=* | --program-tran=* \ | --progr-tra=* | --program-tr=* | --program-t=*) program_transform_name=$ac_optarg ;; -pdfdir | --pdfdir | --pdfdi | --pdfd | --pdf | --pd) ac_prev=pdfdir ;; -pdfdir=* | --pdfdir=* | --pdfdi=* | --pdfd=* | --pdf=* | --pd=*) pdfdir=$ac_optarg ;; -psdir | --psdir | --psdi | --psd | --ps) ac_prev=psdir ;; -psdir=* | --psdir=* | --psdi=* | --psd=* | --ps=*) psdir=$ac_optarg ;; -q | -quiet | --quiet | --quie | --qui | --qu | --q \ | -silent | --silent | --silen | --sile | --sil) silent=yes ;; -runstatedir | --runstatedir | --runstatedi | --runstated \ | --runstate | --runstat | --runsta | --runst | --runs \ | --run | --ru | --r) ac_prev=runstatedir ;; -runstatedir=* | --runstatedir=* | --runstatedi=* | --runstated=* \ | --runstate=* | --runstat=* | --runsta=* | --runst=* | --runs=* \ | --run=* | --ru=* | --r=*) runstatedir=$ac_optarg ;; -sbindir | --sbindir | --sbindi | --sbind | --sbin | --sbi | --sb) ac_prev=sbindir ;; -sbindir=* | --sbindir=* | --sbindi=* | --sbind=* | --sbin=* \ | --sbi=* | --sb=*) sbindir=$ac_optarg ;; -sharedstatedir | --sharedstatedir | --sharedstatedi \ | --sharedstated | --sharedstate | --sharedstat | --sharedsta \ | --sharedst | --shareds | --shared | --share | --shar \ | --sha | --sh) ac_prev=sharedstatedir ;; -sharedstatedir=* | --sharedstatedir=* | --sharedstatedi=* \ | --sharedstated=* | --sharedstate=* | --sharedstat=* | --sharedsta=* \ | --sharedst=* | --shareds=* | --shared=* | --share=* | --shar=* \ | --sha=* | --sh=*) sharedstatedir=$ac_optarg ;; -site | --site | --sit) ac_prev=site ;; -site=* | --site=* | --sit=*) site=$ac_optarg ;; -srcdir | --srcdir | --srcdi | --srcd | --src | --sr) ac_prev=srcdir ;; -srcdir=* | --srcdir=* | --srcdi=* | --srcd=* | --src=* | --sr=*) srcdir=$ac_optarg ;; -sysconfdir | --sysconfdir | --sysconfdi | --sysconfd | --sysconf \ | --syscon | --sysco | --sysc | --sys | --sy) ac_prev=sysconfdir ;; -sysconfdir=* | --sysconfdir=* | --sysconfdi=* | --sysconfd=* | --sysconf=* \ | --syscon=* | --sysco=* | --sysc=* | --sys=* | --sy=*) sysconfdir=$ac_optarg ;; -target | --target | --targe | --targ | --tar | --ta | --t) ac_prev=target_alias ;; -target=* | --target=* | --targe=* | --targ=* | --tar=* | --ta=* | --t=*) target_alias=$ac_optarg ;; -v | -verbose | --verbose | --verbos | --verbo | --verb) verbose=yes ;; -version | --version | --versio | --versi | --vers | -V) ac_init_version=: ;; -with-* | --with-*) ac_useropt=`expr "x$ac_option" : 'x-*with-\([^=]*\)'` # Reject names that are not valid shell variable names. expr "x$ac_useropt" : ".*[^-+._$as_cr_alnum]" >/dev/null && as_fn_error $? "invalid package name: '$ac_useropt'" ac_useropt_orig=$ac_useropt ac_useropt=`printf "%s\n" "$ac_useropt" | sed 's/[-+.]/_/g'` case $ac_user_opts in *" "with_$ac_useropt" "*) ;; *) ac_unrecognized_opts="$ac_unrecognized_opts$ac_unrecognized_sep--with-$ac_useropt_orig" ac_unrecognized_sep=', ';; esac eval with_$ac_useropt=\$ac_optarg ;; -without-* | --without-*) ac_useropt=`expr "x$ac_option" : 'x-*without-\(.*\)'` # Reject names that are not valid shell variable names. expr "x$ac_useropt" : ".*[^-+._$as_cr_alnum]" >/dev/null && as_fn_error $? "invalid package name: '$ac_useropt'" ac_useropt_orig=$ac_useropt ac_useropt=`printf "%s\n" "$ac_useropt" | sed 's/[-+.]/_/g'` case $ac_user_opts in *" "with_$ac_useropt" "*) ;; *) ac_unrecognized_opts="$ac_unrecognized_opts$ac_unrecognized_sep--without-$ac_useropt_orig" ac_unrecognized_sep=', ';; esac eval with_$ac_useropt=no ;; --x) # Obsolete; use --with-x. with_x=yes ;; -x-includes | --x-includes | --x-include | --x-includ | --x-inclu \ | --x-incl | --x-inc | --x-in | --x-i) ac_prev=x_includes ;; -x-includes=* | --x-includes=* | --x-include=* | --x-includ=* | --x-inclu=* \ | --x-incl=* | --x-inc=* | --x-in=* | --x-i=*) x_includes=$ac_optarg ;; -x-libraries | --x-libraries | --x-librarie | --x-librari \ | --x-librar | --x-libra | --x-libr | --x-lib | --x-li | --x-l) ac_prev=x_libraries ;; -x-libraries=* | --x-libraries=* | --x-librarie=* | --x-librari=* \ | --x-librar=* | --x-libra=* | --x-libr=* | --x-lib=* | --x-li=* | --x-l=*) x_libraries=$ac_optarg ;; -*) as_fn_error $? "unrecognized option: '$ac_option' Try '$0 --help' for more information" ;; *=*) ac_envvar=`expr "x$ac_option" : 'x\([^=]*\)='` # Reject names that are not valid shell variable names. case $ac_envvar in #( '' | [0-9]* | *[!_$as_cr_alnum]* ) as_fn_error $? "invalid variable name: '$ac_envvar'" ;; esac eval $ac_envvar=\$ac_optarg export $ac_envvar ;; *) # FIXME: should be removed in autoconf 3.0. printf "%s\n" "$as_me: WARNING: you should use --build, --host, --target" >&2 expr "x$ac_option" : ".*[^-._$as_cr_alnum]" >/dev/null && printf "%s\n" "$as_me: WARNING: invalid host type: $ac_option" >&2 : "${build_alias=$ac_option} ${host_alias=$ac_option} ${target_alias=$ac_option}" ;; esac done if test -n "$ac_prev"; then ac_option=--`echo $ac_prev | sed 's/_/-/g'` as_fn_error $? "missing argument to $ac_option" fi if test -n "$ac_unrecognized_opts"; then case $enable_option_checking in no) ;; fatal) as_fn_error $? "unrecognized options: $ac_unrecognized_opts" ;; *) printf "%s\n" "$as_me: WARNING: unrecognized options: $ac_unrecognized_opts" >&2 ;; esac fi # Check all directory arguments for consistency. for ac_var in exec_prefix prefix bindir sbindir libexecdir datarootdir \ datadir sysconfdir sharedstatedir localstatedir includedir \ oldincludedir docdir infodir htmldir dvidir pdfdir psdir \ libdir localedir mandir runstatedir do eval ac_val=\$$ac_var # Remove trailing slashes. case $ac_val in */ ) ac_val=`expr "X$ac_val" : 'X\(.*[^/]\)' \| "X$ac_val" : 'X\(.*\)'` eval $ac_var=\$ac_val;; esac # Be sure to have absolute directory names. case $ac_val in [\\/$]* | ?:[\\/]* ) continue;; NONE | '' ) case $ac_var in *prefix ) continue;; esac;; esac as_fn_error $? "expected an absolute directory name for --$ac_var: $ac_val" done # There might be people who depend on the old broken behavior: '$host' # used to hold the argument of --host etc. # FIXME: To remove some day. build=$build_alias host=$host_alias target=$target_alias # FIXME: To remove some day. if test "x$host_alias" != x; then if test "x$build_alias" = x; then cross_compiling=maybe elif test "x$build_alias" != "x$host_alias"; then cross_compiling=yes fi fi ac_tool_prefix= test -n "$host_alias" && ac_tool_prefix=$host_alias- test "$silent" = yes && exec 6>/dev/null ac_pwd=`pwd` && test -n "$ac_pwd" && ac_ls_di=`ls -di .` && ac_pwd_ls_di=`cd "$ac_pwd" && ls -di .` || as_fn_error $? "working directory cannot be determined" test "X$ac_ls_di" = "X$ac_pwd_ls_di" || as_fn_error $? "pwd does not report name of working directory" # Find the source files, if location was not specified. if test -z "$srcdir"; then ac_srcdir_defaulted=yes # Try the directory containing this script, then the parent directory. ac_confdir=`$as_dirname -- "$as_myself" || $as_expr X"$as_myself" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ X"$as_myself" : 'X\(//\)[^/]' \| \ X"$as_myself" : 'X\(//\)$' \| \ X"$as_myself" : 'X\(/\)' \| . 2>/dev/null || printf "%s\n" X"$as_myself" | sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ s//\1/ q } /^X\(\/\/\)[^/].*/{ s//\1/ q } /^X\(\/\/\)$/{ s//\1/ q } /^X\(\/\).*/{ s//\1/ q } s/.*/./; q'` srcdir=$ac_confdir if test ! -r "$srcdir/$ac_unique_file"; then srcdir=.. fi else ac_srcdir_defaulted=no fi if test ! -r "$srcdir/$ac_unique_file"; then test "$ac_srcdir_defaulted" = yes && srcdir="$ac_confdir or .." as_fn_error $? "cannot find sources ($ac_unique_file) in $srcdir" fi ac_msg="sources are in $srcdir, but 'cd $srcdir' does not work" ac_abs_confdir=`( cd "$srcdir" && test -r "./$ac_unique_file" || as_fn_error $? "$ac_msg" pwd)` # When building in place, set srcdir=. if test "$ac_abs_confdir" = "$ac_pwd"; then srcdir=. fi # Remove unnecessary trailing slashes from srcdir. # Double slashes in file names in object file debugging info # mess up M-x gdb in Emacs. case $srcdir in */) srcdir=`expr "X$srcdir" : 'X\(.*[^/]\)' \| "X$srcdir" : 'X\(.*\)'`;; esac for ac_var in $ac_precious_vars; do eval ac_env_${ac_var}_set=\${${ac_var}+set} eval ac_env_${ac_var}_value=\$${ac_var} eval ac_cv_env_${ac_var}_set=\${${ac_var}+set} eval ac_cv_env_${ac_var}_value=\$${ac_var} done # # Report the --help message. # if test "$ac_init_help" = "long"; then # Omit some internal or obsolete options to make the list less imposing. # This message is too long to be a string in the A/UX 3.1 sh. cat <<_ACEOF 'configure' configures Why3 1.8.2+git to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... To assign environment variables (e.g., CC, CFLAGS...), specify them as VAR=VALUE. See below for descriptions of some of the useful variables. Defaults for the options are specified in brackets. Configuration: -h, --help display this help and exit --help=short display options specific to this package --help=recursive display the short help of all the included packages -V, --version display version information and exit -q, --quiet, --silent do not print 'checking ...' messages --cache-file=FILE cache test results in FILE [disabled] -C, --config-cache alias for '--cache-file=config.cache' -n, --no-create do not create output files --srcdir=DIR find the sources in DIR [configure dir or '..'] Installation directories: --prefix=PREFIX install architecture-independent files in PREFIX [$ac_default_prefix] --exec-prefix=EPREFIX install architecture-dependent files in EPREFIX [PREFIX] By default, 'make install' will install all the files in '$ac_default_prefix/bin', '$ac_default_prefix/lib' etc. You can specify an installation prefix other than '$ac_default_prefix' using '--prefix', for instance '--prefix=\$HOME'. For better control, use the options below. Fine tuning of the installation directories: --bindir=DIR user executables [EPREFIX/bin] --sbindir=DIR system admin executables [EPREFIX/sbin] --libexecdir=DIR program executables [EPREFIX/libexec] --sysconfdir=DIR read-only single-machine data [PREFIX/etc] --sharedstatedir=DIR modifiable architecture-independent data [PREFIX/com] --localstatedir=DIR modifiable single-machine data [PREFIX/var] --runstatedir=DIR modifiable per-process data [LOCALSTATEDIR/run] --libdir=DIR object code libraries [EPREFIX/lib] --includedir=DIR C header files [PREFIX/include] --oldincludedir=DIR C header files for non-gcc [/usr/include] --datarootdir=DIR read-only arch.-independent data root [PREFIX/share] --datadir=DIR read-only architecture-independent data [DATAROOTDIR] --infodir=DIR info documentation [DATAROOTDIR/info] --localedir=DIR locale-dependent data [DATAROOTDIR/locale] --mandir=DIR man documentation [DATAROOTDIR/man] --docdir=DIR documentation root [DATAROOTDIR/doc/why3] --htmldir=DIR html documentation [DOCDIR] --dvidir=DIR dvi documentation [DOCDIR] --pdfdir=DIR pdf documentation [DOCDIR] --psdir=DIR ps documentation [DOCDIR] _ACEOF cat <<\_ACEOF _ACEOF fi if test -n "$ac_init_help"; then case $ac_init_help in short | recursive ) echo "Configuration of Why3 1.8.2+git:";; esac cat <<\_ACEOF Optional Features: --disable-option-checking ignore unrecognized --enable/--with options --disable-FEATURE do not include FEATURE (same as --enable-FEATURE=no) --enable-FEATURE[=ARG] include FEATURE [ARG=yes] --enable-verbose-make verbose makefile recipes --enable-local use Why3 in the build directory (no installation) --enable-relocation allow for later relocation of Why3 installation --disable-native-code use only the byte-code compiler --disable-why3-lib use an already installed Why3 --disable-ocamlfind do not use Ocamlfind --disable-zip do not use LZ compression to store session files --enable-infer use apron and fixpoint to infer loop invariants --enable-bddinfer use apron and BDDs to infer loop invariants --disable-js-of-ocaml do not use js-of-ocaml --disable-re use Str instead of Re for regular expressions --disable-sexp disable S-expression support for `Ptree` and `why3 pp` --disable-ide do not build Why3 IDE --disable-web-ide do not build Why3 Web IDE --disable-coq-libs do not build Coq realizations --disable-pvs-libs do not build PVS realizations --disable-isabelle-libs do not build Isabelle realizations --disable-mpfr disable support for MPFR --disable-hypothesis-selection do not support hypothesis selection --disable-stackify disable structure reconstruction algorithm for MLCFG --disable-doc do not build documentation --disable-pdf-doc do not build PDF documentation --enable-frama-c enable Frama-C plugin --enable-statmemprof enable statistical memory profiling --disable-emacs-compilation do not compile why3.elc --disable-java do not use java in bench Some influential environment variables: EDITOR default editor CC C compiler command CFLAGS C compiler flags LDFLAGS linker flags, e.g. -L if you have libraries in a nonstandard directory LIBS libraries to pass to the linker, e.g. -l CPPFLAGS (Objective) C/C++ preprocessor flags, e.g. -I if you have headers in a nonstandard directory Use these variables to override the choices made by 'configure' or to help it to find libraries and programs with nonstandard names/locations. Report bugs to the package provider. _ACEOF ac_status=$? fi if test "$ac_init_help" = "recursive"; then # If there are subdirs, report their specific --help. for ac_dir in : $ac_subdirs_all; do test "x$ac_dir" = x: && continue test -d "$ac_dir" || { cd "$srcdir" && ac_pwd=`pwd` && srcdir=. && test -d "$ac_dir"; } || continue ac_builddir=. case "$ac_dir" in .) ac_dir_suffix= ac_top_builddir_sub=. ac_top_build_prefix= ;; *) ac_dir_suffix=/`printf "%s\n" "$ac_dir" | sed 's|^\.[\\/]||'` # A ".." for each directory in $ac_dir_suffix. ac_top_builddir_sub=`printf "%s\n" "$ac_dir_suffix" | sed 's|/[^\\/]*|/..|g;s|/||'` case $ac_top_builddir_sub in "") ac_top_builddir_sub=. ac_top_build_prefix= ;; *) ac_top_build_prefix=$ac_top_builddir_sub/ ;; esac ;; esac ac_abs_top_builddir=$ac_pwd ac_abs_builddir=$ac_pwd$ac_dir_suffix # for backward compatibility: ac_top_builddir=$ac_top_build_prefix case $srcdir in .) # We are building in place. ac_srcdir=. ac_top_srcdir=$ac_top_builddir_sub ac_abs_top_srcdir=$ac_pwd ;; [\\/]* | ?:[\\/]* ) # Absolute name. ac_srcdir=$srcdir$ac_dir_suffix; ac_top_srcdir=$srcdir ac_abs_top_srcdir=$srcdir ;; *) # Relative name. ac_srcdir=$ac_top_build_prefix$srcdir$ac_dir_suffix ac_top_srcdir=$ac_top_build_prefix$srcdir ac_abs_top_srcdir=$ac_pwd/$srcdir ;; esac ac_abs_srcdir=$ac_abs_top_srcdir$ac_dir_suffix cd "$ac_dir" || { ac_status=$?; continue; } # Check for configure.gnu first; this name is used for a wrapper for # Metaconfig's "Configure" on case-insensitive file systems. if test -f "$ac_srcdir/configure.gnu"; then echo && $SHELL "$ac_srcdir/configure.gnu" --help=recursive elif test -f "$ac_srcdir/configure"; then echo && $SHELL "$ac_srcdir/configure" --help=recursive else printf "%s\n" "$as_me: WARNING: no configuration information is in $ac_dir" >&2 fi || ac_status=$? cd "$ac_pwd" || { ac_status=$?; break; } done fi test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF Why3 configure 1.8.2+git generated by GNU Autoconf 2.72 Copyright (C) 2023 Free Software Foundation, Inc. This configure script is free software; the Free Software Foundation gives unlimited permission to copy, distribute and modify it. _ACEOF exit fi ## ------------------------ ## ## Autoconf initialization. ## ## ------------------------ ## # ac_fn_c_try_compile LINENO # -------------------------- # Try to compile conftest.$ac_ext, and return whether this succeeded. ac_fn_c_try_compile () { as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack rm -f conftest.$ac_objext conftest.beam if { { ac_try="$ac_compile" case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" printf "%s\n" "$ac_try_echo"; } >&5 (eval "$ac_compile") 2>conftest.err ac_status=$? if test -s conftest.err; then grep -v '^ *+' conftest.err >conftest.er1 cat conftest.er1 >&5 mv -f conftest.er1 conftest.err fi printf "%s\n" "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; } && { test -z "$ac_c_werror_flag" || test ! -s conftest.err } && test -s conftest.$ac_objext then : ac_retval=0 else case e in #( e) printf "%s\n" "$as_me: failed program was:" >&5 sed 's/^/| /' conftest.$ac_ext >&5 ac_retval=1 ;; esac fi eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno as_fn_set_status $ac_retval } # ac_fn_c_try_compile ac_configure_args_raw= for ac_arg do case $ac_arg in *\'*) ac_arg=`printf "%s\n" "$ac_arg" | sed "s/'/'\\\\\\\\''/g"` ;; esac as_fn_append ac_configure_args_raw " '$ac_arg'" done case $ac_configure_args_raw in *$as_nl*) ac_safe_unquote= ;; *) ac_unsafe_z='|&;<>()$`\\"*?[ '' ' # This string ends in space, tab. ac_unsafe_a="$ac_unsafe_z#~" ac_safe_unquote="s/ '\\([^$ac_unsafe_a][^$ac_unsafe_z]*\\)'/ \\1/g" ac_configure_args_raw=` printf "%s\n" "$ac_configure_args_raw" | sed "$ac_safe_unquote"`;; esac cat >config.log <<_ACEOF This file contains any messages produced by compilers while running configure, to aid debugging if configure makes a mistake. It was created by Why3 $as_me 1.8.2+git, which was generated by GNU Autoconf 2.72. Invocation command line was $ $0$ac_configure_args_raw _ACEOF exec 5>>config.log { cat <<_ASUNAME ## --------- ## ## Platform. ## ## --------- ## hostname = `(hostname || uname -n) 2>/dev/null | sed 1q` uname -m = `(uname -m) 2>/dev/null || echo unknown` uname -r = `(uname -r) 2>/dev/null || echo unknown` uname -s = `(uname -s) 2>/dev/null || echo unknown` uname -v = `(uname -v) 2>/dev/null || echo unknown` /usr/bin/uname -p = `(/usr/bin/uname -p) 2>/dev/null || echo unknown` /bin/uname -X = `(/bin/uname -X) 2>/dev/null || echo unknown` /bin/arch = `(/bin/arch) 2>/dev/null || echo unknown` /usr/bin/arch -k = `(/usr/bin/arch -k) 2>/dev/null || echo unknown` /usr/convex/getsysinfo = `(/usr/convex/getsysinfo) 2>/dev/null || echo unknown` /usr/bin/hostinfo = `(/usr/bin/hostinfo) 2>/dev/null || echo unknown` /bin/machine = `(/bin/machine) 2>/dev/null || echo unknown` /usr/bin/oslevel = `(/usr/bin/oslevel) 2>/dev/null || echo unknown` /bin/universe = `(/bin/universe) 2>/dev/null || echo unknown` _ASUNAME as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac printf "%s\n" "PATH: $as_dir" done IFS=$as_save_IFS } >&5 cat >&5 <<_ACEOF ## ----------- ## ## Core tests. ## ## ----------- ## _ACEOF # Keep a trace of the command line. # Strip out --no-create and --no-recursion so they do not pile up. # Strip out --silent because we don't want to record it for future runs. # Also quote any args containing shell meta-characters. # Make two passes to allow for proper duplicate-argument suppression. ac_configure_args= ac_configure_args0= ac_configure_args1= ac_must_keep_next=false for ac_pass in 1 2 do for ac_arg do case $ac_arg in -no-create | --no-c* | -n | -no-recursion | --no-r*) continue ;; -q | -quiet | --quiet | --quie | --qui | --qu | --q \ | -silent | --silent | --silen | --sile | --sil) continue ;; *\'*) ac_arg=`printf "%s\n" "$ac_arg" | sed "s/'/'\\\\\\\\''/g"` ;; esac case $ac_pass in 1) as_fn_append ac_configure_args0 " '$ac_arg'" ;; 2) as_fn_append ac_configure_args1 " '$ac_arg'" if test $ac_must_keep_next = true; then ac_must_keep_next=false # Got value, back to normal. else case $ac_arg in *=* | --config-cache | -C | -disable-* | --disable-* \ | -enable-* | --enable-* | -gas | --g* | -nfp | --nf* \ | -q | -quiet | --q* | -silent | --sil* | -v | -verb* \ | -with-* | --with-* | -without-* | --without-* | --x) case "$ac_configure_args0 " in "$ac_configure_args1"*" '$ac_arg' "* ) continue ;; esac ;; -* ) ac_must_keep_next=true ;; esac fi as_fn_append ac_configure_args " '$ac_arg'" ;; esac done done { ac_configure_args0=; unset ac_configure_args0;} { ac_configure_args1=; unset ac_configure_args1;} # When interrupted or exit'd, cleanup temporary files, and complete # config.log. We remove comments because anyway the quotes in there # would cause problems or look ugly. # WARNING: Use '\'' to represent an apostrophe within the trap. # WARNING: Do not start the trap code with a newline, due to a FreeBSD 4.0 bug. trap 'exit_status=$? # Sanitize IFS. IFS=" "" $as_nl" # Save into config.log some information that might help in debugging. { echo printf "%s\n" "## ---------------- ## ## Cache variables. ## ## ---------------- ##" echo # The following way of writing the cache mishandles newlines in values, ( for ac_var in `(set) 2>&1 | sed -n '\''s/^\([a-zA-Z_][a-zA-Z0-9_]*\)=.*/\1/p'\''`; do eval ac_val=\$$ac_var case $ac_val in #( *${as_nl}*) case $ac_var in #( *_cv_*) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cache variable $ac_var contains a newline" >&5 printf "%s\n" "$as_me: WARNING: cache variable $ac_var contains a newline" >&2;} ;; esac case $ac_var in #( _ | IFS | as_nl) ;; #( BASH_ARGV | BASH_SOURCE) eval $ac_var= ;; #( *) { eval $ac_var=; unset $ac_var;} ;; esac ;; esac done (set) 2>&1 | case $as_nl`(ac_space='\'' '\''; set) 2>&1` in #( *${as_nl}ac_space=\ *) sed -n \ "s/'\''/'\''\\\\'\'''\''/g; s/^\\([_$as_cr_alnum]*_cv_[_$as_cr_alnum]*\\)=\\(.*\\)/\\1='\''\\2'\''/p" ;; #( *) sed -n "/^[_$as_cr_alnum]*_cv_[_$as_cr_alnum]*=/p" ;; esac | sort ) echo printf "%s\n" "## ----------------- ## ## Output variables. ## ## ----------------- ##" echo for ac_var in $ac_subst_vars do eval ac_val=\$$ac_var case $ac_val in *\'\''*) ac_val=`printf "%s\n" "$ac_val" | sed "s/'\''/'\''\\\\\\\\'\'''\''/g"`;; esac printf "%s\n" "$ac_var='\''$ac_val'\''" done | sort echo if test -n "$ac_subst_files"; then printf "%s\n" "## ------------------- ## ## File substitutions. ## ## ------------------- ##" echo for ac_var in $ac_subst_files do eval ac_val=\$$ac_var case $ac_val in *\'\''*) ac_val=`printf "%s\n" "$ac_val" | sed "s/'\''/'\''\\\\\\\\'\'''\''/g"`;; esac printf "%s\n" "$ac_var='\''$ac_val'\''" done | sort echo fi if test -s confdefs.h; then printf "%s\n" "## ----------- ## ## confdefs.h. ## ## ----------- ##" echo cat confdefs.h echo fi test "$ac_signal" != 0 && printf "%s\n" "$as_me: caught signal $ac_signal" printf "%s\n" "$as_me: exit $exit_status" } >&5 rm -f core *.core core.conftest.* && rm -f -r conftest* confdefs* conf$$* $ac_clean_files && exit $exit_status ' 0 for ac_signal in 1 2 13 15; do trap 'ac_signal='$ac_signal'; as_fn_exit 1' $ac_signal done ac_signal=0 # confdefs.h avoids OS command line length limits that DEFS can exceed. rm -f -r conftest* confdefs.h printf "%s\n" "/* confdefs.h */" > confdefs.h # Predefined preprocessor variables. printf "%s\n" "#define PACKAGE_NAME \"$PACKAGE_NAME\"" >>confdefs.h printf "%s\n" "#define PACKAGE_TARNAME \"$PACKAGE_TARNAME\"" >>confdefs.h printf "%s\n" "#define PACKAGE_VERSION \"$PACKAGE_VERSION\"" >>confdefs.h printf "%s\n" "#define PACKAGE_STRING \"$PACKAGE_STRING\"" >>confdefs.h printf "%s\n" "#define PACKAGE_BUGREPORT \"$PACKAGE_BUGREPORT\"" >>confdefs.h printf "%s\n" "#define PACKAGE_URL \"$PACKAGE_URL\"" >>confdefs.h # Let the site file select an alternate cache file if it wants to. # Prefer an explicitly selected file to automatically selected ones. if test -n "$CONFIG_SITE"; then ac_site_files="$CONFIG_SITE" elif test "x$prefix" != xNONE; then ac_site_files="$prefix/share/config.site $prefix/etc/config.site" else ac_site_files="$ac_default_prefix/share/config.site $ac_default_prefix/etc/config.site" fi for ac_site_file in $ac_site_files do case $ac_site_file in #( */*) : ;; #( *) : ac_site_file=./$ac_site_file ;; esac if test -f "$ac_site_file" && test -r "$ac_site_file"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: loading site script $ac_site_file" >&5 printf "%s\n" "$as_me: loading site script $ac_site_file" >&6;} sed 's/^/| /' "$ac_site_file" >&5 . "$ac_site_file" \ || { { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: in '$ac_pwd':" >&5 printf "%s\n" "$as_me: error: in '$ac_pwd':" >&2;} as_fn_error $? "failed to load site script $ac_site_file See 'config.log' for more details" "$LINENO" 5; } fi done if test -r "$cache_file"; then # Some versions of bash will fail to source /dev/null (special files # actually), so we avoid doing that. DJGPP emulates it as a regular file. if test /dev/null != "$cache_file" && test -f "$cache_file"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: loading cache $cache_file" >&5 printf "%s\n" "$as_me: loading cache $cache_file" >&6;} case $cache_file in [\\/]* | ?:[\\/]* ) . "$cache_file";; *) . "./$cache_file";; esac fi else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: creating cache $cache_file" >&5 printf "%s\n" "$as_me: creating cache $cache_file" >&6;} >$cache_file fi # Test code for whether the C compiler supports C89 (global declarations) ac_c_conftest_c89_globals=' /* Does the compiler advertise C89 conformance? Do not test the value of __STDC__, because some compilers set it to 0 while being otherwise adequately conformant. */ #if !defined __STDC__ # error "Compiler does not advertise C89 conformance" #endif #include #include struct stat; /* Most of the following tests are stolen from RCS 5.7 src/conf.sh. */ struct buf { int x; }; struct buf * (*rcsopen) (struct buf *, struct stat *, int); static char *e (char **p, int i) { return p[i]; } static char *f (char * (*g) (char **, int), char **p, ...) { char *s; va_list v; va_start (v,p); s = g (p, va_arg (v,int)); va_end (v); return s; } /* C89 style stringification. */ #define noexpand_stringify(a) #a const char *stringified = noexpand_stringify(arbitrary+token=sequence); /* C89 style token pasting. Exercises some of the corner cases that e.g. old MSVC gets wrong, but not very hard. */ #define noexpand_concat(a,b) a##b #define expand_concat(a,b) noexpand_concat(a,b) extern int vA; extern int vbee; #define aye A #define bee B int *pvA = &expand_concat(v,aye); int *pvbee = &noexpand_concat(v,bee); /* OSF 4.0 Compaq cc is some sort of almost-ANSI by default. It has function prototypes and stuff, but not \xHH hex character constants. These do not provoke an error unfortunately, instead are silently treated as an "x". The following induces an error, until -std is added to get proper ANSI mode. Curiously \x00 != x always comes out true, for an array size at least. It is necessary to write \x00 == 0 to get something that is true only with -std. */ int osf4_cc_array ['\''\x00'\'' == 0 ? 1 : -1]; /* IBM C 6 for AIX is almost-ANSI by default, but it replaces macro parameters inside strings and character constants. */ #define FOO(x) '\''x'\'' int xlc6_cc_array[FOO(a) == '\''x'\'' ? 1 : -1]; int test (int i, double x); struct s1 {int (*f) (int a);}; struct s2 {int (*f) (double a);}; int pairnames (int, char **, int *(*)(struct buf *, struct stat *, int), int, int);' # Test code for whether the C compiler supports C89 (body of main). ac_c_conftest_c89_main=' ok |= (argc == 0 || f (e, argv, 0) != argv[0] || f (e, argv, 1) != argv[1]); ' # Test code for whether the C compiler supports C99 (global declarations) ac_c_conftest_c99_globals=' /* Does the compiler advertise C99 conformance? */ #if !defined __STDC_VERSION__ || __STDC_VERSION__ < 199901L # error "Compiler does not advertise C99 conformance" #endif // See if C++-style comments work. #include extern int puts (const char *); extern int printf (const char *, ...); extern int dprintf (int, const char *, ...); extern void *malloc (size_t); extern void free (void *); // Check varargs macros. These examples are taken from C99 6.10.3.5. // dprintf is used instead of fprintf to avoid needing to declare // FILE and stderr. #define debug(...) dprintf (2, __VA_ARGS__) #define showlist(...) puts (#__VA_ARGS__) #define report(test,...) ((test) ? puts (#test) : printf (__VA_ARGS__)) static void test_varargs_macros (void) { int x = 1234; int y = 5678; debug ("Flag"); debug ("X = %d\n", x); showlist (The first, second, and third items.); report (x>y, "x is %d but y is %d", x, y); } // Check long long types. #define BIG64 18446744073709551615ull #define BIG32 4294967295ul #define BIG_OK (BIG64 / BIG32 == 4294967297ull && BIG64 % BIG32 == 0) #if !BIG_OK #error "your preprocessor is broken" #endif #if BIG_OK #else #error "your preprocessor is broken" #endif static long long int bignum = -9223372036854775807LL; static unsigned long long int ubignum = BIG64; struct incomplete_array { int datasize; double data[]; }; struct named_init { int number; const wchar_t *name; double average; }; typedef const char *ccp; static inline int test_restrict (ccp restrict text) { // Iterate through items via the restricted pointer. // Also check for declarations in for loops. for (unsigned int i = 0; *(text+i) != '\''\0'\''; ++i) continue; return 0; } // Check varargs and va_copy. static bool test_varargs (const char *format, ...) { va_list args; va_start (args, format); va_list args_copy; va_copy (args_copy, args); const char *str = ""; int number = 0; float fnumber = 0; while (*format) { switch (*format++) { case '\''s'\'': // string str = va_arg (args_copy, const char *); break; case '\''d'\'': // int number = va_arg (args_copy, int); break; case '\''f'\'': // float fnumber = va_arg (args_copy, double); break; default: break; } } va_end (args_copy); va_end (args); return *str && number && fnumber; } ' # Test code for whether the C compiler supports C99 (body of main). ac_c_conftest_c99_main=' // Check bool. _Bool success = false; success |= (argc != 0); // Check restrict. if (test_restrict ("String literal") == 0) success = true; char *restrict newvar = "Another string"; // Check varargs. success &= test_varargs ("s, d'\'' f .", "string", 65, 34.234); test_varargs_macros (); // Check flexible array members. struct incomplete_array *ia = malloc (sizeof (struct incomplete_array) + (sizeof (double) * 10)); ia->datasize = 10; for (int i = 0; i < ia->datasize; ++i) ia->data[i] = i * 1.234; // Work around memory leak warnings. free (ia); // Check named initializers. struct named_init ni = { .number = 34, .name = L"Test wide string", .average = 543.34343, }; ni.number = 58; int dynamic_array[ni.number]; dynamic_array[0] = argv[0][0]; dynamic_array[ni.number - 1] = 543; // work around unused variable warnings ok |= (!success || bignum == 0LL || ubignum == 0uLL || newvar[0] == '\''x'\'' || dynamic_array[ni.number - 1] != 543); ' # Test code for whether the C compiler supports C11 (global declarations) ac_c_conftest_c11_globals=' /* Does the compiler advertise C11 conformance? */ #if !defined __STDC_VERSION__ || __STDC_VERSION__ < 201112L # error "Compiler does not advertise C11 conformance" #endif // Check _Alignas. char _Alignas (double) aligned_as_double; char _Alignas (0) no_special_alignment; extern char aligned_as_int; char _Alignas (0) _Alignas (int) aligned_as_int; // Check _Alignof. enum { int_alignment = _Alignof (int), int_array_alignment = _Alignof (int[100]), char_alignment = _Alignof (char) }; _Static_assert (0 < -_Alignof (int), "_Alignof is signed"); // Check _Noreturn. int _Noreturn does_not_return (void) { for (;;) continue; } // Check _Static_assert. struct test_static_assert { int x; _Static_assert (sizeof (int) <= sizeof (long int), "_Static_assert does not work in struct"); long int y; }; // Check UTF-8 literals. #define u8 syntax error! char const utf8_literal[] = u8"happens to be ASCII" "another string"; // Check duplicate typedefs. typedef long *long_ptr; typedef long int *long_ptr; typedef long_ptr long_ptr; // Anonymous structures and unions -- taken from C11 6.7.2.1 Example 1. struct anonymous { union { struct { int i; int j; }; struct { int k; long int l; } w; }; int m; } v1; ' # Test code for whether the C compiler supports C11 (body of main). ac_c_conftest_c11_main=' _Static_assert ((offsetof (struct anonymous, i) == offsetof (struct anonymous, w.k)), "Anonymous union alignment botch"); v1.i = 2; v1.w.k = 5; ok |= v1.i != 5; ' # Test code for whether the C compiler supports C11 (complete). ac_c_conftest_c11_program="${ac_c_conftest_c89_globals} ${ac_c_conftest_c99_globals} ${ac_c_conftest_c11_globals} int main (int argc, char **argv) { int ok = 0; ${ac_c_conftest_c89_main} ${ac_c_conftest_c99_main} ${ac_c_conftest_c11_main} return ok; } " # Test code for whether the C compiler supports C99 (complete). ac_c_conftest_c99_program="${ac_c_conftest_c89_globals} ${ac_c_conftest_c99_globals} int main (int argc, char **argv) { int ok = 0; ${ac_c_conftest_c89_main} ${ac_c_conftest_c99_main} return ok; } " # Test code for whether the C compiler supports C89 (complete). ac_c_conftest_c89_program="${ac_c_conftest_c89_globals} int main (int argc, char **argv) { int ok = 0; ${ac_c_conftest_c89_main} return ok; } " # Auxiliary files required by this configure script. ac_aux_files="install-sh" # Locations in which to look for auxiliary files. ac_aux_dir_candidates="${srcdir}${PATH_SEPARATOR}${srcdir}/..${PATH_SEPARATOR}${srcdir}/../.." # Search for a directory containing all of the required auxiliary files, # $ac_aux_files, from the $PATH-style list $ac_aux_dir_candidates. # If we don't find one directory that contains all the files we need, # we report the set of missing files from the *first* directory in # $ac_aux_dir_candidates and give up. ac_missing_aux_files="" ac_first_candidate=: printf "%s\n" "$as_me:${as_lineno-$LINENO}: looking for aux files: $ac_aux_files" >&5 as_save_IFS=$IFS; IFS=$PATH_SEPARATOR as_found=false for as_dir in $ac_aux_dir_candidates do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac as_found=: printf "%s\n" "$as_me:${as_lineno-$LINENO}: trying $as_dir" >&5 ac_aux_dir_found=yes ac_install_sh= for ac_aux in $ac_aux_files do # As a special case, if "install-sh" is required, that requirement # can be satisfied by any of "install-sh", "install.sh", or "shtool", # and $ac_install_sh is set appropriately for whichever one is found. if test x"$ac_aux" = x"install-sh" then if test -f "${as_dir}install-sh"; then printf "%s\n" "$as_me:${as_lineno-$LINENO}: ${as_dir}install-sh found" >&5 ac_install_sh="${as_dir}install-sh -c" elif test -f "${as_dir}install.sh"; then printf "%s\n" "$as_me:${as_lineno-$LINENO}: ${as_dir}install.sh found" >&5 ac_install_sh="${as_dir}install.sh -c" elif test -f "${as_dir}shtool"; then printf "%s\n" "$as_me:${as_lineno-$LINENO}: ${as_dir}shtool found" >&5 ac_install_sh="${as_dir}shtool install -c" else ac_aux_dir_found=no if $ac_first_candidate; then ac_missing_aux_files="${ac_missing_aux_files} install-sh" else break fi fi else if test -f "${as_dir}${ac_aux}"; then printf "%s\n" "$as_me:${as_lineno-$LINENO}: ${as_dir}${ac_aux} found" >&5 else ac_aux_dir_found=no if $ac_first_candidate; then ac_missing_aux_files="${ac_missing_aux_files} ${ac_aux}" else break fi fi fi done if test "$ac_aux_dir_found" = yes; then ac_aux_dir="$as_dir" break fi ac_first_candidate=false as_found=false done IFS=$as_save_IFS if $as_found then : else case e in #( e) as_fn_error $? "cannot find required auxiliary files:$ac_missing_aux_files" "$LINENO" 5 ;; esac fi # These three variables are undocumented and unsupported, # and are intended to be withdrawn in a future Autoconf release. # They can cause serious problems if a builder's source tree is in a directory # whose full name contains unusual characters. if test -f "${ac_aux_dir}config.guess"; then ac_config_guess="$SHELL ${ac_aux_dir}config.guess" fi if test -f "${ac_aux_dir}config.sub"; then ac_config_sub="$SHELL ${ac_aux_dir}config.sub" fi if test -f "$ac_aux_dir/configure"; then ac_configure="$SHELL ${ac_aux_dir}configure" fi # Check that the precious variables saved in the cache have kept the same # value. ac_cache_corrupted=false for ac_var in $ac_precious_vars; do eval ac_old_set=\$ac_cv_env_${ac_var}_set eval ac_new_set=\$ac_env_${ac_var}_set eval ac_old_val=\$ac_cv_env_${ac_var}_value eval ac_new_val=\$ac_env_${ac_var}_value case $ac_old_set,$ac_new_set in set,) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: '$ac_var' was set to '$ac_old_val' in the previous run" >&5 printf "%s\n" "$as_me: error: '$ac_var' was set to '$ac_old_val' in the previous run" >&2;} ac_cache_corrupted=: ;; ,set) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: '$ac_var' was not set in the previous run" >&5 printf "%s\n" "$as_me: error: '$ac_var' was not set in the previous run" >&2;} ac_cache_corrupted=: ;; ,);; *) if test "x$ac_old_val" != "x$ac_new_val"; then # differences in whitespace do not lead to failure. ac_old_val_w=`echo x $ac_old_val` ac_new_val_w=`echo x $ac_new_val` if test "$ac_old_val_w" != "$ac_new_val_w"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: '$ac_var' has changed since the previous run:" >&5 printf "%s\n" "$as_me: error: '$ac_var' has changed since the previous run:" >&2;} ac_cache_corrupted=: else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: warning: ignoring whitespace changes in '$ac_var' since the previous run:" >&5 printf "%s\n" "$as_me: warning: ignoring whitespace changes in '$ac_var' since the previous run:" >&2;} eval $ac_var=\$ac_old_val fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: former value: '$ac_old_val'" >&5 printf "%s\n" "$as_me: former value: '$ac_old_val'" >&2;} { printf "%s\n" "$as_me:${as_lineno-$LINENO}: current value: '$ac_new_val'" >&5 printf "%s\n" "$as_me: current value: '$ac_new_val'" >&2;} fi;; esac # Pass precious variables to config.status. if test "$ac_new_set" = set; then case $ac_new_val in *\'*) ac_arg=$ac_var=`printf "%s\n" "$ac_new_val" | sed "s/'/'\\\\\\\\''/g"` ;; *) ac_arg=$ac_var=$ac_new_val ;; esac case " $ac_configure_args " in *" '$ac_arg' "*) ;; # Avoid dups. Use of quotes ensures accuracy. *) as_fn_append ac_configure_args " '$ac_arg'" ;; esac fi done if $ac_cache_corrupted; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: in '$ac_pwd':" >&5 printf "%s\n" "$as_me: error: in '$ac_pwd':" >&2;} { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: changes in the environment can compromise the build" >&5 printf "%s\n" "$as_me: error: changes in the environment can compromise the build" >&2;} as_fn_error $? "run '${MAKE-make} distclean' and/or 'rm $cache_file' and start over" "$LINENO" 5 fi ## -------------------- ## ## Main body of script. ## ## -------------------- ## ac_ext=c ac_cpp='$CPP $CPPFLAGS' ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5' ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' ac_compiler_gnu=$ac_cv_c_compiler_gnu # verbosemake # Check whether --enable-verbose-make was given. if test ${enable_verbose_make+y} then : enableval=$enable_verbose_make; else case e in #( e) enable_verbose_make=no ;; esac fi # LOCAL_CONF # Check whether --enable-local was given. if test ${enable_local+y} then : enableval=$enable_local; else case e in #( e) enable_local=no ;; esac fi # RELOCATABLE INSTALLATION # Check whether --enable-relocation was given. if test ${enable_relocation+y} then : enableval=$enable_relocation; else case e in #( e) enable_relocation=no ;; esac fi # NATIVE # Check whether --enable-native-code was given. if test ${enable_native_code+y} then : enableval=$enable_native_code; else case e in #( e) enable_native_code=yes ;; esac fi # WHY3LIB # Check whether --enable-why3-lib was given. if test ${enable_why3_lib+y} then : enableval=$enable_why3_lib; else case e in #( e) enable_why3_lib=yes ;; esac fi # ocamlfind # Check whether --enable-ocamlfind was given. if test ${enable_ocamlfind+y} then : enableval=$enable_ocamlfind; else case e in #( e) enable_ocamlfind=check ;; esac fi # camlzip # Check whether --enable-zip was given. if test ${enable_zip+y} then : enableval=$enable_zip; else case e in #( e) enable_zip=check ;; esac fi # infer # Check whether --enable-infer was given. if test ${enable_infer+y} then : enableval=$enable_infer; else case e in #( e) enable_infer=no ;; esac fi # bddinfer # Check whether --enable-bddinfer was given. if test ${enable_bddinfer+y} then : enableval=$enable_bddinfer; else case e in #( e) enable_bddinfer=no ;; esac fi # js_of_ocaml # Check whether --enable-js_of_ocaml was given. if test ${enable_js_of_ocaml+y} then : enableval=$enable_js_of_ocaml; else case e in #( e) enable_js_of_ocaml=check ;; esac fi # re # Check whether --enable-re was given. if test ${enable_re+y} then : enableval=$enable_re; else case e in #( e) enable_re=check ;; esac fi # sexp # Check whether --enable-sexp was given. if test ${enable_sexp+y} then : enableval=$enable_sexp; else case e in #( e) enable_sexp=yes ;; esac fi # IDE # Check whether --enable-ide was given. if test ${enable_ide+y} then : enableval=$enable_ide; else case e in #( e) enable_ide=check ;; esac fi # Check whether --enable-web_ide was given. if test ${enable_web_ide+y} then : enableval=$enable_web_ide; else case e in #( e) enable_web_ide=check ;; esac fi # Coq libraries # Check whether --enable-coq-libs was given. if test ${enable_coq_libs+y} then : enableval=$enable_coq_libs; else case e in #( e) enable_coq_libs=check ;; esac fi # PVS libraries # Check whether --enable-pvs-libs was given. if test ${enable_pvs_libs+y} then : enableval=$enable_pvs_libs; else case e in #( e) enable_pvs_libs=yes ;; esac fi # Isabelle libraries # Check whether --enable-isabelle-libs was given. if test ${enable_isabelle_libs+y} then : enableval=$enable_isabelle_libs; else case e in #( e) enable_isabelle_libs=yes ;; esac fi # MLMPFR # Check whether --enable-mpfr was given. if test ${enable_mpfr+y} then : enableval=$enable_mpfr; else case e in #( e) enable_mpfr=check ;; esac fi # hypothesis selection # Check whether --enable-hypothesis-selection was given. if test ${enable_hypothesis_selection+y} then : enableval=$enable_hypothesis_selection; else case e in #( e) enable_hypothesis_selection=check ;; esac fi # stackify # Check whether --enable-stackify was given. if test ${enable_stackify+y} then : enableval=$enable_stackify; else case e in #( e) enable_stackify=check ;; esac fi # documentation # Check whether --enable-doc was given. if test ${enable_doc+y} then : enableval=$enable_doc; else case e in #( e) enable_doc=yes ;; esac fi # Check whether --enable-html-pdf was given. if test ${enable_html_pdf+y} then : enableval=$enable_html_pdf; else case e in #( e) enable_pdf_doc=yes ;; esac fi # Experimental Jessie3 Frama-C plugin, disabled by default # Check whether --enable-frama-c was given. if test ${enable_frama_c+y} then : enableval=$enable_frama_c; else case e in #( e) enable_frama_c=no reason_frama_c=" (disabled by default)" ;; esac fi # profiling with statememprof # Check whether --enable-statmemprof was given. if test ${enable_statmemprof+y} then : enableval=$enable_statmemprof; else case e in #( e) enable_statmemprof=no reason_statmemprof=" (disabled by default)" ;; esac fi # Emacs compilation # Check whether --enable-emacs-compilation was given. if test ${enable_emacs_compilation+y} then : enableval=$enable_emacs_compilation; else case e in #( e) enable_emacs_compilation=yes ;; esac fi # default editor # Java look-up # Check whether --enable-java was given. if test ${enable_java+y} then : enableval=$enable_java; enable_java=${enableval} else case e in #( e) enable_java=yes ;; esac fi # either relocation or local, not both if test "$enable_relocation" = yes -a "$enable_local" = yes ; then as_fn_error $? "cannot use --enable-relocation and --enable-local at the same time." "$LINENO" 5 fi # Check for arch/OS { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking executable suffix" >&5 printf %s "checking executable suffix... " >&6; } if uname -s | grep -q CYGWIN ; then EXE=.exe STRIP='echo "no strip "' BUILD_ENV_TYPE=Cygwin { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: .exe " >&5 printf "%s\n" ".exe " >&6; } elif uname -s | grep -q MINGW ; then EXE=.exe STRIP=strip BUILD_ENV_TYPE=MinGW { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: .exe " >&5 printf "%s\n" ".exe " >&6; } else EXE= STRIP=strip BUILD_ENV_TYPE=Posix { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: " >&5 printf "%s\n" "" >&6; } fi # Check for ocamlc, as we need it to find the C compiler to use # we first look for it in the path; if not present, we fail # Extract the first word of "ocamlc", so it can be a program name with args. set dummy ocamlc; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLC+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLC"; then ac_cv_prog_OCAMLC="$OCAMLC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLC="ocamlc" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLC" && ac_cv_prog_OCAMLC="no" fi ;; esac fi OCAMLC=$ac_cv_prog_OCAMLC if test -n "$OCAMLC"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLC" >&5 printf "%s\n" "$OCAMLC" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLC" = no ; then as_fn_error $? "cannot find ocamlc." "$LINENO" 5 fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking ocaml os type" >&5 printf %s "checking ocaml os type... " >&6; } OCAML_OS_TYPE=$($OCAMLC -config-var os_type) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAML_OS_TYPE" >&5 printf "%s\n" "$OCAML_OS_TYPE" >&6; } ac_ext=c ac_cpp='$CPP $CPPFLAGS' ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5' ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' ac_compiler_gnu=$ac_cv_c_compiler_gnu if test -n "$ac_tool_prefix"; then for ac_prog in "$($OCAMLC -config-var c_compiler)" gcc cl.exe clang do # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args. set dummy $ac_tool_prefix$ac_prog; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_CC+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$CC"; then ac_cv_prog_CC="$CC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_CC="$ac_tool_prefix$ac_prog" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS fi ;; esac fi CC=$ac_cv_prog_CC if test -n "$CC"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $CC" >&5 printf "%s\n" "$CC" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi test -n "$CC" && break done fi if test -z "$CC"; then ac_ct_CC=$CC for ac_prog in "$($OCAMLC -config-var c_compiler)" gcc cl.exe clang do # Extract the first word of "$ac_prog", so it can be a program name with args. set dummy $ac_prog; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_ac_ct_CC+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$ac_ct_CC"; then ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_ac_ct_CC="$ac_prog" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS fi ;; esac fi ac_ct_CC=$ac_cv_prog_ac_ct_CC if test -n "$ac_ct_CC"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5 printf "%s\n" "$ac_ct_CC" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi test -n "$ac_ct_CC" && break done if test "x$ac_ct_CC" = x; then CC="" else case $cross_compiling:$ac_tool_warned in yes:) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5 printf "%s\n" "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;} ac_tool_warned=yes ;; esac CC=$ac_ct_CC fi fi test -z "$CC" && { { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: in '$ac_pwd':" >&5 printf "%s\n" "$as_me: error: in '$ac_pwd':" >&2;} as_fn_error $? "no acceptable C compiler found in \$PATH See 'config.log' for more details" "$LINENO" 5; } # Provide some information about the compiler. printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5 set X $ac_compile ac_compiler=$2 for ac_option in --version -v -V -qversion -version; do { { ac_try="$ac_compiler $ac_option >&5" case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" printf "%s\n" "$ac_try_echo"; } >&5 (eval "$ac_compiler $ac_option >&5") 2>conftest.err ac_status=$? if test -s conftest.err; then sed '10a\ ... rest of stderr output deleted ... 10q' conftest.err >conftest.er1 cat conftest.er1 >&5 fi rm -f conftest.er1 conftest.err printf "%s\n" "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; } done cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ int main (void) { ; return 0; } _ACEOF ac_clean_files_save=$ac_clean_files ac_clean_files="$ac_clean_files a.out a.out.dSYM a.exe b.out" # Try to create an executable without -o first, disregard a.out. # It will help us diagnose broken compilers, and finding out an intuition # of exeext. { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking whether the C compiler works" >&5 printf %s "checking whether the C compiler works... " >&6; } ac_link_default=`printf "%s\n" "$ac_link" | sed 's/ -o *conftest[^ ]*//'` # The possible output files: ac_files="a.out conftest.exe conftest a.exe a_out.exe b.out conftest.*" ac_rmfiles= for ac_file in $ac_files do case $ac_file in *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj ) ;; * ) ac_rmfiles="$ac_rmfiles $ac_file";; esac done rm -f $ac_rmfiles if { { ac_try="$ac_link_default" case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" printf "%s\n" "$ac_try_echo"; } >&5 (eval "$ac_link_default") 2>&5 ac_status=$? printf "%s\n" "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; } then : # Autoconf-2.13 could set the ac_cv_exeext variable to 'no'. # So ignore a value of 'no', otherwise this would lead to 'EXEEXT = no' # in a Makefile. We should not override ac_cv_exeext if it was cached, # so that the user can short-circuit this test for compilers unknown to # Autoconf. for ac_file in $ac_files '' do test -f "$ac_file" || continue case $ac_file in *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj ) ;; [ab].out ) # We found the default executable, but exeext='' is most # certainly right. break;; *.* ) if test ${ac_cv_exeext+y} && test "$ac_cv_exeext" != no; then :; else ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'` fi # We set ac_cv_exeext here because the later test for it is not # safe: cross compilers may not add the suffix if given an '-o' # argument, so we may need to know it at that point already. # Even if this section looks crufty: it has the advantage of # actually working. break;; * ) break;; esac done test "$ac_cv_exeext" = no && ac_cv_exeext= else case e in #( e) ac_file='' ;; esac fi if test -z "$ac_file" then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } printf "%s\n" "$as_me: failed program was:" >&5 sed 's/^/| /' conftest.$ac_ext >&5 { { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: in '$ac_pwd':" >&5 printf "%s\n" "$as_me: error: in '$ac_pwd':" >&2;} as_fn_error 77 "C compiler cannot create executables See 'config.log' for more details" "$LINENO" 5; } else case e in #( e) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } ;; esac fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for C compiler default output file name" >&5 printf %s "checking for C compiler default output file name... " >&6; } { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_file" >&5 printf "%s\n" "$ac_file" >&6; } ac_exeext=$ac_cv_exeext rm -f -r a.out a.out.dSYM a.exe conftest$ac_cv_exeext b.out ac_clean_files=$ac_clean_files_save { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for suffix of executables" >&5 printf %s "checking for suffix of executables... " >&6; } if { { ac_try="$ac_link" case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" printf "%s\n" "$ac_try_echo"; } >&5 (eval "$ac_link") 2>&5 ac_status=$? printf "%s\n" "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; } then : # If both 'conftest.exe' and 'conftest' are 'present' (well, observable) # catch 'conftest.exe'. For instance with Cygwin, 'ls conftest' will # work properly (i.e., refer to 'conftest.exe'), while it won't with # 'rm'. for ac_file in conftest.exe conftest conftest.*; do test -f "$ac_file" || continue case $ac_file in *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj ) ;; *.* ) ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'` break;; * ) break;; esac done else case e in #( e) { { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: in '$ac_pwd':" >&5 printf "%s\n" "$as_me: error: in '$ac_pwd':" >&2;} as_fn_error $? "cannot compute suffix of executables: cannot compile and link See 'config.log' for more details" "$LINENO" 5; } ;; esac fi rm -f conftest conftest$ac_cv_exeext { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_cv_exeext" >&5 printf "%s\n" "$ac_cv_exeext" >&6; } rm -f conftest.$ac_ext EXEEXT=$ac_cv_exeext ac_exeext=$EXEEXT cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ #include int main (void) { FILE *f = fopen ("conftest.out", "w"); if (!f) return 1; return ferror (f) || fclose (f) != 0; ; return 0; } _ACEOF ac_clean_files="$ac_clean_files conftest.out" # Check that the compiler produces executables we can run. If not, either # the compiler is broken, or we cross compile. { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking whether we are cross compiling" >&5 printf %s "checking whether we are cross compiling... " >&6; } if test "$cross_compiling" != yes; then { { ac_try="$ac_link" case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" printf "%s\n" "$ac_try_echo"; } >&5 (eval "$ac_link") 2>&5 ac_status=$? printf "%s\n" "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; } if { ac_try='./conftest$ac_cv_exeext' { { case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" printf "%s\n" "$ac_try_echo"; } >&5 (eval "$ac_try") 2>&5 ac_status=$? printf "%s\n" "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; }; }; then cross_compiling=no else if test "$cross_compiling" = maybe; then cross_compiling=yes else { { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: in '$ac_pwd':" >&5 printf "%s\n" "$as_me: error: in '$ac_pwd':" >&2;} as_fn_error 77 "cannot run C compiled programs. If you meant to cross compile, use '--host'. See 'config.log' for more details" "$LINENO" 5; } fi fi fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $cross_compiling" >&5 printf "%s\n" "$cross_compiling" >&6; } rm -f conftest.$ac_ext conftest$ac_cv_exeext \ conftest.o conftest.obj conftest.out ac_clean_files=$ac_clean_files_save { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for suffix of object files" >&5 printf %s "checking for suffix of object files... " >&6; } if test ${ac_cv_objext+y} then : printf %s "(cached) " >&6 else case e in #( e) cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ int main (void) { ; return 0; } _ACEOF rm -f conftest.o conftest.obj if { { ac_try="$ac_compile" case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" printf "%s\n" "$ac_try_echo"; } >&5 (eval "$ac_compile") 2>&5 ac_status=$? printf "%s\n" "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; } then : for ac_file in conftest.o conftest.obj conftest.*; do test -f "$ac_file" || continue; case $ac_file in *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM ) ;; *) ac_cv_objext=`expr "$ac_file" : '.*\.\(.*\)'` break;; esac done else case e in #( e) printf "%s\n" "$as_me: failed program was:" >&5 sed 's/^/| /' conftest.$ac_ext >&5 { { printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: in '$ac_pwd':" >&5 printf "%s\n" "$as_me: error: in '$ac_pwd':" >&2;} as_fn_error $? "cannot compute suffix of object files: cannot compile See 'config.log' for more details" "$LINENO" 5; } ;; esac fi rm -f conftest.$ac_cv_objext conftest.$ac_ext ;; esac fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_cv_objext" >&5 printf "%s\n" "$ac_cv_objext" >&6; } OBJEXT=$ac_cv_objext ac_objext=$OBJEXT { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking whether the compiler supports GNU C" >&5 printf %s "checking whether the compiler supports GNU C... " >&6; } if test ${ac_cv_c_compiler_gnu+y} then : printf %s "(cached) " >&6 else case e in #( e) cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ int main (void) { #ifndef __GNUC__ choke me #endif ; return 0; } _ACEOF if ac_fn_c_try_compile "$LINENO" then : ac_compiler_gnu=yes else case e in #( e) ac_compiler_gnu=no ;; esac fi rm -f core conftest.err conftest.$ac_objext conftest.beam conftest.$ac_ext ac_cv_c_compiler_gnu=$ac_compiler_gnu ;; esac fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_cv_c_compiler_gnu" >&5 printf "%s\n" "$ac_cv_c_compiler_gnu" >&6; } ac_compiler_gnu=$ac_cv_c_compiler_gnu if test $ac_compiler_gnu = yes; then GCC=yes else GCC= fi ac_test_CFLAGS=${CFLAGS+y} ac_save_CFLAGS=$CFLAGS { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5 printf %s "checking whether $CC accepts -g... " >&6; } if test ${ac_cv_prog_cc_g+y} then : printf %s "(cached) " >&6 else case e in #( e) ac_save_c_werror_flag=$ac_c_werror_flag ac_c_werror_flag=yes ac_cv_prog_cc_g=no CFLAGS="-g" cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ int main (void) { ; return 0; } _ACEOF if ac_fn_c_try_compile "$LINENO" then : ac_cv_prog_cc_g=yes else case e in #( e) CFLAGS="" cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ int main (void) { ; return 0; } _ACEOF if ac_fn_c_try_compile "$LINENO" then : else case e in #( e) ac_c_werror_flag=$ac_save_c_werror_flag CFLAGS="-g" cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ int main (void) { ; return 0; } _ACEOF if ac_fn_c_try_compile "$LINENO" then : ac_cv_prog_cc_g=yes fi rm -f core conftest.err conftest.$ac_objext conftest.beam conftest.$ac_ext ;; esac fi rm -f core conftest.err conftest.$ac_objext conftest.beam conftest.$ac_ext ;; esac fi rm -f core conftest.err conftest.$ac_objext conftest.beam conftest.$ac_ext ac_c_werror_flag=$ac_save_c_werror_flag ;; esac fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_g" >&5 printf "%s\n" "$ac_cv_prog_cc_g" >&6; } if test $ac_test_CFLAGS; then CFLAGS=$ac_save_CFLAGS elif test $ac_cv_prog_cc_g = yes; then if test "$GCC" = yes; then CFLAGS="-g -O2" else CFLAGS="-g" fi else if test "$GCC" = yes; then CFLAGS="-O2" else CFLAGS= fi fi ac_prog_cc_stdc=no if test x$ac_prog_cc_stdc = xno then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $CC option to enable C11 features" >&5 printf %s "checking for $CC option to enable C11 features... " >&6; } if test ${ac_cv_prog_cc_c11+y} then : printf %s "(cached) " >&6 else case e in #( e) ac_cv_prog_cc_c11=no ac_save_CC=$CC cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ $ac_c_conftest_c11_program _ACEOF for ac_arg in '' -std=gnu11 do CC="$ac_save_CC $ac_arg" if ac_fn_c_try_compile "$LINENO" then : ac_cv_prog_cc_c11=$ac_arg fi rm -f core conftest.err conftest.$ac_objext conftest.beam test "x$ac_cv_prog_cc_c11" != "xno" && break done rm -f conftest.$ac_ext CC=$ac_save_CC ;; esac fi if test "x$ac_cv_prog_cc_c11" = xno then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5 printf "%s\n" "unsupported" >&6; } else case e in #( e) if test "x$ac_cv_prog_cc_c11" = x then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: none needed" >&5 printf "%s\n" "none needed" >&6; } else case e in #( e) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c11" >&5 printf "%s\n" "$ac_cv_prog_cc_c11" >&6; } CC="$CC $ac_cv_prog_cc_c11" ;; esac fi ac_cv_prog_cc_stdc=$ac_cv_prog_cc_c11 ac_prog_cc_stdc=c11 ;; esac fi fi if test x$ac_prog_cc_stdc = xno then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $CC option to enable C99 features" >&5 printf %s "checking for $CC option to enable C99 features... " >&6; } if test ${ac_cv_prog_cc_c99+y} then : printf %s "(cached) " >&6 else case e in #( e) ac_cv_prog_cc_c99=no ac_save_CC=$CC cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ $ac_c_conftest_c99_program _ACEOF for ac_arg in '' -std=gnu99 -std=c99 -c99 -qlanglvl=extc1x -qlanglvl=extc99 -AC99 -D_STDC_C99= do CC="$ac_save_CC $ac_arg" if ac_fn_c_try_compile "$LINENO" then : ac_cv_prog_cc_c99=$ac_arg fi rm -f core conftest.err conftest.$ac_objext conftest.beam test "x$ac_cv_prog_cc_c99" != "xno" && break done rm -f conftest.$ac_ext CC=$ac_save_CC ;; esac fi if test "x$ac_cv_prog_cc_c99" = xno then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5 printf "%s\n" "unsupported" >&6; } else case e in #( e) if test "x$ac_cv_prog_cc_c99" = x then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: none needed" >&5 printf "%s\n" "none needed" >&6; } else case e in #( e) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c99" >&5 printf "%s\n" "$ac_cv_prog_cc_c99" >&6; } CC="$CC $ac_cv_prog_cc_c99" ;; esac fi ac_cv_prog_cc_stdc=$ac_cv_prog_cc_c99 ac_prog_cc_stdc=c99 ;; esac fi fi if test x$ac_prog_cc_stdc = xno then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $CC option to enable C89 features" >&5 printf %s "checking for $CC option to enable C89 features... " >&6; } if test ${ac_cv_prog_cc_c89+y} then : printf %s "(cached) " >&6 else case e in #( e) ac_cv_prog_cc_c89=no ac_save_CC=$CC cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ $ac_c_conftest_c89_program _ACEOF for ac_arg in '' -qlanglvl=extc89 -qlanglvl=ansi -std -Ae "-Aa -D_HPUX_SOURCE" "-Xc -D__EXTENSIONS__" do CC="$ac_save_CC $ac_arg" if ac_fn_c_try_compile "$LINENO" then : ac_cv_prog_cc_c89=$ac_arg fi rm -f core conftest.err conftest.$ac_objext conftest.beam test "x$ac_cv_prog_cc_c89" != "xno" && break done rm -f conftest.$ac_ext CC=$ac_save_CC ;; esac fi if test "x$ac_cv_prog_cc_c89" = xno then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5 printf "%s\n" "unsupported" >&6; } else case e in #( e) if test "x$ac_cv_prog_cc_c89" = x then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: none needed" >&5 printf "%s\n" "none needed" >&6; } else case e in #( e) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c89" >&5 printf "%s\n" "$ac_cv_prog_cc_c89" >&6; } CC="$CC $ac_cv_prog_cc_c89" ;; esac fi ac_cv_prog_cc_stdc=$ac_cv_prog_cc_c89 ac_prog_cc_stdc=c89 ;; esac fi fi ac_ext=c ac_cpp='$CPP $CPPFLAGS' ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5' ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' ac_compiler_gnu=$ac_cv_c_compiler_gnu { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for a race-free mkdir -p" >&5 printf %s "checking for a race-free mkdir -p... " >&6; } if test -z "$MKDIR_P"; then if test ${ac_cv_path_mkdir+y} then : printf %s "(cached) " >&6 else case e in #( e) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH$PATH_SEPARATOR/opt/sfw/bin do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_prog in mkdir gmkdir; do for ac_exec_ext in '' $ac_executable_extensions; do as_fn_executable_p "$as_dir$ac_prog$ac_exec_ext" || continue case `"$as_dir$ac_prog$ac_exec_ext" --version 2>&1` in #( 'mkdir ('*'coreutils) '* | \ *'BusyBox '* | \ 'mkdir (fileutils) '4.1*) ac_cv_path_mkdir=$as_dir$ac_prog$ac_exec_ext break 3;; esac done done done IFS=$as_save_IFS ;; esac fi test -d ./--version && rmdir ./--version if test ${ac_cv_path_mkdir+y}; then MKDIR_P="$ac_cv_path_mkdir -p" else # As a last resort, use plain mkdir -p, # in the hope it doesn't have the bugs of ancient mkdir. MKDIR_P='mkdir -p' fi fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $MKDIR_P" >&5 printf "%s\n" "$MKDIR_P" >&6; } # Find a good install program. We prefer a C program (faster), # so one script is as good as another. But avoid the broken or # incompatible versions: # SysV /etc/install, /usr/sbin/install # SunOS /usr/etc/install # IRIX /sbin/install # AIX /bin/install # AmigaOS /C/install, which installs bootblocks on floppy discs # AIX 4 /usr/bin/installbsd, which doesn't work without a -g flag # AFS /usr/afsws/bin/install, which mishandles nonexistent args # SVR4 /usr/ucb/install, which tries to use the nonexistent group "staff" # OS/2's system install, which has a completely different semantic # ./install, which can be erroneously created by make from ./install.sh. # Reject install programs that cannot install multiple files. { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for a BSD-compatible install" >&5 printf %s "checking for a BSD-compatible install... " >&6; } if test -z "$INSTALL"; then if test ${ac_cv_path_install+y} then : printf %s "(cached) " >&6 else case e in #( e) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac # Account for fact that we put trailing slashes in our PATH walk. case $as_dir in #(( ./ | /[cC]/* | \ /etc/* | /usr/sbin/* | /usr/etc/* | /sbin/* | /usr/afsws/bin/* | \ ?:[\\/]os2[\\/]install[\\/]* | ?:[\\/]OS2[\\/]INSTALL[\\/]* | \ /usr/ucb/* ) ;; *) # OSF1 and SCO ODT 3.0 have their own names for install. # Don't use installbsd from OSF since it installs stuff as root # by default. for ac_prog in ginstall scoinst install; do for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_prog$ac_exec_ext"; then if test $ac_prog = install && grep dspmsg "$as_dir$ac_prog$ac_exec_ext" >/dev/null 2>&1; then # AIX install. It has an incompatible calling convention. : elif test $ac_prog = install && grep pwplus "$as_dir$ac_prog$ac_exec_ext" >/dev/null 2>&1; then # program-specific install script used by HP pwplus--don't use. : else rm -rf conftest.one conftest.two conftest.dir echo one > conftest.one echo two > conftest.two mkdir conftest.dir if "$as_dir$ac_prog$ac_exec_ext" -c conftest.one conftest.two "`pwd`/conftest.dir/" && test -s conftest.one && test -s conftest.two && test -s conftest.dir/conftest.one && test -s conftest.dir/conftest.two then ac_cv_path_install="$as_dir$ac_prog$ac_exec_ext -c" break 3 fi fi fi done done ;; esac done IFS=$as_save_IFS rm -rf conftest.one conftest.two conftest.dir ;; esac fi if test ${ac_cv_path_install+y}; then INSTALL=$ac_cv_path_install else # As a last resort, use the slow shell script. Don't cache a # value for INSTALL within a source directory, because that will # break other packages using the cache if that directory is # removed, or if the value is a relative name. INSTALL=$ac_install_sh fi fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $INSTALL" >&5 printf "%s\n" "$INSTALL" >&6; } # Use test -z because SunOS4 sh mishandles braces in ${var-val}. # It thinks the first close brace ends the variable substitution. test -z "$INSTALL_PROGRAM" && INSTALL_PROGRAM='${INSTALL}' test -z "$INSTALL_SCRIPT" && INSTALL_SCRIPT='${INSTALL}' test -z "$INSTALL_DATA" && INSTALL_DATA='${INSTALL} -m 644' # Check for the rest of Ocaml compilers # we extract Ocaml version number OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version *\(.*\)$|\1|p'` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: ocaml version is $OCAMLVERSION" >&5 printf "%s\n" "$as_me: ocaml version is $OCAMLVERSION" >&6;} as_arg_v1=$OCAMLVERSION as_arg_v2=4.08.0 awk "$as_awk_strverscmp" v1="$as_arg_v1" v2="$as_arg_v2" /dev/null case $? in #( 1) : as_fn_error $? "You need Objective Caml 4.08.0 or higher." "$LINENO" 5 ;; #( 0) : ;; #( 2) : ;; #( *) : ;; esac # Ocaml library path # old way: OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d ' ' | tr -d '\\r'` OCAMLLIB=$($OCAMLC -where | tr -d '\r' | tr '\\' '/') { printf "%s\n" "$as_me:${as_lineno-$LINENO}: ocaml library path is $OCAMLLIB" >&5 printf "%s\n" "$as_me: ocaml library path is $OCAMLLIB" >&6;} # then we look for ocamlopt; if not present, we issue a warning # if the version is not the same, we also discard it # we set OCAMLBEST to "opt" or "byte", whether ocamlopt is available or not # Extract the first word of "ocamlopt", so it can be a program name with args. set dummy ocamlopt; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLOPT+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLOPT"; then ac_cv_prog_OCAMLOPT="$OCAMLOPT" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLOPT="ocamlopt" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLOPT" && ac_cv_prog_OCAMLOPT="no" fi ;; esac fi OCAMLOPT=$ac_cv_prog_OCAMLOPT if test -n "$OCAMLOPT"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLOPT" >&5 printf "%s\n" "$OCAMLOPT" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi OCAMLBEST=byte if test "$OCAMLOPT" = no ; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find ocamlopt; bytecode compilation only." >&5 printf "%s\n" "$as_me: WARNING: cannot find ocamlopt; bytecode compilation only." >&2;} else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking ocamlopt version" >&5 printf %s "checking ocamlopt version... " >&6; } TMPVERSION=`$OCAMLOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p'` if test "$TMPVERSION" != "$OCAMLVERSION" ; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: differs from ocamlc; ocamlopt discarded." >&5 printf "%s\n" "differs from ocamlc; ocamlopt discarded." >&6; } OCAMLOPT=no else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: ok" >&5 printf "%s\n" "ok" >&6; } OCAMLBEST=opt fi fi # checking for native-code if test "$enable_native_code" != yes || test "$OCAMLBEST" = byte ; then enable_native_code=no OCAMLBEST=byte OCAMLOPT=no fi # checking for ocamlc.opt # Extract the first word of "ocamlc.opt", so it can be a program name with args. set dummy ocamlc.opt; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLCDOTOPT+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLCDOTOPT"; then ac_cv_prog_OCAMLCDOTOPT="$OCAMLCDOTOPT" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLCDOTOPT="ocamlc.opt" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLCDOTOPT" && ac_cv_prog_OCAMLCDOTOPT="no" fi ;; esac fi OCAMLCDOTOPT=$ac_cv_prog_OCAMLCDOTOPT if test -n "$OCAMLCDOTOPT"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLCDOTOPT" >&5 printf "%s\n" "$OCAMLCDOTOPT" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLCDOTOPT" != no ; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking ocamlc.opt version" >&5 printf %s "checking ocamlc.opt version... " >&6; } TMPVERSION=`$OCAMLCDOTOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p'` if test "$TMPVERSION" != "$OCAMLVERSION" ; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: differs from ocamlc; ocamlc.opt discarded." >&5 printf "%s\n" "differs from ocamlc; ocamlc.opt discarded." >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: ok" >&5 printf "%s\n" "ok" >&6; } OCAMLC=$OCAMLCDOTOPT fi fi # checking for ocamlopt.opt if test "$OCAMLOPT" != no ; then # Extract the first word of "ocamlopt.opt", so it can be a program name with args. set dummy ocamlopt.opt; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLOPTDOTOPT+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLOPTDOTOPT"; then ac_cv_prog_OCAMLOPTDOTOPT="$OCAMLOPTDOTOPT" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLOPTDOTOPT="ocamlopt.opt" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLOPTDOTOPT" && ac_cv_prog_OCAMLOPTDOTOPT="no" fi ;; esac fi OCAMLOPTDOTOPT=$ac_cv_prog_OCAMLOPTDOTOPT if test -n "$OCAMLOPTDOTOPT"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLOPTDOTOPT" >&5 printf "%s\n" "$OCAMLOPTDOTOPT" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLOPTDOTOPT" != no ; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking ocamlc.opt version" >&5 printf %s "checking ocamlc.opt version... " >&6; } TMPVER=`$OCAMLOPTDOTOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p'` if test "$TMPVER" != "$OCAMLVERSION" ; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: differs from ocamlc; ocamlopt.opt discarded." >&5 printf "%s\n" "differs from ocamlc; ocamlopt.opt discarded." >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: ok" >&5 printf "%s\n" "ok" >&6; } OCAMLOPT=$OCAMLOPTDOTOPT fi fi fi # ocamldep, ocamllex and ocamlyacc should also be present in the path # Extract the first word of "ocamldep", so it can be a program name with args. set dummy ocamldep; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLDEP+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLDEP"; then ac_cv_prog_OCAMLDEP="$OCAMLDEP" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLDEP="ocamldep" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLDEP" && ac_cv_prog_OCAMLDEP="no" fi ;; esac fi OCAMLDEP=$ac_cv_prog_OCAMLDEP if test -n "$OCAMLDEP"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLDEP" >&5 printf "%s\n" "$OCAMLDEP" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLDEP" = no ; then as_fn_error $? "cannot find ocamldep." "$LINENO" 5 else # Extract the first word of "ocamldep.opt", so it can be a program name with args. set dummy ocamldep.opt; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLDEPDOTOPT+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLDEPDOTOPT"; then ac_cv_prog_OCAMLDEPDOTOPT="$OCAMLDEPDOTOPT" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLDEPDOTOPT="ocamldep.opt" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLDEPDOTOPT" && ac_cv_prog_OCAMLDEPDOTOPT="no" fi ;; esac fi OCAMLDEPDOTOPT=$ac_cv_prog_OCAMLDEPDOTOPT if test -n "$OCAMLDEPDOTOPT"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLDEPDOTOPT" >&5 printf "%s\n" "$OCAMLDEPDOTOPT" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLDEPDOTOPT" != no ; then OCAMLDEP=$OCAMLDEPDOTOPT fi fi # Extract the first word of "ocamllex", so it can be a program name with args. set dummy ocamllex; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLLEX+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLLEX"; then ac_cv_prog_OCAMLLEX="$OCAMLLEX" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLLEX="ocamllex" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLLEX" && ac_cv_prog_OCAMLLEX="no" fi ;; esac fi OCAMLLEX=$ac_cv_prog_OCAMLLEX if test -n "$OCAMLLEX"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLLEX" >&5 printf "%s\n" "$OCAMLLEX" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLLEX" = no ; then as_fn_error $? "cannot find ocamllex." "$LINENO" 5 else # Extract the first word of "ocamllex.opt", so it can be a program name with args. set dummy ocamllex.opt; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLLEXDOTOPT+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLLEXDOTOPT"; then ac_cv_prog_OCAMLLEXDOTOPT="$OCAMLLEXDOTOPT" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLLEXDOTOPT="ocamllex.opt" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLLEXDOTOPT" && ac_cv_prog_OCAMLLEXDOTOPT="no" fi ;; esac fi OCAMLLEXDOTOPT=$ac_cv_prog_OCAMLLEXDOTOPT if test -n "$OCAMLLEXDOTOPT"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLLEXDOTOPT" >&5 printf "%s\n" "$OCAMLLEXDOTOPT" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLLEXDOTOPT" != no ; then OCAMLLEX=$OCAMLLEXDOTOPT fi fi # Extract the first word of "ocamlyacc", so it can be a program name with args. set dummy ocamlyacc; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLYACC+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLYACC"; then ac_cv_prog_OCAMLYACC="$OCAMLYACC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLYACC="ocamlyacc" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLYACC" && ac_cv_prog_OCAMLYACC="no" fi ;; esac fi OCAMLYACC=$ac_cv_prog_OCAMLYACC if test -n "$OCAMLYACC"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLYACC" >&5 printf "%s\n" "$OCAMLYACC" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLYACC" = no ; then as_fn_error $? "cannot find ocamlyacc." "$LINENO" 5 fi # Extract the first word of "ocamldoc", so it can be a program name with args. set dummy ocamldoc; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLDOC+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLDOC"; then ac_cv_prog_OCAMLDOC="$OCAMLDOC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLDOC="ocamldoc" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLDOC" && ac_cv_prog_OCAMLDOC="true" fi ;; esac fi OCAMLDOC=$ac_cv_prog_OCAMLDOC if test -n "$OCAMLDOC"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLDOC" >&5 printf "%s\n" "$OCAMLDOC" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLDOC" != true ; then # Extract the first word of "ocamldoc.opt", so it can be a program name with args. set dummy ocamldoc.opt; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLDOCOPT+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLDOCOPT"; then ac_cv_prog_OCAMLDOCOPT="$OCAMLDOCOPT" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLDOCOPT="ocamldoc.opt" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLDOCOPT" && ac_cv_prog_OCAMLDOCOPT="no" fi ;; esac fi OCAMLDOCOPT=$ac_cv_prog_OCAMLDOCOPT if test -n "$OCAMLDOCOPT"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLDOCOPT" >&5 printf "%s\n" "$OCAMLDOCOPT" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLDOCOPT" != no ; then OCAMLDOC=$OCAMLDOCOPT fi fi # Extract the first word of "menhir", so it can be a program name with args. set dummy menhir; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_MENHIR+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$MENHIR"; then ac_cv_prog_MENHIR="$MENHIR" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_MENHIR="menhir" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_MENHIR" && ac_cv_prog_MENHIR="no" fi ;; esac fi MENHIR=$ac_cv_prog_MENHIR if test -n "$MENHIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $MENHIR" >&5 printf "%s\n" "$MENHIR" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$MENHIR" = no ; then as_fn_error $? "cannot find menhir." "$LINENO" 5 fi MENHIRVERSION=`$MENHIR --version | sed -n -e 's,.*version *\(.*\)$,\1,p'` as_arg_v1=$MENHIRVERSION as_arg_v2=20170418 awk "$as_awk_strverscmp" v1="$as_arg_v1" v2="$as_arg_v2" /dev/null case $? in #( 1) : as_fn_error $? "You need Menhir 20170418 or higher." "$LINENO" 5 ;; #( 0) : ;; #( 2) : ;; #( *) : ;; esac found_ocamlfind=no if test "$enable_ocamlfind" != no; then # Extract the first word of "ocamlfind", so it can be a program name with args. set dummy ocamlfind; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_OCAMLFIND+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$OCAMLFIND"; then ac_cv_prog_OCAMLFIND="$OCAMLFIND" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_OCAMLFIND="ocamlfind" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_OCAMLFIND" && ac_cv_prog_OCAMLFIND="no" fi ;; esac fi OCAMLFIND=$ac_cv_prog_OCAMLFIND if test -n "$OCAMLFIND"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $OCAMLFIND" >&5 printf "%s\n" "$OCAMLFIND" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$OCAMLFIND" = no; then reason_ocamlfind=" (not found)" else OCAMLFINDLIB=$(ocamlfind printconf stdlib | tr -d '\r' | tr '\\' '/') if test "$OCAMLFINDLIB" != "$OCAMLLIB"; then found_ocamlfind=no reason_ocamlfind=" (incompatible with OCaml)" echo "but your ocamlfind is not compatible with your ocamlc:" echo "ocamlfind: $OCAMLFINDLIB, ocamlc: $OCAMLLIB" else found_ocamlfind=yes fi fi fi if test "$found_ocamlfind" = no; then if test "$enable_ocamlfind" = yes; then as_fn_error $? "cannot use ocamlfind." "$LINENO" 5 fi enable_ocamlfind=no fi if test "$enable_ocamlfind" != no; then #if ocamlfind is used it gives the install path for ocaml library OCAMLINSTALLLIB=$($OCAMLFIND printconf destdir | tr -d '\r' | tr '\\' '/') enable_ocamlfind=yes else OCAMLINSTALLLIB=$OCAMLLIB OCAMLFIND=no fi if test "$enable_why3_lib" = yes ; then WHY3LIB= else if test "$enable_ocamlfind" = no; then as_fn_error $? "cannot use --disable-why3-lib without ocamlfind." "$LINENO" 5 fi WHY3LIB=why3 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for Why3 using ocamlfind" >&5 printf %s "checking for Why3 using ocamlfind... " >&6; } DIR=$($OCAMLFIND query why3 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } WHY3INCLUDE="-I $DIR" else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } as_fn_error $? "cannot use --disable-why3-lib without an installed Why3." "$LINENO" 5 fi fi if test "$enable_local" = no; then LOCALDIR='' else if test "$OCAML_OS_TYPE" = Win32 -a "$BUILD_ENV_TYPE" = Cygwin; then LOCALDIR="$(cygpath -m "$PWD" | tr -d '\r')" else LOCALDIR="$PWD" fi fi # ppx if test "$enable_ocamlfind" = yes; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for ppxlib using ocamlfind" >&5 printf %s "checking for ppxlib using ocamlfind... " >&6; } PPXLIB=$($OCAMLFIND query ppxlib 2> /dev/null | tr -d '\r') if test -n "$PPXLIB"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } enable_ppx=yes else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } enable_ppx=no reason_ppx=" (ppxlib not found)" fi else enable_ppx=no fi # checking for sphinx if test "$enable_doc" = yes; then # Extract the first word of "sphinx-build", so it can be a program name with args. set dummy sphinx-build; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_SPHINX+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$SPHINX"; then ac_cv_prog_SPHINX="$SPHINX" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_SPHINX="sphinx-build" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_SPHINX" && ac_cv_prog_SPHINX="no" fi ;; esac fi SPHINX=$ac_cv_prog_SPHINX if test -n "$SPHINX"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $SPHINX" >&5 printf "%s\n" "$SPHINX" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$SPHINX" = no; then enable_doc=no enable_pdf_doc=no reason_doc=" (sphinx-build not found)" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find sphinx-build, documentation disabled." >&5 printf "%s\n" "$as_me: WARNING: cannot find sphinx-build, documentation disabled." >&2;} fi else enable_pdf_doc=no fi # checking for rubber or latexmk or pdflatex if test "$enable_pdf_doc" = yes; then for ac_prog in latexmk rubber pdflatex do # Extract the first word of "$ac_prog", so it can be a program name with args. set dummy $ac_prog; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_LATEX+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$LATEX"; then ac_cv_prog_LATEX="$LATEX" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_LATEX="$ac_prog" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS fi ;; esac fi LATEX=$ac_cv_prog_LATEX if test -n "$LATEX"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $LATEX" >&5 printf "%s\n" "$LATEX" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi test -n "$LATEX" && break done test -n "$LATEX" || LATEX="no" if test "$LATEX" = no; then enable_pdf_doc=no reason_pdf_doc=" ((rubber|latexmk|pdflatex) not found)" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find any latex compiler, PDF documentation disabled." >&5 printf "%s\n" "$as_me: WARNING: cannot find any latex compiler, PDF documentation disabled." >&2;} fi fi # checking for emacs if test "$enable_emacs_compilation" = yes ; then # Extract the first word of "emacs", so it can be a program name with args. set dummy emacs; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_EMACS+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$EMACS"; then ac_cv_prog_EMACS="$EMACS" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_EMACS="emacs" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_EMACS" && ac_cv_prog_EMACS="no" fi ;; esac fi EMACS=$ac_cv_prog_EMACS if test -n "$EMACS"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $EMACS" >&5 printf "%s\n" "$EMACS" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$EMACS" = no ; then enable_emacs_compilation=no { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find emacs, compilation of why3.elc disabled." >&5 printf "%s\n" "$as_me: WARNING: cannot find emacs, compilation of why3.elc disabled." >&2;} fi fi # checking for Zarith DIR= found_zarith=yes if test "$enable_ocamlfind" = yes; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for zarith using ocamlfind" >&5 printf %s "checking for zarith using ocamlfind... " >&6; } DIR=$($OCAMLFIND query zarith 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } BIGINTINCLUDE="-I $DIR" else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } found_zarith=no fi else BIGINTINCLUDE="-I +zarith" DIR="$OCAMLLIB/zarith" as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/zarith.cma" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/zarith.cma" >&5 printf %s "checking for $DIR/zarith.cma... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/zarith.cma"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_zarith=no ;; esac fi fi if test -n "$DIR"; then as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/z.cmi" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/z.cmi" >&5 printf %s "checking for $DIR/z.cmi... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/z.cmi"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_zarith=no ;; esac fi fi if test "$found_zarith" = no; then as_fn_error $? "cannot find library zarith." "$LINENO" 5 fi # checking for apron for bddinfer if test "$enable_bddinfer" = yes; then if test "$enable_ocamlfind" = yes; then # gmp is a dependency of apron INFERINCLUDE=$($OCAMLFIND query -separator ' ' -i-format apron 2> /dev/null | tr -d '\r') fi if test -n "$INFERINCLUDE"; then echo "ocamlfind found apron in $INFERINCLUDE" INFERLIB="apron" INFERPKG="zarith apron apron.polkaMPQ" else enable_bddinfer=no reason_bddinfer=" (apron not found)" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: Lib apron not found, bddinfer will not be built." >&5 printf "%s\n" "$as_me: WARNING: Lib apron not found, bddinfer will not be built." >&2;} fi else reason_bddinfer=" (disabled by default)" fi # checking for apron and fixpoint if test "$enable_infer" = yes; then if test "$enable_ocamlfind" = yes; then # gmp is a dependency of apron INFERINCLUDE=$($OCAMLFIND query apron camllib 2> /dev/null | tr -d '\r') fi if test -n "$INFERINCLUDE"; then echo "ocamlfind found apron, camllib in $INFERINCLUDE" INFERINCLUDE=$($OCAMLFIND query fixpoint 2> /dev/null | tr -d '\r') if test -n "$INFERINCLUDE"; then echo "ocamlfind found fixpoint in $INFERINCLUDE" INFERINCLUDE="$($OCAMLFIND query -separator ' ' -i-format apron fixpoint camllib gmp 2> /dev/null | tr -d '\r')" INFERLIB="apron fixpoint" INFERPKG="apron fixpoint apron.boxMPQ apron.octMPQ apron.polkaMPQ" else enable_infer=no { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: Lib fixpoint not found, infer will not be built." >&5 printf "%s\n" "$as_me: WARNING: Lib fixpoint not found, infer will not be built." >&2;} reason_infer=" (fixpoint not found)" fi else enable_infer=no reason_infer=" (apron or camllib not found)" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: Lib apron or camllib not found, infer will not be built." >&5 printf "%s\n" "$as_me: WARNING: Lib apron or camllib not found, infer will not be built." >&2;} fi else reason_infer=" (disabled by default)" fi # checking for camlzip if test "$enable_zip" = no; then reason_zip=" (disabled by user)" else DIR= found_zip=yes if test "$enable_ocamlfind" = yes; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for camlzip using ocamlfind" >&5 printf %s "checking for camlzip using ocamlfind... " >&6; } DIR=$($OCAMLFIND query zip 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } ZIPINCLUDE="-I $DIR" else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } found_zip=no fi else ZIPINCLUDE="-I +zip" DIR="$OCAMLLIB/zip" as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/zip.cma" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/zip.cma" >&5 printf %s "checking for $DIR/zip.cma... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/zip.cma"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_zip=no ;; esac fi fi if test -n "$DIR"; then as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/zip.cmi" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/zip.cmi" >&5 printf %s "checking for $DIR/zip.cmi... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/zip.cmi"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_zip=no ;; esac fi fi if test "$found_zip" = no; then if test "$enable_zip" = yes; then as_fn_error $? "cannot find library camlzip." "$LINENO" 5 fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find library camlzip; sessions files will not be compressed." >&5 printf "%s\n" "$as_me: WARNING: cannot find library camlzip; sessions files will not be compressed." >&2;} enable_zip=no reason_zip=" (camlzip not found)" fi fi if test "$enable_zip" != no; then ZIPLIB=zip enable_zip=yes else ZIPLIB= ZIPINCLUDE= fi # checking for menhirlib found_menhirlib=yes DIR= if test "$enable_ocamlfind" = yes; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for menhirLib using ocamlfind" >&5 printf %s "checking for menhirLib using ocamlfind... " >&6; } DIR=$($OCAMLFIND query menhirLib 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } MENHIRINCLUDE="-I $DIR" else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } found_menhirlib=no fi else MENHIRINCLUDE="-I +menhirLib" DIR="$OCAMLLIB/menhirLib" menhirlib_cmo= as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/menhirLib.cmo" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/menhirLib.cmo" >&5 printf %s "checking for $DIR/menhirLib.cmo... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/menhirLib.cmo"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : menhirlib_cmo=yes fi as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/menhirLib.cma" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/menhirLib.cma" >&5 printf %s "checking for $DIR/menhirLib.cma... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/menhirLib.cma"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : menhirlib_cmo=no fi if test -z "$menhirlib_cmo"; then found_menhirlib=no; fi fi if test -n "$DIR"; then as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/menhirLib.cmi" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/menhirLib.cmi" >&5 printf %s "checking for $DIR/menhirLib.cmi... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/menhirLib.cmi"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_menhirlib=no ;; esac fi fi if test "$found_menhirlib" = no; then as_fn_error $? "cannot find library menhirLib." "$LINENO" 5 fi # checking for re if test "$enable_re" = no; then reason_re=" (disabled by user)" else found_re=yes DIR= if test "$enable_ocamlfind" = yes; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for re using ocamlfind" >&5 printf %s "checking for re using ocamlfind... " >&6; } DIR=$($OCAMLFIND query re 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } REINCLUDE="-I $DIR" else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } found_re=no fi else REINCLUDE="-I +re" DIR="$OCAMLLIB/re" as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/re.cmx" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/re.cmx" >&5 printf %s "checking for $DIR/re.cmx... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/re.cmx"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_re=no ;; esac fi fi if test -n "$DIR"; then as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/re.cmi" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/re.cmi" >&5 printf %s "checking for $DIR/re.cmi... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/re.cmi"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_re=no ;; esac fi fi if test "$found_re" = no; then if test "$enable_re" = yes; then as_fn_error $? "cannot find library re." "$LINENO" 5 fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find library re, using Str instead." >&5 printf "%s\n" "$as_me: WARNING: cannot find library re, using Str instead." >&2;} enable_re=no reason_re=" (re not found)" fi fi if test "$enable_re" != no; then RELIB=re enable_re=yes else REINCLUDE= RELIB=str fi # checking for lablgtk3 if test "$enable_ide" = no ; then reason_ide=" (disabled by user)" fi if test "$enable_ide" != no -a "$enable_ocamlfind" = no; then if test "$enable_ide" = yes; then as_fn_error $? "cannot build IDE without ocamlfind." "$LINENO" 5 fi enable_ide=no reason_ide=" (ocamlfind not available)" fi found_lablgtk=no if test "$enable_ide" != no; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for lablgtk3 using ocamlfind" >&5 printf %s "checking for lablgtk3 using ocamlfind... " >&6; } DIR=$($OCAMLFIND query lablgtk3 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } found_lablgtk=yes as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/gtkButton.cmi" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/gtkButton.cmi" >&5 printf %s "checking for $DIR/gtkButton.cmi... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/gtkButton.cmi"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_lablgtk=no ;; esac fi else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } found_lablgtk=no fi if test "$found_lablgtk" = yes; then GTKVERSION=3 PKGS_SOURCEVIEW="lablgtk3-sourceview3 lablgtk3.sourceview3 lablgtksourceview3" fi fi # checking for lablgtksourceview found_lablgtksourceview=no if test "$found_lablgtk" = yes; then for p in $PKGS_SOURCEVIEW; do { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $p using ocamlfind" >&5 printf %s "checking for $p using ocamlfind... " >&6; } DIR=$($OCAMLFIND query $p 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/gSourceView$GTKVERSION.cmi" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/gSourceView$GTKVERSION.cmi" >&5 printf %s "checking for $DIR/gSourceView$GTKVERSION.cmi... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/gSourceView$GTKVERSION.cmi"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) p= ;; esac fi if test -n "$p"; then PKG_SOURCEVIEW=$p break fi else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi done if test -n "$PKG_SOURCEVIEW"; then found_lablgtksourceview=yes fi fi if test "$enable_ide" != no -a "$found_lablgtk" = no; then if test "$enable_ide" = yes; then as_fn_error $? "cannot build IDE without lablgtk3." "$LINENO" 5 fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find library lablgtk3, IDE disabled." >&5 printf "%s\n" "$as_me: WARNING: cannot find library lablgtk3, IDE disabled." >&2;} enable_ide=no reason_ide=" (lablgtk3 not found)" fi if test "$enable_ide" != no -a "$found_lablgtksourceview" = no; then if test "$enable_ide" = yes; then as_fn_error $? "cannot build IDE without lablgtksourceview." "$LINENO" 5 fi { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find library lablgtksourceview, IDE disabled." >&5 printf "%s\n" "$as_me: WARNING: cannot find library lablgtksourceview, IDE disabled." >&2;} enable_ide=no reason_ide=" (lablgtksourceview not found)" fi if test "$enable_ide" != no; then enable_ide=yes LABLGTKPKG="lablgtk$GTKVERSION $PKG_SOURCEVIEW" fi if test "$enable_hypothesis_selection" != no -o "$enable_stackify" != no; then found_ocamlgraph=yes DIR= if test "$enable_ocamlfind" = yes; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for ocamlgraph using ocamlfind" >&5 printf %s "checking for ocamlgraph using ocamlfind... " >&6; } DIR=$($OCAMLFIND query ocamlgraph 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } OCAMLGRAPHLIB="$DIR" else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } found_ocamlgraph=no fi else OCAMLGRAPHLIB="+ocamlgraph" DIR="$OCAMLLIB/ocamlgraph" as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/graph.cma" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/graph.cma" >&5 printf %s "checking for $DIR/graph.cma... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/graph.cma"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_ocamlgraph=no ;; esac fi fi if test -n "$DIR"; then as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/graph.cmi" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/graph.cmi" >&5 printf %s "checking for $DIR/graph.cmi... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/graph.cmi"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_ocamlgraph=no ;; esac fi fi fi if test "$enable_hypothesis_selection" = no; then reason_hypothesis_selection=" (disabled by user)" elif test "$found_ocamlgraph" = no; then if test "$enable_hypothesis_selection" = yes; then as_fn_error $? "cannot enable hypothesis selection without ocamlgraph." "$LINENO" 5 fi enable_hypothesis_selection=no reason_hypothesis_selection=" (ocamlgraph not found)" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find library ocamlgraph, hypothesis selection disabled." >&5 printf "%s\n" "$as_me: WARNING: cannot find library ocamlgraph, hypothesis selection disabled." >&2;} fi if test "$enable_hypothesis_selection" != no; then enable_hypothesis_selection=yes fi if test "$enable_stackify" = no; then reason_stackify=" (disabled by user)" elif test "$found_ocamlgraph" = no; then if test "$enable_stackify" = yes; then as_fn_error $? "cannot enable stackify without ocamlgraph." "$LINENO" 5 fi enable_stackify=no reason_stackify=" (ocamlgraph not found)" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot find library ocamlgraph, stackify disabled." >&5 printf "%s\n" "$as_me: WARNING: cannot find library ocamlgraph, stackify disabled." >&2;} else as_arg_v1=$OCAMLVERSION as_arg_v2=4.12 awk "$as_awk_strverscmp" v1="$as_arg_v1" v2="$as_arg_v2" /dev/null case $? in #( 1) : if test "$enable_stackify" = yes; then as_fn_error $? "cannot enable stackify without ocaml >= 4.12." "$LINENO" 5 fi enable_stackify=no reason_stackify=" (ocaml < 4.12)" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: ocaml is < 4.12, stackify disabled." >&5 printf "%s\n" "$as_me: WARNING: ocaml is < 4.12, stackify disabled." >&2;} ;; #( 0) : ;; #( 2) : ;; #( *) : ;; esac fi if test "$enable_stackify" != no; then enable_stackify=yes fi if test "$enable_hypothesis_selection" != no -o "$enable_stackify" != no; then META_OCAMLGRAPH="ocamlgraph" else META_OCAMLGRAPH= OCAMLGRAPHLIB= fi # MLMPFR found_mlmpfr=no if test "$enable_mpfr" = no; then reason_mpfr=" (disabled by user)" elif test "$enable_ocamlfind" != yes; then reason_mpfr=" (ocamlfind not available)" elif test "$enable_js_of_ocaml" = yes -o "$enable_web_ide" = yes; then if test "$enable_mpfr" = yes; then as_fn_error $? "cannot enable support for both MPFR and Javascript." "$LINENO" 5 fi reason_mpfr=" (incompatible with js_of_ocaml) " else found_mlmpfr=yes { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for mlmpfr" >&5 printf %s "checking for mlmpfr... " >&6; } DIR=$($OCAMLFIND query mlmpfr 2> /dev/null | tr -d '\r') if test -n "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } old_mpfr=no echo "ocamlfind found mlmpfr in $DIR" # Test that MPFR version is higher than 4.0.0 (because of # Faithful constructor incompatibility). MPFRVERSION=$($OCAMLFIND query -format "%v" mlmpfr 2> /dev/null | tr -d '\r') as_arg_v1=$MPFRVERSION as_arg_v2=4.0.0 awk "$as_awk_strverscmp" v1="$as_arg_v1" v2="$as_arg_v2" /dev/null case $? in #( 1) : found_mlmpfr=no reason_mpfr=" (mlmpfr >= 4.0.0 not found)" ;; #( 0) : ;; #( 2) : ;; #( *) : ;; esac as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/mpfr.cmi" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/mpfr.cmi" >&5 printf %s "checking for $DIR/mpfr.cmi... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/mpfr.cmi"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : old_mpfr=yes fi as_ac_File=`printf "%s\n" "ac_cv_file_$DIR/mlmpfr.cma" | sed "$as_sed_sh"` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $DIR/mlmpfr.cma" >&5 printf %s "checking for $DIR/mlmpfr.cma... " >&6; } if eval test \${$as_ac_File+y} then : printf %s "(cached) " >&6 else case e in #( e) test "$cross_compiling" = yes && as_fn_error $? "cannot check for file existence when cross compiling" "$LINENO" 5 if test -r "$DIR/mlmpfr.cma"; then eval "$as_ac_File=yes" else eval "$as_ac_File=no" fi ;; esac fi eval ac_res=\$$as_ac_File { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 printf "%s\n" "$ac_res" >&6; } if eval test \"x\$"$as_ac_File"\" = x"yes" then : else case e in #( e) found_mlmpfr=no reason_mpfr=" (mlmpfr not found)" ;; esac fi else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } reason_mpfr=" (mlmpfr not found)" found_mlmpfr=no fi fi if test "$enable_mpfr" != no -a "$found_mlmpfr" = no; then if test "$enable_mpfr" = yes; then as_fn_error $? "cannot enable MPFR support without mlmpfr." "$LINENO" 5 fi enable_mpfr=no fi if test "$enable_mpfr" != no; then enable_mpfr=yes MLMPFR=mlmpfr fi # checking for js_of_ocaml found_js_of_ocaml=no if test "$enable_js_of_ocaml" = no; then reason_js_of_ocaml=" (disabled by user)" elif test "$enable_mpfr" = yes; then reason_js_of_ocaml=" (incompatible with MPFR support)" elif test "$enable_ocamlfind" != yes; then reason_js_of_ocaml=" (ocamlfind not available)" else found_js_of_ocaml=yes for p in js_of_ocaml js_of_ocaml-ppx zarith_stubs_js; do { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $p" >&5 printf %s "checking for $p... " >&6; } DIR=$($OCAMLFIND query $p 2> /dev/null | tr -d '\r') if test -z "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } found_js_of_ocaml=no reason_js_of_ocaml=" ($p not found)" break else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } fi done fi if test "$enable_js_of_ocaml" != no -a "$found_js_of_ocaml" = no; then if test "$enable_js_of_ocaml" = yes; then as_fn_error $? "cannot enable Javascript support without ocamlfind." "$LINENO" 5 fi enable_js_of_ocaml=no fi if test "$enable_js_of_ocaml" != no; then JSOFOCAMLVERSION=$($OCAMLFIND query -format "%v" js_of_ocaml 2> /dev/null | tr -d '\r') as_arg_v1=$JSOFOCAMLVERSION as_arg_v2=5.6.0 awk "$as_awk_strverscmp" v1="$as_arg_v1" v2="$as_arg_v2" /dev/null case $? in #( 1) : found_js_of_ocaml=no reason_js_of_ocaml=" (js_of_ocaml >= 5.6.0 not found)" ;; #( 0) : ;; #( 2) : ;; #( *) : ;; esac fi if test "$enable_js_of_ocaml" != no -a "$found_js_of_ocaml" = no; then if test "$enable_js_of_ocaml" = yes; then as_fn_error $? "cannot enable Javascript support without js_of_ocaml >= 5.6.0 (found $JSOFOCAMLVERSION)." "$LINENO" 5 fi enable_js_of_ocaml=no fi if test "$enable_js_of_ocaml" != no; then enable_js_of_ocaml=yes JSOFOCAMLPKG="js_of_ocaml js_of_ocaml-ppx" fi # Web IDE if test "$enable_web_ide" = no; then reason_web_ide=" (disabled by user)" elif test "$enable_js_of_ocaml" != yes; then if test "$enable_web_ide" = yes; then as_fn_error $? "cannot enable web IDE without Javascript support." "$LINENO" 5 fi enable_web_ide=no reason_web_ide=" (Javascript support not available)" else enable_web_ide=yes fi # checking for statmemprof if test "$enable_statmemprof" = yes; then if test "$enable_ocamlfind" != yes; then enable_statmemprof=no reason_statmemprof=" (ocamlfind not available)" else DIR=$($OCAMLFIND query statmemprof-emacs 2> /dev/null | tr -d '\r') if test -z "$DIR"; then enable_statmemprof=no reason_statmemprof=" (statmemprof-emacs not found)" fi STATMEMPROFPKG=statmemprof-emacs fi fi # ppx_sexp_conv (only with ocamlfind) SEXPLIBPPX= SEXPLIB= if test "$enable_sexp" = no; then reason_sexp=" (disabled by user)" else if test "$enable_ocamlfind" != yes; then enable_sexp=no reason_sexp=" (ocamlfind not available)" elif test "$enable_ppx" != yes; then enable_sexp=no reason_sexp=" (requires ppx)" else for p in ppx_sexp_conv sexplib ppx_deriving; do { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $p using ocamlfind" >&5 printf %s "checking for $p using ocamlfind... " >&6; } DIR=$($OCAMLFIND query $p 2> /dev/null | tr -d '\r') if test -z "$DIR"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } enable_sexp=no reason_sexp=" ($p not found)" break else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } fi done fi if test "$enable_sexp" = yes; then SEXPLIBPPX="ppx_sexp_conv" SEXPLIB="sexplib" fi fi # Coq enable_coq_support=yes enable_coq_fp_libs=yes coq_compat_version= if test "$enable_coq_libs" = no; then enable_coq_support=no reason_coq_support=" (disabled by user)" fi if test "$enable_coq_support" = yes; then # Extract the first word of "coqc", so it can be a program name with args. set dummy coqc; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_COQC+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$COQC"; then ac_cv_prog_COQC="$COQC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_COQC="coqc" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_COQC" && ac_cv_prog_COQC="no" fi ;; esac fi COQC=$ac_cv_prog_COQC if test -n "$COQC"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $COQC" >&5 printf "%s\n" "$COQC" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$COQC" = no ; then enable_coq_support=no reason_coq_support=" (coqc not found)" fi fi if test "$enable_coq_support" = yes; then COQLIB=`$COQC -where | sed -e 's|\\\|/|g' -e 's| |\\ |g'` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking Coq version" >&5 printf %s "checking Coq version... " >&6; } COQVERSION=`$COQC -v | sed -n -e 's|.*version *\([^ ]*\).*|\1|p'` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $COQVERSION" >&5 printf "%s\n" "$COQVERSION" >&6; } COQNUMVERSION=`echo $COQVERSION | awk -F. '{ printf("%d%02d\n", $1,$2); }'` if test "$COQNUMVERSION" -lt 816; then if test "$enable_coq_libs" = yes; then as_fn_error $? "cannot build Coq libraries without Coq >= 8.16." "$LINENO" 5 fi enable_coq_support=no { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cannot build Coq libraries without Coq >= 8.16." >&5 printf "%s\n" "$as_me: WARNING: cannot build Coq libraries without Coq >= 8.16." >&2;} reason_coq_support=" (need version >= 8.16)" else if test "$COQNUMVERSION" -ge 817; then COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality" fi if test "$COQNUMVERSION" -gt 820; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: unrecognized Coq version, assuming Coq 8.20" >&5 printf "%s\n" "$as_me: WARNING: unrecognized Coq version, assuming Coq 8.20" >&2;} COQNUMVERSION=820 fi coq_compat_version="COQ$COQNUMVERSION" fi if test "$enable_coq_fp_libs" = no; then reason_coq_fp_libs= " (Coq < 8.11)" fi fi if test "$enable_coq_support" = yes; then # Extract the first word of "coqdep", so it can be a program name with args. set dummy coqdep; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_COQDEP+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$COQDEP"; then ac_cv_prog_COQDEP="$COQDEP" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_COQDEP="coqdep" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_COQDEP" && ac_cv_prog_COQDEP="no" fi ;; esac fi COQDEP=$ac_cv_prog_COQDEP if test -n "$COQDEP"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $COQDEP" >&5 printf "%s\n" "$COQDEP" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$COQDEP" = no; then if test "$enable_coq_libs" = yes; then as_fn_error $? "cannot build Coq libraries without Coqdep." "$LINENO" 5 fi enable_coq_support=no reason_coq_support=" (coqdep not found)" fi fi if test "$enable_coq_support" = no; then enable_coq_libs=no enable_coq_fp_libs=no COQVERSION= else enable_coq_libs=yes fi if test "$enable_coq_fp_libs" = yes; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for Flocq" >&5 printf %s "checking for Flocq... " >&6; } if echo "Require Import Flocq.Version BinNat." \ "Goal (30400 <= Flocq_version)%N. easy. Qed." > conftest.v "$COQC" conftest.v > conftest.err then : { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5 printf "%s\n" "yes" >&6; } else case e in #( e) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } enable_coq_fp_libs=no reason_coq_fp_libs=" (Flocq >= 3.4 not found)" ;; esac fi rm -f conftest.v conftest.vo conftest.err fi # PVS if test "$enable_pvs_libs" = no; then enable_pvs_support=no reason_pvs_support=" (disabled by user)" else # Extract the first word of "pvs", so it can be a program name with args. set dummy pvs; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_PVS+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$PVS"; then ac_cv_prog_PVS="$PVS" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_PVS="pvs" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_PVS" && ac_cv_prog_PVS="no" fi ;; esac fi PVS=$ac_cv_prog_PVS if test -n "$PVS"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $PVS" >&5 printf "%s\n" "$PVS" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$PVS" = no ; then enable_pvs_support=no reason_pvs_support=" (pvs not found)" elif $PVS --help 2> /dev/null | grep -q "physical volume"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: pvs does not seem to be the theorem prover" >&5 printf "%s\n" "$as_me: pvs does not seem to be the theorem prover" >&6;} enable_pvs_support=no reason_pvs_support=" (pvs not found)" else PVSLIB=`$PVS -where` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking PVS version" >&5 printf %s "checking PVS version... " >&6; } PVSVERSION=`$PVS -version | sed -n -e 's|.*Version *\([^ ]*\)$|\1|p'` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $PVSVERSION" >&5 printf "%s\n" "$PVSVERSION" >&6; } case $PVSVERSION in 6.*|7.*) enable_pvs_support=yes ;; *) enable_pvs_support=no { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: You need PVS 6.0 or higher; PVS discarded." >&5 printf "%s\n" "$as_me: WARNING: You need PVS 6.0 or higher; PVS discarded." >&2;} reason_pvs_support=" (need version 6.0 or higher)" ;; esac fi fi if test "$enable_pvs_support" = no; then enable_pvs_libs=no PVSVERSION= fi # Isabelle # Default version used for generation of realization in the case Isabelle is not # detected or Why3 is compiled with disable-isabelle. ISABELLEVERSION=2021-1 if test "$enable_isabelle_libs" = no; then enable_isabelle_support=no reason_isabelle_support=" (disabled by user)" else # Extract the first word of "isabelle", so it can be a program name with args. set dummy isabelle; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_ISABELLE+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$ISABELLE"; then ac_cv_prog_ISABELLE="$ISABELLE" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_ISABELLE="isabelle" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_ISABELLE" && ac_cv_prog_ISABELLE="no" fi ;; esac fi ISABELLE=$ac_cv_prog_ISABELLE if test -n "$ISABELLE"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ISABELLE" >&5 printf "%s\n" "$ISABELLE" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$ISABELLE" = no ; then enable_isabelle_support=no reason_isabelle_support=" (isabelle not found)" else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking Isabelle version" >&5 printf %s "checking Isabelle version... " >&6; } ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([^:]*\).*$|\1|p'` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $ISABELLEDETECTEDVERSION" >&5 printf "%s\n" "$ISABELLEDETECTEDVERSION" >&6; } case $ISABELLEDETECTEDVERSION in 2019*) enable_isabelle_support=yes ISABELLEVERSION=2019 ;; 2021-1*) enable_isabelle_support=yes ISABELLEVERSION=2021-1 ;; 2022*) enable_isabelle_support=yes ISABELLEVERSION=2021-1 ;; *) enable_isabelle_support=no { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: You need Isabelle 2019 or later; Isabelle discarded." >&5 printf "%s\n" "$as_me: WARNING: You need Isabelle 2019 or later; Isabelle discarded." >&2;} reason_isabelle_support=" (need version >= 2019)" ;; esac fi fi if test "$enable_isabelle_support" = no; then enable_isabelle_libs=no fi if test "$enable_pvs_libs" = yes; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for NASA PVS library" >&5 printf %s "checking for NASA PVS library... " >&6; } enable_pvs_libs=no reason_pvs_libs=" (no NASA PVS library in PVS_LIBRARY_PATH)" for dir in `echo $PVS_LIBRARY_PATH | tr ':' ' '`; do if test -f $dir/nasalib-version; then enable_pvs_libs=yes reason_pvs_libs="" fi done { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $enable_pvs_libs" >&5 printf "%s\n" "$enable_pvs_libs" >&6; } fi #check frama-c FRAMAC_SUPPORTED=Sulfur if test "$enable_frama_c" = yes ; then # Extract the first word of "frama-c", so it can be a program name with args. set dummy frama-c; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_FRAMAC+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$FRAMAC"; then ac_cv_prog_FRAMAC="$FRAMAC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_FRAMAC="frama-c" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_FRAMAC" && ac_cv_prog_FRAMAC="no" fi ;; esac fi FRAMAC=$ac_cv_prog_FRAMAC if test -n "$FRAMAC"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $FRAMAC" >&5 printf "%s\n" "$FRAMAC" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi if test "$FRAMAC" = no ; then enable_frama_c="no" reason_frama_c=" (frama-c not found)" else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking Frama-C version" >&5 printf %s "checking Frama-C version... " >&6; } FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|\(Version: \)\?\(.*\)$|\2|p'` { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $FRAMAC_VERSION" >&5 printf "%s\n" "$FRAMAC_VERSION" >&6; } case $FRAMAC_VERSION in $FRAMAC_SUPPORTED-*) ;; *) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: Version $FRAMAC_SUPPORTED required." >&5 printf "%s\n" "$as_me: WARNING: Version $FRAMAC_SUPPORTED required." >&2;} enable_frama_c=no reason_frama_c=" (version $FRAMAC_SUPPORTED required)" ;; esac fi fi if test "$enable_frama_c" = yes; then FRAMAC_SHARE=`$FRAMAC -print-path` FRAMAC_LIBDIR=`$FRAMAC -print-libpath` FRAMAC_INCLUDE="-I $FRAMAC_LIBDIR" fi VERSION=$PACKAGE_VERSION # default editor if test -z "$EDITOR"; then case `uname -s` in Darwin) EDITOR=open ;; MINGW*) EDITOR="cmd.exe -c start" ;; *) EDITOR=xdg-open ;; esac fi # Check presence of java and javac used by whyml2java bench if test "$enable_java" = yes; then # Extract the first word of "javac", so it can be a program name with args. set dummy javac; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_JAVAC+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$JAVAC"; then ac_cv_prog_JAVAC="$JAVAC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_JAVAC="javac" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_JAVAC" && ac_cv_prog_JAVAC="no" fi ;; esac fi JAVAC=$ac_cv_prog_JAVAC if test -n "$JAVAC"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $JAVAC" >&5 printf "%s\n" "$JAVAC" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi # Extract the first word of "java", so it can be a program name with args. set dummy java; ac_word=$2 { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 printf %s "checking for $ac_word... " >&6; } if test ${ac_cv_prog_JAVA+y} then : printf %s "(cached) " >&6 else case e in #( e) if test -n "$JAVA"; then ac_cv_prog_JAVA="$JAVA" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir$ac_word$ac_exec_ext"; then ac_cv_prog_JAVA="java" printf "%s\n" "$as_me:${as_lineno-$LINENO}: found $as_dir$ac_word$ac_exec_ext" >&5 break 2 fi done done IFS=$as_save_IFS test -z "$ac_cv_prog_JAVA" && ac_cv_prog_JAVA="no" fi ;; esac fi JAVA=$ac_cv_prog_JAVA if test -n "$JAVA"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: $JAVA" >&5 printf "%s\n" "$JAVA" >&6; } else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: no" >&5 printf "%s\n" "no" >&6; } fi else JAVAC=no JAVA=no fi # substitutions to perform # Finally create the Makefile from Makefile.in ac_config_files="$ac_config_files Makefile" ac_config_files="$ac_config_files src/config.sh" ac_config_files="$ac_config_files lib/why3/META" ac_config_files="$ac_config_files .merlin" ac_config_files="$ac_config_files src/jessie/Makefile" ac_config_files="$ac_config_files src/jessie/.merlin" ac_config_files="$ac_config_files lib/coq/version lib/pvs/version" ac_config_files="$ac_config_files bench/java/Makefile" ac_config_files="$ac_config_files doc/javaexamples/Makefile" ac_config_commands="$ac_config_commands chmod" cat >confcache <<\_ACEOF # This file is a shell script that caches the results of configure # tests run on this system so they can be shared between configure # scripts and configure runs, see configure's option --config-cache. # It is not useful on other systems. If it contains results you don't # want to keep, you may remove or edit it. # # config.status only pays attention to the cache file if you give it # the --recheck option to rerun configure. # # 'ac_cv_env_foo' variables (set or unset) will be overridden when # loading this file, other *unset* 'ac_cv_foo' will be assigned the # following values. _ACEOF # The following way of writing the cache mishandles newlines in values, # but we know of no workaround that is simple, portable, and efficient. # So, we kill variables containing newlines. # Ultrix sh set writes to stderr and can't be redirected directly, # and sets the high bit in the cache file unless we assign to the vars. ( for ac_var in `(set) 2>&1 | sed -n 's/^\([a-zA-Z_][a-zA-Z0-9_]*\)=.*/\1/p'`; do eval ac_val=\$$ac_var case $ac_val in #( *${as_nl}*) case $ac_var in #( *_cv_*) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: cache variable $ac_var contains a newline" >&5 printf "%s\n" "$as_me: WARNING: cache variable $ac_var contains a newline" >&2;} ;; esac case $ac_var in #( _ | IFS | as_nl) ;; #( BASH_ARGV | BASH_SOURCE) eval $ac_var= ;; #( *) { eval $ac_var=; unset $ac_var;} ;; esac ;; esac done (set) 2>&1 | case $as_nl`(ac_space=' '; set) 2>&1` in #( *${as_nl}ac_space=\ *) # 'set' does not quote correctly, so add quotes: double-quote # substitution turns \\\\ into \\, and sed turns \\ into \. sed -n \ "s/'/'\\\\''/g; s/^\\([_$as_cr_alnum]*_cv_[_$as_cr_alnum]*\\)=\\(.*\\)/\\1='\\2'/p" ;; #( *) # 'set' quotes correctly as required by POSIX, so do not add quotes. sed -n "/^[_$as_cr_alnum]*_cv_[_$as_cr_alnum]*=/p" ;; esac | sort ) | sed ' /^ac_cv_env_/b end t clear :clear s/^\([^=]*\)=\(.*[{}].*\)$/test ${\1+y} || &/ t end s/^\([^=]*\)=\(.*\)$/\1=${\1=\2}/ :end' >>confcache if diff "$cache_file" confcache >/dev/null 2>&1; then :; else if test -w "$cache_file"; then if test "x$cache_file" != "x/dev/null"; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: updating cache $cache_file" >&5 printf "%s\n" "$as_me: updating cache $cache_file" >&6;} if test ! -f "$cache_file" || test -h "$cache_file"; then cat confcache >"$cache_file" else case $cache_file in #( */* | ?:*) mv -f confcache "$cache_file"$$ && mv -f "$cache_file"$$ "$cache_file" ;; #( *) mv -f confcache "$cache_file" ;; esac fi fi else { printf "%s\n" "$as_me:${as_lineno-$LINENO}: not updating unwritable cache $cache_file" >&5 printf "%s\n" "$as_me: not updating unwritable cache $cache_file" >&6;} fi fi rm -f confcache test "x$prefix" = xNONE && prefix=$ac_default_prefix # Let make expand exec_prefix. test "x$exec_prefix" = xNONE && exec_prefix='${prefix}' # Transform confdefs.h into DEFS. # Protect against shell expansion while executing Makefile rules. # Protect against Makefile macro expansion. # # If the first sed substitution is executed (which looks for macros that # take arguments), then branch to the quote section. Otherwise, # look for a macro that doesn't take arguments. ac_script=' :mline /\\$/{ N s,\\\n,, b mline } t clear :clear s/^[ ]*#[ ]*define[ ][ ]*\([^ (][^ (]*([^)]*)\)[ ]*\(.*\)/-D\1=\2/g t quote s/^[ ]*#[ ]*define[ ][ ]*\([^ ][^ ]*\)[ ]*\(.*\)/-D\1=\2/g t quote b any :quote s/[][ `~#$^&*(){}\\|;'\''"<>?]/\\&/g s/\$/$$/g H :any ${ g s/^\n// s/\n/ /g p } ' DEFS=`sed -n "$ac_script" confdefs.h` ac_libobjs= ac_ltlibobjs= U= for ac_i in : $LIBOBJS; do test "x$ac_i" = x: && continue # 1. Remove the extension, and $U if already installed. ac_script='s/\$U\././;s/\.o$//;s/\.obj$//' ac_i=`printf "%s\n" "$ac_i" | sed "$ac_script"` # 2. Prepend LIBOBJDIR. When used with automake>=1.10 LIBOBJDIR # will be set to the directory where LIBOBJS objects are built. as_fn_append ac_libobjs " \${LIBOBJDIR}$ac_i\$U.$ac_objext" as_fn_append ac_ltlibobjs " \${LIBOBJDIR}$ac_i"'$U.lo' done LIBOBJS=$ac_libobjs LTLIBOBJS=$ac_ltlibobjs : "${CONFIG_STATUS=./config.status}" ac_write_fail=0 ac_clean_files_save=$ac_clean_files ac_clean_files="$ac_clean_files $CONFIG_STATUS" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: creating $CONFIG_STATUS" >&5 printf "%s\n" "$as_me: creating $CONFIG_STATUS" >&6;} as_write_fail=0 cat >$CONFIG_STATUS <<_ASEOF || as_write_fail=1 #! $SHELL # Generated by $as_me. # Run this file to recreate the current configuration. # Compiler output produced by configure, useful for debugging # configure, is in config.log if it exists. debug=false ac_cs_recheck=false ac_cs_silent=false SHELL=\${CONFIG_SHELL-$SHELL} export SHELL _ASEOF cat >>$CONFIG_STATUS <<\_ASEOF || as_write_fail=1 ## -------------------- ## ## M4sh Initialization. ## ## -------------------- ## # Be more Bourne compatible DUALCASE=1; export DUALCASE # for MKS sh if test ${ZSH_VERSION+y} && (emulate sh) >/dev/null 2>&1 then : emulate sh NULLCMD=: # Pre-4.2 versions of Zsh do word splitting on ${1+"$@"}, which # is contrary to our usage. Disable this feature. alias -g '${1+"$@"}'='"$@"' setopt NO_GLOB_SUBST else case e in #( e) case `(set -o) 2>/dev/null` in #( *posix*) : set -o posix ;; #( *) : ;; esac ;; esac fi # Reset variables that may have inherited troublesome values from # the environment. # IFS needs to be set, to space, tab, and newline, in precisely that order. # (If _AS_PATH_WALK were called with IFS unset, it would have the # side effect of setting IFS to empty, thus disabling word splitting.) # Quoting is to prevent editors from complaining about space-tab. as_nl=' ' export as_nl IFS=" "" $as_nl" PS1='$ ' PS2='> ' PS4='+ ' # Ensure predictable behavior from utilities with locale-dependent output. LC_ALL=C export LC_ALL LANGUAGE=C export LANGUAGE # We cannot yet rely on "unset" to work, but we need these variables # to be unset--not just set to an empty or harmless value--now, to # avoid bugs in old shells (e.g. pre-3.0 UWIN ksh). This construct # also avoids known problems related to "unset" and subshell syntax # in other old shells (e.g. bash 2.01 and pdksh 5.2.14). for as_var in BASH_ENV ENV MAIL MAILPATH CDPATH do eval test \${$as_var+y} \ && ( (unset $as_var) || exit 1) >/dev/null 2>&1 && unset $as_var || : done # Ensure that fds 0, 1, and 2 are open. if (exec 3>&0) 2>/dev/null; then :; else exec 0&1) 2>/dev/null; then :; else exec 1>/dev/null; fi if (exec 3>&2) ; then :; else exec 2>/dev/null; fi # The user is always right. if ${PATH_SEPARATOR+false} :; then PATH_SEPARATOR=: (PATH='/bin;/bin'; FPATH=$PATH; sh -c :) >/dev/null 2>&1 && { (PATH='/bin:/bin'; FPATH=$PATH; sh -c :) >/dev/null 2>&1 || PATH_SEPARATOR=';' } fi # Find who we are. Look in the path if we contain no directory separator. as_myself= case $0 in #(( *[\\/]* ) as_myself=$0 ;; *) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH do IFS=$as_save_IFS case $as_dir in #((( '') as_dir=./ ;; */) ;; *) as_dir=$as_dir/ ;; esac test -r "$as_dir$0" && as_myself=$as_dir$0 && break done IFS=$as_save_IFS ;; esac # We did not find ourselves, most probably we were run as 'sh COMMAND' # in which case we are not to be found in the path. if test "x$as_myself" = x; then as_myself=$0 fi if test ! -f "$as_myself"; then printf "%s\n" "$as_myself: error: cannot find myself; rerun with an absolute file name" >&2 exit 1 fi # as_fn_error STATUS ERROR [LINENO LOG_FD] # ---------------------------------------- # Output "`basename $0`: error: ERROR" to stderr. If LINENO and LOG_FD are # provided, also output the error to LOG_FD, referencing LINENO. Then exit the # script with STATUS, using 1 if that was 0. as_fn_error () { as_status=$1; test $as_status -eq 0 && as_status=1 if test "$4"; then as_lineno=${as_lineno-"$3"} as_lineno_stack=as_lineno_stack=$as_lineno_stack printf "%s\n" "$as_me:${as_lineno-$LINENO}: error: $2" >&$4 fi printf "%s\n" "$as_me: error: $2" >&2 as_fn_exit $as_status } # as_fn_error # as_fn_set_status STATUS # ----------------------- # Set $? to STATUS, without forking. as_fn_set_status () { return $1 } # as_fn_set_status # as_fn_exit STATUS # ----------------- # Exit the shell with STATUS, even in a "trap 0" or "set -e" context. as_fn_exit () { set +e as_fn_set_status $1 exit $1 } # as_fn_exit # as_fn_unset VAR # --------------- # Portably unset VAR. as_fn_unset () { { eval $1=; unset $1;} } as_unset=as_fn_unset # as_fn_append VAR VALUE # ---------------------- # Append the text in VALUE to the end of the definition contained in VAR. Take # advantage of any shell optimizations that allow amortized linear growth over # repeated appends, instead of the typical quadratic growth present in naive # implementations. if (eval "as_var=1; as_var+=2; test x\$as_var = x12") 2>/dev/null then : eval 'as_fn_append () { eval $1+=\$2 }' else case e in #( e) as_fn_append () { eval $1=\$$1\$2 } ;; esac fi # as_fn_append # as_fn_arith ARG... # ------------------ # Perform arithmetic evaluation on the ARGs, and store the result in the # global $as_val. Take advantage of shells that can avoid forks. The arguments # must be portable across $(()) and expr. if (eval "test \$(( 1 + 1 )) = 2") 2>/dev/null then : eval 'as_fn_arith () { as_val=$(( $* )) }' else case e in #( e) as_fn_arith () { as_val=`expr "$@" || test $? -eq 1` } ;; esac fi # as_fn_arith if expr a : '\(a\)' >/dev/null 2>&1 && test "X`expr 00001 : '.*\(...\)'`" = X001; then as_expr=expr else as_expr=false fi if (basename -- /) >/dev/null 2>&1 && test "X`basename -- / 2>&1`" = "X/"; then as_basename=basename else as_basename=false fi if (as_dir=`dirname -- /` && test "X$as_dir" = X/) >/dev/null 2>&1; then as_dirname=dirname else as_dirname=false fi as_me=`$as_basename -- "$0" || $as_expr X/"$0" : '.*/\([^/][^/]*\)/*$' \| \ X"$0" : 'X\(//\)$' \| \ X"$0" : 'X\(/\)' \| . 2>/dev/null || printf "%s\n" X/"$0" | sed '/^.*\/\([^/][^/]*\)\/*$/{ s//\1/ q } /^X\/\(\/\/\)$/{ s//\1/ q } /^X\/\(\/\).*/{ s//\1/ q } s/.*/./; q'` # Avoid depending upon Character Ranges. as_cr_letters='abcdefghijklmnopqrstuvwxyz' as_cr_LETTERS='ABCDEFGHIJKLMNOPQRSTUVWXYZ' as_cr_Letters=$as_cr_letters$as_cr_LETTERS as_cr_digits='0123456789' as_cr_alnum=$as_cr_Letters$as_cr_digits # Determine whether it's possible to make 'echo' print without a newline. # These variables are no longer used directly by Autoconf, but are AC_SUBSTed # for compatibility with existing Makefiles. ECHO_C= ECHO_N= ECHO_T= case `echo -n x` in #((((( -n*) case `echo 'xy\c'` in *c*) ECHO_T=' ';; # ECHO_T is single tab character. xy) ECHO_C='\c';; *) echo `echo ksh88 bug on AIX 6.1` > /dev/null ECHO_T=' ';; esac;; *) ECHO_N='-n';; esac # For backward compatibility with old third-party macros, we provide # the shell variables $as_echo and $as_echo_n. New code should use # AS_ECHO(["message"]) and AS_ECHO_N(["message"]), respectively. as_echo='printf %s\n' as_echo_n='printf %s' rm -f conf$$ conf$$.exe conf$$.file if test -d conf$$.dir; then rm -f conf$$.dir/conf$$.file else rm -f conf$$.dir mkdir conf$$.dir 2>/dev/null fi if (echo >conf$$.file) 2>/dev/null; then if ln -s conf$$.file conf$$ 2>/dev/null; then as_ln_s='ln -s' # ... but there are two gotchas: # 1) On MSYS, both 'ln -s file dir' and 'ln file dir' fail. # 2) DJGPP < 2.04 has no symlinks; 'ln -s' creates a wrapper executable. # In both cases, we have to default to 'cp -pR'. ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe || as_ln_s='cp -pR' elif ln conf$$.file conf$$ 2>/dev/null; then as_ln_s=ln else as_ln_s='cp -pR' fi else as_ln_s='cp -pR' fi rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file rmdir conf$$.dir 2>/dev/null # as_fn_mkdir_p # ------------- # Create "$as_dir" as a directory, including parents if necessary. as_fn_mkdir_p () { case $as_dir in #( -*) as_dir=./$as_dir;; esac test -d "$as_dir" || eval $as_mkdir_p || { as_dirs= while :; do case $as_dir in #( *\'*) as_qdir=`printf "%s\n" "$as_dir" | sed "s/'/'\\\\\\\\''/g"`;; #'( *) as_qdir=$as_dir;; esac as_dirs="'$as_qdir' $as_dirs" as_dir=`$as_dirname -- "$as_dir" || $as_expr X"$as_dir" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ X"$as_dir" : 'X\(//\)[^/]' \| \ X"$as_dir" : 'X\(//\)$' \| \ X"$as_dir" : 'X\(/\)' \| . 2>/dev/null || printf "%s\n" X"$as_dir" | sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ s//\1/ q } /^X\(\/\/\)[^/].*/{ s//\1/ q } /^X\(\/\/\)$/{ s//\1/ q } /^X\(\/\).*/{ s//\1/ q } s/.*/./; q'` test -d "$as_dir" && break done test -z "$as_dirs" || eval "mkdir $as_dirs" } || test -d "$as_dir" || as_fn_error $? "cannot create directory $as_dir" } # as_fn_mkdir_p if mkdir -p . 2>/dev/null; then as_mkdir_p='mkdir -p "$as_dir"' else test -d ./-p && rmdir ./-p as_mkdir_p=false fi # as_fn_executable_p FILE # ----------------------- # Test if FILE is an executable regular file. as_fn_executable_p () { test -f "$1" && test -x "$1" } # as_fn_executable_p as_test_x='test -x' as_executable_p=as_fn_executable_p # Sed expression to map a string onto a valid CPP name. as_sed_cpp="y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g" as_tr_cpp="eval sed '$as_sed_cpp'" # deprecated # Sed expression to map a string onto a valid variable name. as_sed_sh="y%*+%pp%;s%[^_$as_cr_alnum]%_%g" as_tr_sh="eval sed '$as_sed_sh'" # deprecated exec 6>&1 ## ----------------------------------- ## ## Main body of $CONFIG_STATUS script. ## ## ----------------------------------- ## _ASEOF test $as_write_fail = 0 && chmod +x $CONFIG_STATUS || ac_write_fail=1 cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 # Save the log message, to keep $0 and so on meaningful, and to # report actual input values of CONFIG_FILES etc. instead of their # values after options handling. ac_log=" This file was extended by Why3 $as_me 1.8.2+git, which was generated by GNU Autoconf 2.72. Invocation command line was CONFIG_FILES = $CONFIG_FILES CONFIG_HEADERS = $CONFIG_HEADERS CONFIG_LINKS = $CONFIG_LINKS CONFIG_COMMANDS = $CONFIG_COMMANDS $ $0 $@ on `(hostname || uname -n) 2>/dev/null | sed 1q` " _ACEOF case $ac_config_files in *" "*) set x $ac_config_files; shift; ac_config_files=$*;; esac cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 # Files that config.status was made for. config_files="$ac_config_files" config_commands="$ac_config_commands" _ACEOF cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 ac_cs_usage="\ '$as_me' instantiates files and other configuration actions from templates according to the current configuration. Unless the files and actions are specified as TAGs, all are instantiated by default. Usage: $0 [OPTION]... [TAG]... -h, --help print this help, then exit -V, --version print version number and configuration settings, then exit --config print configuration, then exit -q, --quiet, --silent do not print progress messages -d, --debug don't remove temporary files --recheck update $as_me by reconfiguring in the same conditions --file=FILE[:TEMPLATE] instantiate the configuration file FILE Configuration files: $config_files Configuration commands: $config_commands Report bugs to the package provider." _ACEOF ac_cs_config=`printf "%s\n" "$ac_configure_args" | sed "$ac_safe_unquote"` ac_cs_config_escaped=`printf "%s\n" "$ac_cs_config" | sed "s/^ //; s/'/'\\\\\\\\''/g"` cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_cs_config='$ac_cs_config_escaped' ac_cs_version="\\ Why3 config.status 1.8.2+git configured by $0, generated by GNU Autoconf 2.72, with options \\"\$ac_cs_config\\" Copyright (C) 2023 Free Software Foundation, Inc. This config.status script is free software; the Free Software Foundation gives unlimited permission to copy, distribute and modify it." ac_pwd='$ac_pwd' srcdir='$srcdir' INSTALL='$INSTALL' MKDIR_P='$MKDIR_P' test -n "\$AWK" || AWK=awk _ACEOF cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 # The default lists apply if the user does not specify any file. ac_need_defaults=: while test $# != 0 do case $1 in --*=?*) ac_option=`expr "X$1" : 'X\([^=]*\)='` ac_optarg=`expr "X$1" : 'X[^=]*=\(.*\)'` ac_shift=: ;; --*=) ac_option=`expr "X$1" : 'X\([^=]*\)='` ac_optarg= ac_shift=: ;; *) ac_option=$1 ac_optarg=$2 ac_shift=shift ;; esac case $ac_option in # Handling of the options. -recheck | --recheck | --rechec | --reche | --rech | --rec | --re | --r) ac_cs_recheck=: ;; --version | --versio | --versi | --vers | --ver | --ve | --v | -V ) printf "%s\n" "$ac_cs_version"; exit ;; --config | --confi | --conf | --con | --co | --c ) printf "%s\n" "$ac_cs_config"; exit ;; --debug | --debu | --deb | --de | --d | -d ) debug=: ;; --file | --fil | --fi | --f ) $ac_shift case $ac_optarg in *\'*) ac_optarg=`printf "%s\n" "$ac_optarg" | sed "s/'/'\\\\\\\\''/g"` ;; '') as_fn_error $? "missing file argument" ;; esac as_fn_append CONFIG_FILES " '$ac_optarg'" ac_need_defaults=false;; --he | --h | --help | --hel | -h ) printf "%s\n" "$ac_cs_usage"; exit ;; -q | -quiet | --quiet | --quie | --qui | --qu | --q \ | -silent | --silent | --silen | --sile | --sil | --si | --s) ac_cs_silent=: ;; # This is an error. -*) as_fn_error $? "unrecognized option: '$1' Try '$0 --help' for more information." ;; *) as_fn_append ac_config_targets " $1" ac_need_defaults=false ;; esac shift done ac_configure_extra_args= if $ac_cs_silent; then exec 6>/dev/null ac_configure_extra_args="$ac_configure_extra_args --silent" fi _ACEOF cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 if \$ac_cs_recheck; then set X $SHELL '$0' $ac_configure_args \$ac_configure_extra_args --no-create --no-recursion shift \printf "%s\n" "running CONFIG_SHELL=$SHELL \$*" >&6 CONFIG_SHELL='$SHELL' export CONFIG_SHELL exec "\$@" fi _ACEOF cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 exec 5>>config.log { echo sed 'h;s/./-/g;s/^.../## /;s/...$/ ##/;p;x;p;x' <<_ASBOX ## Running $as_me. ## _ASBOX printf "%s\n" "$ac_log" } >&5 _ACEOF cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 _ACEOF cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 # Handling of arguments. for ac_config_target in $ac_config_targets do case $ac_config_target in "Makefile") CONFIG_FILES="$CONFIG_FILES Makefile" ;; "src/config.sh") CONFIG_FILES="$CONFIG_FILES src/config.sh" ;; "lib/why3/META") CONFIG_FILES="$CONFIG_FILES lib/why3/META" ;; ".merlin") CONFIG_FILES="$CONFIG_FILES .merlin" ;; "src/jessie/Makefile") CONFIG_FILES="$CONFIG_FILES src/jessie/Makefile" ;; "src/jessie/.merlin") CONFIG_FILES="$CONFIG_FILES src/jessie/.merlin" ;; "lib/coq/version") CONFIG_FILES="$CONFIG_FILES lib/coq/version" ;; "lib/pvs/version") CONFIG_FILES="$CONFIG_FILES lib/pvs/version" ;; "bench/java/Makefile") CONFIG_FILES="$CONFIG_FILES bench/java/Makefile" ;; "doc/javaexamples/Makefile") CONFIG_FILES="$CONFIG_FILES doc/javaexamples/Makefile" ;; "chmod") CONFIG_COMMANDS="$CONFIG_COMMANDS chmod" ;; *) as_fn_error $? "invalid argument: '$ac_config_target'" "$LINENO" 5;; esac done # If the user did not use the arguments to specify the items to instantiate, # then the envvar interface is used. Set only those that are not. # We use the long form for the default assignment because of an extremely # bizarre bug on SunOS 4.1.3. if $ac_need_defaults; then test ${CONFIG_FILES+y} || CONFIG_FILES=$config_files test ${CONFIG_COMMANDS+y} || CONFIG_COMMANDS=$config_commands fi # Have a temporary directory for convenience. Make it in the build tree # simply because there is no reason against having it here, and in addition, # creating and moving files from /tmp can sometimes cause problems. # Hook for its removal unless debugging. # Note that there is a small window in which the directory will not be cleaned: # after its creation but before its name has been assigned to '$tmp'. $debug || { tmp= ac_tmp= trap 'exit_status=$? : "${ac_tmp:=$tmp}" { test ! -d "$ac_tmp" || rm -fr "$ac_tmp"; } && exit $exit_status ' 0 trap 'as_fn_exit 1' 1 2 13 15 } # Create a (secure) tmp directory for tmp files. { tmp=`(umask 077 && mktemp -d "./confXXXXXX") 2>/dev/null` && test -d "$tmp" } || { tmp=./conf$$-$RANDOM (umask 077 && mkdir "$tmp") } || as_fn_error $? "cannot create a temporary directory in ." "$LINENO" 5 ac_tmp=$tmp # Set up the scripts for CONFIG_FILES section. # No need to generate them if there are no CONFIG_FILES. # This happens for instance with './config.status config.h'. if test -n "$CONFIG_FILES"; then ac_cr=`echo X | tr X '\015'` # On cygwin, bash can eat \r inside `` if the user requested igncr. # But we know of no other shell where ac_cr would be empty at this # point, so we can use a bashism as a fallback. if test "x$ac_cr" = x; then eval ac_cr=\$\'\\r\' fi ac_cs_awk_cr=`$AWK 'BEGIN { print "a\rb" }' /dev/null` if test "$ac_cs_awk_cr" = "a${ac_cr}b"; then ac_cs_awk_cr='\\r' else ac_cs_awk_cr=$ac_cr fi echo 'BEGIN {' >"$ac_tmp/subs1.awk" && _ACEOF { echo "cat >conf$$subs.awk <<_ACEOF" && echo "$ac_subst_vars" | sed 's/.*/&!$&$ac_delim/' && echo "_ACEOF" } >conf$$subs.sh || as_fn_error $? "could not make $CONFIG_STATUS" "$LINENO" 5 ac_delim_num=`echo "$ac_subst_vars" | grep -c '^'` ac_delim='%!_!# ' for ac_last_try in false false false false false :; do . ./conf$$subs.sh || as_fn_error $? "could not make $CONFIG_STATUS" "$LINENO" 5 ac_delim_n=`sed -n "s/.*$ac_delim\$/X/p" conf$$subs.awk | grep -c X` if test $ac_delim_n = $ac_delim_num; then break elif $ac_last_try; then as_fn_error $? "could not make $CONFIG_STATUS" "$LINENO" 5 else ac_delim="$ac_delim!$ac_delim _$ac_delim!! " fi done rm -f conf$$subs.sh cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 cat >>"\$ac_tmp/subs1.awk" <<\\_ACAWK && _ACEOF sed -n ' h s/^/S["/; s/!.*/"]=/ p g s/^[^!]*!// :repl t repl s/'"$ac_delim"'$// t delim :nl h s/\(.\{148\}\)..*/\1/ t more1 s/["\\]/\\&/g; s/^/"/; s/$/\\n"\\/ p n b repl :more1 s/["\\]/\\&/g; s/^/"/; s/$/"\\/ p g s/.\{148\}// t nl :delim h s/\(.\{148\}\)..*/\1/ t more2 s/["\\]/\\&/g; s/^/"/; s/$/"/ p b :more2 s/["\\]/\\&/g; s/^/"/; s/$/"\\/ p g s/.\{148\}// t delim ' >$CONFIG_STATUS || ac_write_fail=1 rm -f conf$$subs.awk cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 _ACAWK cat >>"\$ac_tmp/subs1.awk" <<_ACAWK && for (key in S) S_is_set[key] = 1 FS = "" } { line = $ 0 nfields = split(line, field, "@") substed = 0 len = length(field[1]) for (i = 2; i < nfields; i++) { key = field[i] keylen = length(key) if (S_is_set[key]) { value = S[key] line = substr(line, 1, len) "" value "" substr(line, len + keylen + 3) len += length(value) + length(field[++i]) substed = 1 } else len += 1 + keylen } print line } _ACAWK _ACEOF cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 if sed "s/$ac_cr//" < /dev/null > /dev/null 2>&1; then sed "s/$ac_cr\$//; s/$ac_cr/$ac_cs_awk_cr/g" else cat fi < "$ac_tmp/subs1.awk" > "$ac_tmp/subs.awk" \ || as_fn_error $? "could not setup config files machinery" "$LINENO" 5 _ACEOF # VPATH may cause trouble with some makes, so we remove sole $(srcdir), # ${srcdir} and @srcdir@ entries from VPATH if srcdir is ".", strip leading and # trailing colons and then remove the whole line if VPATH becomes empty # (actually we leave an empty line to preserve line numbers). if test "x$srcdir" = x.; then ac_vpsub='/^[ ]*VPATH[ ]*=[ ]*/{ h s/// s/^/:/ s/[ ]*$/:/ s/:\$(srcdir):/:/g s/:\${srcdir}:/:/g s/:@srcdir@:/:/g s/^:*// s/:*$// x s/\(=[ ]*\).*/\1/ G s/\n// s/^[^=]*=[ ]*$// }' fi cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 fi # test -n "$CONFIG_FILES" eval set X " :F $CONFIG_FILES :C $CONFIG_COMMANDS" shift for ac_tag do case $ac_tag in :[FHLC]) ac_mode=$ac_tag; continue;; esac case $ac_mode$ac_tag in :[FHL]*:*);; :L* | :C*:*) as_fn_error $? "invalid tag '$ac_tag'" "$LINENO" 5;; :[FH]-) ac_tag=-:-;; :[FH]*) ac_tag=$ac_tag:$ac_tag.in;; esac ac_save_IFS=$IFS IFS=: set x $ac_tag IFS=$ac_save_IFS shift ac_file=$1 shift case $ac_mode in :L) ac_source=$1;; :[FH]) ac_file_inputs= for ac_f do case $ac_f in -) ac_f="$ac_tmp/stdin";; *) # Look for the file first in the build tree, then in the source tree # (if the path is not absolute). The absolute path cannot be DOS-style, # because $ac_f cannot contain ':'. test -f "$ac_f" || case $ac_f in [\\/$]*) false;; *) test -f "$srcdir/$ac_f" && ac_f="$srcdir/$ac_f";; esac || as_fn_error 1 "cannot find input file: '$ac_f'" "$LINENO" 5;; esac case $ac_f in *\'*) ac_f=`printf "%s\n" "$ac_f" | sed "s/'/'\\\\\\\\''/g"`;; esac as_fn_append ac_file_inputs " '$ac_f'" done # Let's still pretend it is 'configure' which instantiates (i.e., don't # use $as_me), people would be surprised to read: # /* config.h. Generated by config.status. */ configure_input='Generated from '` printf "%s\n" "$*" | sed 's|^[^:]*/||;s|:[^:]*/|, |g' `' by configure.' if test x"$ac_file" != x-; then configure_input="$ac_file. $configure_input" { printf "%s\n" "$as_me:${as_lineno-$LINENO}: creating $ac_file" >&5 printf "%s\n" "$as_me: creating $ac_file" >&6;} fi # Neutralize special characters interpreted by sed in replacement strings. case $configure_input in #( *\&* | *\|* | *\\* ) ac_sed_conf_input=`printf "%s\n" "$configure_input" | sed 's/[\\\\&|]/\\\\&/g'`;; #( *) ac_sed_conf_input=$configure_input;; esac case $ac_tag in *:-:* | *:-) cat >"$ac_tmp/stdin" \ || as_fn_error $? "could not create $ac_file" "$LINENO" 5 ;; esac ;; esac ac_dir=`$as_dirname -- "$ac_file" || $as_expr X"$ac_file" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ X"$ac_file" : 'X\(//\)[^/]' \| \ X"$ac_file" : 'X\(//\)$' \| \ X"$ac_file" : 'X\(/\)' \| . 2>/dev/null || printf "%s\n" X"$ac_file" | sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ s//\1/ q } /^X\(\/\/\)[^/].*/{ s//\1/ q } /^X\(\/\/\)$/{ s//\1/ q } /^X\(\/\).*/{ s//\1/ q } s/.*/./; q'` as_dir="$ac_dir"; as_fn_mkdir_p ac_builddir=. case "$ac_dir" in .) ac_dir_suffix= ac_top_builddir_sub=. ac_top_build_prefix= ;; *) ac_dir_suffix=/`printf "%s\n" "$ac_dir" | sed 's|^\.[\\/]||'` # A ".." for each directory in $ac_dir_suffix. ac_top_builddir_sub=`printf "%s\n" "$ac_dir_suffix" | sed 's|/[^\\/]*|/..|g;s|/||'` case $ac_top_builddir_sub in "") ac_top_builddir_sub=. ac_top_build_prefix= ;; *) ac_top_build_prefix=$ac_top_builddir_sub/ ;; esac ;; esac ac_abs_top_builddir=$ac_pwd ac_abs_builddir=$ac_pwd$ac_dir_suffix # for backward compatibility: ac_top_builddir=$ac_top_build_prefix case $srcdir in .) # We are building in place. ac_srcdir=. ac_top_srcdir=$ac_top_builddir_sub ac_abs_top_srcdir=$ac_pwd ;; [\\/]* | ?:[\\/]* ) # Absolute name. ac_srcdir=$srcdir$ac_dir_suffix; ac_top_srcdir=$srcdir ac_abs_top_srcdir=$srcdir ;; *) # Relative name. ac_srcdir=$ac_top_build_prefix$srcdir$ac_dir_suffix ac_top_srcdir=$ac_top_build_prefix$srcdir ac_abs_top_srcdir=$ac_pwd/$srcdir ;; esac ac_abs_srcdir=$ac_abs_top_srcdir$ac_dir_suffix case $ac_mode in :F) # # CONFIG_FILE # case $INSTALL in [\\/$]* | ?:[\\/]* ) ac_INSTALL=$INSTALL ;; *) ac_INSTALL=$ac_top_build_prefix$INSTALL ;; esac ac_MKDIR_P=$MKDIR_P case $MKDIR_P in [\\/$]* | ?:[\\/]* ) ;; */*) ac_MKDIR_P=$ac_top_build_prefix$MKDIR_P ;; esac _ACEOF cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 # If the template does not know about datarootdir, expand it. # FIXME: This hack should be removed a few years after 2.60. ac_datarootdir_hack=; ac_datarootdir_seen= ac_sed_dataroot=' /datarootdir/ { p q } /@datadir@/p /@docdir@/p /@infodir@/p /@localedir@/p /@mandir@/p' case `eval "sed -n \"\$ac_sed_dataroot\" $ac_file_inputs"` in *datarootdir*) ac_datarootdir_seen=yes;; *@datadir@*|*@docdir@*|*@infodir@*|*@localedir@*|*@mandir@*) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: $ac_file_inputs seems to ignore the --datarootdir setting" >&5 printf "%s\n" "$as_me: WARNING: $ac_file_inputs seems to ignore the --datarootdir setting" >&2;} _ACEOF cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_datarootdir_hack=' s&@datadir@&$datadir&g s&@docdir@&$docdir&g s&@infodir@&$infodir&g s&@localedir@&$localedir&g s&@mandir@&$mandir&g s&\\\${datarootdir}&$datarootdir&g' ;; esac _ACEOF # Neutralize VPATH when '$srcdir' = '.'. # Shell code in configure.ac might set extrasub. # FIXME: do we really want to maintain this feature? cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_sed_extra="$ac_vpsub $extrasub _ACEOF cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 :t /@[a-zA-Z_][a-zA-Z_0-9]*@/!b s|@configure_input@|$ac_sed_conf_input|;t t s&@top_builddir@&$ac_top_builddir_sub&;t t s&@top_build_prefix@&$ac_top_build_prefix&;t t s&@srcdir@&$ac_srcdir&;t t s&@abs_srcdir@&$ac_abs_srcdir&;t t s&@top_srcdir@&$ac_top_srcdir&;t t s&@abs_top_srcdir@&$ac_abs_top_srcdir&;t t s&@builddir@&$ac_builddir&;t t s&@abs_builddir@&$ac_abs_builddir&;t t s&@abs_top_builddir@&$ac_abs_top_builddir&;t t s&@INSTALL@&$ac_INSTALL&;t t s&@MKDIR_P@&$ac_MKDIR_P&;t t $ac_datarootdir_hack " eval sed \"\$ac_sed_extra\" "$ac_file_inputs" | $AWK -f "$ac_tmp/subs.awk" \ >$ac_tmp/out || as_fn_error $? "could not create $ac_file" "$LINENO" 5 test -z "$ac_datarootdir_hack$ac_datarootdir_seen" && { ac_out=`sed -n '/\${datarootdir}/p' "$ac_tmp/out"`; test -n "$ac_out"; } && { ac_out=`sed -n '/^[ ]*datarootdir[ ]*:*=/p' \ "$ac_tmp/out"`; test -z "$ac_out"; } && { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: $ac_file contains a reference to the variable 'datarootdir' which seems to be undefined. Please make sure it is defined" >&5 printf "%s\n" "$as_me: WARNING: $ac_file contains a reference to the variable 'datarootdir' which seems to be undefined. Please make sure it is defined" >&2;} rm -f "$ac_tmp/stdin" case $ac_file in -) cat "$ac_tmp/out" && rm -f "$ac_tmp/out";; *) rm -f "$ac_file" && mv "$ac_tmp/out" "$ac_file";; esac \ || as_fn_error $? "could not create $ac_file" "$LINENO" 5 ;; :C) { printf "%s\n" "$as_me:${as_lineno-$LINENO}: executing $ac_file commands" >&5 printf "%s\n" "$as_me: executing $ac_file commands" >&6;} ;; esac case $ac_file$ac_mode in "chmod":C) chmod a-w Makefile src/jessie/Makefile; chmod a-w src/config.sh; chmod a-w lib/why3/META; chmod a-w .merlin; chmod a-w src/jessie/Makefile; chmod a-w src/jessie/.merlin; chmod a-w lib/coq/version lib/pvs/version; chmod u+x src/config.sh ;; esac done # for ac_tag as_fn_exit 0 _ACEOF ac_clean_files=$ac_clean_files_save test $ac_write_fail = 0 || as_fn_error $? "write failure creating $CONFIG_STATUS" "$LINENO" 5 # configure is writing to config.log, and then calls config.status. # config.status does its own redirection, appending to config.log. # Unfortunately, on DOS this fails, as config.log is still kept open # by configure, so config.status won't be able to write to it; its # output is simply discarded. So we exec the FD to /dev/null, # effectively closing config.log, so it can be properly (re)opened and # appended to by config.status. When coming back to configure, we # need to make the FD available again. if test "$no_create" != yes; then ac_cs_success=: ac_config_status_args= test "$silent" = yes && ac_config_status_args="$ac_config_status_args --quiet" exec 5>/dev/null $SHELL $CONFIG_STATUS $ac_config_status_args || ac_cs_success=false exec 5>>config.log # Use ||, not &&, to avoid exiting from the if with $? = 1, which # would make configure fail if this is the last instruction. $ac_cs_success || as_fn_exit 1 fi if test -n "$ac_unrecognized_opts" && test "$enable_option_checking" != no; then { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: unrecognized options: $ac_unrecognized_opts" >&5 printf "%s\n" "$as_me: WARNING: unrecognized options: $ac_unrecognized_opts" >&2;} fi # Summary echo echo " Summary" echo "-----------------------------------------" echo "Verbose make : $enable_verbose_make" echo "OCaml compiler : yes" echo " Version : $OCAMLVERSION" echo " Library path : $OCAMLLIB" echo " Ocamlfind : $enable_ocamlfind$reason_ocamlfind" echo " Native compilation : $enable_native_code" echo " Memory profiling : $enable_statmemprof$reason_statmemprof" echo " PPX : $enable_ppx$reason_ppx" echo " S-expressions support : $enable_sexp$reason_sexp" echo " Javascript support : $enable_js_of_ocaml$reason_js_of_ocaml" echo " MPFR support : $enable_mpfr$reason_mpfr" echo " Re support : $enable_re$reason_re" echo "Build environment" echo " OCaml OS Type : $OCAML_OS_TYPE" echo " Build environment type : $BUILD_ENV_TYPE" echo "Components" echo " Why3 library : $enable_why3_lib" echo " GTK IDE : $enable_ide$reason_ide" echo " Web IDE : $enable_web_ide$reason_web_ide" echo " Compressed sessions : $enable_zip$reason_zip" echo " Hypothesis selection : $enable_hypothesis_selection$reason_hypothesis_selection" echo " Stackify : $enable_stackify$reason_stackify" echo " Invariant inference(exp): $enable_infer$reason_infer" echo " Inference with BDDs(exp): $enable_bddinfer$reason_bddinfer" echo " Frama-C support : $enable_frama_c$reason_frama_c" if test "$enable_frama_c" = yes ; then echo " Version : $FRAMAC_VERSION" echo " Share path : $FRAMAC_SHARE" echo " Library path : $FRAMAC_LIBDIR" fi echo "Documentation : $enable_doc$reason_doc" if test "$enable_doc" = yes ; then echo " HTML : yes" echo " PDF : $enable_pdf_doc$reason_pdf_doc" fi echo "Support for interactive proof assistants" echo " Coq : $enable_coq_support$reason_coq_support" if test "$enable_coq_support" = yes ; then echo " Version : $COQVERSION" echo " Library path : $COQLIB" echo " Realization support : $enable_coq_libs$reason_coq_libs" if test "$enable_coq_libs" = yes ; then echo " FP arithmetic : $enable_coq_fp_libs$reason_coq_fp_libs" fi fi echo " PVS : $enable_pvs_support$reason_pvs_support" if test "$enable_pvs_support" = yes ; then echo " Version : $PVSVERSION" echo " Library path : $PVSLIB" echo " Realization support : $enable_pvs_libs$reason_pvs_libs" fi echo " Isabelle : $enable_isabelle_support$reason_isabelle_support" if test "$enable_isabelle_support" = yes ; then echo " Version : $ISABELLEVERSION ($ISABELLEDETECTEDVERSION)" echo " Realization support : $enable_isabelle_libs$reason_isabelle_libs" fi if test "$enable_local" = yes ; then echo "Installable : no" echo " OCaml library path : $OCAMLINSTALLLIB/why3" else echo "Installable : yes" echo " Binary path : $bindir" echo " Library path : $libdir/why3" echo " Data path : $datarootdir/why3" echo " OCaml library path : $OCAMLINSTALLLIB/why3" echo " Relocatable : $enable_relocation" fi