# HG changeset patch # User wenzelm # Date 1300040179 -3600 # Node ID c7297638599b154205771bd53043ae9e5647f5b4 # Parent 117eb7aeddf0a78a78180ea629d85dda2a120f84 cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection; determine swipl_version at runtime; diff -r 117eb7aeddf0 -r c7297638599b Admin/isatest/settings/at-poly --- 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" diff -r 117eb7aeddf0 -r c7297638599b NEWS --- 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 *** diff -r 117eb7aeddf0 -r c7297638599b src/HOL/Matrix/Compute_Oracle/am_ghc.ML --- 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 diff -r 117eb7aeddf0 -r c7297638599b src/HOL/Predicate_Compile_Examples/ROOT.ML --- 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"; ()); diff -r 117eb7aeddf0 -r c7297638599b src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 = diff -r 117eb7aeddf0 -r c7297638599b src/HOL/Tools/Predicate_Compile/etc/settings --- 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")" diff -r 117eb7aeddf0 -r c7297638599b src/HOL/Tools/Predicate_Compile/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 diff -r 117eb7aeddf0 -r c7297638599b src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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 diff -r 117eb7aeddf0 -r c7297638599b src/HOL/ex/ROOT.ML --- 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"; diff -r 117eb7aeddf0 -r c7297638599b src/Tools/Code/code_haskell.ML --- 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 ( diff -r 117eb7aeddf0 -r c7297638599b src/Tools/Code/code_ml.ML --- 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, diff -r 117eb7aeddf0 -r c7297638599b src/Tools/Code/etc/settings --- 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)" \ - "")"