equal
deleted
inserted
replaced
|
1 (* Title: HOL/Tools/Mirabelle/mirabelle_order.ML |
|
2 Author: Martin Desharnais, MPI-INF Saarbrücken |
|
3 |
|
4 Mirabelle action: "order". |
|
5 *) |
|
6 |
|
7 structure Mirabelle_Order: MIRABELLE_ACTION = |
|
8 struct |
|
9 |
|
10 fun make_action ({timeout, ...} : Mirabelle.action_context) = |
|
11 let |
|
12 val _ = HOL_Order_Tac.tac [] |
|
13 fun run ({pre, ...} : Mirabelle.command) = |
|
14 (case Timing.timing (Mirabelle.can_apply timeout (HOL_Order_Tac.tac [])) pre of |
|
15 ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)" |
|
16 | (_, false) => "failed") |
|
17 in ("", {run = run, finalize = K ""}) end |
|
18 |
|
19 val () = Mirabelle.register_action "order" make_action |
|
20 |
|
21 end |