From 328cd1cb92e463b2a9cdd669e7e31090dc905c64 Mon Sep 17 00:00:00 2001 From: glondu Date: Sun, 11 Apr 2010 16:58:12 +0000 Subject: Look for csdp in $PATH at runtime, remove -csdpdir configure option The csdp path computed by the configure script wasn't used at all, but was forcing presence of csdp at configure time whereas it is not used at all in the build process. Instead, we replace the configure-time check with a runtime check for existence of csdp in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7 --- config/coq_config.mli | 2 -- configure | 62 +------------------------------------- lib/system.ml | 20 ++++++++++++ lib/system.mli | 2 ++ 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 *) diff --git a/configure b/configure index 6c62a3c2b..fc77ee10c 100755 --- a/configure +++ b/configure @@ -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 " - printf "\tSpecifies the path of the CSDP solver intallation\n" echo "-browser " printf "\tUse 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 ()) -- cgit v1.2.3