--- a/src/HOL/Data_Structures/Binomial_Heap.thy Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Mon Mar 25 10:16:14 2024 +0100
@@ -472,19 +472,19 @@
subsubsection \<open>Timing Functions\<close>
-define_time_fun link
+time_fun link
lemma T_link[simp]: "T_link t\<^sub>1 t\<^sub>2 = 0"
by(cases t\<^sub>1; cases t\<^sub>2, auto)
-define_time_fun rank
+time_fun rank
lemma T_rank[simp]: "T_rank t = 0"
by(cases t, auto)
-define_time_fun ins_tree
+time_fun ins_tree
-define_time_fun insert
+time_fun insert
lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
by (induction t ts rule: T_ins_tree.induct) auto
@@ -504,7 +504,7 @@
subsubsection \<open>\<open>T_merge\<close>\<close>
-define_time_fun merge
+time_fun merge
(* Warning: \<open>T_merge.induct\<close> is less convenient than the equivalent \<open>merge.induct\<close>,
apparently because of the \<open>let\<close> clauses introduced by pattern_aliases; should be investigated.
@@ -547,14 +547,14 @@
subsubsection \<open>\<open>T_get_min\<close>\<close>
-define_time_fun root
+time_fun root
lemma T_root[simp]: "T_root t = 0"
by(cases t)(simp_all)
-define_time_fun min
+time_fun min
-define_time_fun get_min
+time_fun get_min
lemma T_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts"
by (induction ts rule: T_get_min.induct) auto
@@ -571,7 +571,7 @@
subsubsection \<open>\<open>T_del_min\<close>\<close>
-define_time_fun get_min_rest
+time_fun get_min_rest
(*fun T_get_min_rest :: "'a::linorder trees \<Rightarrow> nat" where
"T_get_min_rest [t] = 1"
| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"*)
@@ -595,7 +595,7 @@
definition "T_rev xs = length xs + 1"
-define_time_fun del_min
+time_fun del_min
lemma T_del_min_bound:
fixes ts
--- a/src/HOL/Data_Structures/Define_Time_0.ML Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_0.ML Mon Mar 25 10:16:14 2024 +0100
@@ -37,7 +37,7 @@
end
val _ =
- Outer_Syntax.command \<^command_keyword>\<open>define_time_0\<close> "ML setup for global theory"
+ Outer_Syntax.command \<^command_keyword>\<open>time_fun_0\<close> "ML setup for global theory"
(Parse.prop >> (Toplevel.theory o save));
end
\ No newline at end of file
--- a/src/HOL/Data_Structures/Define_Time_Function.ML Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Mon Mar 25 10:16:14 2024 +0100
@@ -16,11 +16,10 @@
val print_timing': Proof.context -> pfunc -> pfunc -> unit
val print_timing: Proof.context -> Function.info -> Function.info -> unit
-val reg_and_proove_time_func: theory -> term list -> term list -> term option converter
- -> (bool -> local_theory -> term list -> term option -> term)
+val reg_and_proove_time_func: theory -> term list -> term list
-> bool -> Function.info * theory
-val reg_time_func: theory -> term list -> term list -> term option converter
- -> (bool -> local_theory -> term list -> term option -> term) -> bool -> theory
+val reg_time_func: theory -> term list -> term list
+ -> bool -> theory
val time_dom_tac: Proof.context -> thm -> thm list -> int -> tactic
@@ -316,10 +315,10 @@
if not (casecIsCase T) then error "Internal error: invalid case type" else
let val (nconst, args') = casecArgs f args in
plus
+ (f (List.last args))
(if nconst then
SOME (build_func (Const (t,casecTyp T), args'))
else NONE)
- (f (List.last args))
end
| casec _ _ _ _ _ = error "Internal error: invalid case term"
@@ -332,8 +331,8 @@
val tt = f tt
val ft = f ft
in
- plus (case (tt,ft) of (NONE, NONE) => NONE | _ =>
- (SOME ((Const (If_name, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft)))) (f cond)
+ plus (f cond) (case (tt,ft) of (NONE, NONE) => NONE | _ =>
+ (SOME ((Const (If_name, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft))))
end
fun letc_change_typ (Type ("fun", [T1, Type ("fun", [T2, _])])) = (Type ("fun", [T1, Type ("fun", [change_typ T2, HOLogic.natT])]))
@@ -363,16 +362,16 @@
fun top_converter is_rec _ _ = opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE))
(* Use converter to convert right side of a term *)
-fun to_time ctxt origin converter top_converter term =
- top_converter ctxt origin (walk ctxt origin converter term)
+fun to_time ctxt origin is_rec term =
+ top_converter is_rec ctxt origin (walk ctxt origin converter term)
(* Converts a term to its running time version *)
-fun convert_term ctxt (origin: term list) conv topConv (pT $ (Const (eqN, _) $ l $ r)) =
+fun convert_term ctxt (origin: term list) is_rec (pT $ (Const (eqN, _) $ l $ r)) =
pT
$ (Const (eqN, @{typ "nat \<Rightarrow> nat \<Rightarrow> bool"})
$ (build_func ((walk_func l []) |>> (fun_to_time ctxt origin) |>> Option.valOf ||> conv_args ctxt origin))
- $ (to_time ctxt origin conv topConv r))
- | convert_term _ _ _ _ _ = error "Internal error: invalid term to convert"
+ $ (to_time ctxt origin is_rec r))
+ | convert_term _ _ _ _ = error "Internal error: invalid term to convert"
(* 4. Tactic to prove "f_dom n" *)
fun time_dom_tac ctxt induct_rule domintros =
@@ -389,10 +388,10 @@
handle Empty => error "Function or terms of function not found"
(* Register timing function of a given function *)
-fun reg_and_proove_time_func (theory: theory) (term: term list) (terms: term list) conv topConv print =
- reg_time_func theory term terms conv topConv false
+fun reg_and_proove_time_func (theory: theory) (term: term list) (terms: term list) print =
+ reg_time_func theory term terms false
|> proove_termination term terms print
-and reg_time_func (theory: theory) (term: term list) (terms: term list) conv topConv print =
+and reg_time_func (theory: theory) (term: term list) (terms: term list) print =
let
val lthy = Named_Target.theory_init theory
val _ =
@@ -403,7 +402,7 @@
(* 1. Fix all terms *)
(* Exchange Var in types and terms to Free and check constraints *)
- val terms = map
+ val terms = map
(map_aterms fixTerms
#> map_types (map_atyps fixTypes)
#> fixPartTerms lthy term)
@@ -417,7 +416,7 @@
- On left side change name of function to timing function
- Convert right side of equation with conversion schema
*)
- val timing_terms = map (convert_term lthy term conv (topConv is_rec)) terms
+ val timing_terms = map (convert_term lthy term is_rec) terms
(* 4. Register function and prove termination *)
val names = map Term.term_name term
@@ -522,38 +521,60 @@
(time_info, Local_Theory.exit_global lthy')
end
+fun fix_definition (Const ("Pure.eq", _) $ l $ r) = Const ("HOL.Trueprop", @{typ "bool \<Rightarrow> prop"})
+ $ (Const ("HOL.eq", @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}) $ l $ r)
+ | fix_definition t = t
+fun check_definition [t] = [t]
+ | check_definition _ = error "Only a single defnition is allowed"
+
(* Convert function into its timing function (called by command) *)
-fun reg_time_fun_cmd (funcs, thms) conv topConv (theory: theory) =
+fun reg_time_fun_cmd (funcs, thms) (theory: theory) =
let
val ctxt = Proof_Context.init_global theory
val fterms = map (Syntax.read_term ctxt) funcs
val (_, lthy') = reg_and_proove_time_func theory fterms
(case thms of NONE => get_terms theory (hd fterms)
| SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
- conv topConv true
+ true
in lthy'
end
(* Convert function into its timing function (called by command) with termination proof provided by user*)
-fun reg_time_function_cmd (funcs, thms) conv topConv (theory: theory) =
+fun reg_time_function_cmd (funcs, thms) (theory: theory) =
let
val ctxt = Proof_Context.init_global theory
val fterms = map (Syntax.read_term ctxt) funcs
val theory = reg_time_func theory fterms
(case thms of NONE => get_terms theory (hd fterms)
| SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
- conv topConv true
+ true
in theory
end
+(* Convert function into its timing function (called by command) *)
+fun reg_time_definition_cmd (funcs, thms) (theory: theory) =
+let
+ val ctxt = Proof_Context.init_global theory
+ val fterms = map (Syntax.read_term ctxt) funcs
+ val (_, lthy') = reg_and_proove_time_func theory fterms
+ (case thms of NONE => get_terms theory (hd fterms) |> check_definition |> map fix_definition
+ | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
+ true
+in lthy'
+end
+
val parser = (Scan.repeat1 Parse.prop) -- (Scan.option (Parse.keyword_improper "equations" -- Parse.thms1 >> snd))
-val _ = Outer_Syntax.command @{command_keyword "define_time_fun"}
+val _ = Outer_Syntax.command @{command_keyword "time_fun"}
"Defines runtime function of a function"
- (parser >> (fn p => Toplevel.theory (reg_time_fun_cmd p converter top_converter)))
+ (parser >> (fn p => Toplevel.theory (reg_time_fun_cmd p)))
-val _ = Outer_Syntax.command @{command_keyword "define_time_function"}
+val _ = Outer_Syntax.command @{command_keyword "time_function"}
"Defines runtime function of a function"
- (parser >> (fn p => Toplevel.theory (reg_time_function_cmd p converter top_converter)))
+ (parser >> (fn p => Toplevel.theory (reg_time_function_cmd p)))
+
+val _ = Outer_Syntax.command @{command_keyword "time_definition"}
+ "Defines runtime function of a definition"
+ (parser >> (fn p => Toplevel.theory (reg_time_definition_cmd p)))
end
--- a/src/HOL/Data_Structures/Define_Time_Function.thy Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy Mon Mar 25 10:16:14 2024 +0100
@@ -8,10 +8,11 @@
theory Define_Time_Function
imports Main
- keywords "define_time_fun" :: thy_decl
- and "define_time_function" :: thy_goal
+ keywords "time_fun" :: thy_decl
+ and "time_function" :: thy_goal
+ and "time_definition" :: thy_goal
and "equations"
- and "define_time_0" :: thy_decl
+ and "time_fun_0" :: thy_decl
begin
ML_file Define_Time_0.ML
@@ -31,17 +32,17 @@
The constant-time assumption for \<open>(=)\<close> is justified for recursive data types such as lists and trees
as long as the comparison is of the form \<open>t = c\<close> where \<open>c\<close> is a constant term, for example \<open>xs = []\<close>.\<close>
-define_time_0 "(+)"
-define_time_0 "(-)"
-define_time_0 "(*)"
-define_time_0 "(/)"
-define_time_0 "(div)"
-define_time_0 "(<)"
-define_time_0 "(\<le>)"
-define_time_0 "Not"
-define_time_0 "(\<and>)"
-define_time_0 "(\<or>)"
-define_time_0 "Num.numeral_class.numeral"
-define_time_0 "(=)"
+time_fun_0 "(+)"
+time_fun_0 "(-)"
+time_fun_0 "(*)"
+time_fun_0 "(/)"
+time_fun_0 "(div)"
+time_fun_0 "(<)"
+time_fun_0 "(\<le>)"
+time_fun_0 "Not"
+time_fun_0 "(\<and>)"
+time_fun_0 "(\<or>)"
+time_fun_0 "Num.numeral_class.numeral"
+time_fun_0 "(=)"
end
\ No newline at end of file
--- a/src/HOL/Data_Structures/Leftist_Heap.thy Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Mon Mar 25 10:16:14 2024 +0100
@@ -160,16 +160,16 @@
subsection "Complexity"
text \<open>Auxiliary time functions (which are both 0):\<close>
-define_time_fun mht
-define_time_fun node
+time_fun mht
+time_fun node
lemma T_mht_0[simp]: "T_mht t = 0"
by(cases t)auto
text \<open>Define timing function\<close>
-define_time_fun merge
-define_time_fun insert
-define_time_fun del_min
+time_fun merge
+time_fun insert
+time_fun del_min
lemma T_merge_min_height: "ltree l \<Longrightarrow> ltree r \<Longrightarrow> T_merge l r \<le> min_height l + min_height r + 1"
proof(induction l r rule: merge.induct)
--- a/src/HOL/Data_Structures/Queue_2Lists.thy Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy Mon Mar 25 10:16:14 2024 +0100
@@ -59,10 +59,10 @@
text \<open>Running times:\<close>
-define_time_fun norm
-define_time_fun enq
-define_time_fun tl
-define_time_fun deq
+time_fun norm
+time_fun enq
+time_fun tl
+time_fun deq
lemma T_tl_0: "T_tl xs = 0"
by(cases xs)auto
--- a/src/HOL/Data_Structures/Reverse.thy Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Reverse.thy Mon Mar 25 10:16:14 2024 +0100
@@ -2,8 +2,8 @@
imports Define_Time_Function
begin
-define_time_fun append
-define_time_fun rev
+time_fun append
+time_fun rev
lemma T_append: "T_append xs ys = length xs + 1"
by(induction xs) auto
@@ -21,7 +21,7 @@
lemma itrev_Nil: "itrev xs [] = rev xs"
by(simp add: itrev)
-define_time_fun itrev
+time_fun itrev
lemma T_itrev: "T_itrev xs ys = length xs + 1"
by(induction xs arbitrary: ys) auto
--- a/src/HOL/Data_Structures/Set2_Join.thy Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Set2_Join.thy Mon Mar 25 10:16:14 2024 +0100
@@ -81,36 +81,36 @@
subsection "\<open>split\<close>"
-fun split :: "('a*'b)tree \<Rightarrow> 'a \<Rightarrow> ('a*'b)tree \<times> bool \<times> ('a*'b)tree" where
-"split Leaf k = (Leaf, False, Leaf)" |
-"split (Node l (a, _) r) x =
+fun split :: "'a \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree \<times> bool \<times> ('a*'b)tree" where
+"split x Leaf = (Leaf, False, Leaf)" |
+"split x (Node l (a, _) r) =
(case cmp x a of
- LT \<Rightarrow> let (l1,b,l2) = split l x in (l1, b, join l2 a r) |
- GT \<Rightarrow> let (r1,b,r2) = split r x in (join l a r1, b, r2) |
+ LT \<Rightarrow> let (l1,b,l2) = split x l in (l1, b, join l2 a r) |
+ GT \<Rightarrow> let (r1,b,r2) = split x r in (join l a r1, b, r2) |
EQ \<Rightarrow> (l, True, r))"
-lemma split: "split t x = (l,b,r) \<Longrightarrow> bst t \<Longrightarrow>
+lemma split: "split x t = (l,b,r) \<Longrightarrow> bst t \<Longrightarrow>
set_tree l = {a \<in> set_tree t. a < x} \<and> set_tree r = {a \<in> set_tree t. x < a}
\<and> (b = (x \<in> set_tree t)) \<and> bst l \<and> bst r"
proof(induction t arbitrary: l b r rule: tree2_induct)
case Leaf thus ?case by simp
next
case (Node y a b z l c r)
- consider (LT) l1 xin l2 where "(l1,xin,l2) = split y x"
- and "split \<langle>y, (a, b), z\<rangle> x = (l1, xin, join l2 a z)" and "cmp x a = LT"
- | (GT) r1 xin r2 where "(r1,xin,r2) = split z x"
- and "split \<langle>y, (a, b), z\<rangle> x = (join y a r1, xin, r2)" and "cmp x a = GT"
- | (EQ) "split \<langle>y, (a, b), z\<rangle> x = (y, True, z)" and "cmp x a = EQ"
+ consider (LT) l1 xin l2 where "(l1,xin,l2) = split x y"
+ and "split x \<langle>y, (a, b), z\<rangle> = (l1, xin, join l2 a z)" and "cmp x a = LT"
+ | (GT) r1 xin r2 where "(r1,xin,r2) = split x z"
+ and "split x \<langle>y, (a, b), z\<rangle> = (join y a r1, xin, r2)" and "cmp x a = GT"
+ | (EQ) "split x \<langle>y, (a, b), z\<rangle> = (y, True, z)" and "cmp x a = EQ"
by (force split: cmp_val.splits prod.splits if_splits)
thus ?case
proof cases
case (LT l1 xin l2)
- with Node.IH(1)[OF \<open>(l1,xin,l2) = split y x\<close>[symmetric]] Node.prems
+ with Node.IH(1)[OF \<open>(l1,xin,l2) = split x y\<close>[symmetric]] Node.prems
show ?thesis by (force intro!: bst_join)
next
case (GT r1 xin r2)
- with Node.IH(2)[OF \<open>(r1,xin,r2) = split z x\<close>[symmetric]] Node.prems
+ with Node.IH(2)[OF \<open>(r1,xin,r2) = split x z\<close>[symmetric]] Node.prems
show ?thesis by (force intro!: bst_join)
next
case EQ
@@ -118,7 +118,7 @@
qed
qed
-lemma split_inv: "split t x = (l,b,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
+lemma split_inv: "split x t = (l,b,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
proof(induction t arbitrary: l b r rule: tree2_induct)
case Leaf thus ?case by simp
next
@@ -132,7 +132,7 @@
subsection "\<open>insert\<close>"
definition insert :: "'a \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"insert x t = (let (l,_,r) = split t x in join l x r)"
+"insert x t = (let (l,_,r) = split x t in join l x r)"
lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = {x} \<union> set_tree t"
by(auto simp add: insert_def split split: prod.split)
@@ -147,7 +147,7 @@
subsection "\<open>delete\<close>"
definition delete :: "'a \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"delete x t = (let (l,_,r) = split t x in join2 l r)"
+"delete x t = (let (l,_,r) = split x t in join2 l r)"
lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete x t) = set_tree t - {x}"
by(auto simp: delete_def split split: prod.split)
@@ -166,7 +166,7 @@
(if t1 = Leaf then t2 else
if t2 = Leaf then t1 else
case t1 of Node l1 (a, _) r1 \<Rightarrow>
- let (l2,_ ,r2) = split t2 a;
+ let (l2,_ ,r2) = split a t2;
l' = union l1 l2; r' = union r1 r2
in join l' a r')"
@@ -202,7 +202,7 @@
(if t1 = Leaf then Leaf else
if t2 = Leaf then Leaf else
case t1 of Node l1 (a, _) r1 \<Rightarrow>
- let (l2,b,r2) = split t2 a;
+ let (l2,b,r2) = split a t2;
l' = inter l1 l2; r' = inter r1 r2
in if b then join l' a r' else join2 l' r')"
@@ -224,7 +224,7 @@
case False
let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
have *: "a \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
- obtain l2 b r2 where sp: "split t2 a = (l2,b,r2)" using prod_cases3 by blast
+ obtain l2 b r2 where sp: "split a t2 = (l2,b,r2)" using prod_cases3 by blast
let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?A = "if b then {a} else {}"
have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?A" and
**: "?L2 \<inter> ?R2 = {}" "a \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
@@ -267,7 +267,7 @@
(if t1 = Leaf then Leaf else
if t2 = Leaf then t1 else
case t2 of Node l2 (a, _) r2 \<Rightarrow>
- let (l1,_,r1) = split t1 a;
+ let (l1,_,r1) = split a t1;
l' = diff l1 l2; r' = diff r1 r2
in join2 l' r')"
@@ -288,7 +288,7 @@
next
case False
let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
- obtain l1 b r1 where sp: "split t1 a = (l1,b,r1)" using prod_cases3 by blast
+ obtain l1 b r1 where sp: "split a t1 = (l1,b,r1)" using prod_cases3 by blast
let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?A = "if b then {a} else {}"
have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?A" and
**: "a \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
--- a/src/HOL/Data_Structures/Time_Funs.thy Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy Mon Mar 25 10:16:14 2024 +0100
@@ -48,8 +48,8 @@
lemmas [simp del] = T_nth.simps
-define_time_fun take
-define_time_fun drop
+time_fun take
+time_fun drop
lemma T_take_eq: "T_take n xs = min n (length xs) + 1"
by (induction xs arbitrary: n) (auto split: nat.splits)
--- a/src/HOL/Data_Structures/Tree23_of_List.thy Sat Mar 23 18:55:38 2024 +0100
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy Mon Mar 25 10:16:14 2024 +0100
@@ -118,10 +118,10 @@
subsection "Linear running time"
-define_time_fun join_adj
-define_time_fun join_all
-define_time_fun leaves
-define_time_fun tree23_of_list
+time_fun join_adj
+time_fun join_all
+time_fun leaves
+time_fun tree23_of_list
lemma T_join_adj: "not_T ts \<Longrightarrow> T_join_adj ts \<le> len ts div 2"
by(induction ts rule: T_join_adj.induct) auto
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat Mar 23 18:55:38 2024 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 25 10:16:14 2024 +0100
@@ -228,6 +228,25 @@
args = "-N -X large -X slow",
afp = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
+ Remote_Build("AFP old2", "lrzcloud2", history = 120,
+ java_heap = "8g",
+ options = "-m32 -M1x5 -t AFP" +
+ " -e ISABELLE_GHC=ghc" +
+ " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" +
+ " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
+ " -e ISABELLE_SMLNJ=sml",
+ args = "-a -X large -X slow",
+ afp = true,
+ detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
+ count = () => if (Date.now().unix_epoch_day % 2 == 0) 1 else 0),
+ Remote_Build("AFP old2", "lrzcloud2",
+ java_heap = "8g",
+ options = "-m64 -M8 -U30000 -s10 -t AFP",
+ args = "-g large -g slow",
+ afp = true,
+ bulky = true,
+ detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
+ count = () => if (Date.now().unix_epoch_day % 2 == 1) 1 else 0),
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'",
@@ -369,27 +388,7 @@
}
val remote_builds2: List[List[Remote_Build]] =
- List(
- List(
- Remote_Build("AFP", "lrzcloud2", history = 120,
- java_heap = "8g",
- options = "-m32 -M1x5 -t AFP" +
- " -e ISABELLE_GHC=ghc" +
- " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" +
- " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
- " -e ISABELLE_SMLNJ=sml",
- args = "-a -X large -X slow",
- afp = true,
- detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
- count = () => if (Date.now().unix_epoch_day % 2 == 0) 1 else 0),
- Remote_Build("AFP", "lrzcloud2",
- java_heap = "8g",
- options = "-m64 -M8 -U30000 -s10 -t AFP",
- args = "-g large -g slow",
- afp = true,
- bulky = true,
- detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
- count = () => if (Date.now().unix_epoch_day % 2 == 1) 1 else 0)))
+ List()
def remote_build_history(
rev: String,