# HG changeset patch
# User obua
# Date 1122889173 -7200
# Node ID 37e34f315057cada50b2f66ece7b87976cacf35e
# Parent  46697fa536ab0e44c03b32fdf9920de1734678a5
1. changed configuration variables for linear programming (Cplex_tools):
   LP_SOLVER is either CPLEX or GLPK
   CPLEX_PATH is the path to the cplex binary
   GLPK_PATH is the path to the glpk binary
   The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML

diff -r 46697fa536ab -r 37e34f315057 etc/settings
--- a/etc/settings	Mon Aug 01 11:24:19 2005 +0200
+++ b/etc/settings	Mon Aug 01 11:39:33 2005 +0200
@@ -219,9 +219,13 @@
 HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
 
 # For configuring HOL/Matrix/cplex
+# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
 # First option: use the commercial cplex solver
-#LP_SOLVER_NAME=CPLEX
-#LP_SOLVER_PATH=cplex
+# LP_SOLVER=CPLEX
+# CPLEX_PATH=cplex
 # Second option: use the open source glpk solver
-#LP_SOLVER_NAME=GLPK
-#LP_SOLVER_PATH=glpsol
+# LP_SOLVER=GLPK
+# GLPK_PATH=glpsol
+
+# toogles the detail of the error message in case of a cyclic definition
+DEFS_CHAIN_HISTORY=ON
diff -r 46697fa536ab -r 37e34f315057 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Library/Library.thy	Mon Aug 01 11:39:33 2005 +0200
@@ -17,9 +17,7 @@
   While_Combinator
   Word
   Zorn
-  (*List_Prefix*)
   Char_ord
-  List_lexord
 begin
 end
 (*>*)
diff -r 46697fa536ab -r 37e34f315057 src/HOL/Library/Library/ROOT.ML
--- a/src/HOL/Library/Library/ROOT.ML	Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Library/Library/ROOT.ML	Mon Aug 01 11:39:33 2005 +0200
@@ -1,1 +1,3 @@
 use_thy "Library";
+use_thy "List_Prefix";
+use_thy "List_lexord";
diff -r 46697fa536ab -r 37e34f315057 src/HOL/Matrix/cplex/Cplex_tools.ML
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Mon Aug 01 11:39:33 2005 +0200
@@ -35,6 +35,8 @@
 			 | Optimal of string * 
 				      (((* name *) string * 
 					(* value *) string) list)
+
+    datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
 						     
     exception Load_cplexFile of string
     exception Load_cplexResult of string
@@ -51,12 +53,20 @@
 
     val is_normed_cplexProg : cplexProg -> bool
 
+    val get_solver : unit -> cplexSolver
+    val set_solver : cplexSolver -> unit
     val solve : cplexProg -> cplexResult
 end;
 
 structure Cplex  : CPLEX =
 struct
 
+datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
+
+val cplexsolver = ref SOLVER_DEFAULT;
+fun get_solver () = !cplexsolver;
+fun set_solver s = (cplexsolver := s);
+
 exception Load_cplexFile of string;
 exception Load_cplexResult of string;
 exception Save_cplexFile of string;
@@ -1139,7 +1149,7 @@
 	val lpname = tmp_file (name^".lp")
 	val resultname = tmp_file (name^".txt")
 	val _ = save_cplexFile lpname prog		
-	val cplex_path = getenv "LP_SOLVER_PATH"
+	val cplex_path = getenv "GLPK_PATH"
 	val cplex = if cplex_path = "" then "glpsol" else cplex_path
 	val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
 	val answer = execute command
@@ -1171,7 +1181,7 @@
 	val resultname = tmp_file (name^".txt")
 	val scriptname = tmp_file (name^".script")
 	val _ = save_cplexFile lpname prog		
-	val cplex_path = getenv "LP_SOLVER_PATH"
+	val cplex_path = getenv "CPLEX_PATH"
 	val cplex = if cplex_path = "" then "cplex" else cplex_path
 	val _ = write_script scriptname lpname resultname
 	val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
@@ -1188,10 +1198,14 @@
     end
 
 fun solve prog = 
-    case getenv "LP_SOLVER_NAME" of
-	"CPLEX" => solve_cplex prog
-      | "GLPK" => solve_glpk prog
-      | _ => raise (Execute ("LP_SOLVER_NAME must be set to CPLEX or to GLPK"));
+    case get_solver () of
+      SOLVER_DEFAULT => 
+        (case getenv "LP_SOLVER" of
+	   "CPLEX" => solve_cplex prog
+         | "GLPK" => solve_glpk prog
+         | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
+    | SOLVER_CPLEX => solve_cplex prog
+    | SOLVER_GLPK => solve_glpk prog
 		   
 end;