Job 1699

CakeML:2c2b4c83b857a26ba3318c77300e798965c5dfed
  Refix parsing/fromSexp given unlisting of theorems in quantHeuristics [Dec 22 06:37:04]
HOL:9d2d0e89bd165c1ea71279ed6f2ed14ed6c15d27
  Add comment to explain function of a somewhat mysterious file [Dec 20 05:01:21]
Machine:oven3+4.19.67.1.amd64-smp+
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Dec 22 07:53:15 Claimed job
Dec 22 07:53:29 Building+HOL
Dec 22 08:12:46 Starting+developers
Dec 22 08:12:54 Finished+developers++++++++++++++++++++++++++++++++++++++++8.26+161652
Dec 22 08:12:55 Starting+developers/bin
Dec 22 08:13:05 Finished+developers/bin++++++++++++++++++++++++++++++++++++10.06+673640
Dec 22 08:13:05 Starting+semantics/ffi
Dec 22 08:13:24 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++18.92+234300
Dec 22 08:13:24 Starting+semantics
Dec 22 08:16:42 Finished+semantics+++++++++++++++++++++++++++++++++++++++++197.14+1271712
Dec 22 08:16:42 Starting+semantics/proofs
Dec 22 08:24:17 Finished+semantics/proofs++++++++++++++++++++++++++++++++++454.74+1011068
Dec 22 08:24:17 Starting+semantics/alt_semantics
Dec 22 08:24:41 Finished+semantics/alt_semantics+++++++++++++++++++++++++++23.84+420504
Dec 22 08:24:41 Starting+semantics/alt_semantics/proofs
Dec 22 08:29:49 Finished+semantics/alt_semantics/proofs++++++++++++++++++++307.73+977184
Dec 22 08:29:50 Starting+basis/pure
Dec 22 08:35:41 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++351.46+869240
Dec 22 08:35:42 Starting+translator
Dec 22 08:41:27 Finished+translator++++++++++++++++++++++++++++++++++++++++345.55+1483004
Dec 22 08:41:27 Starting+compiler/parsing
Dec 22 08:44:08 Finished+compiler/parsing++++++++++++++++++++++++++++++++++159.98+2302752
Dec 22 08:44:08 Starting+characteristic
Dec 22 08:56:15 Finished+characteristic++++++++++++++++++++++++++++++++++++726.83+1908340
Dec 22 08:56:15 Starting+translator/monadic
Dec 22 08:59:44 Finished+translator/monadic++++++++++++++++++++++++++++++++208.86+1777744
Dec 22 08:59:44 Starting+basis
Dec 22 10:39:15 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++5970.62+21774712
Dec 22 10:39:16 Starting+compiler/inference
Dec 22 10:41:55 Finished+compiler/inference++++++++++++++++++++++++++++++++158.94+1195184
Dec 22 10:41:55 Starting+compiler/backend/reg_alloc
Dec 22 10:43:58 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++123.23+1427260
Dec 22 10:43:59 Starting+compiler/backend/gc
Dec 22 10:50:49 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++410.63+1990040
Dec 22 10:50:50 Starting+compiler/backend
Dec 22 10:59:36 Finished+compiler/backend++++++++++++++++++++++++++++++++++525.84+2387260
Dec 22 10:59:36 Starting+compiler/encoders/asm
Dec 22 11:00:25 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++48.66+783632
Dec 22 11:00:25 Starting+compiler/encoders/x64
Dec 22 11:02:39 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++133.96+1029364
Dec 22 11:02:39 Starting+compiler/encoders/arm7
Dec 22 11:07:13 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++273.64+1599620
Dec 22 11:07:14 Starting+compiler/encoders/arm8
Dec 22 11:08:33 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++79.30+933204
Dec 22 11:08:33 Starting+compiler/encoders/mips
Dec 22 11:11:43 Finished+compiler/encoders/mips++++++++++++++++++++++++++++189.96+1340876
Dec 22 11:11:44 Starting+compiler/encoders/riscv
Dec 22 11:15:24 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++220.34+1228244
Dec 22 11:15:24 Starting+compiler/encoders/ag32
Dec 22 11:16:04 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++39.44+881832
Dec 22 11:16:04 Starting+compiler/backend/x64
Dec 22 11:16:46 Finished+compiler/backend/x64++++++++++++++++++++++++++++++41.84+1354672
Dec 22 11:16:47 Starting+compiler/backend/arm7
Dec 22 11:17:32 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++45.39+1517996
Dec 22 11:17:32 Starting+compiler/backend/arm8
Dec 22 11:18:16 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++42.94+1450992
Dec 22 11:18:16 Starting+compiler/backend/mips
Dec 22 11:19:02 Finished+compiler/backend/mips+++++++++++++++++++++++++++++46.45+1492404
Dec 22 11:19:03 Starting+compiler/backend/riscv
Dec 22 11:19:44 Finished+compiler/backend/riscv++++++++++++++++++++++++++++41.16+1376248
Dec 22 11:19:44 Starting+compiler/backend/ag32
Dec 22 11:22:08 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++143.34+1653840
Dec 22 11:22:08 Starting+compiler/parsing/proofs
Dec 22 11:30:25 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++496.46+1238512
Dec 22 11:30:25 Starting+compiler/inference/proofs
Dec 22 11:35:47 Finished+compiler/inference/proofs+++++++++++++++++++++++++322.05+1061212
Dec 22 11:35:47 Starting+compiler/backend/semantics
Dec 22 12:37:22 Finished+compiler/backend/semantics++++++++++++++++++++++++3692.83+2415684
Dec 22 12:37:22 Starting+compiler/backend/reg_alloc/proofs
Dec 22 12:44:46 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++443.74+1033432
Dec 22 12:44:47 Starting+compiler/backend/proofs
Dec 22 14:25:08 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6020.20+13784600
Dec 22 14:25:08 Starting+compiler/backend/serialiser
Dec 22 14:27:40 Finished+compiler/backend/serialiser+++++++++++++++++++++++152.06+1969196
Dec 22 14:27:41 Starting+compiler/encoders/x64/proofs
Dec 22 14:49:16 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1295.05+4309580
Dec 22 14:49:16 Starting+compiler/encoders/arm7/proofs
Dec 22 15:18:37 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1760.54+4883180
Dec 22 15:18:37 Starting+compiler/encoders/arm8/proofs
Dec 22 15:34:09 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++930.94+1225184
Dec 22 15:34:09 Starting+compiler/encoders/mips/proofs
Dec 22 15:56:46 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1357.30+2110668
Dec 22 15:56:47 Starting+compiler/encoders/riscv/proofs
Dec 22 16:17:01 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1214.26+1224392
Dec 22 16:17:01 Starting+compiler/encoders/ag32/proofs
Dec 22 16:22:45 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++343.23+859148
Dec 22 16:22:45 Starting+compiler/backend/x64/proofs
Dec 22 16:23:33 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++47.91+1568572
Dec 22 16:23:33 Starting+compiler/backend/arm7/proofs
Dec 22 16:24:21 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++47.81+1459048
Dec 22 16:24:22 Starting+compiler/backend/arm8/proofs
Dec 22 16:25:11 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++49.51+1604188
Dec 22 16:25:12 Starting+compiler/backend/mips/proofs
Dec 22 16:26:02 Finished+compiler/backend/mips/proofs++++++++++++++++++++++50.80+1691676
Dec 22 16:26:03 Starting+compiler/backend/riscv/proofs
Dec 22 16:26:51 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++48.09+2154648
Dec 22 16:26:51 Starting+compiler/backend/ag32/proofs
Dec 22 16:55:06 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1694.01+2838748
Dec 22 16:55:06 Starting+compiler/proofs
Dec 22 16:59:19 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++252.48+3608444
Dec 22 16:59:19 Starting+candle/set-theory
Dec 22 17:00:17 Finished+candle/set-theory+++++++++++++++++++++++++++++++++57.79+729596
Dec 22 17:00:17 Starting+candle/syntax-lib
Dec 22 17:00:42 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++24.53+487328
Dec 22 17:00:42 Starting+candle/standard/syntax
Dec 22 17:04:34 Finished+candle/standard/syntax++++++++++++++++++++++++++++232.21+1073000
Dec 22 17:04:35 Starting+candle/standard/semantics
Dec 22 17:08:19 Finished+candle/standard/semantics+++++++++++++++++++++++++223.80+1595096
Dec 22 17:08:19 Starting+candle/standard/monadic
Dec 22 17:11:58 Finished+candle/standard/monadic+++++++++++++++++++++++++++218.66+1202884
Dec 22 17:11:58 Starting+candle/standard/ml_kernel
Dec 22 17:23:31 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++692.89+2957016
Dec 22 17:23:31 Starting+candle/overloading/syntax
Dec 22 17:30:03 Finished+candle/overloading/syntax+++++++++++++++++++++++++391.40+1576268
Dec 22 17:30:03 Starting+candle/overloading/semantics
Dec 22 17:55:49 Finished+candle/overloading/semantics++++++++++++++++++++++1544.21+2916016
Dec 22 17:55:50 Starting+pancake
Dec 22 17:59:46 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++236.15+2276660
Dec 22 17:59:46 Starting+pancake/ffi
Dec 22 17:59:47 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.46+7692
Dec 22 17:59:47 Starting+pancake/semantics
Dec 22 18:04:36 Finished+pancake/semantics+++++++++++++++++++++++++++++++++288.72+1379796
Dec 22 18:04:36 Starting+pancake/proofs
Dec 22 18:30:28 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1551.25+6770080
Dec 22 18:30:28 Starting+characteristic/examples
Dec 22 18:33:19 Finished+characteristic/examples+++++++++++++++++++++++++++171.00+3060240
Dec 22 18:33:19 Starting+tutorial/solutions
Dec 22 19:08:01 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2080.95+8867660
Dec 22 19:08:01 Starting+translator/monadic/examples
Dec 22 19:13:37 Finished+translator/monadic/examples+++++++++++++++++++++++336.43+2765804
Dec 22 19:13:38 Starting+examples
Dec 22 19:31:11 Finished+examples++++++++++++++++++++++++++++++++++++++++++1053.52+4084388
Dec 22 19:31:12 Starting+examples/compilation/x64
Dec 23 00:59:50 Finished+examples/compilation/x64++++++++++++++++++++++++++19718.34+20283004
Dec 23 00:59:50 Starting+examples/compilation/x64/proofs
Dec 23 01:03:35 Finished+examples/compilation/x64/proofs+++++++++++++++++++224.79+3472328
Dec 23 01:03:36 Starting+examples/compilation/ag32
Dec 23 02:19:54 Finished+examples/compilation/ag32+++++++++++++++++++++++++4578.30+8753032
Dec 23 02:19:55 Starting+examples/compilation/ag32/proofs
Dec 23 02:21:28 Finished+examples/compilation/ag32/proofs++++++++++++++++++93.42+3224008
Dec 23 02:21:28 Starting+examples/cost
Dec 23 04:17:02 Finished+examples/cost+++++++++++++++++++++++++++++++++++++6933.56+9572148
Dec 23 04:17:03 Starting+examples/lpr_checker
Dec 23 04:18:44 Finished+examples/lpr_checker++++++++++++++++++++++++++++++101.21+1015580
Dec 23 04:18:44 Starting+examples/lpr_checker/array
Dec 23 05:21:32 Finished+examples/lpr_checker/array++++++++++++++++++++++++3767.60+7665312
Dec 23 05:21:32 Starting+examples/lpr_checker/array/compilation
Dec 23 08:24:39 Finished+examples/lpr_checker/array/compilation++++++++++++10986.27+38723804
Dec 23 08:24:39 Starting+examples/lpr_checker/array/compilation/proofs
Dec 23 08:27:11 Finished+examples/lpr_checker/array/compilation/proofs+++++151.82+6253368
Dec 23 08:27:12 Starting+examples/opentheory
Dec 23 08:47:49 Finished+examples/opentheory+++++++++++++++++++++++++++++++1237.46+4008584
Dec 23 08:47:50 Starting+examples/opentheory
Dec 23 08:47:52 Finished+examples/opentheory+++++++++++++++++++++++++++++++2.50+33296
Dec 23 08:47:52 Starting+examples/opentheory/compilation
Dec 23 10:09:06 Finished+examples/opentheory/compilation+++++++++++++++++++4872.89+40981376
Dec 23 10:09:06 Starting+examples/opentheory/compilation/proofs
Dec 23 10:10:46 Finished+examples/opentheory/compilation/proofs++++++++++++99.80+2976212
Dec 23 10:10:46 Starting+examples/opentheory/compilation/ag32
Dec 23 11:37:34 Finished+examples/opentheory/compilation/ag32++++++++++++++5206.97+33948392
Dec 23 11:37:34 Starting+examples/opentheory/compilation/ag32/proofs
Dec 23 11:41:03 Finished+examples/opentheory/compilation/ag32/proofs+++++++208.80+6736048
Dec 23 11:41:03 Starting+examples/sat_encodings
Dec 23 11:44:53 Finished+examples/sat_encodings++++++++++++++++++++++++++++230.13+875316
Dec 23 11:44:54 Starting+examples/sat_encodings/case_studies
Dec 23 11:48:14 Finished+examples/sat_encodings/case_studies+++++++++++++++199.94+806780
Dec 23 11:48:14 Starting+examples/sat_encodings/translation
Dec 23 12:00:02 Finished+examples/sat_encodings/translation++++++++++++++++708.16+5306884
Dec 23 12:00:03 Starting+examples/sat_encodings/translation/compilation
Dec 23 13:27:03 Finished+examples/sat_encodings/translation/compilation++++5220.17+27898760
Dec 23 13:27:03 Starting+translator/okasaki-examples
Dec 23 13:36:26 Finished+translator/okasaki-examples+++++++++++++++++++++++562.58+1898348
Dec 23 13:36:26 Starting+translator/other-examples
Dec 23 13:40:01 Finished+translator/other-examples+++++++++++++++++++++++++214.11+1607360
Dec 23 13:40:01 Starting+compiler/parsing/tests
Dec 23 13:41:06 Finished+compiler/parsing/tests++++++++++++++++++++++++++++64.90+595376
Dec 23 13:41:06 Starting+compiler/inference/tests
Dec 23 13:56:53 Finished+compiler/inference/tests++++++++++++++++++++++++++946.21+5495340
Dec 23 13:56:53 Starting+compiler/bootstrap/translation
Dec 23 19:32:05 Finished+compiler/bootstrap/translation++++++++++++++++++++20111.69+24667984
Dec 23 19:32:05 Starting+unverified/sexpr-bootstrap/x64/64
Dec 23 19:51:59 Finished+unverified/sexpr-bootstrap/x64/64+++++++++++++++++1192.69+9413308
Dec 23 19:51:59 Starting+unverified/sexpr-bootstrap/x64/32
Dec 23 20:09:29 Finished+unverified/sexpr-bootstrap/x64/32+++++++++++++++++1049.22+8364732
Dec 23 20:09:29 Starting+compiler/benchmarks
Dec 23 20:09:34 Finished+compiler/benchmarks+++++++++++++++++++++++++++++++4.41+43524
Dec 23 20:09:34 Starting+compiler/bootstrap/compilation/x64/64
Dec 24 23:23:50 Finished+compiler/bootstrap/compilation/x64/64+++++++++++++98055.59+77440704
Dec 24 23:23:51 Starting+compiler/bootstrap/compilation/x64/64/proofs
Dec 24 23:28:23 Finished+compiler/bootstrap/compilation/x64/64/proofs++++++272.69+15234148
Dec 24 23:28:24 Starting+compiler/bootstrap/compilation/x64/32
Dec 26 02:13:03 Finished+compiler/bootstrap/compilation/x64/32+++++++++++++96278.04+110101100
Dec 26 02:13:03 Starting+compiler/bootstrap/compilation/x64/32/proofs
Dec 26 02:17:16 Finished+compiler/bootstrap/compilation/x64/32/proofs++++++252.48+16056520
Dec 26 02:17:16 Starting+compiler/bootstrap/compilation/ag32/32
Dec 27 03:59:44 Finished+compiler/bootstrap/compilation/ag32/32++++++++++++92547.37+111208604
Dec 27 03:59:44 Starting+compiler/bootstrap/compilation/ag32/32/proofs
Dec 27 04:19:40 Finished+compiler/bootstrap/compilation/ag32/32/proofs+++++1196.22+37732172
Dec 27 04:19:40 SUCCESS