cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
determine swipl_version at runtime;
--- a/Admin/isatest/settings/at-poly Sun Mar 13 17:35:35 2011 +0100
+++ b/Admin/isatest/settings/at-poly Sun Mar 13 19:16:19 2011 +0100
@@ -24,9 +24,9 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
-EXEC_GHC="/home/isabelle/contrib_devel/ghc/x86-linux/ghc"
-EXEC_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml"
-EXEC_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl"
+ISABELLE_GHC="/home/isabelle/contrib_devel/ghc/x86-linux/ghc"
+ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml"
+ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl"
init_component "$HOME/contrib_devel/kodkodi"
--- a/NEWS Sun Mar 13 17:35:35 2011 +0100
+++ b/NEWS Sun Mar 13 19:16:19 2011 +0100
@@ -22,11 +22,16 @@
discontinued. INCOMPATIBILITY.
* Various optional external tools are referenced more robustly and
-uniformly by explicit Isabelle settings as follows, without automated
-detection from the shell environment or path (potential
-INCOMPATIBILITY):
-
- ISABELLE_CSDP (formerly CSDP_EXE)
+uniformly by explicit Isabelle settings as follows:
+
+ ISABELLE_CSDP (formerly CSDP_EXE)
+ ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH)
+ ISABELLE_OCAML (formerly EXEC_OCAML)
+ ISABELLE_SWIPL (formerly EXEC_SWIPL)
+ ISABELLE_YAP (formerly EXEC_YAP)
+
+Note that automated detection from the file-system or search path has
+been discontinued. INCOMPATIBILITY.
*** HOL ***
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Sun Mar 13 17:35:35 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Sun Mar 13 19:16:19 2011 +0100
@@ -2,7 +2,8 @@
Author: Steven Obua
*)
-structure AM_GHC : ABSTRACT_MACHINE = struct
+structure AM_GHC : ABSTRACT_MACHINE =
+struct
open AbstractMachine;
@@ -214,8 +215,6 @@
fun writeTextFile name s = File.write (Path.explode name) s
-val ghc = Unsynchronized.ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
-
fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
fun compile cache_patterns const_arity eqs =
@@ -228,8 +227,11 @@
val module_file = tmp_file (module^".hs")
val object_file = tmp_file (module^".o")
val _ = writeTextFile module_file source
- val _ = bash ((!ghc)^" -c "^module_file)
- val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
+ val _ = bash ("\"$ISABELLE_GHC\" -c " ^ module_file)
+ val _ =
+ if not (fileExists object_file) then
+ raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
+ else ()
in
(guid, module_file, arity)
end
@@ -309,8 +311,9 @@
val term = print_term arity_of 0 t
val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
val _ = writeTextFile call_file call_source
- val _ = bash ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
- val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
+ val _ = bash ("\"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
+ val result = readResultFile result_file handle IO.Io _ =>
+ raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
val t' = parse_result arity_of result
val _ = OS.FileSys.remove call_file
val _ = OS.FileSys.remove result_file
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Sun Mar 13 17:35:35 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Sun Mar 13 19:16:19 2011 +0100
@@ -9,10 +9,12 @@
(* "IMP_3",
"IMP_4"*)];
-if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
+if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then
(warning "No prolog system found - skipping some example theories"; ())
else
- if not (getenv "EXEC_SWIPL" = "") orelse (getenv "SWIPL_VERSION" = "5.10.1") then
+ if not (getenv "ISABELLE_SWIPL" = "") orelse
+ #1 (bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") = "5.10.1"
+ then
(use_thys [
"Code_Prolog_Examples",
"Context_Free_Grammar_Example",
@@ -20,4 +22,4 @@
"Lambda_Example",
"List_Examples"];
Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"])
- else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ());
+ else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ());
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Mar 13 17:35:35 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Mar 13 19:16:19 2011 +0100
@@ -751,7 +751,7 @@
"\\n', [" ^ space_implode ", " vnames ^ "]), writelist(SolutionTail).\n"
val swi_prolog_prelude =
- "#!/usr/bin/swipl -q -t main -f\n\n" ^
+ "#!/usr/bin/swipl -q -t main -f\n\n" ^ (* FIXME hardwired executable!? *)
":- use_module(library('dialect/ciao/aggregates')).\n" ^
":- style_check(-singleton).\n" ^
":- style_check(-discontiguous).\n" ^
@@ -787,14 +787,15 @@
let
val (env_var, cmd) =
(case system of
- SWI_PROLOG => ("EXEC_SWIPL", "\"$EXEC_SWIPL\" -f ")
- | YAP => ("EXEC_YAP", "\"$EXEC_YAP\" -L "))
+ SWI_PROLOG => ("ISABELLE_SWIPL", "\"$ISABELLE_SWIPL\" -f ")
+ | YAP => ("ISABELLE_YAP", "\"$ISABELLE_YAP\" -L "))
in
if getenv env_var = "" then
(warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
else fst (bash_output (cmd ^ File.shell_path file))
end
+
(* parsing prolog solution *)
val scan_number =
--- a/src/HOL/Tools/Predicate_Compile/etc/settings Sun Mar 13 17:35:35 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/etc/settings Sun Mar 13 19:16:19 2011 +0100
@@ -1,20 +1,4 @@
# -*- shell-script -*- :mode=shellscript:
-# FIXME contrib_devel not official
-# FIXME $(type -p swipl) etc. does not allow spaces in file name
+ISABELLE_PREDICATE_COMPILE="$COMPONENT"
-EXEC_SWIPL="$(choosefrom \
- "$ISABELLE_HOME/contrib/swipl/$ISABELLE_PLATFORM/bin/swipl" \
- "$ISABELLE_HOME/contrib_devel/swipl/$ISABELLE_PLATFORM/bin/swipl" \
- "$ISABELLE_HOME/../swipl" \
- $(type -p swipl) \
- "")"
-
-EXEC_YAP="$(choosefrom \
- "$ISABELLE_HOME/contrib/yap/$ISABELLE_PLATFORM/bin/yap" \
- "$ISABELLE_HOME/contrib_devel/yap/$ISABELLE_PLATFORM/bin/yap" \
- "$ISABELLE_HOME/../yap" \
- $(type -p yap) \
- "")"
-
-SWIPL_VERSION="$("$COMPONENT/lib/scripts/swipl_version")"
--- a/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Sun Mar 13 17:35:35 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Sun Mar 13 19:16:19 2011 +0100
@@ -4,14 +4,12 @@
#
# Determine SWI-Prolog version
-if [ "$EXEC_SWIPL" = "" ]; then
- echo ""
-else
- VERSION="$("$EXEC_SWIPL" --version)"
+if [ "$ISABELLE_SWIPL" != "" ]; then
+ VERSION="$("$ISABELLE_SWIPL" --version)"
REGEXP='^SWI-Prolog version ([0-9\.]*) for .*$'
if [[ "$VERSION" =~ $REGEXP ]]; then
- echo "${BASH_REMATCH[1]}"
+ echo -n "${BASH_REMATCH[1]}"
else
- echo undefined
+ echo -n undefined
fi
fi
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Mar 13 17:35:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Mar 13 19:16:19 2011 +0100
@@ -43,7 +43,7 @@
val _ = File.write narrowing_engine_file narrowing_engine
val _ = File.write main_file main
val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
- val cmd = "\"$EXEC_GHC\" -fglasgow-exts " ^
+ val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
(space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
" -o " ^ executable ^ " && " ^ executable
in
--- a/src/HOL/ex/ROOT.ML Sun Mar 13 17:35:35 2011 +0100
+++ b/src/HOL/ex/ROOT.ML Sun Mar 13 19:16:19 2011 +0100
@@ -76,7 +76,7 @@
"Set_Algebras"
];
-if getenv "EXEC_GHC" = "" then ()
+if getenv "ISABELLE_GHC" = "" then ()
else use_thy "Quickcheck_Narrowing_Examples";
use_thy "SVC_Oracle";
--- a/src/Tools/Code/code_haskell.ML Sun Mar 13 17:35:35 2011 +0100
+++ b/src/Tools/Code/code_haskell.ML Sun Mar 13 19:16:19 2011 +0100
@@ -452,9 +452,9 @@
val setup =
Code_Target.add_target
(target, { serializer = serializer, literals = literals,
- check = { env_var = "EXEC_GHC", make_destination = I,
+ check = { env_var = "ISABELLE_GHC", make_destination = I,
make_command = fn module_name =>
- "\"$EXEC_GHC\" -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^
+ "\"$ISABELLE_GHC\" -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^
module_name ^ ".hs" } })
#> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_ml.ML Sun Mar 13 17:35:35 2011 +0100
+++ b/src/Tools/Code/code_ml.ML Sun Mar 13 19:16:19 2011 +0100
@@ -841,9 +841,9 @@
make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
#> Code_Target.add_target
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
- check = { env_var = "EXEC_OCAML",
+ check = { env_var = "ISABELLE_OCAML",
make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
- make_command = fn _ => "\"$EXEC_OCAML\" -w pu nums.cma ROOT.ocaml" } })
+ make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
#> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/etc/settings Sun Mar 13 17:35:35 2011 +0100
+++ b/src/Tools/Code/etc/settings Sun Mar 13 19:16:19 2011 +0100
@@ -2,14 +2,3 @@
ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-EXEC_GHC="$(choosefrom \
- "$ISABELLE_HOME/contrib/ghc/$ISABELLE_PLATFORM/ghc" \
- "$ISABELLE_HOME/../ghc/$ISABELLE_PLATFORM/ghc" \
- "$(type -p ghc)" \
- "")"
-
-EXEC_OCAML="$(choosefrom \
- "$ISABELLE_HOME/contrib/ocaml/$ISABELLE_PLATFORM/ocaml" \
- "$ISABELLE_HOME/../ocaml/$ISABELLE_PLATFORM/ocaml" \
- "$(type -p ocaml)" \
- "")"