diff options
| -rw-r--r-- | config/coq_config.mli | 2 | ||||
| -rwxr-xr-x | configure | 62 | ||||
| -rw-r--r-- | lib/system.ml | 20 | ||||
| -rw-r--r-- | lib/system.mli | 2 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 9 |
5 files changed, 29 insertions, 66 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index 5feb96303..2cd1e4543 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -55,8 +55,6 @@ val plugins_dirs : string list val exec_extension : string (* "" under Unix, ".exe" under MS-windows *) val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *) -val csdp : string option (* the path to CSDP, for the Micromega plugin *) - val browser : string (** default web browser to use, may be overriden by environment variable COQREMOTEBROWSER *) @@ -1,4 +1,4 @@ -#!/bin/bash +#!/bin/sh ################################## # @@ -69,8 +69,6 @@ usage () { printf "\tSpecifies whether or not to compile Coqide\n" echo "-uim-script-path" printf "\tSpecifies where uim's .scm files are installed\n" - echo "-csdpdir <dir>" - printf "\tSpecifies the path of the CSDP solver intallation\n" echo "-browser <command>" printf "\tUse <command> to open URL %%s\n" echo "-with-doc (yes|no)" @@ -119,8 +117,6 @@ gcc_exec=gcc ar_exec=ar ranlib_exec=ranlib -csdpexec= - local=false coqrunbyteflags_spec=no coqtoolsbyteflags_spec=no @@ -217,9 +213,6 @@ while : ; do *) COQIDE=no esac shift;; - -csdpdir|--csdpdir) - csdpdir="$2" - shift;; -browser|--browser) browser_spec=yes BROWSER=$2 shift;; @@ -660,51 +653,6 @@ if which uim-fep; then done fi -# Borcher's C library for semidefinite programming (CSDP) is required for the -# micromega plugin to be fully functional. -# -# We test for its presence; when not found we -# - fail if the path was explicitely provided via the "-csdpdir" option, -# - issue a warning else. - -if [ "$csdpdir" != "" ]; then - if [ ! -f "$csdpdir/csdp" ]; then - echo "Cannot find the csdp binary in $csdpdir ($csdpdir/csdp not found)." - echo "Configuration script failed!" - exit 1 - else - if [ ! -x "$csdpdir/csdp" ]; then - echo "The csdp binary in $csdpdir is not executable: check your permissions." - echo "Configuration script failed!" - exit 1 - fi - fi - USE_CSDP="yes" - CSDP=$csdpdir/csdp -else - CSDP=`which csdp` - if [ ! -f "$CSDP" ]; then - echo "*Warning* Cannot find the csdp executable. Have you installed it?" - echo " CSDP can be found pre-packaged as part of your software distribution," - echo " or at https://projects.coin-or.org/csdp." - USE_CSDP="no" - else - if [ ! -x "$CSDP" ]; then - echo "*Warning* The csdp binary at $CSDP is not executable: check your permissions." - USE_CSDP="noexec" - else - USE_CSDP="yes" - fi - fi -fi - -# Finally, set the ML configuration variable to reflect the state of the CSDP -# installation. -case $USE_CSDP in - yes) csdpexec="Some \"$CSDP\"";; - no|noexec) csdpexec="None";; -esac - # strip command case $ARCH in @@ -919,13 +867,6 @@ else echo " Documentation : None" fi echo " CoqIde : $COQIDE" -if test "$USE_CSDP" = "yes"; then -echo " CSDP for Micromega : $CSDP" -else if test "$USE_CSDP" = "no"; then -echo " CSDP for Micromega : None" -else if test "$USE_CSDP" = "noexec"; then -echo " CSDP for Micromega : $CSDP found, but is not executable" -fi fi fi echo " Web browser : $BROWSER" echo " Coq web site : $WWWCOQ" echo "" @@ -1069,7 +1010,6 @@ let vo_magic_number = $VOMAGIC let state_magic_number = $STATEMAGIC let exec_extension = "$EXE" let with_geoproof = ref $with_geoproof -let csdp = $csdpexec let browser = "$BROWSER" let wwwcoq = "$WWWCOQ" let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/" diff --git a/lib/system.ml b/lib/system.ml index 4afae3918..4b657e485 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -284,6 +284,26 @@ let run_command converter f c = done; (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) +let path_separator = if Sys.os_type = "Unix" then ':' else ';' + +let search_exe_in_path exe = + try + let path = Sys.getenv "PATH" in + let n = String.length path in + let rec aux i = + if i < n then + let j = + try String.index_from path i path_separator + with Not_found -> n + in + let dir = String.sub path i (j-i) in + let exe = Filename.concat dir exe in + if Sys.file_exists exe then Some exe else aux (i+1) + else + None + in aux 0 + with Not_found -> None + (* Time stamps. *) type time = float * float * float diff --git a/lib/system.mli b/lib/system.mli index 2932d7b66..cc55f4d66 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -66,6 +66,8 @@ val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a val run_command : (string -> string) -> (string -> unit) -> string -> Unix.process_status * string +val search_exe_in_path : string -> string option + (*s Time stamps. *) type time diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 88b4f90e6..abe4b3680 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1465,12 +1465,15 @@ let csdp_cache = "csdp.cache" * Throw CsdpNotFound if a Coq isn't aware of any csdp executable. *) +let require_csdp = + match System.search_exe_in_path "csdp" with + | Some _ -> lazy () + | _ -> lazy (raise CsdpNotFound) + let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivstellensatz option = fun provername poly -> - match Coq_config.csdp with - | None -> raise CsdpNotFound (* caugth in micromega_gen *) - | Some _ -> () ; + Lazy.force require_csdp; let cmdname = List.fold_left Filename.concat (Envars.coqlib ()) |