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
---
 plugins/micromega/coq_micromega.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 88b4f90e63..abe4b36801 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