equal
deleted
inserted
replaced
18 val groups: Map[String, String] = |
18 val groups: Map[String, String] = |
19 Map("large" -> "full 64-bit memory model or word arithmetic required", |
19 Map("large" -> "full 64-bit memory model or word arithmetic required", |
20 "slow" -> "CPU time much higher than 60min (on mid-range hardware)", |
20 "slow" -> "CPU time much higher than 60min (on mid-range hardware)", |
21 "very_slow" -> "elapsed time of many hours (on high-end hardware)") |
21 "very_slow" -> "elapsed time of many hours (on high-end hardware)") |
22 |
22 |
23 def groups_bulky: List[String] = List("large", "slow") |
23 val groups_bulky: List[String] = List("large", "slow") |
|
24 |
|
25 val chapter: String = "AFP" |
24 |
26 |
25 val force_partition1: List[String] = List("Category3", "HOL-ODE") |
27 val force_partition1: List[String] = List("Category3", "HOL-ODE") |
26 |
28 |
27 def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP = |
29 def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP = |
28 new AFP(options, base_dir) |
30 new AFP(options, base_dir) |