decentralized historic settings;
authorwenzelm
Sun May 12 14:25:16 2013 +0200 (2013-05-12 ago)
changeset 51940958d439b3013
parent 51939 65548ab2fc55
child 51941 ead4248aef3b
decentralized historic settings;
etc/settings
src/HOL/Matrix_LP/Cplex_tools.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/svc_funcs.ML
     1.1 --- a/etc/settings	Sun May 12 13:56:21 2013 +0200
     1.2 +++ b/etc/settings	Sun May 12 14:25:16 2013 +0200
     1.3 @@ -142,36 +142,6 @@
     1.4  #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
     1.5  #SMLNJ_CYGWIN_RUNTIME=1
     1.6  
     1.7 -## Set HOME only for tools you have installed!
     1.8 -
     1.9 -# SVC (Stanford Validity Checker)
    1.10 -#SVC_HOME=
    1.11 -#SVC_MACHINE=i386-redhat-linux
    1.12 -#SVC_MACHINE=sparc-sun-solaris
    1.13 -
    1.14 -# MiniSat 1.14 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
    1.15 -#MINISAT_HOME=/usr/local/bin
    1.16 -
    1.17 -# zChaff (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
    1.18 -#ZCHAFF_HOME=/usr/local/bin
    1.19 -
    1.20 -# BerkMin561 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
    1.21 -#BERKMIN_HOME=/usr/local/bin
    1.22 -#BERKMIN_EXE=BerkMin561-linux
    1.23 -#BERKMIN_EXE=BerkMin561-solaris
    1.24 -
    1.25 -# Jerusat 1.3 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
    1.26 -#JERUSAT_HOME=/usr/local/bin
    1.27 -
    1.28 -# For configuring HOL/Matrix/cplex
    1.29 -# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
    1.30 -# First option: use the commercial cplex solver
    1.31 -#LP_SOLVER=CPLEX
    1.32 -#CPLEX_PATH=cplex
    1.33 -# Second option: use the open source glpk solver
    1.34 -#LP_SOLVER=GLPK
    1.35 -#GLPK_PATH=glpsol
    1.36 -
    1.37  # Misc programming languages
    1.38  #ISABELLE_GHC="/usr/bin/ghc"
    1.39  #ISABELLE_OCAML="/usr/bin/ocaml"
     2.1 --- a/src/HOL/Matrix_LP/Cplex_tools.ML	Sun May 12 13:56:21 2013 +0200
     2.2 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Sun May 12 14:25:16 2013 +0200
     2.3 @@ -1,5 +1,15 @@
     2.4  (*  Title:      HOL/Matrix_LP/Cplex_tools.ML
     2.5      Author:     Steven Obua
     2.6 +
     2.7 +Relevant Isabelle environment settings:
     2.8 +
     2.9 +  # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
    2.10 +  # First option: use the commercial cplex solver
    2.11 +  #LP_SOLVER=CPLEX
    2.12 +  #CPLEX_PATH=cplex
    2.13 +  # Second option: use the open source glpk solver
    2.14 +  #LP_SOLVER=GLPK
    2.15 +  #GLPK_PATH=glpsol
    2.16  *)
    2.17  
    2.18  signature CPLEX =
     3.1 --- a/src/HOL/Tools/sat_solver.ML	Sun May 12 13:56:21 2013 +0200
     3.2 +++ b/src/HOL/Tools/sat_solver.ML	Sun May 12 14:25:16 2013 +0200
     3.3 @@ -3,6 +3,22 @@
     3.4      Copyright   2004-2009
     3.5  
     3.6  Interface to external SAT solvers, and (simple) built-in SAT solvers.
     3.7 +
     3.8 +Relevant Isabelle environment settings:
     3.9 +
    3.10 +  # MiniSat 1.14
    3.11 +  #MINISAT_HOME=/usr/local/bin
    3.12 +
    3.13 +  # zChaff
    3.14 +  #ZCHAFF_HOME=/usr/local/bin
    3.15 +
    3.16 +  # BerkMin561
    3.17 +  #BERKMIN_HOME=/usr/local/bin
    3.18 +  #BERKMIN_EXE=BerkMin561-linux
    3.19 +  #BERKMIN_EXE=BerkMin561-solaris
    3.20 +
    3.21 +  # Jerusat 1.3
    3.22 +  #JERUSAT_HOME=/usr/local/bin
    3.23  *)
    3.24  
    3.25  signature SAT_SOLVER =
     4.1 --- a/src/HOL/ex/svc_funcs.ML	Sun May 12 13:56:21 2013 +0200
     4.2 +++ b/src/HOL/ex/svc_funcs.ML	Sun May 12 14:25:16 2013 +0200
     4.3 @@ -14,6 +14,12 @@
     4.4    in either operand.
     4.5  
     4.6  For each variable of type nat, an assumption is added that it is non-negative.
     4.7 +
     4.8 +Relevant Isabelle environment settings:
     4.9 +
    4.10 +  #SVC_HOME=
    4.11 +  #SVC_MACHINE=i386-redhat-linux
    4.12 +  #SVC_MACHINE=sparc-sun-solaris
    4.13  *)
    4.14  
    4.15  structure Svc =