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,542 +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 [] = \<^term>\()\ | mk_tuples [t] = t | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts) fun dest_tuples (Const (\<^const_name>\Pair\, _) $ 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 = [] val extend = I 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 = - let - val dir = - Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) - val _ = Isabelle_System.make_directory dir - in Exn.release (Exn.capture f dir) end + Path.append (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 o apfst) Long_Name.implode 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 (\<^const_name>\Trueprop\, _) $ t) = add_eval t | add_eval (Const (\<^const_name>\HOL.eq\, _) $ lhs $ rhs) = (fn acc => acc |> add_eval rhs |> add_eval lhs |> cons rhs |> cons lhs) | add_eval (Const (\<^const_name>\Not\, _) $ t) = add_eval t | add_eval (Const (\<^const_name>\Orderings.ord_class.less_eq\, _) $ lhs $ rhs) = (fn acc => lhs :: rhs :: acc) | add_eval (Const (\<^const_name>\Orderings.ord_class.less\, _) $ lhs $ rhs) = (fn acc => lhs :: rhs :: acc) | add_eval _ = I fun mk_term_of [] = \<^term>\None :: (unit \ yxml_of_term) option\ | mk_term_of ts = let val tuple = mk_tuples ts val T = fastype_of tuple in \<^term>\Some :: (unit \ yxml_of_term) \ (unit \ yxml_of_term) option\ $ (absdummy \<^typ>\unit\ (\<^const>\yxml_string_of_term\ $ (Const (\<^const_name>\Code_Evaluation.term_of\, T --> \<^typ>\term\) $ 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 \<^typ>\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 (\<^term>\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 = Path.append dir (Path.basic "generated.sml") val driver_path = Path.append dir (Path.basic "driver.sml") val out_path = Path.append 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 = Path.append dir (Path.basic generatedN) val driver_path = Path.append dir (Path.basic driverN) val basis_path = Path.append 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 (Path.append 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 = Path.append dir (Path.basic generatedN) val driver_path = Path.append 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 = Path.append dir (Path.basic "generated.ml") val driver_path = Path.append 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 = Path.append 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 = Path.append 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 (Path.append dir (Path.basic name)) code) code_files val _ = File.write driver_path driver val compiled_path = Path.append 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 = Path.append dir (Path.basic (generatedN ^ ".scala")) val driver_path = Path.append dir (Path.basic driverN) val out_path = Path.append 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 true (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/HOL/Tools/Quickcheck/narrowing_generators.ML b/src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML @@ -1,548 +1,547 @@ (* Title: HOL/Tools/Quickcheck/narrowing_generators.ML Author: Lukas Bulwahn, TU Muenchen Narrowing-based counterexample generation. *) signature NARROWING_GENERATORS = sig val allow_existentials : bool Config.T val finite_functions : bool Config.T val overlord : bool Config.T val ghc_options : string Config.T (* FIXME prefer settings, i.e. getenv (!?) *) val active : bool Config.T datatype counterexample = Universal_Counterexample of (term * counterexample) | Existential_Counterexample of (term * counterexample) list | Empty_Assignment val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context end structure Narrowing_Generators : NARROWING_GENERATORS = struct (* configurations *) val allow_existentials = Attrib.setup_config_bool \<^binding>\quickcheck_allow_existentials\ (K true) val finite_functions = Attrib.setup_config_bool \<^binding>\quickcheck_finite_functions\ (K true) val overlord = Attrib.setup_config_bool \<^binding>\quickcheck_narrowing_overlord\ (K false) val ghc_options = Attrib.setup_config_string \<^binding>\quickcheck_narrowing_ghc_options\ (K "") (* partial_term_of instances *) fun mk_partial_term_of (x, T) = Const (\<^const_name>\Quickcheck_Narrowing.partial_term_of_class.partial_term_of\, Term.itselfT T --> \<^typ>\narrowing_term\ --> \<^typ>\Code_Evaluation.term\) $ Logic.mk_type T $ x (** formal definition **) fun add_partial_term_of tyco raw_vs thy = let val vs = map (fn (v, _) => (v, \<^sort>\typerep\)) raw_vs val ty = Type (tyco, map TFree vs) val lhs = Const (\<^const_name>\partial_term_of\, Term.itselfT ty --> \<^typ>\narrowing_term\ --> \<^typ>\Code_Evaluation.term\) $ Free ("x", Term.itselfT ty) $ Free ("t", \<^typ>\narrowing_term\) val rhs = \<^term>\undefined :: Code_Evaluation.term\ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv" in thy |> Class.instantiation ([tyco], vs, \<^sort>\partial_term_of\) |> `(fn lthy => Syntax.check_term lthy eq) |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq)) |> snd |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) end fun ensure_partial_term_of (tyco, (raw_vs, _)) thy = let val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\partial_term_of\) andalso Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\typerep\ in if need_inst then add_partial_term_of tyco raw_vs thy else thy end (** code equations for datatypes **) fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) = let val frees = map Free (Name.invent_names Name.context "a" (map (K \<^typ>\narrowing_term\) tys)) val narrowing_term = \<^term>\Quickcheck_Narrowing.Narrowing_constructor\ $ HOLogic.mk_number \<^typ>\integer\ i $ HOLogic.mk_list \<^typ>\narrowing_term\ (rev frees) val rhs = fold (fn u => fn t => \<^term>\Code_Evaluation.App\ $ t $ u) (map mk_partial_term_of (frees ~~ tys)) (\<^term>\Code_Evaluation.Const\ $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty)) val insts = map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), narrowing_term, rhs] val cty = Thm.global_ctyp_of thy ty in @{thm partial_term_of_anything} |> Thm.instantiate' [SOME cty] insts |> Thm.varifyT_global end fun add_partial_term_of_code tyco raw_vs raw_cs thy = let val algebra = Sign.classes_of thy val vs = map (fn (v, sort) => (v, curry (Sorts.inter_sort algebra) \<^sort>\typerep\ sort)) raw_vs val ty = Type (tyco, map TFree vs) val cs = (map o apsnd o apsnd o map o map_atyps) (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs val const = Axclass.param_of_inst thy (\<^const_name>\partial_term_of\, tyco) val var_insts = map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), \<^term>\Quickcheck_Narrowing.Narrowing_variable p tt\, \<^term>\Code_Evaluation.Free (STR ''_'')\ $ HOLogic.mk_typerep ty] val var_eq = @{thm partial_term_of_anything} |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts |> Thm.varifyT_global val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs in thy |> Code.declare_default_eqns_global (map (rpair true) eqs) end fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = let val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\partial_term_of\ in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end (* narrowing generators *) (** narrowing specific names and types **) exception FUNCTION_TYPE val narrowingN = "narrowing" fun narrowingT T = \<^typ>\integer\ --> Type (\<^type_name>\Quickcheck_Narrowing.narrowing_cons\, [T]) fun mk_cons c T = Const (\<^const_name>\Quickcheck_Narrowing.cons\, T --> narrowingT T) $ Const (c, T) fun mk_apply (T, t) (U, u) = let val (_, U') = dest_funT U in (U', Const (\<^const_name>\Quickcheck_Narrowing.apply\, narrowingT U --> narrowingT T --> narrowingT U') $ u $ t) end fun mk_sum (t, u) = let val T = fastype_of t in Const (\<^const_name>\Quickcheck_Narrowing.sum\, T --> T --> T) $ t $ u end (** deriving narrowing instances **) fun mk_equations descr vs narrowings = let fun mk_call T = (T, Const (\<^const_name>\Quickcheck_Narrowing.narrowing_class.narrowing\, narrowingT T)) fun mk_aux_call fTs (k, _) (tyco, Ts) = let val T = Type (tyco, Ts) val _ = if not (null fTs) then raise FUNCTION_TYPE else () in (T, nth narrowings k) end fun mk_consexpr simpleT (c, xs) = let val Ts = map fst xs in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end fun mk_rhs exprs = foldr1 mk_sum exprs val rhss = Old_Datatype_Aux.interpret_construction descr vs { atyp = mk_call, dtyp = mk_aux_call } |> (map o apfst) Type |> map (fn (T, cs) => map (mk_consexpr T) cs) |> map mk_rhs val lhss = narrowings val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) in eqs end fun contains_recursive_type_under_function_types xs = exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT => (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = let val _ = Old_Datatype_Aux.message config "Creating narrowing generators ..." val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames) in if not (contains_recursive_type_under_function_types descr) then thy |> Class.instantiation (tycos, vs, \<^sort>\narrowing\) |> Quickcheck_Common.define_functions (fn narrowings => mk_equations descr vs narrowings, NONE) prfx [] narrowingsN (map narrowingT (Ts @ Us)) |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) else thy end (* testing framework *) val target = "Haskell_Quickcheck" (** invocation of Haskell interpreter **) val narrowing_engine = File.read \<^file>\~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\ val pnf_narrowing_engine = File.read \<^file>\~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\ fun exec verbose code = ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context {line = 0, file = "generated code", verbose = verbose, debug = false} code) fun with_overlord_dir name f = - let - val path = - Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) - val _ = Isabelle_System.make_directory path - in Exn.release (Exn.capture f path) end + Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) + |> Isabelle_System.make_directory + |> Exn.capture f + |> Exn.release fun elapsed_time description e = let val ({elapsed, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds elapsed)) end fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) = let val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie fun message s = if quiet then () else writeln s fun verbose_message s = if not quiet andalso verbose then writeln s else () val current_size = Unsynchronized.ref 0 val current_result = Unsynchronized.ref Quickcheck.empty_result val tmp_prefix = "Quickcheck_Narrowing" val ghc_options = Config.get ctxt ghc_options val with_tmp_dir = if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir fun run in_path = let fun mk_code_file module = let val (paths, base) = split_last module in Path.appends (in_path :: map Path.basic (paths @ [suffix ".hs" base])) end; val generatedN_suffix = suffix ".hs" Code_Target.generatedN; val includes = AList.delete (op =) [generatedN_suffix] code_modules |> (map o apfst) mk_code_file val code = the (AList.lookup (op =) code_modules [generatedN_suffix]) val code_file = mk_code_file [Code_Target.generatedN] val narrowing_engine_file = mk_code_file ["Narrowing_Engine"] val main_file = mk_code_file ["Main"] val main = "module Main where {\n\n" ^ "import System.IO;\n" ^ "import System.Environment;\n" ^ "import Narrowing_Engine;\n" ^ "import " ^ Code_Target.generatedN ^ " ;\n\n" ^ "main = getArgs >>= \\[potential, size] -> " ^ "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ Code_Target.generatedN ^ ".value ())\n\n}\n" val _ = map (uncurry File.write) (includes @ [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine), (code_file, code), (main_file, main)]) val executable = Path.append in_path (Path.basic "isabelle_quickcheck_narrowing") val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^ (space_implode " " (map File.bash_platform_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ " -o " ^ File.bash_platform_path executable ^ ";" val (_, compilation_time) = elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) val _ = Quickcheck.add_timing compilation_time current_result fun haskell_string_of_bool v = if v then "True" else "False" val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else () fun with_size genuine_only k = if k > size then (NONE, !current_result) else let val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k) val _ = current_size := k val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k) (fn () => Isabelle_System.bash_output (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k)) val _ = Quickcheck.add_timing timing current_result in if response = "NONE\n" then with_size genuine_only (k + 1) else let val output_value = the_default "NONE" (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response) val ml_code = "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))" val ctxt' = ctxt |> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) |> Context.proof_map (exec false ml_code) val counterexample = get ctxt' () in if is_genuine counterexample then (counterexample, !current_result) else let val cex = Option.map (rpair []) (counterexample_of counterexample) val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)) val _ = message "Quickcheck continues to find a genuine counterexample..." in with_size true (k + 1) end end end in with_size genuine_only 0 end in with_tmp_dir tmp_prefix run end fun dynamic_value_strict opts cookie ctxt postproc t = let fun evaluator program _ vs_ty_t deps = Exn.interruptible_capture (value opts ctxt cookie) (Code_Target.compilation_text ctxt target program deps true vs_ty_t) in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end (** counterexample generator **) datatype counterexample = Universal_Counterexample of (term * counterexample) | Existential_Counterexample of (term * counterexample) list | Empty_Assignment fun map_counterexample _ Empty_Assignment = Empty_Assignment | map_counterexample f (Universal_Counterexample (t, c)) = Universal_Counterexample (f t, map_counterexample f c) | map_counterexample f (Existential_Counterexample cs) = Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs) structure Data = Proof_Data ( type T = (unit -> (bool * term list) option) * (unit -> counterexample option) val empty: T = (fn () => raise Fail "counterexample", fn () => raise Fail "existential_counterexample") fun init _ = empty ) val get_counterexample = #1 o Data.get; val get_existential_counterexample = #2 o Data.get; val put_counterexample = Data.map o @{apply 2(1)} o K val put_existential_counterexample = Data.map o @{apply 2(2)} o K fun finitize_functions (xTs, t) = let val (names, boundTs) = split_list xTs fun mk_eval_ffun dT rT = Const (\<^const_name>\Quickcheck_Narrowing.eval_ffun\, Type (\<^type_name>\Quickcheck_Narrowing.ffun\, [dT, rT]) --> dT --> rT) fun mk_eval_cfun dT rT = Const (\<^const_name>\Quickcheck_Narrowing.eval_cfun\, Type (\<^type_name>\Quickcheck_Narrowing.cfun\, [rT]) --> dT --> rT) fun eval_function (Type (\<^type_name>\fun\, [dT, rT])) = let val (rt', rT') = eval_function rT in (case dT of Type (\<^type_name>\fun\, _) => (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)), Type (\<^type_name>\Quickcheck_Narrowing.cfun\, [rT'])) | _ => (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)), Type (\<^type_name>\Quickcheck_Narrowing.ffun\, [dT, rT']))) end | eval_function (T as Type (\<^type_name>\prod\, [fT, sT])) = let val (ft', fT') = eval_function fT val (st', sT') = eval_function sT val T' = Type (\<^type_name>\prod\, [fT', sT']) val map_const = Const (\<^const_name>\map_prod\, (fT' --> fT) --> (sT' --> sT) --> T' --> T) fun apply_dummy T t = absdummy T (t (Bound 0)) in (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T') end | eval_function T = (I, T) val (tt, boundTs') = split_list (map eval_function boundTs) val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t) in (names ~~ boundTs', t') end fun dest_ffun (Type (\<^type_name>\Quickcheck_Narrowing.ffun\, [dT, rT])) = (dT, rT) fun eval_finite_functions (Const (\<^const_name>\Quickcheck_Narrowing.ffun.Constant\, T) $ value) = absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value) | eval_finite_functions (Const (\<^const_name>\Quickcheck_Narrowing.ffun.Update\, T) $ a $ b $ f) = let val (T1, T2) = dest_ffun (body_type T) in Quickcheck_Common.mk_fun_upd T1 T2 (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f) end | eval_finite_functions t = t (** tester **) val rewrs = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) (@{thms all_simps} @ @{thms ex_simps}) @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}, @{thm meta_eq_to_obj_eq [OF Ex1_def]}] fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t fun strip_quantifiers (Const (\<^const_name>\Ex\, _) $ Abs (x, T, t)) = apfst (cons (\<^const_name>\Ex\, (x, T))) (strip_quantifiers t) | strip_quantifiers (Const (\<^const_name>\All\, _) $ Abs (x, T, t)) = apfst (cons (\<^const_name>\All\, (x, T))) (strip_quantifiers t) | strip_quantifiers t = ([], t) fun contains_existentials t = exists (fn (Q, _) => Q = \<^const_name>\Ex\) (fst (strip_quantifiers t)) fun mk_property qs t = let fun enclose (\<^const_name>\Ex\, (x, T)) t = Const (\<^const_name>\Quickcheck_Narrowing.exists\, (T --> \<^typ>\property\) --> \<^typ>\property\) $ Abs (x, T, t) | enclose (\<^const_name>\All\, (x, T)) t = Const (\<^const_name>\Quickcheck_Narrowing.all\, (T --> \<^typ>\property\) --> \<^typ>\property\) $ Abs (x, T, t) in fold_rev enclose qs (\<^term>\Quickcheck_Narrowing.Property\ $ t) end fun mk_case_term ctxt p ((\<^const_name>\Ex\, (x, T)) :: qs') (Existential_Counterexample cs) = Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) => (t, mk_case_term ctxt (p - 1) qs' c)) cs) | mk_case_term ctxt p ((\<^const_name>\All\, _) :: qs') (Universal_Counterexample (t, c)) = if p = 0 then t else mk_case_term ctxt (p - 1) qs' c val post_process = perhaps (try Quickcheck_Common.post_process_term) o eval_finite_functions fun mk_terms ctxt qs result = let val ps = filter (fn (_, (\<^const_name>\All\, _)) => true | _ => false) (map_index I qs) in map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps |> map (apsnd post_process) end fun test_term ctxt catch_code_errors (t, _) = let fun dest_result (Quickcheck.Result r) = r val opts = ((Config.get ctxt Quickcheck.genuine_only, (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)), Config.get ctxt Quickcheck.size) val thy = Proof_Context.theory_of ctxt val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t val pnf_t = make_pnf_term thy t' in if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then let fun wrap f (qs, t) = let val (qs1, qs2) = split_list qs in apfst (map2 pair qs1) (f (qs2, t)) end val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I val (qs, prop_t) = finitize (strip_quantifiers pnf_t) val act = if catch_code_errors then try else (fn f => SOME o f) val execute = dynamic_value_strict (true, opts) ((K true, fn _ => error ""), (get_existential_counterexample, put_existential_counterexample, "Narrowing_Generators.put_existential_counterexample")) ctxt (apfst o Option.map o map_counterexample) in (case act execute (mk_property qs prop_t) of SOME (counterexample, result) => Quickcheck.Result {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample, evaluation_terms = Option.map (K []) counterexample, timings = #timings (dest_result result), reports = #reports (dest_result result)} | NONE => (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing"; Quickcheck.empty_result)) end else let val frees = Term.add_frees t [] val t' = fold_rev absfree frees t fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t)) val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I fun ensure_testable t = Const (\<^const_name>\Quickcheck_Narrowing.ensure_testable\, fastype_of t --> fastype_of t) $ t fun is_genuine (SOME (true, _)) = true | is_genuine _ = false val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process)) val act = if catch_code_errors then try else (fn f => SOME o f) val execute = dynamic_value_strict (false, opts) ((is_genuine, counterexample_of), (get_counterexample, put_counterexample, "Narrowing_Generators.put_counterexample")) ctxt (apfst o Option.map o apsnd o map) in (case act execute (ensure_testable (finitize t')) of SOME (counterexample, result) => Quickcheck.Result {counterexample = counterexample_of counterexample, evaluation_terms = Option.map (K []) counterexample, timings = #timings (dest_result result), reports = #reports (dest_result result)} | NONE => (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing"; Quickcheck.empty_result)) end end fun test_goals ctxt catch_code_errors insts goals = if not (getenv "ISABELLE_GHC" = "") then let val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing..." val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals in Quickcheck_Common.collect_results (test_term ctxt catch_code_errors) (maps (map snd) correct_inst_goals) [] end else (if Config.get ctxt Quickcheck.quiet then () else writeln ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set " ^ "this variable to your GHC Haskell compiler in your settings file. " ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false."); [Quickcheck.empty_result]) (* setup *) val active = Attrib.setup_config_bool \<^binding>\quickcheck_narrowing_active\ (K false) val _ = Theory.setup (Code.datatype_interpretation ensure_partial_term_of #> Code.datatype_interpretation ensure_partial_term_of_code #> Quickcheck_Common.datatype_interpretation \<^plugin>\quickcheck_narrowing\ (\<^sort>\narrowing\, instantiate_narrowing_datatype) #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))) end diff --git a/src/Pure/Admin/build_cygwin.scala b/src/Pure/Admin/build_cygwin.scala --- a/src/Pure/Admin/build_cygwin.scala +++ b/src/Pure/Admin/build_cygwin.scala @@ -1,89 +1,88 @@ /* Title: Pure/Admin/build_cygwin.scala Author: Makarius Produce pre-canned Cygwin distribution for Isabelle. */ package isabelle object Build_Cygwin { val default_mirror: String = "https://isabelle.sketis.net/cygwin_2021" val packages: List[String] = List("curl", "libgmp-devel", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip") def build_cygwin(progress: Progress, mirror: String = default_mirror, more_packages: List[String] = Nil) { require(Platform.is_windows) Isabelle_System.with_tmp_dir("cygwin")(tmp_dir => { val cygwin = tmp_dir + Path.explode("cygwin") val cygwin_etc = cygwin + Path.explode("etc") - val cygwin_isabelle = cygwin + Path.explode("isabelle") - Isabelle_System.make_directory(cygwin_isabelle) + val cygwin_isabelle = Isabelle_System.make_directory(cygwin + Path.explode("isabelle")) val cygwin_exe_name = mirror + "/setup-x86_64.exe" val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe") Bytes.write(cygwin_exe, try { Bytes.read(Url(cygwin_exe_name)) } catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) }) File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror) File.set_executable(cygwin_exe, true) Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h /dev/null").check val res = progress.bash( File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" + " --local-package-dir 'C:\\temp'" + " --root " + File.bash_platform_path(cygwin) + " --packages " + quote((packages ::: more_packages).mkString(",")) + " --no-shortcuts --no-startmenu --no-desktop --quiet-mode", echo = true) if (!res.ok || !cygwin_etc.is_dir) error("Failed") for (name <- List("hosts", "protocols", "services", "networks", "passwd", "group")) (cygwin_etc + Path.explode(name)).file.delete (cygwin + Path.explode("Cygwin.bat")).file.delete val archive = "cygwin-" + Date.Format("uuuuMMdd")(Date.now()) + ".tar.gz" Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle", args => { var mirror = default_mirror var more_packages: List[String] = Nil val getopts = Getopts(""" Usage: isabelle build_cygwin [OPTIONS] Options are: -R MIRROR Cygwin mirror site (default """ + quote(default_mirror) + """) -p NAME additional Cygwin package Produce pre-canned Cygwin distribution for Isabelle: this requires Windows administrator mode. """, "R:" -> (arg => mirror = arg), "p:" -> (arg => more_packages ::= arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages) }) } diff --git a/src/Pure/Admin/build_e.scala b/src/Pure/Admin/build_e.scala --- a/src/Pure/Admin/build_e.scala +++ b/src/Pure/Admin/build_e.scala @@ -1,184 +1,182 @@ /* Title: Pure/Admin/build_e.scala Author: Makarius Build Isabelle E prover component from official downloads. */ package isabelle object Build_E { /* build E prover */ val default_version = "2.5" val default_download_url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD" val default_runepar_url = "https://raw.githubusercontent.com/JUrban/MPTP2/66f03e5b6df8/MaLARea/bin/runepar.pl" def build_e( version: String = default_version, download_url: String = default_download_url, runepar_url: String = default_runepar_url, verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current) { Isabelle_System.with_tmp_dir("e")(tmp_dir => { /* component */ val component_name = "e-" + version val component_dir = target_dir + Path.basic(component_name) if (component_dir.is_dir) error("Component directory already exists: " + component_dir) else { progress.echo("Component " + component_dir) Isabelle_System.make_directory(component_dir) } val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) .getOrElse(error("No 64bit platform")) - val platform_dir = component_dir + Path.basic(platform_name) - Isabelle_System.make_directory(platform_dir) + val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name)) /* runepar.pl */ val runepar_path = platform_dir + Path.basic("runepar.pl") Isabelle_System.download(runepar_url, runepar_path, progress = progress) File.write(runepar_path, File.read(runepar_path) .replace("#!/usr/bin/perl", "#!/usr/bin/env perl") .replace("bin/eprover", "$ENV{E_HOME}/eprover") .replace("bin/eproof", "$ENV{E_HOME}/eproof")) File.set_executable(runepar_path, true) /* download source */ val e_url = download_url + "/V_" + version + "/E.tgz" val e_path = tmp_dir + Path.explode("E.tgz") Isabelle_System.download(e_url, e_path, progress = progress) Isabelle_System.bash("tar xzf " + e_path, cwd = tmp_dir.file).check Isabelle_System.bash("tar xzf " + e_path + " && mv E src", cwd = component_dir.file).check /* build */ progress.echo("Building E prover ...") val build_dir = tmp_dir + Path.basic("E") val build_options = { val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file) if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else "" } val build_script = "./configure" + build_options + " && make" Isabelle_System.bash(build_script, cwd = build_dir.file, progress_stdout = progress.echo_if(verbose, _), progress_stderr = progress.echo_if(verbose, _)).check /* install */ File.copy(build_dir + Path.basic("COPYING"), component_dir + Path.basic("LICENSE")) val install_files = List("epclextract", "eproof_ram", "eprover", "eprover-ho") for (name <- install_files ::: install_files.map(_ + ".exe")) { val path = build_dir + Path.basic("PROVER") + Path.basic(name) if (path.is_file) File.copy(path, platform_dir) } Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi", cwd = platform_dir.file).check val eproof_ram = platform_dir + Path.basic("eproof_ram") if (eproof_ram.is_file) { File.write(eproof_ram, File.read(eproof_ram) .replace("EXECPATH=.", "EXECPATH=`dirname \"$0\"`")) } /* settings */ - val etc_dir = component_dir + Path.basic("etc") - Isabelle_System.make_directory(etc_dir) + val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) File.write(etc_dir + Path.basic("settings"), """# -*- shell-script -*- :mode=shellscript: E_HOME="$COMPONENT/$ISABELLE_PLATFORM64" E_VERSION=""" + quote(version) + """ """) /* README */ File.write(component_dir + Path.basic("README"), "This is E prover " + version + " from\n" + e_url + """ The distribution has been built like this: cd src && """ + build_script + """ Only a few executables from PROVERS/ have been moved to the platform-specific Isabelle component directory: x86_64-linux etc. This includes a copy of Josef Urban's "runepar.pl" script, modified to use the correct path. Makarius """ + Date.Format.date(Date.now()) + "\n") }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_e", "build Isabelle E prover component from official download", args => { var download_url = default_download_url var target_dir = Path.current var runepar_url = default_runepar_url var version = default_version var verbose = false val getopts = Getopts(""" Usage: isabelle build_e [OPTIONS] Options are: -E URL E prover download URL (default: """ + default_download_url + """) -D DIR target directory (default ".") -R URL URL for runepar.pl by Josef Urban (default: """ + default_runepar_url + """) -V VERSION E prover version (default: """ + default_version + """) -v verbose Build E prover component from the specified download URLs and version. """, "E:" -> (arg => download_url = arg), "D:" -> (arg => target_dir = Path.explode(arg)), "R:" -> (arg => runepar_url = arg), "V:" -> (arg => version = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_e(version = version, download_url = download_url, runepar_url = runepar_url, verbose = verbose, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_fonts.scala b/src/Pure/Admin/build_fonts.scala --- a/src/Pure/Admin/build_fonts.scala +++ b/src/Pure/Admin/build_fonts.scala @@ -1,364 +1,363 @@ /* Title: Pure/Admin/build_fonts.scala Author: Makarius Build standard Isabelle fonts: DejaVu base + Isabelle symbols. */ package isabelle object Build_Fonts { /* relevant codepoint ranges */ object Range { def base_font: Seq[Int] = (0x0020 to 0x007e) ++ // ASCII (0x00a0 to 0x024f) ++ // Latin Extended-A/B (0x0400 to 0x04ff) ++ // Cyrillic (0x0600 to 0x06ff) ++ // Arabic Seq( 0x02dd, // hungarumlaut 0x2018, // single quote 0x2019, // single quote 0x201a, // single quote 0x201c, // double quote 0x201d, // double quote 0x201e, // double quote 0x2039, // single guillemet 0x203a, // single guillemet 0x204b, // FOOTNOTE 0x20ac, // Euro 0x2710, // pencil 0xfb01, // ligature fi 0xfb02, // ligature fl 0xfffd, // replacement character ) def isabelle_font: Seq[Int] = Seq( 0x05, // X 0x06, // Y 0x07, // EOF 0x7f, // DEL 0xaf, // INVERSE 0xac, // logicalnot 0xb0, // degree 0xb1, // plusminus 0xb7, // periodcentered 0xd7, // multiply 0xf7, // divide ) ++ (0x0370 to 0x03ff) ++ // Greek (pseudo math) (0x0590 to 0x05ff) ++ // Hebrew (non-mono) Seq( 0x2010, // hyphen 0x2013, // dash 0x2014, // dash 0x2015, // dash 0x2020, // dagger 0x2021, // double dagger 0x2022, // bullet 0x2026, // ellipsis 0x2030, // perthousand 0x2032, // minute 0x2033, // second 0x2038, // caret 0x20cd, // currency symbol ) ++ (0x2100 to 0x214f) ++ // Letterlike Symbols (0x2190 to 0x21ff) ++ // Arrows (0x2200 to 0x22ff) ++ // Mathematical Operators (0x2300 to 0x23ff) ++ // Miscellaneous Technical Seq( 0x2423, // graphic for space 0x2500, // box drawing 0x2501, // box drawing 0x2508, // box drawing 0x2509, // box drawing 0x2550, // box drawing ) ++ (0x25a0 to 0x25ff) ++ // Geometric Shapes Seq( 0x261b, // ACTION 0x2660, // spade suit 0x2661, // heart suit 0x2662, // diamond suit 0x2663, // club suit 0x266d, // musical flat 0x266e, // musical natural 0x266f, // musical sharp 0x2756, // UNDEFINED 0x2759, // BOLD 0x27a7, // DESCR 0x27e6, // left white square bracket 0x27e7, // right white square bracket 0x27e8, // left angle bracket 0x27e9, // right angle bracket 0x27ea, // left double angle bracket 0x27eb, // right double angle bracket ) ++ (0x27f0 to 0x27ff) ++ // Supplemental Arrows-A (0x2900 to 0x297f) ++ // Supplemental Arrows-B (0x2980 to 0x29ff) ++ // Miscellaneous Mathematical Symbols-B (0x2a00 to 0x2aff) ++ // Supplemental Mathematical Operators Seq(0x2b1a) ++ // VERBATIM (0x1d400 to 0x1d7ff) ++ // Mathematical Alphanumeric Symbols Seq( 0x1f310, // globe with meridians (Symbola font) 0x1f4d3, // notebook (Symbola font) 0x1f5c0, // folder (Symbola font) 0x1f5cf, // page (Symbola font) ) def isabelle_math_font: Seq[Int] = (0x21 to 0x2f) ++ // bang .. slash (0x3a to 0x40) ++ // colon .. atsign (0x5b to 0x5f) ++ // leftbracket .. underscore (0x7b to 0x7e) ++ // leftbrace .. tilde Seq( 0xa9, // copyright 0xae, // registered ) val vacuous_font: Seq[Int] = Seq(0x3c) // "<" as template } /* font families */ sealed case class Family( plain: String = "", bold: String = "", italic: String = "", bold_italic: String = "") { val fonts: List[String] = proper_string(plain).toList ::: proper_string(bold).toList ::: proper_string(italic).toList ::: proper_string(bold_italic).toList def get(index: Int): String = fonts(index % fonts.length) } object Family { def isabelle_symbols: Family = Family( plain = "IsabelleSymbols.sfd", bold = "IsabelleSymbolsBold.sfd") def deja_vu_sans_mono: Family = Family( plain = "DejaVuSansMono.ttf", bold = "DejaVuSansMono-Bold.ttf", italic = "DejaVuSansMono-Oblique.ttf", bold_italic = "DejaVuSansMono-BoldOblique.ttf") def deja_vu_sans: Family = Family( plain = "DejaVuSans.ttf", bold = "DejaVuSans-Bold.ttf", italic = "DejaVuSans-Oblique.ttf", bold_italic = "DejaVuSans-BoldOblique.ttf") def deja_vu_serif: Family = Family( plain = "DejaVuSerif.ttf", bold = "DejaVuSerif-Bold.ttf", italic = "DejaVuSerif-Italic.ttf", bold_italic = "DejaVuSerif-BoldItalic.ttf") def vacuous: Family = Family(plain = "Vacuous.sfd") } /* hinting */ // see https://www.freetype.org/ttfautohint/doc/ttfautohint.html private def auto_hint(source: Path, target: Path) { Isabelle_System.bash("ttfautohint -i " + File.bash_path(source) + " " + File.bash_path(target)).check } private def hinted_path(hinted: Boolean): Path = if (hinted) Path.basic("ttf-hinted") else Path.basic("ttf") private val hinting = List(false, true) /* build fonts */ private def find_file(dirs: List[Path], name: String): Path = { val path = Path.explode(name) dirs.collectFirst({ case dir if (dir + path).is_file => dir + path }) match { case Some(file) => file case None => error(cat_lines( ("Failed to find font file " + path + " in directories:") :: dirs.map(dir => " " + dir.toString))) } } val default_sources: List[Family] = List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif) val default_target_dir: Path = Path.explode("isabelle_fonts") def build_fonts( sources: List[Family] = default_sources, source_dirs: List[Path] = Nil, target_prefix: String = "Isabelle", target_version: String = "", target_dir: Path = default_target_dir, progress: Progress = new Progress) { progress.echo("Directory " + target_dir) hinting.foreach(hinted => Isabelle_System.make_directory(target_dir + hinted_path(hinted))) val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts")) for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir) // Isabelle fonts val targets = for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex } yield { val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index)) val source_file = find_file(font_dirs, source_font) val source_names = Fontforge.font_names(source_file) val target_names = source_names.update(prefix = target_prefix, version = target_version) Isabelle_System.with_tmp_file("font", "ttf")(tmp_file => { for (hinted <- hinting) { val target_file = target_dir + hinted_path(hinted) + target_names.ttf progress.echo("Font " + target_file.toString + " ...") if (hinted) auto_hint(source_file, tmp_file) else File.copy(source_file, tmp_file) Fontforge.execute( Fontforge.commands( Fontforge.open(isabelle_file), Fontforge.select(Range.isabelle_font), Fontforge.copy, Fontforge.close, Fontforge.open(tmp_file), Fontforge.select(Range.base_font), Fontforge.select_invert, Fontforge.clear, Fontforge.select(Range.isabelle_font), Fontforge.paste, target_names.set, Fontforge.generate(target_file), Fontforge.close) ).check } }) (target_names.ttf, index) } // Vacuous font { val vacuous_file = find_file(font_dirs, Family.vacuous.get(0)) val target_names = Fontforge.font_names(vacuous_file) val target_file = target_dir + hinted_path(false) + target_names.ttf progress.echo("Font " + target_file.toString + " ...") val domain = (for ((name, index) <- targets if index == 0) yield Fontforge.font_domain(target_dir + hinted_path(false) + name)) .flatten.distinct.sorted Fontforge.execute( Fontforge.commands( Fontforge.open(vacuous_file), Fontforge.select(Range.vacuous_font), Fontforge.copy) + domain.map(code => Fontforge.commands( Fontforge.select(Seq(code)), Fontforge.paste)) .mkString("\n", "\n", "\n") + Fontforge.commands( Fontforge.generate(target_file), Fontforge.close) ).check } // etc/settings - val settings_path = Components.settings(target_dir) - Isabelle_System.make_directory(settings_path.dir) + val settings_path = Isabelle_System.make_directory(Components.settings(target_dir)) def fonts_settings(hinted: Boolean): String = "\n isabelle_fonts \\\n" + (for ((target, _) <- targets) yield """ "$COMPONENT/""" + hinted_path(hinted).file_name + "/" + target.file_name + "\"") .mkString(" \\\n") File.write(settings_path, """# -*- shell-script -*- :mode=shellscript: if grep "isabelle_fonts_hinted.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null then""" + fonts_settings(false) + """ else""" + fonts_settings(true) + """ fi isabelle_fonts_hidden "$COMPONENT/""" + hinted_path(false).file_name + """/Vacuous.ttf" """) // README File.copy(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_fonts", "construct Isabelle fonts", args => { var source_dirs: List[Path] = Nil val getopts = Getopts(""" Usage: isabelle build_fonts [OPTIONS] Options are: -d DIR additional source directory Construct Isabelle fonts from DejaVu font families and Isabelle symbols. """, "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg)))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val target_version = Date.Format("uuuuMMdd")(Date.now()) val target_dir = Path.explode("isabelle_fonts-" + target_version) val progress = new Console_Progress build_fonts(source_dirs = source_dirs, target_dir = target_dir, target_version = target_version, progress = progress) }) } diff --git a/src/Pure/Admin/build_jdk.scala b/src/Pure/Admin/build_jdk.scala --- a/src/Pure/Admin/build_jdk.scala +++ b/src/Pure/Admin/build_jdk.scala @@ -1,240 +1,239 @@ /* Title: Pure/Admin/build_jdk.scala Author: Makarius Build Isabelle jdk component from original platform installations. */ package isabelle import java.io.{File => JFile} import java.nio.file.Files import java.nio.file.attribute.PosixFilePermission import scala.util.matching.Regex object Build_JDK { /* version */ def detect_version(s: String): String = { val Version_Dir_Entry = """^jdk-([0-9.]+\+\d+)$""".r s match { case Version_Dir_Entry(version) => version case _ => error("Cannot detect JDK version from " + quote(s)) } } /* platform */ sealed case class JDK_Platform(name: String, home: String, exe: String, regex: Regex) { override def toString: String = name def detect(jdk_dir: Path): Boolean = { val path = jdk_dir + Path.explode(exe) if (path.is_file) { val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out regex.pattern.matcher(file_descr).matches } else false } } val jdk_platforms = List( JDK_Platform("x86_64-linux", ".", "bin/java", """.*ELF 64-bit.*x86[-_]64.*""".r), JDK_Platform("x86_64-windows", ".", "bin/java.exe", """.*PE32\+ executable.*x86[-_]64.*""".r), JDK_Platform("x86_64-darwin", "Contents/Home", "Contents/Home/bin/java", """.*Mach-O 64-bit.*x86[-_]64.*""".r)) /* README */ def readme(version: String): String = """This is OpenJDK """ + version + """ as required for Isabelle. See https://adoptopenjdk.net for the original downloads, which are covered the GPL2 (with various liberal exceptions, see legal/*). Linux, Windows, Mac OS X all work uniformly, depending on certain platform-specific subdirectories. """ /* settings */ val settings = """# -*- shell-script -*- :mode=shellscript: case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; windows) ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; macos) ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM/Contents/Home" ;; esac """ /* extract archive */ private def suppress_name(name: String): Boolean = name.startsWith("._") def extract_archive(dir: Path, archive: Path): (String, JDK_Platform) = { try { - val tmp_dir = dir + Path.explode("tmp") - Isabelle_System.make_directory(tmp_dir) + val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp")) if (archive.get_ext == "zip") { Isabelle_System.bash( "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check } else { Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check } val dir_entry = File.read_dir(tmp_dir).filterNot(suppress_name) match { case List(s) => s case _ => error("Archive contains multiple directories") } val version = detect_version(dir_entry) val jdk_dir = tmp_dir + Path.explode(dir_entry) val platform = jdk_platforms.find(_.detect(jdk_dir)) getOrElse error("Failed to detect JDK platform") val platform_dir = dir + Path.explode(platform.name) if (platform_dir.is_dir) error("Directory already exists: " + platform_dir) File.link(Path.current, jdk_dir + Path.explode(platform.home) + Path.explode("jre")) File.move(jdk_dir, platform_dir) (version, platform) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) } } /* build jdk */ def build_jdk( archives: List[Path], progress: Progress = new Progress, target_dir: Path = Path.current) { if (Platform.is_windows) error("Cannot build jdk on Windows") Isabelle_System.with_tmp_dir("jdk")(dir => { progress.echo("Extracting ...") val extracted = archives.map(extract_archive(dir, _)) val version = extracted.map(_._1).distinct match { case List(version) => version case Nil => error("No archives") case versions => error("Archives contain multiple JDK versions: " + commas_quote(versions)) } val missing_platforms = jdk_platforms.filterNot(p1 => extracted.exists({ case (_, p2) => p1.name == p2.name })) if (missing_platforms.nonEmpty) error("Missing platforms: " + commas_quote(missing_platforms.map(_.name))) val jdk_name = "jdk-" + version val jdk_path = Path.explode(jdk_name) val component_dir = dir + jdk_path Isabelle_System.make_directory(component_dir + Path.explode("etc")) File.write(Components.settings(component_dir), settings) File.write(component_dir + Path.explode("README"), readme(version)) for ((_, platform) <- extracted) File.move(dir + Path.explode(platform.name), component_dir) for (file <- File.find_files(component_dir.file, include_dirs = true)) { val path = file.toPath val perms = Files.getPosixFilePermissions(path) perms.add(PosixFilePermission.OWNER_READ) perms.add(PosixFilePermission.GROUP_READ) perms.add(PosixFilePermission.OTHERS_READ) perms.add(PosixFilePermission.OWNER_WRITE) if (file.isDirectory) { perms.add(PosixFilePermission.OWNER_WRITE) perms.add(PosixFilePermission.OWNER_EXECUTE) perms.add(PosixFilePermission.GROUP_EXECUTE) perms.add(PosixFilePermission.OTHERS_EXECUTE) } Files.setPosixFilePermissions(path, perms) } File.find_files((component_dir + Path.explode("x86_64-darwin")).file, file => suppress_name(file.getName)).foreach(_.delete) progress.echo("Sharing ...") val main_dir :: other_dirs = jdk_platforms.map(platform => (component_dir + Path.explode(platform.name)).file.toPath) for { file1 <- File.find_files(main_dir.toFile).iterator path1 = file1.toPath dir2 <- other_dirs.iterator } { val path2 = dir2.resolve(main_dir.relativize(path1)) val file2 = path2.toFile if (!Files.isSymbolicLink(path2) && file2.isFile && File.eq_content(file1, file2)) { file2.delete Files.createLink(path2, path1) } } progress.echo("Archiving ...") Isabelle_System.gnutar( "-czf " + File.bash_path(target_dir + jdk_path.ext("tar.gz")) + " " + jdk_name, dir = dir).check }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives", args => { var target_dir = Path.current val getopts = Getopts(""" Usage: isabelle build_jdk [OPTIONS] ARCHIVES... Options are: -D DIR target directory (default ".") Build jdk component from tar.gz archives, with original jdk archives for x86_64 Linux, Windows, Mac OS X. """, "D:" -> (arg => target_dir = Path.explode(arg))) val more_args = getopts(args) if (more_args.isEmpty) getopts.usage() val archives = more_args.map(Path.explode) val progress = new Console_Progress() build_jdk(archives = archives, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_polyml.scala b/src/Pure/Admin/build_polyml.scala --- a/src/Pure/Admin/build_polyml.scala +++ b/src/Pure/Admin/build_polyml.scala @@ -1,322 +1,321 @@ /* Title: Pure/Admin/build_polyml.scala Author: Makarius Build Poly/ML from sources. */ package isabelle import scala.util.matching.Regex object Build_PolyML { /** platform-specific build **/ sealed case class Platform_Info( options: List[String] = Nil, setup: String = "", copy_files: List[String] = Nil, ldd_pattern: Option[(String, Regex)] = None) private val platform_info = Map( "linux" -> Platform_Info( options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"), ldd_pattern = Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))), "darwin" -> Platform_Info( options = List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include", "CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64", "LDFLAGS=-segprot POLY rwx rwx"), setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin", ldd_pattern = Some(("otool -L", """\s*(\S+lib(?:polyml|gmp).*dylib).*""".r))), "windows" -> Platform_Info( options = List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), setup = """PATH=/usr/bin:/bin:/mingw64/bin export CONFIG_SITE=/mingw64/etc/config.site""", copy_files = List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll", "$MSYS/mingw64/bin/libgmp-10.dll", "$MSYS/mingw64/bin/libstdc++-6.dll", "$MSYS/mingw64/bin/libwinpthread-1.dll"))) def build_polyml( root: Path, sha1_root: Option[Path] = None, progress: Progress = new Progress, arch_64: Boolean = false, options: List[String] = Nil, msys_root: Option[Path] = None) { if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) error("Bad Poly/ML root directory: " + root) val platform = Isabelle_Platform.self val platform_arch = if (arch_64) platform.arch_64 else if (platform.is_intel) "x86_64_32" else platform.arch_32 val polyml_platform = platform_arch + "-" + platform.os_name val sha1_platform = platform.arch_64 + "-" + platform.os_name val info = platform_info.getOrElse(platform.os_name, error("Bad OS platform: " + quote(platform.os_name))) val settings = msys_root match { case None if platform.is_windows => error("Windows requires specification of msys root directory") case None => Isabelle_System.settings() case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode) } if (platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) { error("""Missing "chrpath" executable on Linux""") } /* bash */ def bash( cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = { val script1 = msys_root match { case None => script case Some(msys) => File.bash_path(msys + Path.explode("usr/bin/bash")) + " -c " + Bash.string(script) } progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo) } /* configure and make */ val configure_options = List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") ::: info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit")) bash(root, info.setup + "\n" + """ [ -f Makefile ] && make distclean { ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """ rm -rf target make compiler && make compiler && make install } || { echo "Build failed" >&2; exit 2; } """, redirect = true, echo = true).check val ldd_files = { info.ldd_pattern match { case Some((ldd, pattern)) => val lines = bash(root, ldd + " target/bin/poly").check.out_lines for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib case None => Nil } } /* sha1 library */ val sha1_files = if (sha1_root.isDefined) { val dir1 = sha1_root.get bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check val dir2 = dir1 + Path.explode(sha1_platform) File.read_dir(dir2).map(entry => dir2.implode + "/" + entry) } else Nil /* target */ val target = Path.explode(polyml_platform) Isabelle_System.rm_tree(target) Isabelle_System.make_directory(target) for (file <- info.copy_files ::: ldd_files ::: sha1_files) File.copy(Path.explode(file).expand_env(settings), target) for { d <- List("target/bin", "target/lib") dir = root + Path.explode(d) entry <- File.read_dir(dir) } File.move(dir + Path.explode(entry), target) /* poly: library path */ if (platform.is_linux) { bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check } else if (platform.is_macos) { for (file <- ldd_files) { bash(target, """install_name_tool -change """ + Bash.string(file) + " " + Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check } } /* polyc: directory prefix */ { val polyc_path = target + Path.explode("polyc") val Header = "#! */bin/sh".r val polyc_patched = split_lines(File.read(polyc_path)) match { case Header() :: lines => val lines1 = lines.map(line => if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\"" else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\"" else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\"" else line) cat_lines("#!/usr/bin/env bash" ::lines1) case lines => error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3))) } File.write(polyc_path, polyc_patched) } } /** skeleton for component **/ private def extract_sources(source_archive: Path, component_dir: Path) = { if (source_archive.get_ext == "zip") { Isabelle_System.bash( "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check } else { Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check } val src_dir = component_dir + Path.explode("src") File.read_dir(component_dir) match { case List(s) => File.move(component_dir + Path.basic(s), src_dir) case _ => error("Source archive contains multiple directories") } val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML"))) val ml_files = for { line <- lines rest <- Library.try_unprefix("use", line) } yield "ML_file" + rest File.write(src_dir + Path.explode("ROOT.ML"), """(* Poly/ML Compiler root file. When this file is open in the Prover IDE, the ML files of the Poly/ML compiler can be explored interactively. This is a separate copy: it does not affect the running ML session. *) """ + ml_files.mkString("\n", "\n", "\n")) } def build_polyml_component( source_archive: Path, component_dir: Path, sha1_root: Option[Path] = None) { if (component_dir.is_file || component_dir.is_dir) error("Component directory already exists: " + component_dir) Isabelle_System.make_directory(component_dir) extract_sources(source_archive, component_dir) File.copy(Path.explode("~~/Admin/polyml/README"), component_dir) - val etc_dir = component_dir + Path.explode("etc") - Isabelle_System.make_directory(etc_dir) + val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc")) File.copy(Path.explode("~~/Admin/polyml/settings"), etc_dir) sha1_root match { case Some(dir) => Mercurial.repository(dir).archive(File.standard_path(component_dir + Path.explode("sha1"))) case None => } } /** Isabelle tool wrappers **/ val isabelle_tool1 = Isabelle_Tool("build_polyml", "build Poly/ML from sources", args => { var msys_root: Option[Path] = None var arch_64 = Isabelle_Platform.self.is_arm var sha1_root: Option[Path] = None val getopts = Getopts(""" Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] Options are: -M DIR msys root directory (for Windows) -m ARCH processor architecture (32 or 64, default: """ + (if (arch_64) "64" else "32") + """) -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 Build Poly/ML in the ROOT directory of its sources, with additional CONFIGURE_OPTIONS (e.g. --without-gmp). """, "M:" -> (arg => msys_root = Some(Path.explode(arg))), "m:" -> { case "32" => arch_64 = false case "64" => arch_64 = true case bad => error("Bad processor architecture: " + quote(bad)) }, "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) val more_args = getopts(args) val (root, options) = more_args match { case root :: options => (Path.explode(root), options) case Nil => getopts.usage() } build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress, arch_64 = arch_64, options = options, msys_root = msys_root) }) val isabelle_tool2 = Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args => { var sha1_root: Option[Path] = None val getopts = Getopts(""" Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR Options are: -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 Make skeleton for Poly/ML component, based on official source archive (zip or tar.gz). """, "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) val more_args = getopts(args) val (source_archive, component_dir) = more_args match { case List(archive, dir) => (Path.explode(archive), Path.explode(dir)) case _ => getopts.usage() } build_polyml_component(source_archive, component_dir, sha1_root = sha1_root) }) } diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala +++ b/src/Pure/Admin/build_release.scala @@ -1,847 +1,846 @@ /* Title: Pure/Admin/build_release.scala Author: Makarius Build full Isabelle distribution from repository. */ package isabelle object Build_Release { /** release info **/ sealed case class Bundle_Info( platform: Platform.Family.Value, platform_description: String, name: String) { def path: Path = Path.explode(name) } class Release private[Build_Release]( progress: Progress, val date: Date, val dist_name: String, val dist_dir: Path, val dist_version: String, val ident: String) { val isabelle_dir: Path = dist_dir + Path.explode(dist_name) val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") def other_isabelle(dir: Path): Other_Isabelle = Other_Isabelle(dir + Path.explode(dist_name), isabelle_identifier = dist_name + "-build", progress = progress) def bundle_info(platform: Platform.Family.Value): Bundle_Info = platform match { case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz") case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz") case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe") } } /** generated content **/ /* patch release */ private def change_file(dir: Path, name: String, f: String => String) { val file = dir + Path.explode(name) File.write(file, f(File.read(file))) } private val getsettings_file: String = "lib/scripts/getsettings" private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r def patch_release(release: Release, is_official: Boolean) { val dir = release.isabelle_dir for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala")) { change_file(dir, name, s => s.replaceAllLiterally("val is_identified = false", "val is_identified = true") .replaceAllLiterally("val is_official = false", "val is_official = " + is_official)) } change_file(dir, getsettings_file, s => s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident)) .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name))) change_file(dir, "lib/html/library_index_header.template", s => s.replaceAllLiterally("{ISABELLE}", release.dist_name)) for { name <- List( "src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala", "lib/Tools/version") } { change_file(dir, name, s => s.replaceAllLiterally("repository version", release.dist_version)) } change_file(dir, "README", s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version)) } /* ANNOUNCE */ def make_announce(release: Release) { File.write(release.isabelle_dir + Path.explode("ANNOUNCE"), """ IMPORTANT NOTE ============== This is a snapshot of Isabelle/""" + release.ident + """ from the repository. """) } /* NEWS */ def make_news(other_isabelle: Other_Isabelle, dist_version: String) { val target = other_isabelle.isabelle_home + Path.explode("doc") - val target_fonts = target + Path.explode("fonts") - Isabelle_System.make_directory(target_fonts) + val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts")) other_isabelle.copy_fonts(target_fonts) HTML.write_document(target, "NEWS.html", List(HTML.title("NEWS (" + dist_version + ")")), List( HTML.chapter("NEWS"), HTML.source( Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS")))))) } /* bundled components */ class Bundled(platform: Option[Platform.Family.Value] = None) { def detect(s: String): Boolean = s.startsWith("#bundled") && !s.startsWith("#bundled ") def apply(name: String): String = "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name private val Pattern1 = ("""^#bundled:(.*)$""").r private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r def unapply(s: String): Option[String] = s match { case Pattern1(name) => Some(name) case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name) case _ => None } } def record_bundled_components(dir: Path) { val catalogs = List("main", "bundled").map((_, new Bundled())) ::: default_platform_families.flatMap(platform => List(platform.toString, "bundled-" + platform.toString). map((_, new Bundled(platform = Some(platform))))) File.append(Components.components(dir), terminate_lines("#bundled components" :: (for { (catalog, bundled) <- catalogs.iterator path = Components.admin(dir) + Path.basic(catalog) if path.is_file line <- split_lines(File.read(path)) if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build") } yield bundled(line)).toList)) } def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = { val Bundled = new Bundled(platform = Some(platform)) val components = for { Bundled(name) <- Components.read_components(dir) if !name.startsWith("jedit_build") } yield name val jdk_component = components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") (components, jdk_component) } def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String]) { def contrib_name(name: String): String = Components.contrib(name = name).implode val Bundled = new Bundled(platform = Some(platform)) Components.write_components(dir, Components.read_components(dir).flatMap(line => line match { case Bundled(name) => if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) else None case _ => if (Bundled.detect(line)) None else Some(line) }) ::: more_names.map(contrib_name)) } def make_contrib(dir: Path) { Isabelle_System.make_directory(Components.contrib(dir)) File.write(Components.contrib(dir, "README"), """This directory contains add-on components that contribute to the main Isabelle distribution. Separate licensing conditions apply, see each directory individually. """) } /** build release **/ private def execute(dir: Path, script: String): Unit = Isabelle_System.bash(script, cwd = dir.file).check private def execute_tar(dir: Path, args: String): Unit = Isabelle_System.gnutar(args, dir = dir).check /* build heaps on remote server */ private def remote_build_heaps( options: Options, platform: Platform.Family.Value, build_sessions: List[String], local_dir: Path) { val server_option = "build_host_" + platform.toString options.string(server_option) match { case SSH.Target(user, host) => using(SSH.open_session(options, host = host, user = user))(ssh => { Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar => { execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") ssh.with_tmp_dir(remote_dir => { val remote_tmp_tar = remote_dir + Path.basic("tmp.tar") ssh.write_file(remote_tmp_tar, local_tmp_tar) val remote_commands = List( "cd " + File.bash_path(remote_dir), "tar -xf tmp.tar", "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions), "tar -cf tmp.tar heaps") ssh.execute(remote_commands.mkString(" && ")).check ssh.read_file(remote_tmp_tar, local_tmp_tar) }) execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar)) }) }) case s => error("Bad " + server_option + ": " + quote(s)) } } /* main */ private val default_platform_families: List[Platform.Family.Value] = List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos) def build_release(base_dir: Path, options: Options, components_base: Path = Components.default_components_base, progress: Progress = new Progress, rev: String = "", afp_rev: String = "", official_release: Boolean = false, proper_release_name: Option[String] = None, platform_families: List[Platform.Family.Value] = default_platform_families, more_components: List[Path] = Nil, website: Option[Path] = None, build_sessions: List[String] = Nil, build_library: Boolean = false, parallel_jobs: Int = 1): Release = { val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) val release = { val date = Date.now() val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date)) val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute val version = proper_string(rev) orElse proper_release_name getOrElse "tip" val ident = try { hg.id(version) } catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) } val dist_version = proper_release_name match { case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date) case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date) } new Release(progress, date, dist_name, dist_dir, dist_version, ident) } /* make distribution */ if (release.isabelle_archive.is_file) { progress.echo_warning("Release archive already exists: " + release.isabelle_archive) val archive_ident = Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val getsettings = Path.explode(release.dist_name + "/" + getsettings_file) execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings)) split_lines(File.read(tmp_dir + getsettings)) .collectFirst({ case ISABELLE_ID(ident) => ident }) .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive)) }) if (release.ident != archive_ident) { error("Mismatch of release identification " + release.ident + " vs. archive " + archive_ident) } } else { progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...") Isabelle_System.make_directory(release.dist_dir) if (release.isabelle_dir.is_dir) error("Directory " + release.isabelle_dir + " already exists") progress.echo_warning("Retrieving Mercurial repository version " + release.ident) hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files") for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { (release.isabelle_dir + Path.explode(name)).file.delete } progress.echo_warning("Preparing distribution " + quote(release.dist_name)) patch_release(release, proper_release_name.isDefined && official_release) if (proper_release_name.isEmpty) make_announce(release) make_contrib(release.isabelle_dir) execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""") record_bundled_components(release.isabelle_dir) /* build tools and documentation */ val other_isabelle = release.other_isabelle(release.dist_dir) other_isabelle.init_settings( other_isabelle.init_components(components_base = components_base, catalogs = List("main"))) other_isabelle.resolve_components(echo = true) try { val export_classpath = "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) } try { other_isabelle.bash( "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) } make_news(other_isabelle, release.dist_version) for (name <- List("Admin", "browser_info", "heaps")) { Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) } other_isabelle.cleanup() progress.echo_warning("Creating distribution archive " + release.isabelle_archive) def execute_dist_name(script: String): Unit = Isabelle_System.bash(script, cwd = release.dist_dir.file, env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check execute_dist_name(""" set -e chmod -R a+r "$DIST_NAME" chmod -R u+w "$DIST_NAME" chmod -R g=o "$DIST_NAME" find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w """) execute_tar(release.dist_dir, "-czf " + File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name)) execute_dist_name(""" set -e mv "$DIST_NAME" "${DIST_NAME}-old" mkdir "$DIST_NAME" mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \ "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME" mkdir "$DIST_NAME/doc" mv "${DIST_NAME}-old/doc/"*.pdf \ "${DIST_NAME}-old/doc/"*.html \ "${DIST_NAME}-old/doc/"*.css \ "${DIST_NAME}-old/doc/fonts" \ "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc" rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle rm -rf "${DIST_NAME}-old" """) } /* make application bundles */ val bundle_infos = platform_families.map(release.bundle_info) for (bundle_info <- bundle_infos) { val isabelle_name = release.dist_name val platform = bundle_info.platform progress.echo("\nApplication bundle for " + platform) Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { // release archive execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive)) val other_isabelle = release.other_isabelle(tmp_dir) val isabelle_target = other_isabelle.isabelle_home // bundled components progress.echo("Bundled components:") val contrib_dir = Components.contrib(isabelle_target) val (bundled_components, jdk_component) = get_bundled_components(isabelle_target, platform) Components.resolve(components_base, bundled_components, target_dir = Some(contrib_dir), copy_dir = Some(release.dist_dir + Path.explode("contrib")), progress = progress) val more_components_names = more_components.map(Components.unpack(contrib_dir, _, progress = progress)) Components.purge(contrib_dir, platform) activate_components(isabelle_target, platform, more_components_names) // Java parameters val java_options_title = "# Java runtime options" val java_options: List[String] = (for { variable <- List( "ISABELLE_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_OPTIONS") opt <- Word.explode(other_isabelle.getenv(variable)) } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name) val classpath: List[Path] = { val base = isabelle_target.absolute Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path => { val abs_path = path.absolute File.relative_path(base, abs_path) match { case Some(rel_path) => rel_path case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path) } }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar")) } val jedit_options = Path.explode("src/Tools/jEdit/etc/options") val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props") // build heaps if (build_sessions.nonEmpty) { progress.echo("Building heaps ...") remote_build_heaps(options, platform, build_sessions, isabelle_target) } // application bundling platform match { case Platform.Family.linux => File.write(isabelle_target + jedit_options, File.read(isabelle_target + jedit_options) .replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24")) File.write(isabelle_target + jedit_props, File.read(isabelle_target + jedit_props) .replaceAll("console.fontsize=.*", "console.fontsize=18") .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18") .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18") .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18") .replaceAll("view.fontsize=.*", "view.fontsize=24") .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16")) File.write(isabelle_target + Path.explode("Isabelle.options"), terminate_lines(java_options_title :: java_options)) val isabelle_app = isabelle_target + Path.explode("lib/scripts/Isabelle_app") File.write(isabelle_app, File.read(Path.explode("~~/Admin/Linux/Isabelle_app")) .replaceAllLiterally("{CLASSPATH}", classpath.map("$ISABELLE_HOME/" + _).mkString(":")) .replaceAllLiterally("/jdk/", "/" + jdk_component + "/")) File.set_executable(isabelle_app, true) val linux_app = isabelle_target + Path.explode("contrib/linux_app") File.move(linux_app + Path.explode("Isabelle"), isabelle_target + Path.explode(isabelle_name)) Isabelle_System.rm_tree(linux_app) val archive_name = isabelle_name + "_linux.tar.gz" progress.echo("Packaging " + archive_name + " ...") execute_tar(tmp_dir, "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + Bash.string(isabelle_name)) case Platform.Family.macos => File.write(isabelle_target + jedit_props, File.read(isabelle_target + jedit_props) .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel") .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")) // MacOS application bundle File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir) val isabelle_app = Path.explode(isabelle_name + ".app") val app_dir = tmp_dir + isabelle_app File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir) val app_contents = app_dir + Path.explode("Contents") val app_resources = app_contents + Path.explode("Resources") File.move(tmp_dir + Path.explode(isabelle_name), app_resources) File.write(app_contents + Path.explode("Info.plist"), File.read(Path.explode("~~/Admin/MacOS/Info.plist")) .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) .replaceAllLiterally("{JAVA_OPTIONS}", terminate_lines(java_options.map(opt => "" + opt + "")))) for (cp <- classpath) { File.link( Path.explode("../Resources/" + isabelle_name + "/") + cp, app_contents + Path.explode("Java"), force = true) } File.link( Path.explode("../Resources/" + isabelle_name + "/contrib/" + jdk_component + "/x86_64-darwin"), app_contents + Path.explode("PlugIns/bundled.jdk"), force = true) File.link( Path.explode("../../Info.plist"), app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"), force = true) File.link( Path.explode("Contents/Resources/" + isabelle_name), app_dir + Path.explode("Isabelle"), force = true) // application archive val archive_name = isabelle_name + "_macos.tar.gz" progress.echo("Packaging " + archive_name + " ...") execute_tar(tmp_dir, "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + File.bash_path(isabelle_app)) case Platform.Family.windows => File.write(isabelle_target + jedit_props, File.read(isabelle_target + jedit_props) .replaceAll("lookAndFeel=.*", "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel") .replaceAll("foldPainter=.*", "foldPainter=Square")) // application launcher File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) val app_template = Path.explode("~~/Admin/Windows/launch4j") File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), (java_options_title :: java_options).map(_ + "\r\n").mkString) val isabelle_xml = Path.explode("isabelle.xml") val isabelle_exe = Path.explode(isabelle_name + ".exe") File.write(tmp_dir + isabelle_xml, File.read(app_template + isabelle_xml) .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) .replaceAllLiterally("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe)) .replaceAllLiterally("{ICON}", File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) .replaceAllLiterally("{SPLASH}", File.platform_path(app_template + Path.explode("isabelle.bmp"))) .replaceAllLiterally("{CLASSPATH}", cat_lines(classpath.map(cp => " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + ""))) .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\")) execute(tmp_dir, "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml") File.copy(app_template + Path.explode("manifest.xml"), isabelle_target + isabelle_exe.ext("manifest")) // Cygwin setup val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target) val cygwin_mirror = File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror")) val cygwin_bat = Path.explode("Cygwin-Setup.bat") File.write(isabelle_target + cygwin_bat, File.read(cygwin_template + cygwin_bat) .replaceAllLiterally("{MIRROR}", cygwin_mirror)) File.set_executable(isabelle_target + cygwin_bat, true) for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) { val path = Path.explode(name) File.copy(cygwin_template + path, isabelle_target + Path.explode("contrib/cygwin") + path) } execute(isabelle_target, """find . -type f -not -name "*.exe" -not -name "*.dll" """ + (if (Platform.is_macos) "-perm +100" else "-executable") + " -print0 > contrib/cygwin/isabelle/executables") execute(isabelle_target, """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ + """> contrib/cygwin/isabelle/symlinks""") execute(isabelle_target, """find . -type l -exec rm "{}" ";" """) File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") // executable archive (self-extracting 7z) val archive_name = isabelle_name + ".7z" val exe_archive = tmp_dir + Path.explode(archive_name) exe_archive.file.delete progress.echo("Packaging " + archive_name + " ...") execute(tmp_dir, "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name)) if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive) val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx") val sfx_txt = File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")). replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) Bytes.write(release.dist_dir + isabelle_exe, Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive)) File.set_executable(release.dist_dir + isabelle_exe, true) } }) progress.echo("DONE") } /* minimal website */ for (dir <- website) { val website_platform_bundles = for { bundle_info <- bundle_infos if (release.dist_dir + bundle_info.path).is_file } yield (bundle_info.name, bundle_info) val isabelle_link = HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident, HTML.text("Isabelle/" + release.ident)) val afp_link = HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", List(HTML.title(release.dist_name)), List( HTML.section(release.dist_name), HTML.subsection("Platforms"), HTML.itemize( website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })), HTML.subsection("Repositories"), HTML.itemize( List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link)))))) for ((bundle, _) <- website_platform_bundles) File.copy(release.dist_dir + Path.explode(bundle), dir) } /* HTML library */ if (build_library) { if (release.isabelle_library_archive.is_file) { progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive) } else { Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val bundle = release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz") execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) val other_isabelle = release.other_isabelle(tmp_dir) Isabelle_System.make_directory(other_isabelle.etc) File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name)) execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name)) execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) + " " + Bash.string(release.dist_name + "/browser_info")) }) } } release } /** command line entry point **/ def main(args: Array[String]) { Command_Line.tool { var afp_rev = "" var components_base: Path = Components.default_components_base var official_release = false var proper_release_name: Option[String] = None var website: Option[Path] = None var build_sessions: List[String] = Nil var more_components: List[Path] = Nil var parallel_jobs = 1 var build_library = false var options = Options.init() var platform_families = default_platform_families var rev = "" val getopts = Getopts(""" Usage: Admin/build_release [OPTIONS] BASE_DIR Options are: -A REV corresponding AFP changeset id -C DIR base directory for Isabelle components (default: """ + Components.default_components_base + """) -O official release (not release-candidate) -R RELEASE proper release with name -W WEBSITE produce minimal website in given directory -b SESSIONS build platform-specific session images (separated by commas) -c ARCHIVE clean bundling with additional component .tar.gz archive -j INT maximum number of parallel jobs (default 1) -l build library -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) -r REV Mercurial changeset id (default: RELEASE or tip) Build Isabelle release in base directory, using the local repository clone. """, "A:" -> (arg => afp_rev = arg), "C:" -> (arg => components_base = Path.explode(arg)), "O" -> (_ => official_release = true), "R:" -> (arg => proper_release_name = Some(arg)), "W:" -> (arg => website = Some(Path.explode(arg))), "b:" -> (arg => build_sessions = space_explode(',', arg)), "c:" -> (arg => { val path = Path.explode(arg) Components.Archive.get_name(path.file_name) more_components = more_components ::: List(path) }), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), "r:" -> (arg => rev = arg)) val more_args = getopts(args) val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } val progress = new Console_Progress() if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) error("Building for windows requires 7z") build_release(Path.explode(base_dir), options, components_base = components_base, progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release, proper_release_name = proper_release_name, website = website, platform_families = if (platform_families.isEmpty) default_platform_families else platform_families, more_components = more_components, build_sessions = build_sessions, build_library = build_library, parallel_jobs = parallel_jobs) } } } diff --git a/src/Pure/Admin/build_sqlite.scala b/src/Pure/Admin/build_sqlite.scala --- a/src/Pure/Admin/build_sqlite.scala +++ b/src/Pure/Admin/build_sqlite.scala @@ -1,119 +1,117 @@ /* Title: Pure/Admin/build_sqlite.scala Author: Makarius Build Isabelle sqlite-jdbc component from official download. */ package isabelle object Build_SQLite { /* build sqlite */ def build_sqlite( download_url: String, progress: Progress = new Progress, target_dir: Path = Path.current) { val Download_Name = """^.*/([^/]+)\.jar""".r val download_name = download_url match { case Download_Name(download_name) => download_name case _ => error("Malformed jar download URL: " + quote(download_url)) } /* component */ val component_dir = target_dir + Path.basic(download_name) if (component_dir.is_dir) error("Component directory already exists: " + component_dir) else { progress.echo("Component " + component_dir) Isabelle_System.make_directory(component_dir) } /* README */ File.write(component_dir + Path.basic("README"), "This is " + download_name + " from\n" + download_url + "\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n") /* settings */ - val etc_dir = component_dir + Path.basic("etc") - Isabelle_System.make_directory(etc_dir) + val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) File.write(etc_dir + Path.basic("settings"), """# -*- shell-script -*- :mode=shellscript: ISABELLE_SQLITE_HOME="$COMPONENT" classpath "$ISABELLE_SQLITE_HOME/""" + download_name + """.jar" """) /* jar */ val jar = component_dir + Path.basic(download_name).ext("jar") Isabelle_System.download(download_url, jar, progress = progress) Isabelle_System.with_tmp_dir("sqlite")(jar_dir => { progress.echo("Unpacking " + jar) Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute), cwd = jar_dir.file).check val jar_files = List( "META-INF/maven/org.xerial/sqlite-jdbc/LICENSE" -> ".", "META-INF/maven/org.xerial/sqlite-jdbc/LICENSE.zentus" -> ".", "org/sqlite/native/Linux/aarch64/libsqlitejdbc.so" -> "arm64-linux", "org/sqlite/native/Linux/x86_64/libsqlitejdbc.so" -> "x86_64-linux", "org/sqlite/native/Mac/x86_64/libsqlitejdbc.jnilib" -> "x86_64-darwin", "org/sqlite/native/Windows/x86_64/sqlitejdbc.dll" -> "x86_64-windows") for ((file, dir) <- jar_files) { - val target = component_dir + Path.explode(dir) - Isabelle_System.make_directory(target) + val target = Isabelle_System.make_directory(component_dir + Path.explode(dir)) File.copy(jar_dir + Path.explode(file), target) } File.set_executable(component_dir + Path.explode("x86_64-windows/sqlitejdbc.dll"), true) }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_sqlite", "build Isabelle sqlite-jdbc component from official download", args => { var target_dir = Path.current val getopts = Getopts(""" Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD Options are: -D DIR target directory (default ".") Build sqlite-jdbc component from the specified download URL (JAR), see also https://github.com/xerial/sqlite-jdbc/releases """, "D:" -> (arg => target_dir = Path.explode(arg))) val more_args = getopts(args) val download_url = more_args match { case List(download_url) => download_url case _ => getopts.usage() } val progress = new Console_Progress() build_sqlite(download_url, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_status.scala b/src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala +++ b/src/Pure/Admin/build_status.scala @@ -1,622 +1,621 @@ /* Title: Pure/Admin/build_status.scala Author: Makarius Present recent build status information from database. */ package isabelle object Build_Status { /* defaults */ val default_target_dir = Path.explode("build_status") val default_image_size = (800, 600) val default_history = 30 def default_profiles: List[Profile] = Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles /* data profiles */ sealed case class Profile( description: String, history: Int = 0, afp: Boolean = false, bulky: Boolean = false, sql: String) { def days(options: Options): Int = options.int("build_log_history") max history def stretch(options: Options): Double = (days(options) max default_history min (default_history * 5)).toDouble / default_history def select(options: Options, columns: List[SQL.Column], only_sessions: Set[String]): SQL.Source = { Build_Log.Data.universal_table.select(columns, distinct = true, sql = "WHERE " + Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) + " AND " + SQL.member(Build_Log.Data.status.ident, List( Build_Log.Session_Status.finished.toString, Build_Log.Session_Status.failed.toString)) + (if (only_sessions.isEmpty) "" else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) + " AND " + SQL.enclose(sql)) } } /* build status */ def build_status(options: Options, progress: Progress = new Progress, profiles: List[Profile] = default_profiles, only_sessions: Set[String] = Set.empty, verbose: Boolean = false, target_dir: Path = default_target_dir, ml_statistics: Boolean = false, image_size: (Int, Int) = default_image_size) { val ml_statistics_domain = Iterator(ML_Statistics.heap_fields, ML_Statistics.program_fields, ML_Statistics.tasks_fields, ML_Statistics.workers_fields).flatMap(_._2).toSet val data = read_data(options, progress = progress, profiles = profiles, only_sessions = only_sessions, verbose = verbose, ml_statistics = ml_statistics, ml_statistics_domain = ml_statistics_domain) present_data(data, progress = progress, target_dir = target_dir, image_size = image_size) } /* read data */ sealed case class Data(date: Date, entries: List[Data_Entry]) sealed case class Data_Entry( name: String, hosts: List[String], stretch: Double, sessions: List[Session]) { def failed_sessions: List[Session] = sessions.filter(_.head.failed).sortBy(_.name) } sealed case class Session( name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics, ml_statistics_date: Long) { require(entries.nonEmpty) lazy val sorted_entries: List[Entry] = entries.sortBy(entry => - entry.date) def head: Entry = sorted_entries.head def order: Long = - head.timing.elapsed.ms def finished_entries: List[Entry] = sorted_entries.filter(_.finished) def finished_entries_size: Int = finished_entries.map(_.date).toSet.size def check_timing: Boolean = finished_entries_size >= 3 def check_heap: Boolean = finished_entries_size >= 3 && finished_entries.forall(entry => entry.maximum_heap > 0 || entry.average_heap > 0 || entry.stored_heap > 0) def make_csv: CSV.File = { val header = List("session_name", "chapter", "pull_date", "afp_pull_date", "isabelle_version", "afp_version", "timing_elapsed", "timing_cpu", "timing_gc", "ml_timing_elapsed", "ml_timing_cpu", "ml_timing_gc", "maximum_code", "average_code", "maximum_stack", "average_stack", "maximum_heap", "average_heap", "stored_heap", "status") val date_format = Date.Format("uuuu-MM-dd HH:mm:ss") val records = for (entry <- sorted_entries) yield { CSV.Record(name, entry.chapter, date_format(entry.pull_date), entry.afp_pull_date match { case Some(date) => date_format(date) case None => "" }, entry.isabelle_version, entry.afp_version, entry.timing.elapsed.ms, entry.timing.cpu.ms, entry.timing.gc.ms, entry.ml_timing.elapsed.ms, entry.ml_timing.cpu.ms, entry.ml_timing.gc.ms, entry.maximum_code, entry.average_code, entry.maximum_stack, entry.average_stack, entry.maximum_heap, entry.average_heap, entry.stored_heap, entry.status) } CSV.File(name, header, records) } } sealed case class Entry( chapter: String, pull_date: Date, afp_pull_date: Option[Date], isabelle_version: String, afp_version: String, timing: Timing, ml_timing: Timing, maximum_code: Long, average_code: Long, maximum_stack: Long, average_stack: Long, maximum_heap: Long, average_heap: Long, stored_heap: Long, status: Build_Log.Session_Status.Value, errors: List[String]) { val date: Long = (afp_pull_date getOrElse pull_date).unix_epoch def finished: Boolean = status == Build_Log.Session_Status.finished def failed: Boolean = status == Build_Log.Session_Status.failed def present_errors(name: String): XML.Body = { if (errors.isEmpty) HTML.text(name + print_version(isabelle_version, afp_version, chapter)) else { HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) :: HTML.text(print_version(isabelle_version, afp_version, chapter)) } } } sealed case class Image(name: String, width: Int, height: Int) { def path: Path = Path.basic(name) } def print_version( isabelle_version: String, afp_version: String = "", chapter: String = AFP.chapter): String = { val body = proper_string(isabelle_version).map("Isabelle/" + _).toList ::: (if (chapter == AFP.chapter) proper_string(afp_version).map("AFP/" + _) else None).toList if (body.isEmpty) "" else body.mkString(" (", ", ", ")") } def read_data(options: Options, progress: Progress = new Progress, profiles: List[Profile] = default_profiles, only_sessions: Set[String] = Set.empty, ml_statistics: Boolean = false, ml_statistics_domain: String => Boolean = (key: String) => true, verbose: Boolean = false): Data = { val date = Date.now() var data_hosts = Map.empty[String, Set[String]] var data_stretch = Map.empty[String, Double] var data_entries = Map.empty[String, Map[String, Session]] def get_hosts(data_name: String): Set[String] = data_hosts.getOrElse(data_name, Set.empty) val store = Build_Log.store(options) using(store.open_database())(db => { for (profile <- profiles.sortBy(_.description)) { progress.echo("input " + quote(profile.description)) val afp = profile.afp val columns = List( Build_Log.Data.pull_date(afp = false), Build_Log.Data.pull_date(afp = true), Build_Log.Prop.build_host, Build_Log.Prop.isabelle_version, Build_Log.Prop.afp_version, Build_Log.Settings.ISABELLE_BUILD_OPTIONS, Build_Log.Settings.ML_PLATFORM, Build_Log.Data.session_name, Build_Log.Data.chapter, Build_Log.Data.groups, Build_Log.Data.threads, Build_Log.Data.timing_elapsed, Build_Log.Data.timing_cpu, Build_Log.Data.timing_gc, Build_Log.Data.ml_timing_elapsed, Build_Log.Data.ml_timing_cpu, Build_Log.Data.ml_timing_gc, Build_Log.Data.heap_size, Build_Log.Data.status, Build_Log.Data.errors) ::: (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil) val Threads_Option = """threads\s*=\s*(\d+)""".r val sql = profile.select(options, columns, only_sessions) progress.echo_if(verbose, sql) db.using_statement(sql)(stmt => { val res = stmt.execute_query() while (res.next()) { val session_name = res.string(Build_Log.Data.session_name) val chapter = res.string(Build_Log.Data.chapter) val groups = split_lines(res.string(Build_Log.Data.groups)) val threads = { val threads1 = res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { case Threads_Option(Value.Int(i)) => i case _ => 1 } val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1) threads1 max threads2 } val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) val data_name = profile.description + (if (ml_platform.startsWith("x86_64-")) ", 64bit" else "") + (if (threads == 1) "" else ", " + threads + " threads") res.get_string(Build_Log.Prop.build_host).foreach(host => data_hosts += (data_name -> (get_hosts(data_name) + host))) data_stretch += (data_name -> profile.stretch(options)) val isabelle_version = res.string(Build_Log.Prop.isabelle_version) val afp_version = res.string(Build_Log.Prop.afp_version) val ml_stats = ML_Statistics( if (ml_statistics) { Properties.uncompress( res.bytes(Build_Log.Data.ml_statistics), cache = store.xz_cache) } else Nil, domain = ml_statistics_domain, heading = session_name + print_version(isabelle_version, afp_version, chapter)) val entry = Entry( chapter = chapter, pull_date = res.date(Build_Log.Data.pull_date(afp = false)), afp_pull_date = if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None, isabelle_version = isabelle_version, afp_version = afp_version, timing = res.timing( Build_Log.Data.timing_elapsed, Build_Log.Data.timing_cpu, Build_Log.Data.timing_gc), ml_timing = res.timing( Build_Log.Data.ml_timing_elapsed, Build_Log.Data.ml_timing_cpu, Build_Log.Data.ml_timing_gc), maximum_code = ml_stats.maximum(ML_Statistics.CODE_SIZE).toLong, average_code = ml_stats.average(ML_Statistics.CODE_SIZE).toLong, maximum_stack = ml_stats.maximum(ML_Statistics.STACK_SIZE).toLong, average_stack = ml_stats.average(ML_Statistics.STACK_SIZE).toLong, maximum_heap = ml_stats.maximum(ML_Statistics.HEAP_SIZE).toLong, average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong, stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)), status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)), errors = Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors), cache = store.xz_cache)) val sessions = data_entries.getOrElse(data_name, Map.empty) val session = sessions.get(session_name) match { case None => Session(session_name, threads, List(entry), ml_stats, entry.date) case Some(old) => val (ml_stats1, ml_stats1_date) = if (entry.date > old.ml_statistics_date) (ml_stats, entry.date) else (old.ml_statistics, old.ml_statistics_date) Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date) } if ((!afp || chapter == AFP.chapter) && (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) { data_entries += (data_name -> (sessions + (session_name -> session))) } } }) } }) val sorted_entries = (for { (name, sessions) <- data_entries.toList sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order)) } yield { val hosts = get_hosts(name).toList.sorted val stretch = data_stretch(name) Data_Entry(name, hosts, stretch, sorted_sessions) }).sortBy(_.name) Data(date, sorted_entries) } /* present data */ def present_data(data: Data, progress: Progress = new Progress, target_dir: Path = default_target_dir, image_size: (Int, Int) = default_image_size) { def clean_name(name: String): String = name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString) HTML.write_document(target_dir, "index.html", List(HTML.title("Isabelle build status")), List(HTML.chapter("Isabelle build status"), HTML.par( List(HTML.description( List(HTML.text("status date:") -> HTML.text(data.date.toString))))), HTML.par( List(HTML.itemize(data.entries.map({ case data_entry => List( HTML.link(clean_name(data_entry.name) + "/index.html", HTML.text(data_entry.name))) ::: (data_entry.failed_sessions match { case Nil => Nil case sessions => HTML.break ::: List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) ::: List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name)))) }) })))))) for (data_entry <- data.entries) { val data_name = data_entry.name val (image_width, image_height) = image_size val image_width_stretch = (image_width * data_entry.stretch).toInt progress.echo("output " + quote(data_name)) - val dir = target_dir + Path.basic(clean_name(data_name)) - Isabelle_System.make_directory(dir) + val dir = Isabelle_System.make_directory(target_dir + Path.basic(clean_name(data_name))) val data_files = (for (session <- data_entry.sessions) yield { val csv_file = session.make_csv csv_file.write(dir) session.name -> csv_file }).toMap val session_plots = Par_List.map((session: Session) => Isabelle_System.with_tmp_file(session.name, "data") { data_file => Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file => def plot_name(kind: String): String = session.name + "_" + kind + ".png" File.write(data_file, cat_lines( session.finished_entries.map(entry => List(entry.date, entry.timing.elapsed.minutes, entry.timing.resources.minutes, entry.ml_timing.elapsed.minutes, entry.ml_timing.resources.minutes, entry.maximum_code, entry.maximum_code, entry.average_stack, entry.maximum_stack, entry.average_heap, entry.average_heap, entry.stored_heap).mkString(" ")))) val max_time = ((0.0 /: session.finished_entries){ case (m, entry) => m.max(entry.timing.elapsed.minutes). max(entry.timing.resources.minutes). max(entry.ml_timing.elapsed.minutes). max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1 val timing_range = "[0:" + max_time + "]" def gnuplot(plot_name: String, plots: List[String], range: String): Image = { val image = Image(plot_name, image_width_stretch, image_height) File.write(gnuplot_file, """ set terminal png size """ + image.width + "," + image.height + """ set output """ + quote(File.standard_path(dir + image.path)) + """ set xdata time set timefmt "%s" set format x "%d-%b" set xlabel """ + quote(session.name) + """ noenhanced set key left bottom plot [] """ + range + " " + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n") val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file)) if (!result.ok) result.error("Gnuplot failed for " + data_name + "/" + plot_name).check image } val timing_plots = { val plots1 = List( """ using 1:2 smooth sbezier title "elapsed time (smooth)" """, """ using 1:2 smooth csplines title "elapsed time" """) val plots2 = List( """ using 1:3 smooth sbezier title "cpu time (smooth)" """, """ using 1:3 smooth csplines title "cpu time" """) if (session.threads == 1) plots1 else plots1 ::: plots2 } val ml_timing_plots = List( """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """, """ using 1:4 smooth csplines title "ML elapsed time" """, """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """, """ using 1:5 smooth csplines title "ML cpu time" """) val heap_plots = List( """ using 1:10 smooth sbezier title "heap maximum (smooth)" """, """ using 1:10 smooth csplines title "heap maximum" """, """ using 1:11 smooth sbezier title "heap average (smooth)" """, """ using 1:11 smooth csplines title "heap average" """, """ using 1:12 smooth sbezier title "heap stored (smooth)" """, """ using 1:12 smooth csplines title "heap stored" """) def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image = { val image = Image(plot_name, image_width, image_height) val chart = session.ml_statistics.chart( fields._1 + ": " + session.ml_statistics.heading, fields._2) Graphics_File.write_chart_png( (dir + image.path).file, chart, image.width, image.height) image } val images = (if (session.check_timing) List( gnuplot(plot_name("timing"), timing_plots, timing_range), gnuplot(plot_name("ml_timing"), ml_timing_plots, timing_range)) else Nil) ::: (if (session.check_heap) List(gnuplot(plot_name("heap"), heap_plots, "[0:]")) else Nil) ::: (if (session.ml_statistics.content.nonEmpty) List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields), jfreechart(plot_name("program_chart"), ML_Statistics.program_fields)) ::: (if (session.threads > 1) List( jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields), jfreechart(plot_name("workers_chart"), ML_Statistics.workers_fields)) else Nil) else Nil) session.name -> images } }, data_entry.sessions).toMap HTML.write_document(dir, "index.html", List(HTML.title("Isabelle build status for " + data_name)), HTML.chapter("Isabelle build status for " + data_name) :: HTML.par( List(HTML.description( List( HTML.text("status date:") -> HTML.text(data.date.toString), HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) :: HTML.par( List(HTML.itemize( data_entry.sessions.map(session => HTML.link("#session_" + session.name, HTML.text(session.name)) :: HTML.text(" (" + session.head.timing.message_resources + ")"))))) :: data_entry.sessions.flatMap(session => List( HTML.section(HTML.id("session_" + session.name), session.name), HTML.par( HTML.description( List( HTML.text("data:") -> List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))), HTML.text("timing:") -> HTML.text(session.head.timing.message_resources), HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) ::: ML_Statistics.mem_print(session.head.maximum_code).map(s => HTML.text("code maximum:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.average_code).map(s => HTML.text("code average:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.maximum_stack).map(s => HTML.text("stack maximum:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.average_stack).map(s => HTML.text("stack average:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.maximum_heap).map(s => HTML.text("heap maximum:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.average_heap).map(s => HTML.text("heap average:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.stored_heap).map(s => HTML.text("heap stored:") -> HTML.text(s)).toList ::: proper_string(session.head.isabelle_version).map(s => HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: proper_string(session.head.afp_version).map(s => HTML.text("AFP version:") -> HTML.text(s)).toList) :: session_plots.getOrElse(session.name, Nil).map(image => HTML.size(image.width / 2, image.height / 2)(HTML.image(image.name))))))) } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_status", "present recent build status information from database", args => { var target_dir = default_target_dir var ml_statistics = false var only_sessions = Set.empty[String] var options = Options.init() var image_size = default_image_size var verbose = false val getopts = Getopts(""" Usage: isabelle build_status [OPTIONS] Options are: -D DIR target directory (default """ + default_target_dir + """) -M include full ML statistics -S SESSIONS only given SESSIONS (comma separated) -l DAYS length of relevant history (default """ + options.int("build_log_history") + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """) -v verbose Present performance statistics from build log database, which is specified via system options build_log_database_host, build_log_database_user, build_log_history etc. """, "D:" -> (arg => target_dir = Path.explode(arg)), "M" -> (_ => ml_statistics = true), "S:" -> (arg => only_sessions = space_explode(',', arg).toSet), "l:" -> (arg => options = options + ("build_log_history=" + arg)), "o:" -> (arg => options = options + arg), "s:" -> (arg => space_explode('x', arg).map(Value.Int.parse(_)) match { case List(w, h) if w > 0 && h > 0 => image_size = (w, h) case _ => error("Error bad PNG image size: " + quote(arg)) }), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose, target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size) }) } 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,620 +1,619 @@ /* 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 import scala.collection.mutable 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 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_source = "https://isabelle.sketis.net/repos/isabelle" val isabelle_repos: Path = main_dir + Path.explode("isabelle") val afp_repos: Path = main_dir + Path.explode("AFP") 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_repos_source, isabelle_repos) Mercurial.setup_repository(AFP.repos_source, 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.file.toPath, current_log.file.toPath) }) val exit: Logger_Task = Logger_Task("exit", logger => { Isabelle_System.bash( "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.") .check }) /* build release */ val build_release: Logger_Task = Logger_Task("build_release", logger => { Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev()) }) /* integrity test of build_history vs. build_history_base */ val build_history_base: Logger_Task = Logger_Task("build_history_base", logger => { using(logger.ssh_context.open_session("lxbroy10"))(ssh => { val results = Build_History.remote_build_history(ssh, isabelle_repos, isabelle_repos.ext("build_history_base"), isabelle_identifier = "cronjob_build_history", self_update = true, rev = "build_history_base", options = "-f", args = "HOL") for ((log_name, bytes) <- results) { Bytes.write(logger.log_dir + Path.explode(log_name), bytes) } }) }) /* 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: SQL.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, actual_host: String = "", user: String = "", port: Int = 0, proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, self_update: Boolean = false, 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: SQL.Source = "", active: Boolean = true) { def ssh_session(context: SSH.Context): SSH.Session = context.open_session(host = host, user = user, port = port, actual_host = actual_host, proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, permissive = proxy_host.nonEmpty) def sql: SQL.Source = Build_Log.Prop.build_engine + " = " + 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 = (List.empty[Item] /: runs)({ 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) }) } } val remote_builds_old: List[Remote_Build] = List( Remote_Build("AFP old bulky", "lrzcloud1", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", options = "-m64 -M6 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, bulky = true, detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), Remote_Build("AFP old", "lxbroy7", args = "-N -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags + " = " + 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 + " = " + 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 + " = " + 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 Mac OS X", "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 + " = " + SQL.string("polyml-5.7")), Remote_Build("Poly/ML 5.7.1 Mac OS X", "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 + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), 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 + " = " + SQL.string("polyml-test")), Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start + " < 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 + " = " + SQL.string("AFP")) } } val remote_builds1: List[List[Remote_Build]] = { List( List(Remote_Build("Linux A", "lxbroy9", java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing")), List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), List(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 + " = " + SQL.string("Benchmarks"))), List( Remote_Build("Mac OS X", "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("Mac OS X, 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 + " = " + SQL.string("quick_and_dirty"), history_base = "2c0f24e927dd"), Remote_Build("Mac OS X, skip_proofs", "macbroy2", options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"), history_base = "2c0f24e927dd")), List( Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a", detect = Build_Log.Prop.build_start + " > date '2017-03-03'")), List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a")), List(Remote_Build("Mac OS X 10.13 High Sierra", "lapbroy68", options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", self_update = true, args = "-a -d '~~/src/Benchmarks'")), List(Remote_Build("Mac OS X 10.14 Mojave", "lapnipkow3", options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false", self_update = true, args = "-a -d '~~/src/Benchmarks'")), List(Remote_Build("Mac OS X 10.15 Catalina", "laramac01", user = "makarius", proxy_host = "laraserver", proxy_user = "makarius", self_update = true, 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, self_update = true, options = "-m32 -M4" + " -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 + " = " + SQL.string("x86-windows") + " OR " + Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")), Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, options = "-m64 -M4" + " -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 + " = " + SQL.string("x86_64-windows")))) } val remote_builds2: List[List[Remote_Build]] = List( List( Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", java_heap = "8g", options = "-m32 -M1x8 -t AFP" + " -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 = "-a -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", 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 + " = " + 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.ssh_session(logger.ssh_context))(ssh => { val results = Build_History.remote_build_history(ssh, isabelle_repos, isabelle_repos.ext(r.host), isabelle_identifier = "cronjob_build_history", self_update = r.self_update, rev = rev, afp_rev = afp_rev, options = " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) + " -f -h " + Bash.string(r.host) + " " + (r.java_heap match { case "" => "" case h => "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' " }) + r.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(SSH.init_context(options), progress) } class Log_Service private(val ssh_context: SSH.Context, 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() { 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) { 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]( val log_service: Log_Service, val start_date: Date, val task_name: String) { def ssh_context: SSH.Context = log_service.ssh_context def options: Options = ssh_context.options def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg) def log_end(end_date: Date, err: Option[String]) { 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: Path = main_dir + Build_Log.log_subdir(start_date) + val log_dir = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date)) - Isabelle_System.make_directory(log_dir) 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]) { /* 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) { log_service.run_task(start_date, task) } def run_now(task: Logger_Task) { 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]) { 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 + " " + log_service.hostname) run(main_start_date, Logger_Task("isabelle_cronjob", logger => run_now( SEQ(List( init, build_history_base, 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]) { 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") } } } diff --git a/src/Pure/General/ssh.scala b/src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala +++ b/src/Pure/General/ssh.scala @@ -1,510 +1,513 @@ /* Title: Pure/General/ssh.scala Author: Makarius SSH client based on JSch (see also http://www.jcraft.com/jsch/examples). */ package isabelle import java.io.{InputStream, OutputStream, ByteArrayOutputStream} import scala.collection.mutable import scala.util.matching.Regex import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException, OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS, JSchException} object SSH { /* target machine: user@host syntax */ object Target { val User_Host: Regex = "^([^@]+)@(.+)$".r def parse(s: String): (String, String) = s match { case User_Host(user, host) => (user, host) case _ => ("", s) } def unapplySeq(s: String): Option[List[String]] = parse(s) match { case (_, "") => None case (user, host) => Some(List(user, host)) } } val default_port = 22 def make_port(port: Int): Int = if (port > 0) port else default_port def port_suffix(port: Int): String = if (port == default_port) "" else ":" + port def user_prefix(user: String): String = proper_string(user) match { case None => "" case Some(name) => name + "@" } def connect_timeout(options: Options): Int = options.seconds("ssh_connect_timeout").ms.toInt def alive_interval(options: Options): Int = options.seconds("ssh_alive_interval").ms.toInt def alive_count_max(options: Options): Int = options.int("ssh_alive_count_max") /* init context */ def init_context(options: Options): Context = { val config_dir = Path.explode(options.string("ssh_config_dir")) if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir) val jsch = new JSch val config_file = Path.explode(options.string("ssh_config_file")) if (config_file.is_file) jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) val known_hosts = config_dir + Path.explode("known_hosts") if (!known_hosts.is_file) known_hosts.file.createNewFile jsch.setKnownHosts(File.platform_path(known_hosts)) val identity_files = space_explode(':', options.string("ssh_identity_files")).map(Path.explode) for (identity_file <- identity_files if identity_file.is_file) { try { jsch.addIdentity(File.platform_path(identity_file)) } catch { case exn: JSchException => error("Error in ssh identity file " + identity_file + ": " + exn.getMessage) } } new Context(options, jsch) } def open_session(options: Options, host: String, user: String = "", port: Int = 0, actual_host: String = "", proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, permissive: Boolean = false): Session = init_context(options).open_session( host = host, user = user, port = port, actual_host = actual_host, proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, permissive = permissive) class Context private[SSH](val options: Options, val jsch: JSch) { def update_options(new_options: Options): Context = new Context(new_options, jsch) private def connect_session(host: String, user: String = "", port: Int = 0, host_key_permissive: Boolean = false, nominal_host: String = "", nominal_user: String = "", on_close: () => Unit = () => ()): Session = { val session = jsch.getSession(proper_string(user).orNull, host, make_port(port)) session.setUserInfo(No_User_Info) session.setServerAliveInterval(alive_interval(options)) session.setServerAliveCountMax(alive_count_max(options)) session.setConfig("MaxAuthTries", "3") if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no") if (nominal_host != "") session.setHostKeyAlias(nominal_host) if (options.bool("ssh_compression")) { session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") session.setConfig("compression_level", "9") } session.connect(connect_timeout(options)) new Session(options, session, on_close, proper_string(nominal_host) getOrElse host, proper_string(nominal_user) getOrElse user) } def open_session( host: String, user: String = "", port: Int = 0, actual_host: String = "", proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, permissive: Boolean = false): Session = { val connect_host = proper_string(actual_host) getOrElse host if (proxy_host == "") connect_session(host = connect_host, user = user, port = port) else { val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user) val fw = try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) } catch { case exn: Throwable => proxy.close; throw exn } try { connect_session(host = fw.local_host, port = fw.local_port, host_key_permissive = permissive, nominal_host = host, nominal_user = user, user = user, on_close = () => { fw.close; proxy.close }) } catch { case exn: Throwable => fw.close; proxy.close; throw exn } } } } /* logging */ def logging(verbose: Boolean = true, debug: Boolean = false) { JSch.setLogger(if (verbose) new Logger(debug) else null) } private class Logger(debug: Boolean) extends JSch_Logger { def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug def log(level: Int, msg: String) { level match { case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) case JSch_Logger.WARN => Output.warning(msg) case _ => Output.writeln(msg) } } } /* user info */ object No_User_Info extends UserInfo { def getPassphrase: String = null def getPassword: String = null def promptPassword(msg: String): Boolean = false def promptPassphrase(msg: String): Boolean = false def promptYesNo(msg: String): Boolean = false def showMessage(msg: String): Unit = Output.writeln(msg) } /* port forwarding */ object Port_Forwarding { def open(ssh: Session, ssh_close: Boolean, local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding = { val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port) new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port) } } class Port_Forwarding private[SSH]( ssh: SSH.Session, ssh_close: Boolean, val local_host: String, val local_port: Int, val remote_host: String, val remote_port: Int) extends AutoCloseable { override def toString: String = local_host + ":" + local_port + ":" + remote_host + ":" + remote_port def close() { ssh.session.delPortForwardingL(local_host, local_port) if (ssh_close) ssh.close() } } /* Sftp channel */ type Attrs = SftpATTRS sealed case class Dir_Entry(name: String, is_dir: Boolean) { def is_file: Boolean = !is_dir } /* exec channel */ private val exec_wait_delay = Time.seconds(0.3) class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable { override def toString: String = "exec " + session.toString def close() { channel.disconnect } val exit_status: Future[Int] = Future.thread("ssh_wait") { while (!channel.isClosed) exec_wait_delay.sleep channel.getExitStatus } val stdin: OutputStream = channel.getOutputStream val stdout: InputStream = channel.getInputStream val stderr: InputStream = channel.getErrStream // connect after preparing streams channel.connect(connect_timeout(session.options)) def result( progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true): Process_Result = { stdin.close def read_lines(stream: InputStream, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] val line_buffer = new ByteArrayOutputStream(100) def line_flush() { val line = Library.trim_line(line_buffer.toString(UTF8.charset_name)) progress(line) result += line line_buffer.reset } var c = 0 var finished = false while (!finished) { while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c) if (c == 10) line_flush() else if (channel.isClosed) { if (line_buffer.size > 0) line_flush() finished = true } else exec_wait_delay.sleep } result.toList } val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) } val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) } def terminate() { close out_lines.join err_lines.join exit_status.join } val rc = try { exit_status.join } catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } close if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() Process_Result(rc, out_lines.join, err_lines.join) } } /* session */ class Session private[SSH]( val options: Options, val session: JSch_Session, on_close: () => Unit, val nominal_host: String, val nominal_user: String) extends System with AutoCloseable { def update_options(new_options: Options): Session = new Session(new_options, session, on_close, nominal_host, nominal_user) def host: String = if (session.getHost == null) "" else session.getHost override def hg_url: String = "ssh://" + user_prefix(nominal_user) + nominal_host + "/" override def toString: String = user_prefix(session.getUserName) + host + port_suffix(session.getPort) + (if (session.isConnected) "" else " (disconnected)") /* port forwarding */ def port_forwarding( remote_port: Int, remote_host: String = "localhost", local_port: Int = 0, local_host: String = "localhost", ssh_close: Boolean = false): Port_Forwarding = Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port) /* sftp channel */ val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp] sftp.connect(connect_timeout(options)) def close() { sftp.disconnect; session.disconnect; on_close() } val settings: Map[String, String] = { val home = sftp.getHome Map("HOME" -> home, "USER_HOME" -> home) } override def expand_path(path: Path): Path = path.expand_env(settings) def remote_path(path: Path): String = expand_path(path).implode override def bash_path(path: Path): String = Bash.string(remote_path(path)) def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path)) def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2)) def rm(path: Path): Unit = sftp.rm(remote_path(path)) def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path)) def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path)) private def test_entry(path: Path, as_dir: Boolean): Boolean = try { val is_dir = sftp.stat(remote_path(path)).isDir if (as_dir) is_dir else !is_dir } catch { case _: SftpException => false } override def is_dir(path: Path): Boolean = test_entry(path, true) override def is_file(path: Path): Boolean = test_entry(path, false) def is_link(path: Path): Boolean = try { sftp.lstat(remote_path(path)).isLink } catch { case _: SftpException => false } - override def make_directory(path: Path): Unit = + override def make_directory(path: Path): Path = + { if (!is_dir(path)) { execute( "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"") if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path))) } + path + } def read_dir(path: Path): List[Dir_Entry] = { if (!is_dir(path)) error("No such directory: " + path.toString) val dir_name = remote_path(path) val dir = sftp.ls(dir_name) (for { i <- (0 until dir.size).iterator a = dir.get(i).asInstanceOf[AnyRef] name = Untyped.get[String](a, "filename") attrs = Untyped.get[Attrs](a, "attrs") if name != "." && name != ".." } yield { Dir_Entry(name, if (attrs.isLink) { try { sftp.stat(dir_name + "/" + name).isDir } catch { case _: SftpException => false } } else attrs.isDir) }).toList.sortBy(_.name) } def find_files( start: Path, pred: Path => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false): List[Path] = { val result = new mutable.ListBuffer[Path] def check(path: Path) { if (pred(path)) result += path } def find(dir: Path) { if (include_dirs) check(dir) if (follow_links || !is_link(dir)) { for (entry <- read_dir(dir)) { val path = dir + Path.basic(entry.name) if (entry.is_file) check(path) else find(path) } } } if (is_file(start)) check(start) else find(start) result.toList } def open_input(path: Path): InputStream = sftp.get(remote_path(path)) def open_output(path: Path): OutputStream = sftp.put(remote_path(path)) def read_file(path: Path, local_path: Path): Unit = sftp.get(remote_path(path), File.platform_path(local_path)) def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) def read(path: Path): String = using(open_input(path))(File.read_stream) def write_file(path: Path, local_path: Path): Unit = sftp.put(File.platform_path(local_path), remote_path(path)) def write_bytes(path: Path, bytes: Bytes): Unit = using(open_output(path))(bytes.write_stream) def write(path: Path, text: String): Unit = using(open_output(path))(stream => Bytes(text).write_stream(stream)) /* exec channel */ def exec(command: String): Exec = { val channel = session.openChannel("exec").asInstanceOf[ChannelExec] channel.setCommand("export USER_HOME=\"$HOME\"\n" + command) new Exec(this, channel) } override def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true): Process_Result = exec(command).result(progress_stdout, progress_stderr, strict) override def isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(this)) /* tmp dirs */ def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) def rm_tree(remote_dir: String): Unit = execute("rm -r -f " + Bash.string(remote_dir)).check def tmp_dir(): String = execute("mktemp -d -t tmp.XXXXXXXXXX").check.out def with_tmp_dir[A](body: Path => A): A = { val remote_dir = tmp_dir() try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) } } } /* system operations */ trait System { def hg_url: String = "" def expand_path(path: Path): Path = path.expand def bash_path(path: Path): String = File.bash_path(path) def is_dir(path: Path): Boolean = path.is_dir def is_file(path: Path): Boolean = path.is_file - def make_directory(path: Path): Unit = Isabelle_System.make_directory(path) + def make_directory(path: Path): Path = Isabelle_System.make_directory(path) def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true): Process_Result = Isabelle_System.bash(command, progress_stdout = progress_stdout, progress_stderr = progress_stderr, strict = strict) def isabelle_platform: Isabelle_Platform = Isabelle_Platform() } object Local extends System } diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML +++ b/src/Pure/System/isabelle_system.ML @@ -1,123 +1,123 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig val bash_output_check: string -> string val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list val check_bash_function: Proof.context -> string * Position.T -> string val rm_tree: Path.T -> unit - val make_directory: Path.T -> unit + val make_directory: Path.T -> Path.T val mkdir: Path.T -> unit val copy_dir: Path.T -> Path.T -> unit val copy_file: Path.T -> Path.T -> unit val copy_file_base: Path.T * Path.T -> Path.T -> unit val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val with_tmp_dir: string -> (Path.T -> 'a) -> 'a end; structure Isabelle_System: ISABELLE_SYSTEM = struct (* bash *) fun bash_output_check s = (case Bash.process s of {rc = 0, out, ...} => (trim_line out) | {err, ...} => error (trim_line err)); fun bash_output s = let val {out, err, rc, ...} = Bash.process s; val _ = warning (trim_line err); in (out, rc) end; fun bash s = let val (out, rc) = bash_output s; val _ = writeln (trim_line out); in rc end; (* bash functions *) fun bash_functions () = bash_output_check "declare -Fx" |> split_lines |> map_filter (space_explode " " #> try List.last); fun check_bash_function ctxt arg = Completion.check_entity Markup.bash_functionN (bash_functions () |> map (rpair Position.none)) ctxt arg; (* directory operations *) fun system_command cmd = if bash cmd <> 0 then error ("System command failed: " ^ cmd) else (); fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path); fun make_directory path = - if File.is_dir path then () - else - (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\""); - if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path)); + let + val _ = + if File.is_dir path then () + else + (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\""); + if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path)); + in path end; fun mkdir path = if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path); fun copy_dir src dst = if File.eq (src, dst) then () else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ()); fun copy_file src0 dst0 = let val src = Path.expand src0; val dst = Path.expand dst0; val target = if File.is_dir dst then Path.append dst (Path.base src) else dst; in if File.eq (src, target) then () else ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target)) end; fun copy_file_base (base_dir, src0) target_dir = let val src = Path.expand src0; val src_dir = Path.dir src; val _ = if Path.starts_basic src then () else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory"); - val _ = make_directory (Path.append target_dir src_dir); - in copy_file (Path.append base_dir src) (Path.append target_dir src) end; + in copy_file (Path.append base_dir src) (make_directory (Path.append target_dir src_dir)) end; (* tmp files *) fun create_tmp_path name ext = let val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); val _ = File.exists path andalso raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; fun with_tmp_file name ext f = let val path = create_tmp_path name ext in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; (* tmp dirs *) fun with_tmp_dir name f = - let - val path = create_tmp_path name ""; - val _ = make_directory path; - in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end; + let val path = create_tmp_path name "" + in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end; end; diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,422 +1,425 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes import scala.annotation.tailrec object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ abstract class Service @volatile private var _settings: Option[Map[String, String]] = None @volatile private var _services: Option[List[Class[Service]]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def services(): List[Class[Service]] = { if (_services.isEmpty) init() // unsynchronized check _services.get } def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty || _services.isEmpty) { val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") else "" if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) def set_cygwin_root() { if (Platform.is_windows) _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) } set_cygwin_root() def default(env: Map[String, String], entry: (String, String)): Map[String, String] = if (env.isDefinedAt(entry._1) || entry._2 == "") env else env + entry val env = { val temp_windows = { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" } val user_home = System.getProperty("user.home", "") val isabelle_app = System.getProperty("isabelle.app", "") default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") } val settings = { val dump = JFile.createTempFile("settings", null) dump.deleteOnExit try { val cmd1 = if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l", File.standard_path(isabelle_root1 + "\\bin\\isabelle")) else List(isabelle_root1 + "/bin/isabelle") val cmd = cmd1 ::: List("getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output) val entries = (for (entry <- File.read(dump).split("\u0000") if entry != "") yield { val i = entry.indexOf('=') if (i <= 0) entry -> "" else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } finally { dump.delete } } _settings = Some(settings) set_cygwin_root() val variable = "ISABELLE_SCALA_SERVICES" val services = for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) yield { def err(msg: String): Nothing = error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[Service]] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } _services = Some(services) } } /* getenv */ private def getenv_error(name: String): Nothing = error("Undefined Isabelle environment variable: " + quote(name)) def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") def isabelle_id(): String = proper_string(getenv("ISABELLE_ID")) getOrElse Mercurial.repository(Path.explode("~~")).parent() /** file-system operations **/ /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ - def make_directory(path: Path): Unit = + def make_directory(path: Path): Path = + { if (!path.is_dir) { bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"") if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path))) } + path + } def copy_dir(dir1: Path, dir2: Path): Unit = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: Path): Unit = rm_tree(root.file) def rm_tree(root: JFile) { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit) { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) File.move(dir, old_dir) File.move(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close proc.getErrorStream.close proc.destroy Exn.Interrupt.dispose() } (output, rc) } def kill(signal: String, group_pid: String): (String, Int) = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout, progress_stderr, strict) } def jconsole(): Process_Result = bash("isabelle_jdk jconsole " + java.lang.ProcessHandle.current().pid).check private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, redirect: Boolean = false): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } private lazy val curl_check: Unit = try { bash("curl --version").check } catch { case ERROR(_) => error("Cannot download files: missing curl") } def download(url: String, file: Path, progress: Progress = new Progress): Unit = { curl_check progress.echo("Getting " + quote(url)) try { bash("curl --fail --silent --location " + Bash.string(url) + " > " + File.bash_path(file)).check } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url), msg) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC") } } } diff --git a/src/Pure/Thy/html.scala b/src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala +++ b/src/Pure/Thy/html.scala @@ -1,401 +1,398 @@ /* Title: Pure/Thy/html.scala Author: Makarius HTML presentation elements. */ package isabelle object HTML { /* output text with control symbols */ private val control = Map( Symbol.sub -> "sub", Symbol.sub_decoded -> "sub", Symbol.sup -> "sup", Symbol.sup_decoded -> "sup", Symbol.bold -> "b", Symbol.bold_decoded -> "b") private val control_block = Map( Symbol.bsub -> "", Symbol.bsub_decoded -> "", Symbol.esub -> "", Symbol.esub_decoded -> "", Symbol.bsup -> "", Symbol.bsup_decoded -> "", Symbol.esup -> "", Symbol.esup_decoded -> "") def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym) def output_char_permissive(c: Char, s: StringBuilder) { c match { case '<' => s ++= "<" case '>' => s ++= ">" case '&' => s ++= "&" case _ => s += c } } def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean) { def output_char(c: Char): Unit = if (permissive) output_char_permissive(c, s) else XML.output_char(c, s) def output_string(str: String): Unit = str.iterator.foreach(output_char) def output_hidden(body: => Unit): Unit = if (hidden) { s ++= ""; body; s ++= "" } def output_symbol(sym: Symbol.Symbol): Unit = if (sym != "") { control_block.get(sym) match { case Some(html) if html.startsWith(" s ++= html; output_hidden(output_string(sym)) case Some(html) => output_hidden(output_string(sym)); s ++= html case None => if (hidden && Symbol.is_control_encoded(sym)) { output_hidden(output_string(Symbol.control_prefix)) s ++= "" output_string(Symbol.control_name(sym).get) s ++= "" output_hidden(output_string(Symbol.control_suffix)) } else output_string(sym) } } var ctrl = "" for (sym <- Symbol.iterator(text)) { if (is_control(sym)) { output_symbol(ctrl); ctrl = sym } else { control.get(ctrl) match { case Some(elem) if Symbol.is_controllable(sym) => output_hidden(output_symbol(ctrl)) s += '<'; s ++= elem; s += '>' output_symbol(sym) s ++= "' case _ => output_symbol(ctrl) output_symbol(sym) } ctrl = "" } } output_symbol(ctrl) } def output(text: String): String = Library.make_string(output(text, _, hidden = false, permissive = true)) /* output XML as HTML */ private val structural_elements = Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", "ul", "ol", "dl", "li", "dt", "dd") def output(body: XML.Body, s: StringBuilder, hidden: Boolean, structural: Boolean) { def elem(markup: Markup) { s ++= markup.name for ((a, b) <- markup.properties) { s += ' ' s ++= a s += '=' s += '"' output(b, s, hidden = hidden, permissive = false) s += '"' } } def tree(t: XML.Tree): Unit = t match { case XML.Elem(markup, Nil) => s += '<'; elem(markup); s ++= "/>" case XML.Elem(markup, ts) => if (structural && structural_elements(markup.name)) s += '\n' s += '<'; elem(markup); s += '>' ts.foreach(tree) s ++= "' if (structural && structural_elements(markup.name)) s += '\n' case XML.Text(txt) => output(txt, s, hidden = hidden, permissive = true) } body.foreach(tree) } def output(body: XML.Body, hidden: Boolean, structural: Boolean): String = Library.make_string(output(body, _, hidden, structural)) def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String = output(List(tree), hidden, structural) /* attributes */ class Attribute(val name: String, value: String) { def xml: XML.Attribute = name -> value def apply(elem: XML.Elem): XML.Elem = elem + xml } def id(s: String): Attribute = new Attribute("id", s) def class_(name: String): Attribute = new Attribute("class", name) def width(w: Int): Attribute = new Attribute("width", w.toString) def height(h: Int): Attribute = new Attribute("height", h.toString) def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem)) /* structured markup operators */ def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) val no_text: XML.Tree = XML.Text("") val break: XML.Body = List(XML.elem("br")) class Operator(val name: String) { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body)) def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body) } class Heading(name: String) extends Operator(name) { def apply(txt: String): XML.Elem = super.apply(text(txt)) def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt)) def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt)) } val div = new Operator("div") val span = new Operator("span") val pre = new Operator("pre") val par = new Operator("p") val emph = new Operator("em") val bold = new Operator("b") val code = new Operator("code") val item = new Operator("li") val list = new Operator("ul") val enum = new Operator("ol") val descr = new Operator("dl") val dt = new Operator("dt") val dd = new Operator("dd") val title = new Heading("title") val chapter = new Heading("h1") val section = new Heading("h2") val subsection = new Heading("h3") val subsubsection = new Heading("h4") val paragraph = new Heading("h5") val subparagraph = new Heading("h6") def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_))) def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_))) def description(items: List[(XML.Body, XML.Body)]): XML.Elem = descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) })) def link(href: String, body: XML.Body = Nil): XML.Elem = XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body) def image(src: String, alt: String = ""): XML.Elem = XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) def source(body: XML.Body): XML.Elem = pre("source", body) def source(src: String): XML.Elem = source(text(src)) def style(s: String): XML.Elem = XML.elem("style", text(s)) def style_file(href: String): XML.Elem = XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil) def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file)) def script(s: String): XML.Elem = XML.elem("script", text(s)) def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil) def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file)) /* messages */ // background val writeln_message: Attribute = class_("writeln_message") val warning_message: Attribute = class_("warning_message") val error_message: Attribute = class_("error_message") // underline val writeln: Attribute = class_("writeln") val warning: Attribute = class_("warning") val error: Attribute = class_("error") /* tooltips */ def tooltip(item: XML.Body, tip: XML.Body): XML.Elem = span(item ::: List(div("tooltip", tip))) def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem = HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg))))) /* GUI elements */ object GUI { private def optional_value(text: String): XML.Attributes = proper_string(text).map(a => "value" -> a).toList private def optional_name(name: String): XML.Attributes = proper_string(name).map(a => "name" -> a).toList private def optional_title(tooltip: String): XML.Attributes = proper_string(tooltip).map(a => "title" -> a).toList private def optional_submit(submit: Boolean): XML.Attributes = if (submit) List("onChange" -> "this.form.submit()") else Nil private def optional_checked(selected: Boolean): XML.Attributes = if (selected) List("checked" -> "") else Nil private def optional_action(action: String): XML.Attributes = proper_string(action).map(a => "action" -> a).toList private def optional_onclick(script: String): XML.Attributes = proper_string(script).map(a => "onclick" -> a).toList private def optional_onchange(script: String): XML.Attributes = proper_string(script).map(a => "onchange" -> a).toList def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, script: String = ""): XML.Elem = XML.Elem( Markup("button", List("type" -> (if (submit) "submit" else "button"), "value" -> "true") ::: optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body) def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, selected: Boolean = false, script: String = ""): XML.Elem = XML.elem("label", XML.elem( Markup("input", List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) ::: optional_title(tooltip) ::: optional_submit(submit) ::: optional_checked(selected) ::: optional_onchange(script))) :: body) def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "", submit: Boolean = false, script: String = ""): XML.Elem = XML.elem(Markup("input", List("type" -> "text") ::: (if (columns > 0) List("size" -> columns.toString) else Nil) ::: optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) ::: optional_submit(submit) ::: optional_onchange(script))) def parameter(text: String = "", name: String = ""): XML.Elem = XML.elem( Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name))) def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false) : XML.Elem = XML.Elem( Markup("form", optional_name(name) ::: optional_action(action) ::: (if (http_post) List("method" -> "post") else Nil)), body) } /* GUI layout */ object Wrap_Panel { object Alignment extends Enumeration { val left, right, center = Value } def apply(contents: List[XML.Elem], name: String = "", action: String = "", alignment: Alignment.Value = Alignment.right): XML.Elem = { val body = Library.separate(XML.Text(" "), contents) GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))), name = name, action = action) } } /* document */ val header: String = XML.header + """ """ val head_meta: XML.Elem = XML.Elem(Markup("meta", List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css", hidden: Boolean = true, structural: Boolean = true): String = { cat_lines( List(header, output( XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), hidden = hidden, structural = structural), output(XML.elem("body", body), hidden = hidden, structural = structural))) } /* fonts */ def fonts_url(): String => String = (for (entry <- Isabelle_Fonts.fonts(hidden = true)) yield (entry.path.file_name -> Url.print_file(entry.path.file))).toMap def fonts_dir(prefix: String)(ttf_name: String): String = prefix + "/" + ttf_name def fonts_css(make_url: String => String = fonts_url()): String = { def font_face(entry: Isabelle_Fonts.Entry): String = cat_lines( List( "@font-face {", " font-family: '" + entry.family + "';", " src: url('" + make_url(entry.path.file_name) + "') format('truetype');") ::: (if (entry.is_bold) List(" font-weight: bold;") else Nil) ::: (if (entry.is_italic) List(" font-style: italic;") else Nil) ::: List("}")) ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face)) .mkString("", "\n\n", "\n") } /* document directory */ def isabelle_css: Path = Path.explode("~~/etc/isabelle.css") def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts")) { File.write(dir + isabelle_css.base, fonts_css(make_url) + "\n\n" + File.read(isabelle_css)) } - def init_dir(dir: Path) - { - Isabelle_System.make_directory(dir) - write_isabelle_css(dir) - } + def init_dir(dir: Path): Unit = + write_isabelle_css(Isabelle_System.make_directory(dir)) def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, css: String = isabelle_css.file_name, hidden: Boolean = true, structural: Boolean = true) { init_dir(dir) File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden, structural = structural)) } } diff --git a/src/Pure/Thy/present.scala b/src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala +++ b/src/Pure/Thy/present.scala @@ -1,313 +1,312 @@ /* Title: Pure/Thy/present.scala Author: Makarius Theory presentation: HTML. */ package isabelle import java.io.{File => JFile} import scala.collection.immutable.SortedMap object Present { /* maintain chapter index -- NOT thread-safe */ private val sessions_path = Path.basic(".sessions") private def read_sessions(dir: Path): List[(String, String)] = { val path = dir + sessions_path if (path.is_file) { import XML.Decode._ list(pair(string, string))(Symbol.decode_yxml(File.read(path))) } else Nil } private def write_sessions(dir: Path, sessions: List[(String, String)]) { import XML.Encode._ File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) } def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) { - val dir = browser_info + Path.basic(chapter) - Isabelle_System.make_directory(dir) + val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter)) val sessions0 = try { read_sessions(dir) } catch { case _: XML.Error => Nil } val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList write_sessions(dir, sessions) val title = "Isabelle/" + chapter + " sessions" HTML.write_document(dir, "index.html", List(HTML.title(title + " (" + Distribution.version + ")")), HTML.chapter(title) :: (if (sessions.isEmpty) Nil else List(HTML.div("sessions", List(HTML.description( sessions.map({ case (name, description) => val descr = Symbol.trim_blank_lines(description) (List(HTML.link(name + "/index.html", HTML.text(name))), if (descr == "") Nil else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) } def make_global_index(browser_info: Path) { if (!(browser_info + Path.explode("index.html")).is_file) { Isabelle_System.make_directory(browser_info) File.copy(Path.explode("~~/lib/logo/isabelle.gif"), browser_info + Path.explode("isabelle.gif")) File.write(browser_info + Path.explode("index.html"), File.read(Path.explode("~~/lib/html/library_index_header.template")) + File.read(Path.explode("~~/lib/html/library_index_content.template")) + File.read(Path.explode("~~/lib/html/library_index_footer.template"))) } } /* finish session */ def finish( progress: Progress, browser_info: Path, graph_file: JFile, info: Sessions.Info, name: String) { val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) val session_fonts = session_prefix + Path.explode("fonts") if (info.options.bool("browser_info")) { Isabelle_System.make_directory(session_fonts) val session_graph = session_prefix + Path.basic("session_graph.pdf") File.copy(graph_file, session_graph.file) Isabelle_System.chmod("a+r", session_graph) HTML.write_isabelle_css(session_prefix) for (entry <- Isabelle_Fonts.fonts(hidden = true)) File.copy(entry.path, session_fonts) } } /** preview **/ sealed case class Preview(title: String, content: String) def preview( resources: Resources, snapshot: Document.Snapshot, plain_text: Boolean = false, fonts_url: String => String = HTML.fonts_url()): Preview = { require(!snapshot.is_outdated) def output_document(title: String, body: XML.Body): String = HTML.output_document( List( HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), HTML.title(title)), List(HTML.source(body)), css = "", structural = false) val name = snapshot.node_name if (plain_text) { val title = "File " + quote(name.path.file_name) val content = output_document(title, HTML.text(snapshot.node.source)) Preview(title, content) } else { resources.make_preview(snapshot) match { case Some(preview) => preview case None => val title = if (name.is_theory) "Theory " + quote(name.theory_base_name) else "File " + quote(name.path.file_name) val content = output_document(title, pide_document(snapshot)) Preview(title, content) } } } /* PIDE document */ private val document_elements = Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements + Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE private val div_elements = Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, HTML.descr.name) private def html_div(html: XML.Body): Boolean = html exists { case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) case XML.Text(_) => false } private def html_class(c: String, html: XML.Body): XML.Tree = if (html.forall(_ == HTML.no_text)) HTML.no_text else if (html_div(html)) HTML.div(c, html) else HTML.span(c, html) private def make_html(xml: XML.Body): XML.Body = xml map { case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => html_class(Markup.Language.DOCUMENT, make_html(body)) case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body)) case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body)) case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text case XML.Elem(Markup.Markdown_List(kind), body) => if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body)) case XML.Elem(markup, body) => val name = markup.name val html = markup.properties match { case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => List(html_class(kind, make_html(body))) case _ => make_html(body) } Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { case Some(c) => html_class(c.toString, html) case None => html_class(name, html) } case XML.Text(text) => XML.Text(Symbol.decode(text)) } def pide_document(snapshot: Document.Snapshot): XML.Body = make_html(snapshot.markup_to_XML(Text.Range.full, document_elements)) /** build document **/ val document_format = "pdf" val default_document_name = "document" def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name) def document_tags(tags: List[String]): String = { cat_lines( tags.map(tag => tag.toList match { case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" case cs => "\\isakeeptag{" + cs.mkString + "}" })) + "\n" } def build_document( document_name: String = default_document_name, document_dir: Option[Path] = None, tags: List[String] = Nil) { val document_target = Path.parent + Path.explode(document_name).ext(document_format) val dir = document_dir getOrElse default_document_dir(document_name) if (!dir.is_dir) error("Bad document output directory " + dir) val root_name = { val root1 = "root_" + document_name if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root" } /* bash scripts */ def root_bash(ext: String): String = Bash.string(root_name + "." + ext) def latex_bash(fmt: String, ext: String = "tex"): String = "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext) def bash(script: String): Process_Result = Isabelle_System.bash(script, cwd = dir.file) /* prepare document */ File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags)) List("log", "blg").foreach(ext => (dir + Path.explode(root_name).ext(ext)).file.delete) val result = if ((dir + Path.explode("build")).is_file) { bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name)) } else { bash( List( latex_bash("sty"), latex_bash(document_format), "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", latex_bash(document_format), latex_bash(document_format)).mkString(" && ")) } /* result */ if (!result.ok) { cat_error( Library.trim_line(result.err), cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)), "Failed to build document in " + File.path(dir.absolute_file)) } bash("if [ -f " + root_bash(document_format) + " ]; then cp -f " + root_bash(document_format) + " " + File.bash_path(document_target) + "; fi").check } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("document", "prepare theory session document", args => { var document_dir: Option[Path] = None var document_name = default_document_name var tags: List[String] = Nil val getopts = Getopts(""" Usage: isabelle document [OPTIONS] Options are: -d DIR document output directory (default """ + default_document_dir(default_document_name) + """) -n NAME document name (default """ + quote(default_document_name) + """) -t TAGS markup for tagged regions Prepare the theory session document in document directory, producing the specified output format. """, "d:" -> (arg => document_dir = Some(Path.explode(arg))), "n:" -> (arg => document_name = arg), "t:" -> (arg => tags = space_explode(',', arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() try { build_document(document_dir = document_dir, document_name = document_name, tags = tags) } catch { case ERROR(msg) => Output.writeln(msg); sys.exit(2) } }) } diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala +++ b/src/Pure/Tools/build.scala @@ -1,961 +1,960 @@ /* Title: Pure/Tools/build.scala Author: Makarius Options: :folding=explicit: Build and manage Isabelle sessions. */ package isabelle import scala.collection.{SortedSet, mutable} import scala.annotation.tailrec object Build { /** auxiliary **/ /* persistent build info */ sealed case class Session_Info( sources: String, input_heaps: List[String], output_heap: Option[String], return_code: Int) { def ok: Boolean = return_code == 0 } /* queue with scheduling information */ private object Queue { type Timings = (List[Properties.T], Double) def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings = { val no_timings: Timings = (Nil, 0.0) store.access_database(session_name) match { case None => no_timings case Some(db) => def ignore_error(msg: String) = { progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg)) no_timings } try { val command_timings = store.read_command_timings(db, session_name) val session_timing = store.read_session_timing(db, session_name) match { case Markup.Elapsed(t) => t case _ => 0.0 } (command_timings, session_timing) } catch { case ERROR(msg) => ignore_error(msg) case exn: java.lang.Error => ignore_error(Exn.message(exn)) case _: XML.Error => ignore_error("") } finally { db.close } } } def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double]) : Map[String, Double] = { val maximals = sessions_structure.build_graph.maximals.toSet def desc_timing(session_name: String): Double = { if (maximals.contains(session_name)) timing(session_name) else { val descendants = sessions_structure.build_descendants(List(session_name)).toSet val g = sessions_structure.build_graph.restrict(descendants) (0.0 :: g.maximals.flatMap(desc => { val ps = g.all_preds(List(desc)) if (ps.exists(p => !timing.isDefinedAt(p))) None else Some(ps.map(timing(_)).sum) })).max } } timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0) } def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store) : Queue = { val graph = sessions_structure.build_graph val names = graph.keys val timings = names.map(name => (name, load_timings(progress, store, name))) val command_timings = timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil) val session_timing = make_session_timing(sessions_structure, timings.map({ case (name, (_, t)) => (name, t) }).toMap) object Ordering extends scala.math.Ordering[String] { def compare_timing(name1: String, name2: String): Int = { val t1 = session_timing(name1) val t2 = session_timing(name2) if (t1 == 0.0 || t2 == 0.0) 0 else t1 compare t2 } def compare(name1: String, name2: String): Int = compare_timing(name2, name1) match { case 0 => sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { case 0 => name1 compare name2 case ord => ord } case ord => ord } } new Queue(graph, SortedSet(names: _*)(Ordering), command_timings) } } private class Queue( graph: Graph[String, Sessions.Info], order: SortedSet[String], val command_timings: String => List[Properties.T]) { def is_inner(name: String): Boolean = !graph.is_maximal(name) def is_empty: Boolean = graph.is_empty def - (name: String): Queue = new Queue(graph.del_node(name), order - name, // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? command_timings) def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] = { val it = order.iterator.dropWhile(name => skip(name) || !graph.defined(name) // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? || !graph.is_minimal(name)) if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) } else None } } /* PIDE protocol handler */ /* job: running prover process */ private class Job(progress: Progress, session_name: String, val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, verbose: Boolean, val numa_node: Option[Int], command_timings0: List[Properties.T]) { val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display) private val export_consumer = Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache) private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val base = deps(parent) val args_yxml = YXML.string_of_body( { import XML.Encode._ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), pair(list(string), list(string)))))))))))))))))( (Symbol.codes, (command_timings0, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (session_name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (base.doc_names, (base.global_theories.toList, (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))) }) val env = Isabelle_System.settings() + ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) val is_pure = Sessions.is_pure(session_name) val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = if (do_store) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) } else Nil val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) { override val xml_cache: XML.Cache = store.xml_cache override val xz_cache: XZ.Cache = store.xz_cache } object Build_Session_Errors { private val promise: Promise[List[String]] = Future.promise def result: Exn.Result[List[String]] = promise.join_result def cancel: Unit = promise.cancel def apply(errs: List[String]) { try { promise.fulfill(errs) } catch { case _: IllegalStateException => } } } val stdout = new StringBuilder(1000) val stderr = new StringBuilder(1000) val messages = new mutable.ListBuffer[XML.Elem] val command_timings = new mutable.ListBuffer[Properties.T] val theory_timings = new mutable.ListBuffer[Properties.T] val session_timings = new mutable.ListBuffer[Properties.T] val runtime_statistics = new mutable.ListBuffer[Properties.T] val task_statistics = new mutable.ListBuffer[Properties.T] def fun( name: String, acc: mutable.ListBuffer[Properties.T], unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) = { name -> ((msg: Prover.Protocol_Output) => unapply(msg.properties) match { case Some(props) => acc += props; true case _ => false }) } session.init_protocol_handler(new Session.Protocol_Handler { override def exit() { Build_Session_Errors.cancel } private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { val (rc, errors) = try { val (rc, errs) = { import XML.Decode._ pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) } val errors = for (err <- errs) yield { val prt = Protocol_Message.expose_no_reports(err) Pretty.string_of(prt, metric = Symbol.Metric) } (rc, errors) } catch { case ERROR(err) => (2, List(err)) } session.protocol_command("Prover.stop", rc.toString) Build_Session_Errors(errors) true } private def loading_theory(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Loading_Theory(name) => progress.theory(Progress.Theory(name, session = session_name)) true case _ => false } private def export(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Protocol.Export(args) => export_consumer(session_name, args, msg.bytes) true case _ => false } private def command_timing(props: Properties.T): Option[Properties.T] = for { props1 <- Markup.Command_Timing.unapply(props) elapsed <- Markup.Elapsed.unapply(props1) elapsed_time = Time.seconds(elapsed) if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") } yield props1.filter(p => Markup.command_timing_properties(p._1)) override val functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory, Markup.EXPORT -> export, fun(Markup.Command_Timing.name, command_timings, command_timing), fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) }) session.runtime_statistics += Session.Consumer("ML_statistics") { case Session.Runtime_Statistics(props) => runtime_statistics += props } session.all_messages += Session.Consumer[Any]("build_session_output") { case msg: Prover.Output => val message = msg.message if (msg.is_stdout) { stdout ++= Symbol.encode(XML.content(message)) } else if (msg.is_stderr) { stderr ++= Symbol.encode(XML.content(message)) } else if (Protocol.is_exported(message)) { messages += message } else if (msg.is_exit) { val err = "Prover terminated" + (msg.properties match { case Markup.Process_Result(result) => ": " + result.print_rc case _ => "" }) Build_Session_Errors(List(err)) } case _ => } val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = Isabelle_Process(session, options, sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) val errors = Isabelle_Thread.interrupt_handler(_ => process.terminate) { Exn.capture { process.await_startup } match { case Exn.Res(_) => session.protocol_command("build_session", args_yxml) Build_Session_Errors.result case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) } } val process_result = Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } val process_output = stdout.toString :: messages.toList.map(message => Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) ::: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) ::: session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) val result = process_result.output(process_output).error(Library.trim_line(stderr.toString)) errors match { case Exn.Res(Nil) => result case Exn.Res(errs) => result.error_rc.output( errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: errs.map(Protocol.Error_Message_Marker.apply)) case Exn.Exn(Exn.Interrupt()) => if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result case Exn.Exn(exn) => throw exn } } def terminate: Unit = future_result.cancel def is_finished: Boolean = future_result.is_finished private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout > Time.zero) Some(Event_Timer.request(Time.now() + info.timeout) { terminate }) else None } def join: (Process_Result, Option[String]) = { val result0 = future_result.join val result1 = export_consumer.shutdown(close = true).map(Output.error_message_text) match { case Nil => result0 case errs => result0.errors(errs).error_rc } if (result1.ok) { for (document_output <- proper_string(options.string("document_output"))) { - val document_output_dir = info.dir + Path.explode(document_output) - Isabelle_System.make_directory(document_output_dir) - + val document_output_dir = + Isabelle_System.make_directory(info.dir + Path.explode(document_output)) val base = deps(session_name) File.write(document_output_dir + Path.explode("session.tex"), base.session_theories.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString) } Present.finish(progress, store.browser_info, graph_file, info, session_name) } graph_file.delete val was_timeout = timeout_request match { case None => false case Some(request) => !request.cancel } val result2 = if (result1.interrupted) { if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout else result1.error(Output.error_message_text("Interrupt")) } else result1 val heap_digest = if (result2.ok && do_store && store.output_heap(session_name).is_file) Some(Sessions.write_heap_digest(store.output_heap(session_name))) else None (result2, heap_digest) } } /** build with results **/ class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) { def sessions: Set[String] = results.keySet def cancelled(name: String): Boolean = results(name)._1.isEmpty def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1)) def info(name: String): Sessions.Info = results(name)._2 val rc: Int = (0 /: results.iterator.map( { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _) def ok: Boolean = rc == 0 override def toString: String = rc.toString } def session_finished(session_name: String, process_result: Process_Result): String = "Finished " + session_name + " (" + process_result.timing.message_resources + ")" def session_timing(session_name: String, build_log: Build_Log.Session_Info): String = { val props = build_log.session_timing val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1 val timing = Markup.Timing_Properties.parse(props) "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")" } def build( options: Options, selection: Sessions.Selection = Sessions.Selection.empty, progress: Progress = new Progress, check_unknown_files: Boolean = false, build_heap: Boolean = false, clean_build: Boolean = false, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Sessions.Info] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, list_files: Boolean = false, check_keywords: Set[String] = Set.empty, fresh_build: Boolean = false, no_build: Boolean = false, soft_build: Boolean = false, verbose: Boolean = false, export_files: Boolean = false): Results = { val build_options = options + "completion_limit=0" + "editor_tracing_messages=0" + "pide_reports=false" val store = Sessions.store(build_options) Isabelle_Fonts.init() /* session selection and dependencies */ val full_sessions = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos) def sources_stamp(deps: Sessions.Deps, session_name: String): String = { val digests = full_sessions(session_name).meta_digest :: deps.sources(session_name) ::: deps.imported_sources(session_name) SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString } val deps = { val deps0 = Sessions.deps(full_sessions.selection(selection), progress = progress, inlined_files = true, verbose = verbose, list_files = list_files, check_keywords = check_keywords).check_errors if (soft_build && !fresh_build) { val outdated = deps0.sessions_structure.build_topological_order.flatMap(name => store.access_database(name) match { case Some(db) => using(db)(store.read_build(_, name)) match { case Some(build) if build.ok && build.sources == sources_stamp(deps0, name) => None case _ => Some(name) } case None => Some(name) }) Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)), progress = progress, inlined_files = true).check_errors } else deps0 } /* check unknown files */ if (check_unknown_files) { val source_files = (for { (_, base) <- deps.session_bases.iterator (path, _) <- base.sources.iterator } yield path).toList val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file) val unknown_files = Mercurial.check_files(source_files)._2. filterNot(path => exclude_files.contains(path.canonical_file)) if (unknown_files.nonEmpty) { progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" + unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", "")) } } /* main build process */ val queue = Queue(progress, deps.sessions_structure, store) store.prepare_output_dir() if (clean_build) { for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) { val (relevant, ok) = store.clean_output(name) if (relevant) { if (ok) progress.echo("Cleaned " + name) else progress.echo(name + " FAILED to clean") } } } // scheduler loop case class Result( current: Boolean, heap_digest: Option[String], process: Option[Process_Result], info: Sessions.Info) { def ok: Boolean = process match { case None => false case Some(res) => res.rc == 0 } } def sleep() { Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep } } val numa_nodes = new NUMA.Nodes(numa_shuffling) @tailrec def loop( pending: Queue, running: Map[String, (List[String], Job)], results: Map[String, Result]): Map[String, Result] = { def used_node(i: Int): Boolean = running.iterator.exists( { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i }) if (pending.is_empty) results else { if (progress.stopped) { for ((_, (_, job)) <- running) job.terminate } running.find({ case (_, (_, job)) => job.is_finished }) match { case Some((session_name, (input_heaps, job))) => //{{{ finish job val (process_result, heap_digest) = job.join val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) val process_result_tail = { val tail = job.info.options.int("process_output_tail") process_result.copy( out_lines = "(see also " + store.output_log(session_name).file.toString + ")" :: (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0))) } val build_log = Build_Log.Log_File(session_name, process_result.out_lines). parse_session_info( command_timings = true, theory_timings = true, ml_statistics = true, task_statistics = true) // write log file if (process_result.ok) { File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) } else File.write(store.output_log(session_name), terminate_lines(log_lines)) // write database using(store.open_database(session_name, output = true))(db => store.write_session_info(db, session_name, build_log = if (process_result.timeout) build_log.error("Timeout") else build_log, build = Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest, process_result.rc))) // messages process_result.err_lines.foreach(progress.echo) if (process_result.ok) { if (verbose) progress.echo(session_timing(session_name, build_log)) progress.echo(session_finished(session_name, process_result)) } else { progress.echo(session_name + " FAILED") if (!process_result.interrupted) progress.echo(process_result_tail.out) } loop(pending - session_name, running - session_name, results + (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info))) //}}} case None if running.size < (max_jobs max 1) => //{{{ check/start next job pending.dequeue(running.isDefinedAt) match { case Some((session_name, info)) => val ancestor_results = deps.sessions_structure.build_requirements(List(session_name)). filterNot(_ == session_name).map(results(_)) val ancestor_heaps = ancestor_results.flatMap(_.heap_digest) val do_store = build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name) val (current, heap_digest) = { store.access_database(session_name) match { case Some(db) => using(db)(store.read_build(_, session_name)) match { case Some(build) => val heap_digest = store.find_heap_digest(session_name) val current = !fresh_build && build.ok && build.sources == sources_stamp(deps, session_name) && build.input_heaps == ancestor_heaps && build.output_heap == heap_digest && !(do_store && heap_digest.isEmpty) (current, heap_digest) case None => (false, None) } case None => (false, None) } } val all_current = current && ancestor_results.forall(_.current) if (all_current) loop(pending - session_name, running, results + (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info))) else if (no_build) { progress.echo_if(verbose, "Skipping " + session_name + " ...") loop(pending - session_name, running, results + (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info))) } else if (ancestor_results.forall(_.ok) && !progress.stopped) { progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") store.clean_output(session_name) using(store.open_database(session_name, output = true))( store.init_session_info(_, session_name)) val numa_node = numa_nodes.next(used_node) val job = new Job(progress, session_name, info, deps, store, do_store, verbose, numa_node, queue.command_timings(session_name)) loop(pending, running + (session_name -> (ancestor_heaps, job)), results) } else { progress.echo(session_name + " CANCELLED") loop(pending - session_name, running, results + (session_name -> Result(false, heap_digest, None, info))) } case None => sleep(); loop(pending, running, results) } ///}}} case None => sleep(); loop(pending, running, results) } } } /* build results */ val results0 = if (deps.is_empty) { progress.echo_warning("Nothing to build") Map.empty[String, Result] } else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) } val results = new Results( (for ((name, result) <- results0.iterator) yield (name, (result.process, result.info))).toMap) if (export_files) { for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) { val info = results.info(name) if (info.export_files.nonEmpty) { progress.echo("Exporting " + info.name + " ...") for ((dir, prune, pats) <- info.export_files) { Export.export_files(store, name, info.dir + dir, progress = if (verbose) progress else new Progress, export_prune = prune, export_patterns = pats) } } } } if (results.rc != 0 && (verbose || !no_build)) { val unfinished = (for { name <- results.sessions.iterator if !results(name).ok } yield name).toList.sorted progress.echo("Unfinished session(s): " + commas(unfinished)) } /* global browser info */ if (!no_build) { val browser_chapters = (for { (name, result) <- results0.iterator if result.ok info = full_sessions(name) if info.options.bool("browser_info") } yield (info.chapter, (name, info.description))).toList.groupBy(_._1). map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) for ((chapter, entries) <- browser_chapters) Present.update_chapter_index(store.browser_info, chapter, entries) if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info) } results } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args => { val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var requirements = false var soft_build = false var exclude_session_groups: List[String] = Nil var all_sessions = false var build_heap = false var clean_build = false var dirs: List[Path] = Nil var export_files = false var fresh_build = false var session_groups: List[String] = Nil var max_jobs = 1 var check_keywords: Set[String] = Set.empty var list_files = false var no_build = false var options = Options.init(opts = build_options) var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle build [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -R refer to requirements of selected sessions -S soft build: only observe changes of sources, not heap images -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b build heap images -c clean build -d DIR include session directory -e export files from session specification into file-system -f fresh build -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files -n no build -- test dependencies only -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants Build and manage Isabelle sessions, depending on implicit settings: """ + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n", "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "R" -> (_ => requirements = true), "S" -> (_ => soft_build = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "b" -> (_ => build_heap = true), "c" -> (_ => clean_build = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e" -> (_ => export_files = true), "f" -> (_ => fresh_build = true), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "k:" -> (arg => check_keywords = check_keywords + arg), "l" -> (_ => list_files = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() if (verbose) { progress.echo( "Started at " + Build_Log.print_date(start_date) + " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")") progress.echo(Build_Log.Settings.show() + "\n") } val results = progress.interrupt_handler { build(options, selection = Sessions.Selection( requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions), progress = progress, check_unknown_files = Mercurial.is_repository(Path.explode("~~")), build_heap = build_heap, clean_build = clean_build, dirs = dirs, select_dirs = select_dirs, numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), max_jobs = max_jobs, list_files = list_files, check_keywords = check_keywords, fresh_build = fresh_build, no_build = no_build, soft_build = soft_build, verbose = verbose, export_files = export_files) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time if (verbose) { progress.echo("\nFinished at " + Build_Log.print_date(end_date)) } val total_timing = (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) /* build logic image */ def build_logic(options: Options, logic: String, progress: Progress = new Progress, build_heap: Boolean = false, dirs: List[Path] = Nil, fresh: Boolean = false, strict: Boolean = false): Int = { val selection = Sessions.Selection.session(logic) val rc = if (!fresh && build(options, selection = selection, build_heap = build_heap, no_build = true, dirs = dirs).ok) 0 else { progress.echo("Build started for Isabelle/" + logic + " ...") Build.build(options, selection = selection, progress = progress, build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc } if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc } } diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala +++ b/src/Pure/Tools/phabricator.scala @@ -1,1075 +1,1074 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius Support for Phabricator server, notably for Ubuntu 18.04 LTS. See also: - https://www.phacility.com/phabricator - https://secure.phabricator.com/book/phabricator */ package isabelle import scala.collection.mutable import scala.util.matching.Regex object Phabricator { /** defaults **/ /* required packages */ val packages: List[String] = Build_Docker.packages ::: Linux.packages ::: List( // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages "php-xml", "php-zip", "python-pygments", "ssh", "subversion", // mercurial build packages "make", "gcc", "python", "python-dev", "python-docutils", "python-pygments", "python-openssl") /* global system resources */ val www_user = "www-data" val daemon_user = "phabricator" val sshd_config: Path = Path.explode("/etc/ssh/sshd_config") /* installation parameters */ val default_name = "vcs" def phabricator_name(name: String = "", ext: String = ""): String = "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext) def isabelle_phabricator_name(name: String = "", ext: String = ""): String = "isabelle-" + phabricator_name(name = name, ext = ext) def default_root(name: String): Path = Path.explode("/var/www") + Path.basic(phabricator_name(name = name)) def default_repo(name: String): Path = default_root(name) + Path.basic("repo") val default_mailers: Path = Path.explode("mailers.json") val default_system_port: Int = SSH.default_port val alternative_system_port = 222 val default_server_port = 2222 val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz" /** global configuration **/ val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf")) def global_config_script( init: String = "", body: String = "", exit: String = ""): String = { """#!/bin/bash """ + (if (init.nonEmpty) "\n" + init else "") + """ { while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do NAME="$(echo "$REPLY" | cut -d: -f1)" ROOT="$(echo "$REPLY" | cut -d: -f2)" { """ + Library.prefix_lines(" ", body) + """ } < /dev/null done } < """ + File.bash_path(global_config) + "\n" + (if (exit.nonEmpty) "\n" + exit + "\n" else "") } sealed case class Config(name: String, root: Path) { def home: Path = root + Path.explode(phabricator_name()) def execute(command: String): Process_Result = Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check } def read_config(): List[Config] = { if (global_config.is_file) { for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty) yield { space_explode(':', entry) match { case List(name, root) => Config(name, Path.explode(root)) case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry)) } } } else Nil } def write_config(configs: List[Config]) { File.write(global_config, configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n")) } def get_config(name: String): Config = read_config().find(config => config.name == name) getOrElse error("Bad Isabelle/Phabricator installation " + quote(name)) /** administrative tools **/ /* Isabelle tool wrapper */ val isabelle_tool1 = Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args => { var list = false var name = default_name val getopts = Getopts(""" Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] Options are: -l list available Phabricator installations -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Invoke a command-line tool within the home directory of the named Phabricator installation. """, "l" -> (_ => list = true), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.isEmpty && !list) getopts.usage() val progress = new Console_Progress if (list) { for (config <- read_config()) { progress.echo("phabricator " + quote(config.name) + " root " + config.root) } } else { val config = get_config(name) val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true) if (!result.ok) error(result.print_return_code) } }) /** setup **/ def user_setup(name: String, description: String, ssh_setup: Boolean = false) { if (!Linux.user_exists(name)) { Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup) } else if (Linux.user_description(name) != description) { error("User " + quote(name) + " already exists --" + " for Phabricator it should have the description:\n " + quote(description)) } } def command_setup(name: String, init: String = "", body: String = "", exit: String = ""): Path = { val command = Path.explode("/usr/local/bin") + Path.basic(name) File.write(command, global_config_script(init = init, body = body, exit = exit)) Isabelle_System.chmod("755", command) Isabelle_System.chown("root:root", command) command } def mercurial_setup(mercurial_source: String, progress: Progress = new Progress) { progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...") Isabelle_System.with_tmp_dir("mercurial")(tmp_dir => { val archive = if (Url.is_wellformed(mercurial_source)) { val archive = tmp_dir + Path.basic("mercurial.tar.gz") Bytes.write(archive, Url.read_bytes(Url(mercurial_source))) archive } else Path.explode(mercurial_source) Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check File.read_dir(tmp_dir).filter(name => (tmp_dir + Path.basic(name)).is_dir) match { case List(dir) => val build_dir = tmp_dir + Path.basic(dir) progress.bash("make all && make install", cwd = build_dir.file, echo = true).check case dirs => error("Bad archive " + archive + (if (dirs.isEmpty) "" else "\nmultiple directory entries " + commas_quote(dirs))) } }) } def phabricator_setup( options: Options, name: String = default_name, root: String = "", repo: String = "", package_update: Boolean = false, mercurial_source: String = "", progress: Progress = new Progress) { /* system environment */ Linux.check_system_root() progress.echo("System packages ...") if (package_update) { Linux.package_update(progress = progress) Linux.check_reboot_required() } Linux.package_install(packages, progress = progress) Linux.check_reboot_required() if (mercurial_source.nonEmpty) { for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } { error("Cannot install Mercurial from source:\n" + "package package " + quote(name) + " already installed") } mercurial_setup(mercurial_source, progress = progress) } /* users */ if (name.contains((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) || Set("", "ssh", "phd", "dump", daemon_user).contains(name)) { error("Bad installation name: " + quote(name)) } user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true) user_setup(name, "Phabricator SSH User") /* basic installation */ progress.echo("\nPhabricator installation ...") val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name) val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name) val configs = read_config() for (config <- configs if config.name == name) { error("Duplicate Phabricator installation " + quote(name) + " in " + config.root) } if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { error("Failed to create root directory " + root_path) } Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path) Isabelle_System.chmod("755", root_path) progress.bash(cwd = root_path.file, echo = true, script = """ set -e echo "Cloning distribution repositories:" git clone --branch stable https://github.com/phacility/arcanist.git git -C arcanist reset --hard """ + Bash.string(options.string("phabricator_version_arcanist")) + """ git clone --branch stable https://github.com/phacility/phabricator.git git -C phabricator reset --hard """ + Bash.string(options.string("phabricator_version_phabricator")) + """ """).check val config = Config(name, root_path) write_config(configs ::: List(config)) config.execute("config set pygments.enabled true") /* local repository directory */ progress.echo("\nRepository hosting setup ...") if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { error("Failed to create local repository directory " + repo_path) } Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path) Isabelle_System.chmod("755", repo_path) config.execute("config set repository.default-local-path " + File.bash_path(repo_path)) val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name(name = name)) File.write(sudoers_file, www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" + name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n") Isabelle_System.chmod("440", sudoers_file) config.execute("config set diffusion.ssh-user " + Bash.string(config.name)) /* MySQL setup */ progress.echo("\nMySQL setup ...") File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")), """[mysqld] max_allowed_packet = 32M innodb_buffer_pool_size = 1600M local_infile = 0 """) Linux.service_restart("mysql") def mysql_conf(R: Regex, which: String): String = { val conf = Path.explode("/etc/mysql/debian.cnf") split_lines(File.read(conf)).collectFirst({ case R(a) => a }) match { case Some(res) => res case None => error("Cannot determine " + which + " from " + conf) } } val mysql_root_user = mysql_conf("""^user\s*=\s*(\S*)\s*$""".r, "superuser name") val mysql_root_password = mysql_conf("""^password\s*=\s*(\S*)\s*$""".r, "superuser password") val mysql_name = phabricator_name(name = name).replace("-", "_") val mysql_user_string = SQL.string(mysql_name) + "@'localhost'" val mysql_password = Linux.generate_password() Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) + " --password=" + Bash.string(mysql_root_password) + " --execute=" + Bash.string( """DROP USER IF EXISTS """ + mysql_user_string + "; " + """CREATE USER """ + mysql_user_string + """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ + """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") + """`.* TO """ + mysql_user_string + ";")).check config.execute("config set mysql.user " + Bash.string(mysql_name)) config.execute("config set mysql.pass " + Bash.string(mysql_password)) config.execute("config set phabricator.cache-namespace " + Bash.string(mysql_name)) config.execute("config set storage.default-namespace " + Bash.string(mysql_name)) config.execute("config set storage.mysql-engine.max-size 8388608") progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check /* database dump */ val dump_name = isabelle_phabricator_name(name = "dump") command_setup(dump_name, body = """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database" [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz" echo -n "Creating $ROOT/database/dump.sql.gz ..." "$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure' echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """) /* Phabricator upgrade */ command_setup(isabelle_phabricator_name(name = "upgrade"), init = """BRANCH="${1:-stable}" if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ] then echo "Bad branch: \"$BRANCH\"" exit 1 fi systemctl stop isabelle-phabricator-phd systemctl stop apache2 """, body = """echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..." for REPO in arcanist phabricator do cd "$ROOT/$REPO" echo -e "\nUpdating \"$REPO\" ..." git checkout "$BRANCH" git pull done echo -e "\nUpgrading storage ..." "$ROOT/phabricator/bin/storage" upgrade --force """, exit = """systemctl start apache2 systemctl start isabelle-phabricator-phd""") /* PHP setup */ val php_version = Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""") .check.out val php_conf = Path.explode("/etc/php") + Path.basic(php_version) + // educated guess Path.explode("apache2/conf.d") + Path.basic(isabelle_phabricator_name(ext = "ini")) File.write(php_conf, "post_max_size = 32M\n" + "opcache.validate_timestamps = 0\n" + "memory_limit = 512M\n" + "max_execution_time = 120\n") /* Apache setup */ progress.echo("Apache setup ...") val apache_root = Path.explode("/etc/apache2") val apache_sites = apache_root + Path.explode("sites-available") if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites) val server_name = phabricator_name(name = name, ext = "lvh.me") // alias for "localhost" for testing val server_url = "http://" + server_name File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")), """ ServerName """ + server_name + """ ServerAdmin webmaster@localhost DocumentRoot """ + config.home.implode + """/webroot ErrorLog ${APACHE_LOG_DIR}/error.log CustomLog ${APACHE_LOG_DIR}/access.log combined RewriteEngine on RewriteRule ^(.*)$ /index.php?__path__=$1 [B,L,QSA] # vim: syntax=apache ts=4 sw=4 sts=4 sr noet """) Isabelle_System.bash( """ set -e a2enmod rewrite a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check config.execute("config set phabricator.base-uri " + Bash.string(server_url)) Linux.service_restart("apache2") progress.echo("\nFurther manual configuration via " + server_url) /* PHP daemon */ progress.echo("\nPHP daemon setup ...") - val phd_log_path = Path.explode("/var/tmp/phd") - Isabelle_System.make_directory(phd_log_path) + val phd_log_path = Isabelle_System.make_directory(Path.explode("/var/tmp/phd")) Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path) Isabelle_System.chmod("755", phd_log_path) config.execute("config set phd.user " + Bash.string(daemon_user)) config.execute("config set phd.log-directory /var/tmp/phd/" + isabelle_phabricator_name(name = name) + "/log") val phd_name = isabelle_phabricator_name(name = "phd") Linux.service_shutdown(phd_name) val phd_command = command_setup(phd_name, body = """"$ROOT/phabricator/bin/phd" "$@" """) try { Linux.service_install(phd_name, """[Unit] Description=PHP daemon manager for Isabelle/Phabricator After=syslog.target network.target apache2.service mysql.service [Service] Type=oneshot User=""" + daemon_user + """ Group=""" + daemon_user + """ Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin ExecStart=""" + phd_command.implode + """ start --force ExecStop=""" + phd_command.implode + """ stop RemainAfterExit=yes [Install] WantedBy=multi-user.target """) } catch { case ERROR(msg) => progress.bash("bin/phd status", cwd = config.home.file, echo = true).check error(msg) } } /* Isabelle tool wrapper */ val isabelle_tool2 = Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args => { var mercurial_source = "" var repo = "" var package_update = false var name = default_name var options = Options.init() var root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] Options are: -M SOURCE install Mercurial from source: local PATH, or URL, or ":" for """ + standard_mercurial_source + """ -R DIR repository directory (default: """ + default_repo("NAME") + """) -U full update of system packages before installation -n NAME Phabricator installation name (default: """ + quote(default_name) + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r DIR installation root directory (default: """ + default_root("NAME") + """) Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). The installation name (default: """ + quote(default_name) + """) is mapped to a regular Unix user; this is relevant for public SSH access. """, "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)), "R:" -> (arg => repo = arg), "U" -> (_ => package_update = true), "n:" -> (arg => name = arg), "o:" -> (arg => options = options + arg), "r:" -> (arg => root = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress val release = Linux.Release() if (!release.is_ubuntu_18_04) error("Bad Linux version: Ubuntu 18.04 LTS required") phabricator_setup(options, name = name, root = root, repo = repo, package_update = package_update, mercurial_source = mercurial_source, progress = progress) }) /** setup mail **/ val mailers_template: String = """[ { "key": "example.org", "type": "smtp", "options": { "host": "mail.example.org", "port": 465, "user": "phabricator@example.org", "password": "********", "protocol": "ssl", "message-id": true } } ]""" def phabricator_setup_mail( name: String = default_name, config_file: Option[Path] = None, test_user: String = "", progress: Progress = new Progress) { Linux.check_system_root() val config = get_config(name) val default_config_file = config.root + default_mailers val mail_config = config_file getOrElse default_config_file def setup_mail { progress.echo("Using mail configuration from " + mail_config) config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config)) if (test_user.nonEmpty) { progress.echo("Sending test mail to " + quote(test_user)) progress.bash(cwd = config.home.file, echo = true, script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ + Bash.string(test_user)).check } } if (config_file.isEmpty) { if (!default_config_file.is_file) { File.write(default_config_file, mailers_template) Isabelle_System.chmod("600", default_config_file) } if (File.read(default_config_file) == mailers_template) { progress.echo("Please invoke the tool again, after providing details in\n " + default_config_file.implode + "\n") } else setup_mail } else setup_mail } /* Isabelle tool wrapper */ val isabelle_tool3 = Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation", args => { var test_user = "" var name = default_name var config_file: Option[Path] = None val getopts = Getopts(""" Usage: isabelle phabricator_setup_mail [OPTIONS] Options are: -T USER send test mail to Phabricator user -f FILE config file (default: """ + default_mailers + """ within Phabricator root) -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Provide mail configuration for existing Phabricator installation. """, "T:" -> (arg => test_user = arg), "f:" -> (arg => config_file = Some(Path.explode(arg))), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_mail(name = name, config_file = config_file, test_user = test_user, progress = progress) }) /** setup ssh **/ /* sshd config */ private val Port = """^\s*Port\s+(\d+)\s*$""".r private val No_Port = """^#\s*Port\b.*$""".r private val Any_Port = """^#?\s*Port\b.*$""".r def conf_ssh_port(port: Int): String = if (port == SSH.default_port) "#Port " + SSH.default_port else "Port " + port def read_ssh_port(conf: Path): Int = { val lines = split_lines(File.read(conf)) val ports = lines.flatMap({ case Port(Value.Int(p)) => Some(p) case No_Port() => Some(SSH.default_port) case _ => None }) ports match { case List(port) => port case Nil => error("Missing Port specification in " + conf) case _ => error("Multiple Port specifications in " + conf) } } def write_ssh_port(conf: Path, port: Int): Boolean = { val old_port = read_ssh_port(conf) if (old_port == port) false else { val lines = split_lines(File.read(conf)) val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line }) File.write(conf, cat_lines(lines1)) true } } /* phabricator_setup_ssh */ def phabricator_setup_ssh( server_port: Int = default_server_port, system_port: Int = default_system_port, progress: Progress = new Progress) { Linux.check_system_root() val configs = read_config() if (server_port == system_port) { error("Port for Phabricator sshd coincides with system port: " + system_port) } val sshd_conf_system = Path.explode("/etc/ssh/sshd_config") val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name()) val ssh_name = isabelle_phabricator_name(name = "ssh") Linux.service_shutdown(ssh_name) val old_system_port = read_ssh_port(sshd_conf_system) if (old_system_port != system_port) { progress.echo("Reconfigurig system ssh service") Linux.service_shutdown("ssh") write_ssh_port(sshd_conf_system, system_port) Linux.service_start("ssh") } progress.echo("Configuring " + ssh_name + " service") val ssh_command = command_setup(ssh_name, body = """if [ "$1" = "$NAME" ] then exec "$ROOT/phabricator/bin/ssh-auth" "$@" fi""", exit = "exit 1") File.write(sshd_conf_server, """# OpenBSD Secure Shell server for Isabelle/Phabricator AuthorizedKeysCommand """ + ssh_command.implode + """ AuthorizedKeysCommandUser """ + daemon_user + """ AuthorizedKeysFile none AllowUsers """ + configs.map(_.name).mkString(" ") + """ Port """ + server_port + """ Protocol 2 PermitRootLogin no AllowAgentForwarding no AllowTcpForwarding no PrintMotd no PrintLastLog no PasswordAuthentication no ChallengeResponseAuthentication no PidFile /var/run/""" + ssh_name + """.pid """) Linux.service_install(ssh_name, """[Unit] Description=OpenBSD Secure Shell server for Isabelle/Phabricator After=network.target auditd.service ConditionPathExists=!/etc/ssh/sshd_not_to_be_run [Service] EnvironmentFile=-/etc/default/ssh ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecReload=/bin/kill -HUP $MAINPID KillMode=process Restart=on-failure RestartPreventExitStatus=255 Type=notify RuntimeDirectory=sshd-phabricator RuntimeDirectoryMode=0755 [Install] WantedBy=multi-user.target Alias=""" + ssh_name + """.service """) for (config <- configs) { progress.echo("phabricator " + quote(config.name) + " port " + server_port) config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString)) if (server_port == SSH.default_port) config.execute("config delete diffusion.ssh-port") } } /* Isabelle tool wrapper */ val isabelle_tool4 = Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations", args => { var server_port = default_server_port var system_port = default_system_port val getopts = Getopts(""" Usage: isabelle phabricator_setup_ssh [OPTIONS] Options are: -p PORT sshd port for Phabricator servers (default: """ + default_server_port + """) -q PORT sshd port for the operating system (default: """ + default_system_port + """) Configure ssh service for all Phabricator installations: a separate sshd is run in addition to the one of the operating system, and ports need to be distinct. A particular Phabricator installation is addressed by using its name as the ssh user; the actual Phabricator user is determined via stored ssh keys. """, "p:" -> (arg => server_port = Value.Int.parse(arg)), "q:" -> (arg => system_port = Value.Int.parse(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_ssh( server_port = server_port, system_port = system_port, progress = progress) }) /** conduit API **/ object API { /* user information */ sealed case class User( id: Long, phid: String, name: String, real_name: String, roles: List[String]) { def is_valid: Boolean = roles.contains("verified") && roles.contains("approved") && roles.contains("activated") def is_admin: Boolean = roles.contains("admin") def is_regular: Boolean = !(roles.contains("bot") || roles.contains("list")) } /* repository information */ sealed case class Repository( vcs: VCS.Value, id: Long, phid: String, name: String, callsign: String, short_name: String, importing: Boolean, ssh_url: String) { def is_hg: Boolean = vcs == VCS.hg } object VCS extends Enumeration { val hg, git, svn = Value def read(s: String): Value = try { withName(s) } catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) } } def edits(typ: String, value: JSON.T): List[JSON.Object.T] = List(JSON.Object("type" -> typ, "value" -> value)) def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] = value.toList.flatMap(edits(typ, _)) /* result with optional error */ sealed case class Result(result: JSON.T, error: Option[String]) { def ok: Boolean = error.isEmpty def get: JSON.T = if (ok) result else Exn.error(error.get) def get_value[A](unapply: JSON.T => Option[A]): A = unapply(get) getOrElse Exn.error("Bad JSON result: " + JSON.Format(result)) def get_string: String = get_value(JSON.Value.String.unapply) } def make_result(json: JSON.T): Result = { val result = JSON.value(json, "result").getOrElse(JSON.Object.empty) val error_info = JSON.string(json, "error_info") val error_code = JSON.string(json, "error_code") Result(result, error_info orElse error_code) } /* context for operations */ def apply(user: String, host: String, port: Int = SSH.default_port): API = new API(user, host, port) } final class API private(ssh_user: String, ssh_host: String, ssh_port: Int) { /* connection */ require(ssh_host.nonEmpty && ssh_port >= 0) private def ssh_user_prefix: String = SSH.user_prefix(ssh_user) private def ssh_port_suffix: String = SSH.port_suffix(ssh_port) override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix /* execute methods */ def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T = { Isabelle_System.with_tmp_file("params", "json")(params_file => { File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params)))) val result = Isabelle_System.bash( "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) + " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check JSON.parse(result.out, strict = false) }) } def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result = API.make_result(execute_raw(method, params = params)) def execute_search[A]( method: String, params: JSON.Object.T, unapply: JSON.T => Option[A]): List[A] = { val results = new mutable.ListBuffer[A] var after = "" do { val result = execute(method, params = params ++ JSON.optional("after" -> proper_string(after))) results ++= result.get_value(JSON.list(_, "data", unapply)) after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after"))) } while (after.nonEmpty) results.toList } def ping(): String = execute("conduit.ping").get_string /* users */ lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid")) lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName")) def get_users( all: Boolean = false, phid: String = "", name: String = ""): List[API.User] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "usernames" -> name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("user.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "username") real_name <- JSON.string0(fields, "realName") roles <- JSON.strings(fields, "roles") } yield API.User(id, phid, name, real_name, roles))) } def the_user(phid: String): API.User = get_users(phid = phid) match { case List(user) => user case _ => error("Bad user PHID " + quote(phid)) } /* repositories */ def get_repositories( all: Boolean = false, phid: String = "", callsign: String = "", short_name: String = ""): List[API.Repository] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "callsigns" -> callsign, "shortNames" -> short_name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("diffusion.repository.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { vcs_name <- JSON.string(fields, "vcs") id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "name") callsign <- JSON.string0(fields, "callsign") short_name <- JSON.string0(fields, "shortName") importing <- JSON.bool(fields, "isImporting") } yield { val vcs = API.VCS.read(vcs_name) val url_path = if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name val ssh_url = vcs match { case API.VCS.hg => hg_url + url_path case API.VCS.git => hg_url + url_path + ".git" case API.VCS.svn => "" } API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url) })) } def the_repository(phid: String): API.Repository = get_repositories(phid = phid) match { case List(repo) => repo case _ => error("Bad repository PHID " + quote(phid)) } def create_repository( name: String, callsign: String = "", // unique name, UPPERCASE short_name: String = "", // unique name description: String = "", public: Boolean = false, vcs: API.VCS.Value = API.VCS.hg): API.Repository = { require(name.nonEmpty) val transactions = API.edits("vcs", vcs.toString) ::: API.edits("name", name) ::: API.opt_edits("callsign", proper_string(callsign)) ::: API.opt_edits("shortName", proper_string(short_name)) ::: API.opt_edits("description", proper_string(description)) ::: (if (public) Nil else API.edits("view", user_phid) ::: API.edits("policy.push", user_phid)) ::: API.edits("status", "active") val phid = execute("diffusion.repository.edit", params = JSON.Object("transactions" -> transactions)) .get_value(JSON.value(_, "object", JSON.string(_, "phid"))) execute("diffusion.looksoon", params = JSON.Object("repositories" -> List(phid))).get the_repository(phid) } } } diff --git a/src/Pure/Tools/scala_project.scala b/src/Pure/Tools/scala_project.scala --- a/src/Pure/Tools/scala_project.scala +++ b/src/Pure/Tools/scala_project.scala @@ -1,149 +1,148 @@ /* Title: Pure/Tools/scala_project.scala Author: Makarius Setup Gradle project for Isabelle/Scala/jEdit. */ package isabelle object Scala_Project { /* groovy syntax */ def groovy_string(s: String): String = { s.map(c => c match { case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c case _ => c.toString }).mkString("'", "", "'") } /* file and directories */ def isabelle_files(): List[String] = { val files1 = { val isabelle_home = Path.explode("~~").canonical Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")). map(path => File.relative_path(isabelle_home, path).getOrElse(path).implode) } val files2 = (for { path <- List( Path.explode("~~/lib/classes/Pure.shasum"), Path.explode("~~/src/Tools/jEdit/dist/Isabelle-jEdit.shasum")) line <- Library.trim_split_lines(File.read(path)) name = if (line.length > 42 && line(41) == '*') line.substring(42) else error("Bad shasum entry: " + quote(line)) if name != "lib/classes/Pure.jar" && name != "src/Tools/jEdit/dist/jedit.jar" && name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit-base.jar" && name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" } yield name) files1 ::: files2 } val isabelle_dirs: List[(String, Path)] = List( "src/Pure/" -> Path.explode("isabelle"), "src/Tools/Graphview/" -> Path.explode("isabelle.graphview"), "src/Tools/VSCode/" -> Path.explode("isabelle.vscode"), "src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"), "src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"), "src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick")) /* scala project */ def scala_project(project_dir: Path, symlinks: Boolean = false) { if (symlinks && Platform.is_windows) error("Cannot create symlinks on Windows") if (project_dir.is_file || project_dir.is_dir) error("Project directory already exists: " + project_dir) val src_dir = project_dir + Path.explode("src/main/scala") val java_src_dir = project_dir + Path.explode("src/main/java") - val scala_src_dir = project_dir + Path.explode("src/main/scala") - Isabelle_System.make_directory(scala_src_dir) + val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala")) Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir) val files = isabelle_files() for (file <- files if file.endsWith(".scala")) { val (path, target) = isabelle_dirs.collectFirst({ case (prfx, p) if file.startsWith(prfx) => (Path.explode("~~") + Path.explode(file), scala_src_dir + p) }).getOrElse(error("Unknown directory prefix for " + quote(file))) Isabelle_System.make_directory(target) if (symlinks) File.link(path, target) else File.copy(path, target) } val jars = for (file <- files if file.endsWith(".jar")) yield { if (file.startsWith("/")) file else Isabelle_System.getenv("ISABELLE_HOME") + "/" + file } File.write(project_dir + Path.explode("settings.gradle"), "rootProject.name = 'Isabelle'\n") File.write(project_dir + Path.explode("build.gradle"), """plugins { id 'scala' } repositories { mavenCentral() } dependencies { implementation 'org.scala-lang:scala-library:""" + scala.util.Properties.versionNumberString + """' compile files( """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n ", ")") + """ } """) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit", args => { var symlinks = false val getopts = Getopts(""" Usage: isabelle scala_project [OPTIONS] PROJECT_DIR Options are: -L make symlinks to original scala files Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs such as IntelliJ IDEA. """, "L" -> (_ => symlinks = true)) val more_args = getopts(args) val project_dir = more_args match { case List(dir) => Path.explode(dir) case _ => getopts.usage() } scala_project(project_dir, symlinks = symlinks) }) }