diff --git a/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,171 +1,172 @@ # -*- shell-script -*- :mode=shellscript: # # Isabelle system settings. # # Important notes: # * See the "system" manual for explanations on Isabelle settings # * User settings go into $ISABELLE_HOME_USER/etc/settings # * DO NOT EDIT the repository copy of this file! # * DO NOT COPY this file into the $ISABELLE_HOME_USER directory! ### ### Isabelle/Scala ### ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0" ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 11 -target 11" ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -deprecation -release 11 -source 3.1 -old-syntax -no-indent -color never -pagewidth 78 -J-Xms512m -J-Xmx4g -J-Xss16m" ISABELLE_SCALA_JAR="$ISABELLE_HOME/lib/classes/isabelle.jar" #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS ### ### Interactive sessions (cf. isabelle console) ### ISABELLE_LINE_EDITOR="rlwrap" ### ### Batch sessions (cf. isabelle build) ### ISABELLE_BUILD_OPTIONS="" ### ### Document preparation (cf. isabelle latex) ### if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -c-style-errors" else ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -file-line-error" fi ISABELLE_LUALATEX="lualatex --interaction=nonstopmode --file-line-error" ISABELLE_BIBTEX="bibtex" ISABELLE_MAKEINDEX="makeindex -c -q" ISABELLE_EPSTOPDF="epstopdf" ### ### Misc path settings ### isabelle_directory '~' isabelle_directory '$ISABELLE_HOME_USER' isabelle_directory '~~' ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components" ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib" # The place for user configuration, heap files, etc. if [ -z "$ISABELLE_IDENTIFIER" ]; then ISABELLE_HOME_USER="$USER_HOME/.isabelle" else ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER" fi # Where to look for isabelle tools (multiple dirs separated by ':'). ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" # Location for temporary files (should be on a local file system). ISABELLE_TMP_PREFIX="/tmp/isabelle-${USER:-$LOGNAME}" # Heap locations. ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps" ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps" # HTML browser info. ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info" # Site settings check -- just to make it a little bit harder to copy this file verbatim! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } ISABELLE_SITE_SETTINGS_PRESENT=true ### ### Default logic ### ISABELLE_LOGIC=HOL ### ### Docs and external files ### # Where to look for docs (multiple dirs separated by ':'). ISABELLE_DOCS="$ISABELLE_HOME/doc" ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY" ISABELLE_DOCS_EXAMPLES="~~/src/HOL/Examples/Seq.thy:~~/src/HOL/Examples/Drinker.thy:~~/src/HOL/Examples/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML" # "open" within desktop environment (potentially asynchronous) case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_OPEN="xdg-open" ;; macos) ISABELLE_OPEN="open" ;; windows) ISABELLE_OPEN="cygstart" ;; esac PDF_VIEWER="$ISABELLE_OPEN" ISABELLE_EXTERNAL_FILES="bmp:eps:gif:jpeg:jpg:pdf:png:xmp" ### ### Symbol rendering ### ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols" ### ### OCaml ### ISABELLE_OPAM_ROOT="$USER_HOME/.opam" ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.12.0" ### ### Haskell ### ISABELLE_STACK_ROOT="$USER_HOME/.stack" ISABELLE_STACK_RESOLVER="lts-18.12" ISABELLE_GHC_VERSION="ghc-8.10.7" ### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_MLTON="/usr/bin/mlton" +#ISABELLE_MLTON_OPTIONS="-pi-style npi" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/src/HOL/Library/code_test.ML b/src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML +++ b/src/HOL/Library/code_test.ML @@ -1,539 +1,541 @@ (* Title: HOL/Library/code_test.ML Author: Andreas Lochbihler, ETH Zürich Test infrastructure for the code generator. *) signature CODE_TEST = sig val add_driver: string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory val debug: bool Config.T val test_terms: Proof.context -> term list -> string -> unit val test_code_cmd: string list -> string list -> Proof.context -> unit val eval_term: string -> Proof.context -> term -> term val check_settings: string -> string -> string -> unit val compile: string -> string -> unit val evaluate: string -> string -> string val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string val ghc_options: string Config.T val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string val target_Scala: string val target_Haskell: string end structure Code_Test: CODE_TEST = struct (* convert a list of terms into nested tuples and back *) fun mk_tuples [] = \<^Const>\Unity\ | mk_tuples [t] = t | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts) fun dest_tuples \<^Const_>\Pair _ _ for l r\ = l :: dest_tuples r | dest_tuples t = [t] fun last_field sep str = let val n = size sep val len = size str fun find i = if i < 0 then NONE else if String.substring (str, i, n) = sep then SOME i else find (i - 1) in (case find (len - n) of NONE => NONE | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) end fun split_first_last start stop s = (case first_field start s of NONE => NONE | SOME (initial, rest) => (case last_field stop rest of NONE => NONE | SOME (middle, tail) => SOME (initial, middle, tail))) (* data slot for drivers *) structure Drivers = Theory_Data ( type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list val empty = [] fun merge data : T = AList.merge (op =) (K true) data ) val add_driver = Drivers.map o AList.update (op =) val get_driver = AList.lookup (op =) o Drivers.get (* Test drivers must produce output of the following format: The start of the relevant data is marked with start_marker, its end with end_marker. Between these two markers, every line corresponds to one test. Lines of successful tests start with success, failures start with failure. The failure failure may continue with the YXML encoding of the evaluated term. There must not be any additional whitespace in between. *) (* parsing of results *) val success = "True" val failure = "False" val start_marker = "*@*Isabelle/Code_Test-start*@*" val end_marker = "*@*Isabelle/Code_Test-end*@*" fun parse_line line = if String.isPrefix success line then (true, NONE) else if String.isPrefix failure line then (false, if size line > size failure then String.extract (line, size failure, NONE) |> YXML.parse_body |> Term_XML.Decode.term_raw |> dest_tuples |> SOME else NONE) else raise Fail ("Cannot parse result of evaluation:\n" ^ line) fun parse_result target out = (case split_first_last start_marker end_marker out of NONE => error ("Evaluation failed for " ^ target ^ "!\nCompiler output:\n" ^ out) | SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line) (* pretty printing of test results *) fun pretty_eval _ NONE _ = [] | pretty_eval ctxt (SOME evals) ts = [Pretty.fbrk, Pretty.big_list "Evaluated terms" (map (fn (t, eval) => Pretty.block [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1, Syntax.pretty_term ctxt eval]) (ts ~~ evals))] fun pretty_failure ctxt target (((_, evals), query), eval_ts) = Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @ pretty_eval ctxt evals eval_ts) fun pretty_failures ctxt target failures = Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures)) (* driver invocation *) val debug = Attrib.setup_config_bool \<^binding>\test_code_debug\ (K false) fun with_debug_dir name f = (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ())) |> Isabelle_System.make_directory |> Exn.capture f |> Exn.release; fun dynamic_value_strict ctxt t compiler = let val thy = Proof_Context.theory_of ctxt val (driver, target) = (case get_driver thy compiler of NONE => error ("No driver for target " ^ compiler) | SOME drv => drv) val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir fun eval result = with_dir "Code_Test" (driver ctxt ((apfst o map) (apfst Long_Name.implode #> apsnd Bytes.content) result)) |> parse_result compiler fun evaluator program _ vs_ty deps = Exn.interruptible_capture eval (Code_Target.compilation_text ctxt target program deps true vs_ty) fun postproc f = map (apsnd (Option.map (map f))) in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end (* term preprocessing *) fun add_eval \<^Const_>\Trueprop for t\ = add_eval t | add_eval \<^Const_>\HOL.eq _ for lhs rhs\ = (fn acc => acc |> add_eval rhs |> add_eval lhs |> cons rhs |> cons lhs) | add_eval \<^Const_>\Not for t\ = add_eval t | add_eval \<^Const_>\less_eq _ for lhs rhs\ = (fn acc => lhs :: rhs :: acc) | add_eval \<^Const_>\less _ for lhs rhs\ = (fn acc => lhs :: rhs :: acc) | add_eval _ = I fun mk_term_of [] = \<^Const>\None \<^typ>\unit \ yxml_of_term\\ | mk_term_of ts = let val tuple = mk_tuples ts val T = fastype_of tuple in \<^Const>\Some \<^typ>\unit \ yxml_of_term\ for \absdummy \<^Type>\unit\ \<^Const>\yxml_string_of_term for \<^Const>\Code_Evaluation.term_of T for tuple\\\\ end fun test_terms ctxt ts target = let val thy = Proof_Context.theory_of ctxt fun term_of t = Sign.of_sort thy (fastype_of t, \<^sort>\term_of\) fun ensure_bool t = (case fastype_of t of \<^Type>\bool\ => () | _ => error (Pretty.string_of (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1, Syntax.pretty_term ctxt t]))) val _ = List.app ensure_bool ts val evals = map (fn t => filter term_of (add_eval t [])) ts val eval = map mk_term_of evals val t = HOLogic.mk_list \<^typ>\bool \ (unit \ yxml_of_term) option\ (map HOLogic.mk_prod (ts ~~ eval)) val result = dynamic_value_strict ctxt t target val failed = filter_out (fst o fst o fst) (result ~~ ts ~~ evals) handle ListPair.UnequalLengths => error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result)) in (case failed of [] => () | _ => error (Pretty.string_of (pretty_failures ctxt target failed))) end fun test_code_cmd raw_ts targets ctxt = let val ts = Syntax.read_terms ctxt raw_ts val frees = fold Term.add_frees ts [] val _ = if null frees then () else error (Pretty.string_of (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees)))) in List.app (test_terms ctxt ts) targets end fun eval_term target ctxt t = let val frees = Term.add_frees t [] val _ = if null frees then () else error (Pretty.string_of (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees)))) val T = fastype_of t val _ = if Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\term_of\) then () else error ("Type " ^ Syntax.string_of_typ ctxt T ^ " of term not of sort " ^ Syntax.string_of_sort ctxt \<^sort>\term_of\) val t' = HOLogic.mk_list \<^typ>\bool \ (unit \ yxml_of_term) option\ [HOLogic.mk_prod (\<^Const>\False\, mk_term_of [t])] val result = dynamic_value_strict ctxt t' target in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end (* check and invoke compiler *) fun check_settings compiler var descr = if getenv var = "" then error (Pretty.string_of (Pretty.para ("Environment variable " ^ var ^ " is not set. To test code generation with " ^ compiler ^ ", set this variable to your " ^ descr ^ " in the $ISABELLE_HOME_USER/etc/settings file."))) else () fun compile compiler cmd = let val (out, ret) = Isabelle_System.bash_output cmd in if ret = 0 then () else error ("Compilation with " ^ compiler ^ " failed:\n" ^ cmd ^ "\n" ^ out) end fun evaluate compiler cmd = let val (out, res) = Isabelle_System.bash_output cmd in if res = 0 then out else error ("Evaluation for " ^ compiler ^ " terminated with error code " ^ string_of_int res ^ "\nCompiler output:\n" ^ out) end (* driver for PolyML *) val polymlN = "PolyML" fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir = let val code_path = dir + Path.basic "generated.sml" val driver_path = dir + Path.basic "driver.sml" val out_path = dir + Path.basic "out" val code = #2 (the_single code_files) val driver = \<^verbatim>\ fun main () = let fun format (true, _) = \ ^ ML_Syntax.print_string success ^ \<^verbatim>\ ^ "\n" | format (false, NONE) = \ ^ ML_Syntax.print_string failure ^ \<^verbatim>\ ^ "\n" | format (false, SOME t) = \ ^ ML_Syntax.print_string failure ^ \<^verbatim>\ ^ t () ^ "\n" val result = \ ^ value_name ^ \<^verbatim>\ () val result_text = \ ^ ML_Syntax.print_string start_marker ^ \<^verbatim>\ ^ String.concat (map format result) ^ \ ^ ML_Syntax.print_string end_marker ^ \<^verbatim>\ val out = BinIO.openOut \ ^ ML_Syntax.print_platform_path out_path ^ \<^verbatim>\ val _ = BinIO.output (out, Byte.stringToBytes result_text) val _ = BinIO.closeOut out in () end; \ val _ = File.write code_path code val _ = File.write driver_path driver val _ = ML_Context.eval {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE, writeln = writeln, warning = warning} Position.none (ML_Lex.read_text (code, Path.position code_path) @ ML_Lex.read_text (driver, Path.position driver_path) @ ML_Lex.read "main ()") handle ERROR msg => error ("Evaluation for " ^ polymlN ^ " failed:\n" ^ msg) in File.read out_path end (* driver for mlton *) val mltonN = "MLton" val ISABELLE_MLTON = "ISABELLE_MLTON" fun evaluate_in_mlton (_: Proof.context) (code_files, value_name) dir = let val compiler = mltonN val generatedN = "generated.sml" val driverN = "driver.sml" val projectN = "test" val code_path = dir + Path.basic generatedN val driver_path = dir + Path.basic driverN val basis_path = dir + Path.basic (projectN ^ ".mlb") val driver = \<^verbatim>\ fun format (true, _) = \ ^ ML_Syntax.print_string success ^ \<^verbatim>\ ^ "\n" | format (false, NONE) = \ ^ ML_Syntax.print_string failure ^ \<^verbatim>\ ^ "\n" | format (false, SOME t) = \ ^ ML_Syntax.print_string failure ^ \<^verbatim>\ ^ t () ^ "\n" val result = \ ^ value_name ^ \<^verbatim>\ () val _ = print \ ^ ML_Syntax.print_string start_marker ^ \<^verbatim>\ val _ = List.app (print o format) result val _ = print \ ^ ML_Syntax.print_string end_marker ^ \<^verbatim>\ \ val _ = check_settings compiler ISABELLE_MLTON "MLton executable" val _ = List.app (File.write code_path o snd) code_files val _ = File.write driver_path driver val _ = File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN) in - compile compiler ("\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path); - evaluate compiler (File.bash_path (dir + Path.basic projectN)) + compile compiler + (\<^verbatim>\"$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf \ ^ + File.bash_platform_path basis_path); + evaluate compiler (File.bash_platform_path (dir + Path.basic projectN)) end (* driver for SML/NJ *) val smlnjN = "SMLNJ" val ISABELLE_SMLNJ = "ISABELLE_SMLNJ" fun evaluate_in_smlnj (_: Proof.context) (code_files, value_name) dir = let val compiler = smlnjN val generatedN = "generated.sml" val driverN = "driver.sml" val code_path = dir + Path.basic generatedN val driver_path = dir + Path.basic driverN val driver = \<^verbatim>\ structure Test = struct fun main () = let fun format (true, _) = \ ^ ML_Syntax.print_string success ^ \<^verbatim>\ ^ "\n" | format (false, NONE) = \ ^ ML_Syntax.print_string failure ^ \<^verbatim>\ ^ "\n" | format (false, SOME t) = \ ^ ML_Syntax.print_string failure ^ \<^verbatim>\ ^ t () ^ "\n" val result = \ ^ value_name ^ \<^verbatim>\ () val _ = print \ ^ ML_Syntax.print_string start_marker ^ \<^verbatim>\ val _ = List.app (print o format) result val _ = print \ ^ ML_Syntax.print_string end_marker ^ \<^verbatim>\ in 0 end end \ val _ = check_settings compiler ISABELLE_SMLNJ "SMLNJ executable" val _ = List.app (File.write code_path o snd) code_files val _ = File.write driver_path driver val ml_source = "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^ "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^ "; use " ^ ML_Syntax.print_string (File.platform_path driver_path) ^ "; Test.main ();" in evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"") end (* driver for OCaml *) val ocamlN = "OCaml" val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND" fun evaluate_in_ocaml (_: Proof.context) (code_files, value_name) dir = let val compiler = ocamlN val code_path = dir + Path.basic "generated.ml" val driver_path = dir + Path.basic "driver.ml" val driver = "let format_term = function\n" ^ " | None -> \"\"\n" ^ " | Some t -> t ();;\n" ^ "let format = function\n" ^ " | (true, _) -> \"" ^ success ^ "\\n\"\n" ^ " | (false, x) -> \"" ^ failure ^ "\" ^ format_term x ^ \"\\n\";;\n" ^ "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^ "let main x =\n" ^ " let _ = print_string \"" ^ start_marker ^ "\" in\n" ^ " let _ = List.map (fun x -> print_string (format x)) result in\n" ^ " print_string \"" ^ end_marker ^ "\";;\n" ^ "main ();;" val compiled_path = dir + Path.basic "test" val _ = check_settings compiler ISABELLE_OCAMLFIND "ocamlfind executable" val _ = List.app (File.write code_path o snd) code_files val _ = File.write driver_path driver val cmd = "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^ " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " \code_test_ghc\ (K "") fun evaluate_in_ghc ctxt (code_files, value_name) dir = let val compiler = ghcN val modules = map fst code_files val driver_path = dir + Path.basic "Main.hs" val driver = "module Main where {\n" ^ implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^ "main = do {\n" ^ " let {\n" ^ " format_term Nothing = \"\";\n" ^ " format_term (Just t) = t ();\n" ^ " format (True, _) = \"" ^ success ^ "\\n\";\n" ^ " format (False, to) = \"" ^ failure ^ "\" ++ format_term to ++ \"\\n\";\n" ^ " result = " ^ value_name ^ " ();\n" ^ " };\n" ^ " Prelude.putStr \"" ^ start_marker ^ "\";\n" ^ " Prelude.mapM_ (putStr . format) result;\n" ^ " Prelude.putStr \"" ^ end_marker ^ "\";\n" ^ " }\n" ^ "}\n" val _ = check_settings compiler ISABELLE_GHC "GHC executable" val _ = List.app (fn (name, code) => File.write (dir + Path.basic name) code) code_files val _ = File.write driver_path driver val compiled_path = dir + Path.basic "test" val cmd = "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ Config.get ctxt ghc_options ^ " -o " ^ File.bash_platform_path compiled_path ^ " " ^ File.bash_platform_path driver_path ^ " -i" ^ File.bash_platform_path dir in compile compiler cmd; evaluate compiler (File.bash_path compiled_path) end (* driver for Scala *) val scalaN = "Scala" fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir = let val generatedN = "Generated_Code" val driverN = "Driver.scala" val code_path = dir + Path.basic (generatedN ^ ".scala") val driver_path = dir + Path.basic driverN val out_path = dir + Path.basic "out" val code = #2 (the_single code_files) val driver = \<^verbatim>\ { val result = \ ^ value_name ^ \<^verbatim>\(()) val result_text = result.map( { case (true, _) => "True\n" case (false, None) => "False\n" case (false, Some(t)) => "False" + t(()) + "\n" }).mkString isabelle.File.write( isabelle.Path.explode(\ ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\), \ ^ quote start_marker ^ \<^verbatim>\ + result_text + \ ^ quote end_marker ^ \<^verbatim>\) }\ val _ = File.write code_path code val _ = File.write driver_path driver val _ = Scala_Compiler.toplevel (code ^ driver) handle ERROR msg => error ("Evaluation for " ^ scalaN ^ " failed:\n" ^ msg) in File.read out_path end (* command setup *) val _ = Outer_Syntax.command \<^command_keyword>\test_code\ "compile test cases to target languages, execute them and report results" (Scan.repeat1 Parse.prop -- (\<^keyword>\in\ |-- Scan.repeat1 Parse.name) >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of))) val target_Scala = "Scala_eval" val target_Haskell = "Haskell_eval" val _ = Theory.setup (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)]) #> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)]) #> fold add_driver [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)), (mltonN, (evaluate_in_mlton, Code_ML.target_SML)), (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)), (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)), (ghcN, (evaluate_in_ghc, target_Haskell)), (scalaN, (evaluate_in_scala, target_Scala))] #> fold (fn target => Value_Command.add_evaluator (Binding.name target, eval_term target) #> #2) [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]) end diff --git a/src/Pure/Admin/isabelle_cronjob.scala b/src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala +++ b/src/Pure/Admin/isabelle_cronjob.scala @@ -1,637 +1,637 @@ /* Title: Pure/Admin/isabelle_cronjob.scala Author: Makarius Main entry point for administrative cronjob at TUM. */ package isabelle import java.nio.file.Files import scala.annotation.tailrec object Isabelle_Cronjob { /* global resources: owned by main cronjob */ val backup = "lxbroy10:cronjob" val main_dir: Path = Path.explode("~/cronjob") val main_state_file: Path = main_dir + Path.explode("run/main.state") val build_release_log: Path = main_dir + Path.explode("run/build_release.log") val current_log: Path = main_dir + Path.explode("run/main.log") // owned by log service val cumulative_log: Path = main_dir + Path.explode("log/main.log") // owned by log service val isabelle_repos: Path = main_dir + Path.explode("isabelle") val afp_repos: Path = main_dir + Path.explode("AFP") val mailman_archives_dir = Path.explode("~/cronjob/Mailman") val build_log_dirs = List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log")) /** logger tasks **/ sealed case class Logger_Task(name: String = "", body: Logger => Unit) /* init and exit */ def get_rev(): String = Mercurial.repository(isabelle_repos).id() def get_afp_rev(): String = Mercurial.repository(afp_repos).id() val init: Logger_Task = Logger_Task("init", { logger => Isabelle_Devel.make_index() Mercurial.setup_repository(Isabelle_System.afp_repository.root, afp_repos) File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date), Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev()))) Isabelle_System.bash( """rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ + Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check if (!Isabelle_Devel.cronjob_log.is_file) Files.createSymbolicLink(Isabelle_Devel.cronjob_log.java_path, current_log.java_path) }) val exit: Logger_Task = Logger_Task("exit", { logger => Isabelle_System.bash( "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.") .check }) /* Mailman archives */ val mailman_archives: Logger_Task = Logger_Task("mailman_archives", { logger => Mailman.Isabelle_Users.download(mailman_archives_dir) Mailman.Isabelle_Dev.download(mailman_archives_dir) }) /* build release */ val build_release: Logger_Task = Logger_Task("build_release", { logger => build_release_log.file.delete Isabelle_Devel.release_snapshot(logger.options, get_rev(), get_afp_rev(), progress = new File_Progress(build_release_log)) }) /* remote build_history */ sealed case class Item( known: Boolean, isabelle_version: String, afp_version: Option[String], pull_date: Date ) { def unknown: Boolean = !known def versions: (String, Option[String]) = (isabelle_version, afp_version) def known_versions(rev: String, afp_rev: Option[String]): Boolean = known && rev != "" && isabelle_version == rev && (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev) } def recent_items( db: SQL.Database, days: Int, rev: String, afp_rev: Option[String], sql: PostgreSQL.Source ): List[Item] = { val afp = afp_rev.isDefined val select = Build_Log.Data.select_recent_versions( days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql) db.using_statement(select)(stmt => stmt.execute_query().iterator({ res => val known = res.bool(Build_Log.Data.known) val isabelle_version = res.string(Build_Log.Prop.isabelle_version) val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None val pull_date = res.date(Build_Log.Data.pull_date(afp)) Item(known, isabelle_version, afp_version, pull_date) }).toList) } def unknown_runs(items: List[Item]): List[List[Item]] = { val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known)) if (run.nonEmpty) run :: unknown_runs(rest) else Nil } sealed case class Remote_Build( description: String, host: String, user: String = "", port: Int = 0, historic: Boolean = false, history: Int = 0, history_base: String = "build_history_base", java_heap: String = "", options: String = "", args: String = "", afp: Boolean = false, bulky: Boolean = false, more_hosts: List[String] = Nil, detect: PostgreSQL.Source = "", active: Boolean = true ) { def open_session(options: Options): SSH.Session = SSH.open_session(options, host = host, user = user, port = port) def sql: PostgreSQL.Source = Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " + SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) + (if (detect == "") "" else " AND " + SQL.enclose(detect)) def profile: Build_Status.Profile = Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql) def pick( options: Options, rev: String = "", filter: Item => Boolean = _ => true ): Option[(String, Option[String])] = { val afp_rev = if (afp) Some(get_afp_rev()) else None val store = Build_Log.store(options) using(store.open_database()) { db => def pick_days(days: Int, gap: Int): Option[(String, Option[String])] = { val items = recent_items(db, days, rev, afp_rev, sql).filter(filter) def runs = unknown_runs(items).filter(run => run.length >= gap) if (historic || items.exists(_.known_versions(rev, afp_rev))) { val longest_run = runs.foldLeft(List.empty[Item]) { case (item1, item2) => if (item1.length >= item2.length) item1 else item2 } if (longest_run.isEmpty) None else Some(longest_run(longest_run.length / 2).versions) } else if (rev != "") Some((rev, afp_rev)) else runs.flatten.headOption.map(_.versions) } pick_days(options.int("build_log_history") max history, 2) orElse pick_days(200, 5) orElse pick_days(2000, 1) } } def build_history_options: String = " -h " + Bash.string(host) + " " + (java_heap match { case "" => "" case h => "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' " }) + options } val remote_builds_old: List[Remote_Build] = List( Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius", options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'"), Remote_Build("Linux A", "i21of4", user = "i21isatest", options = "-m32 -M1x4,2,4" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_MLTON=mlton" + " -e ISABELLE_SMLNJ=sml" + " -e ISABELLE_SWIPL=swipl", args = "-a -d '~~/src/Benchmarks'"), Remote_Build("Linux A", "lxbroy9", java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing"), Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90, java_heap = "2g", options = "-m32 -B -M1x2,2 -t Benchmarks" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" + " -e ISABELLE_SWIPL=swipl", args = "-N -a -d '~~/src/Benchmarks'", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("Benchmarks")), Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3", options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'"), Remote_Build("AFP old bulky", "lrzcloud1", options = "-m64 -M6 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, bulky = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("AFP old", "lxbroy7", args = "-N -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", history_base = "37074e22e8be", options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7") + " AND " + Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")), Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("Poly/ML 5.7 macOS", "macbroy2", history_base = "37074e22e8be", options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-a", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7")), Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-a", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("macOS", "macbroy2", options = "-m32 -M8" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_OPAM_ROOT=\"$ISABELLE_HOME/opam\"" + " -e ISABELLE_SMLNJ=/home/isabelle/smlnj/110.85/bin/sml" + " -p pide_session=false", args = "-a", detect = Build_Log.Prop.build_tags.undefined, history_base = "2c0f24e927dd"), Remote_Build("macOS, quick_and_dirty", "macbroy2", options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"), history_base = "2c0f24e927dd"), Remote_Build("macOS, skip_proofs", "macbroy2", options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"), history_base = "2c0f24e927dd"), Remote_Build("Poly/ML test", "lxbroy8", options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-test")), Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a", detect = Build_Log.Prop.build_start.toString + " > date '2017-03-03'"), Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"), Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start.toString + " < date '2017-03-03'")) ::: { for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) } yield { Remote_Build("AFP old", host = hosts.head, more_hosts = hosts.tail, options = "-m32 -M1x2 -t AFP -P" + n + " -e ISABELLE_GHC=ghc" + " -e ISABELLE_MLTON=mlton" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + " -e ISABELLE_SMLNJ=sml", args = "-N -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")) } } val remote_builds1: List[List[Remote_Build]] = { List( List(Remote_Build("Linux A", "augsburg1", options = "-m32 -B -M4" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + " -e ISABELLE_GHC_SETUP=true" + - " -e ISABELLE_MLTON=mlton" + + " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" + " -e ISABELLE_SMLNJ=sml" + " -e ISABELLE_SWIPL=swipl", args = "-a -d '~~/src/Benchmarks'")), List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68", options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("macOS 11 Big Sur", "mini1", options = "-m32 -B -M1x2,2,4 -p pide_session=false" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + - " -e ISABELLE_MLTON=/usr/local/bin/mlton" + + " -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" + " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" + " -e ISABELLE_SWIPL=/usr/local/bin/swipl", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("macOS 10.14 Mojave", "mini2", options = "-m32 -B -M1x2,2,4 -p pide_session=false" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + - " -e ISABELLE_MLTON=/usr/local/bin/mlton" + + " -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" + " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" + " -e ISABELLE_SWIPL=/usr/local/bin/swipl", args = "-a -d '~~/src/Benchmarks'"), Remote_Build("macOS, quick_and_dirty", "mini2", options = "-m32 -M4 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty")), Remote_Build("macOS, skip_proofs", "mini2", options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))), List( Remote_Build("macOS 10.15 Catalina", "monterey", user = "makarius", options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, options = "-m32 -M4" + " -C /cygdrive/d/isatest/contrib" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86-windows") + " OR " + Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")), Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, options = "-m64 -M4" + " -C /cygdrive/d/isatest/contrib" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows")))) } val remote_builds2: List[List[Remote_Build]] = List( List( Remote_Build("AFP", "lrzcloud2", java_heap = "8g", options = "-m32 -M1x6 -t AFP" + " -e ISABELLE_GHC=ghc" + - " -e ISABELLE_MLTON=mlton" + + " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + " -e ISABELLE_SMLNJ=sml", args = "-a -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("AFP", "lrzcloud2", java_heap = "8g", options = "-m64 -M8 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, bulky = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")))) def remote_build_history( rev: String, afp_rev: Option[String], i: Int, r: Remote_Build ) : Logger_Task = { val task_name = "build_history-" + r.host Logger_Task(task_name, { logger => using(r.open_session(logger.options)) { ssh => val results = Build_History.remote_build(ssh, isabelle_repos, isabelle_repos.ext(r.host), isabelle_identifier = "cronjob_build_history", rev = rev, afp_repos = if (afp_rev.isDefined) Some(afp_repos) else None, afp_rev = afp_rev.getOrElse(""), options = " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) + " -R " + Bash.string(Components.default_component_repository) + " -C '$USER_HOME/.isabelle/contrib' -f " + r.build_history_options, args = "-o timeout=10800 " + r.args) for ((log_name, bytes) <- results) { logger.log(Date.now(), log_name) Bytes.write(logger.log_dir + Path.explode(log_name), bytes) } } }) } val build_status_profiles: List[Build_Status.Profile] = (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile) /** task logging **/ object Log_Service { def apply(options: Options, progress: Progress = new Progress): Log_Service = new Log_Service(options, progress) } class Log_Service private(val options: Options, progress: Progress) { current_log.file.delete private val thread: Consumer_Thread[String] = Consumer_Thread.fork("cronjob: logger", daemon = true)( consume = { (text: String) => // critical File.append(current_log, text + "\n") File.append(cumulative_log, text + "\n") progress.echo(text) true }) def shutdown(): Unit = { thread.shutdown() } val hostname: String = Isabelle_System.hostname() def log(date: Date, task_name: String, msg: String): Unit = if (task_name != "") thread.send( "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg) def start_logger(start_date: Date, task_name: String): Logger = new Logger(this, start_date, task_name) def run_task(start_date: Date, task: Logger_Task): Unit = { val logger = start_logger(start_date, task.name) val res = Exn.capture { task.body(logger) } val end_date = Date.now() val err = res match { case Exn.Res(_) => None case Exn.Exn(exn) => Output.writeln("Exception trace for " + quote(task.name) + ":") exn.printStackTrace() val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception" Some(first_line) } logger.log_end(end_date, err) } def fork_task(start_date: Date, task: Logger_Task): Task = new Task(task.name, run_task(start_date, task)) } class Logger private[Isabelle_Cronjob]( log_service: Log_Service, val start_date: Date, val task_name: String ) { def options: Options = log_service.options def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg) def log_end(end_date: Date, err: Option[String]): Unit = { val elapsed_time = end_date.time - start_date.time val msg = (if (err.isEmpty) "finished" else "ERROR " + err.get) + (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)") log(end_date, msg) } val log_dir = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date)) log(start_date, "started") } class Task private[Isabelle_Cronjob](name: String, body: => Unit) { private val future: Future[Unit] = Future.thread("cronjob: " + name) { body } def is_finished: Boolean = future.is_finished } /** cronjob **/ def cronjob(progress: Progress, exclude_task: Set[String]): Unit = { /* soft lock */ val still_running = try { Some(File.read(main_state_file)) } catch { case ERROR(_) => None } still_running match { case None | Some("") => case Some(running) => error("Isabelle cronjob appears to be still running: " + running) } /* log service */ val log_service = Log_Service(Options.init(), progress = progress) def run(start_date: Date, task: Logger_Task): Unit = log_service.run_task(start_date, task) def run_now(task: Logger_Task): Unit = run(Date.now(), task) /* structured tasks */ def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "") run_now(task)) def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = { _ => @tailrec def join(running: List[Task]): Unit = { running.partition(_.is_finished) match { case (Nil, Nil) => case (Nil, _ :: _) => Time.seconds(0.5).sleep(); join(running) case (_ :: _, remaining) => join(remaining) } } val start_date = Date.now() val running = for (task <- tasks if !exclude_task(task.name)) yield log_service.fork_task(start_date, task) join(running) }) /* repository structure */ val hg = Mercurial.repository(isabelle_repos) val hg_graph = hg.graph() def history_base_filter(r: Remote_Build): Item => Boolean = { val base_rev = hg.id(r.history_base) val nodes = hg_graph.all_succs(List(base_rev)).toSet (item: Item) => nodes(item.isabelle_version) } /* main */ val main_start_date = Date.now() File.write(main_state_file, main_start_date.toString + " " + log_service.hostname) run(main_start_date, Logger_Task("isabelle_cronjob", logger => run_now( SEQ(List( init, PAR(List(mailman_archives, build_release)), PAR( List(remote_builds1, remote_builds2).map(remote_builds => SEQ(List( PAR(remote_builds.map(_.filter(_.active)).map(seq => SEQ( for { (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex) (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r)) } yield remote_build_history(rev, afp_rev, i, r)))), Logger_Task("jenkins_logs", _ => Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)), Logger_Task("build_log_database", logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)), Logger_Task("build_status", logger => Isabelle_Devel.build_status(logger.options)))))), exit))))) log_service.shutdown() main_state_file.file.delete } /** command line entry point **/ def main(args: Array[String]): Unit = { Command_Line.tool { var force = false var verbose = false var exclude_task = Set.empty[String] val getopts = Getopts(""" Usage: Admin/cronjob/main [OPTIONS] Options are: -f apply force to do anything -v verbose -x NAME exclude tasks with this name """, "f" -> (_ => force = true), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_task += arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = if (verbose) new Console_Progress() else new Progress if (force) cronjob(progress, exclude_task) else error("Need to apply force to do anything") } } }