Job 1700

CakeML:2c2b4c83b857a26ba3318c77300e798965c5dfed
  Refix parsing/fromSexp given unlisting of theorems in quantHeuristics [Dec 22 06:37:04]
HOL:288eed203f9e91e52a1707519ea31e41041b2f48
  Move more examples into parallel build process [Dec 23 06:36:48]
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 27 09:19:59 Claimed job
Dec 27 09:20:11 Building+HOL
Dec 27 09:39:45 Starting+developers
Dec 27 09:39:53 Finished+developers++++++++++++++++++++++++++++++++++++++++8.00+144864
Dec 27 09:39:53 Starting+developers/bin
Dec 27 09:40:03 Finished+developers/bin++++++++++++++++++++++++++++++++++++9.46+677604
Dec 27 09:40:03 Starting+semantics/ffi
Dec 27 09:40:23 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++19.07+237564
Dec 27 09:40:23 Starting+semantics
Dec 27 09:43:34 Finished+semantics+++++++++++++++++++++++++++++++++++++++++190.67+1211112
Dec 27 09:43:34 Starting+semantics/proofs
Dec 27 09:51:12 Finished+semantics/proofs++++++++++++++++++++++++++++++++++457.74+1522596
Dec 27 09:51:12 Starting+semantics/alt_semantics
Dec 27 09:51:37 Finished+semantics/alt_semantics+++++++++++++++++++++++++++24.70+402352
Dec 27 09:51:37 Starting+semantics/alt_semantics/proofs
Dec 27 09:56:51 Finished+semantics/alt_semantics/proofs++++++++++++++++++++313.91+1039504
Dec 27 09:56:52 Starting+basis/pure
Dec 27 10:02:50 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++358.31+818988
Dec 27 10:02:50 Starting+translator
Dec 27 10:08:36 Finished+translator++++++++++++++++++++++++++++++++++++++++345.61+1718368
Dec 27 10:08:36 Starting+compiler/parsing
Dec 27 10:11:13 Finished+compiler/parsing++++++++++++++++++++++++++++++++++156.03+2154472
Dec 27 10:11:13 Starting+characteristic
Dec 27 10:23:03 Finished+characteristic++++++++++++++++++++++++++++++++++++710.06+2099352
Dec 27 10:23:04 Starting+translator/monadic
Dec 27 10:26:26 Finished+translator/monadic++++++++++++++++++++++++++++++++202.60+1492612
Dec 27 10:26:27 Starting+basis
Dec 27 12:04:05 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++5857.59+12921396
Dec 27 12:04:05 Starting+compiler/inference
Dec 27 12:06:51 Finished+compiler/inference++++++++++++++++++++++++++++++++165.43+963500
Dec 27 12:06:51 Starting+compiler/backend/reg_alloc
Dec 27 12:08:56 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++125.35+1242188
Dec 27 12:08:57 Starting+compiler/backend/gc
Dec 27 12:15:46 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++409.27+1581428
Dec 27 12:15:47 Starting+compiler/backend
Dec 27 12:24:39 Finished+compiler/backend++++++++++++++++++++++++++++++++++532.07+1978812
Dec 27 12:24:39 Starting+compiler/encoders/asm
Dec 27 12:25:30 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++50.41+771812
Dec 27 12:25:30 Starting+compiler/encoders/x64
Dec 27 12:27:45 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++134.90+991276
Dec 27 12:27:45 Starting+compiler/encoders/arm7
Dec 27 12:32:21 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++275.22+1457016
Dec 27 12:32:21 Starting+compiler/encoders/arm8
Dec 27 12:33:41 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++79.58+613508
Dec 27 12:33:41 Starting+compiler/encoders/mips
Dec 27 12:36:47 Finished+compiler/encoders/mips++++++++++++++++++++++++++++185.12+1344300
Dec 27 12:36:47 Starting+compiler/encoders/riscv
Dec 27 12:40:33 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++226.10+1305764
Dec 27 12:40:33 Starting+compiler/encoders/ag32
Dec 27 12:41:11 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++37.58+677692
Dec 27 12:41:11 Starting+compiler/backend/x64
Dec 27 12:41:53 Finished+compiler/backend/x64++++++++++++++++++++++++++++++41.36+1417236
Dec 27 12:41:53 Starting+compiler/backend/arm7
Dec 27 12:42:38 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++44.81+1673304
Dec 27 12:42:38 Starting+compiler/backend/arm8
Dec 27 12:43:21 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++42.80+1409140
Dec 27 12:43:22 Starting+compiler/backend/mips
Dec 27 12:44:02 Finished+compiler/backend/mips+++++++++++++++++++++++++++++40.24+1446776
Dec 27 12:44:02 Starting+compiler/backend/riscv
Dec 27 12:44:44 Finished+compiler/backend/riscv++++++++++++++++++++++++++++41.28+1428504
Dec 27 12:44:44 Starting+compiler/backend/ag32
Dec 27 12:47:13 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++148.49+1378172
Dec 27 12:47:13 Starting+compiler/parsing/proofs
Dec 27 12:55:33 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++499.28+1263812
Dec 27 12:55:33 Starting+compiler/inference/proofs
Dec 27 13:00:51 Finished+compiler/inference/proofs+++++++++++++++++++++++++317.72+1052612
Dec 27 13:00:51 Starting+compiler/backend/semantics
Dec 27 14:01:53 Finished+compiler/backend/semantics++++++++++++++++++++++++3661.79+1950520
Dec 27 14:01:54 Starting+compiler/backend/reg_alloc/proofs
Dec 27 14:09:29 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++455.44+1118984
Dec 27 14:09:29 Starting+compiler/backend/proofs
Dec 27 15:50:23 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6052.27+18413500
Dec 27 15:50:23 Starting+compiler/backend/serialiser
Dec 27 15:52:52 Finished+compiler/backend/serialiser+++++++++++++++++++++++148.05+1904316
Dec 27 15:52:52 Starting+compiler/encoders/x64/proofs
Dec 27 16:14:07 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1274.58+4588580
Dec 27 16:14:07 Starting+compiler/encoders/arm7/proofs
Dec 27 16:43:43 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1775.51+6996208
Dec 27 16:43:43 Starting+compiler/encoders/arm8/proofs
Dec 27 16:59:19 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++935.98+1462448
Dec 27 16:59:20 Starting+compiler/encoders/mips/proofs
Dec 27 17:21:53 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1353.46+2640484
Dec 27 17:21:54 Starting+compiler/encoders/riscv/proofs
Dec 27 17:42:06 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1211.86+1295892
Dec 27 17:42:06 Starting+compiler/encoders/ag32/proofs
Dec 27 17:47:48 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++341.23+895608
Dec 27 17:47:48 Starting+compiler/backend/x64/proofs
Dec 27 17:48:38 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++49.74+1523140
Dec 27 17:48:38 Starting+compiler/backend/arm7/proofs
Dec 27 17:49:29 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++50.80+1633272
Dec 27 17:49:29 Starting+compiler/backend/arm8/proofs
Dec 27 17:50:19 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++48.98+1522712
Dec 27 17:50:19 Starting+compiler/backend/mips/proofs
Dec 27 17:51:09 Finished+compiler/backend/mips/proofs++++++++++++++++++++++49.87+1297484
Dec 27 17:51:09 Starting+compiler/backend/riscv/proofs
Dec 27 17:52:00 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++50.23+1517820
Dec 27 17:52:00 Starting+compiler/backend/ag32/proofs
Dec 27 18:19:47 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1666.58+3631848
Dec 27 18:19:47 Starting+compiler/proofs
Dec 27 18:24:01 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++254.04+3721540
Dec 27 18:24:02 Starting+candle/set-theory
Dec 27 18:24:58 Finished+candle/set-theory+++++++++++++++++++++++++++++++++56.00+707824
Dec 27 18:24:58 Starting+candle/syntax-lib
Dec 27 18:25:21 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++22.71+447504
Dec 27 18:25:21 Starting+candle/standard/syntax
Dec 27 18:29:09 Finished+candle/standard/syntax++++++++++++++++++++++++++++227.58+1031660
Dec 27 18:29:10 Starting+candle/standard/semantics
Dec 27 18:32:53 Finished+candle/standard/semantics+++++++++++++++++++++++++223.65+1260192
Dec 27 18:32:54 Starting+candle/standard/monadic
Dec 27 18:36:35 Finished+candle/standard/monadic+++++++++++++++++++++++++++221.20+1084172
Dec 27 18:36:35 Starting+candle/standard/ml_kernel
Dec 27 18:48:04 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++688.67+3827456
Dec 27 18:48:05 Starting+candle/overloading/syntax
Dec 27 18:54:37 Finished+candle/overloading/syntax+++++++++++++++++++++++++392.53+1123752
Dec 27 18:54:38 Starting+candle/overloading/semantics
Dec 27 19:19:22 Finished+candle/overloading/semantics++++++++++++++++++++++1484.37+3003748
Dec 27 19:19:22 Starting+pancake
Dec 27 19:23:22 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++239.41+2821268
Dec 27 19:23:22 Starting+pancake/ffi
Dec 27 19:23:23 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.47+9688
Dec 27 19:23:23 Starting+pancake/semantics
Dec 27 19:28:13 Finished+pancake/semantics+++++++++++++++++++++++++++++++++289.55+1140468
Dec 27 19:28:13 Starting+pancake/proofs
Dec 27 19:53:41 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1527.25+7008996
Dec 27 19:53:41 Starting+characteristic/examples
Dec 27 19:56:54 Finished+characteristic/examples+++++++++++++++++++++++++++192.75+3408700
Dec 27 19:56:54 Starting+tutorial/solutions
Dec 27 20:32:00 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2105.02+9404160
Dec 27 20:32:00 Starting+translator/monadic/examples
Dec 27 20:37:47 Finished+translator/monadic/examples+++++++++++++++++++++++347.02+2842792
Dec 27 20:37:48 Starting+examples
Dec 27 20:55:24 Finished+examples++++++++++++++++++++++++++++++++++++++++++1056.48+3451112
Dec 27 20:55:25 Starting+examples/compilation/x64
Dec 28 02:21:46 Finished+examples/compilation/x64++++++++++++++++++++++++++19580.53+20559712
Dec 28 02:21:46 Starting+examples/compilation/x64/proofs
Dec 28 02:25:33 Finished+examples/compilation/x64/proofs+++++++++++++++++++226.94+3949380
Dec 28 02:25:33 Starting+examples/compilation/ag32
Dec 28 03:43:06 Finished+examples/compilation/ag32+++++++++++++++++++++++++4652.63+9476052
Dec 28 03:43:07 Starting+examples/compilation/ag32/proofs
Dec 28 03:44:43 Finished+examples/compilation/ag32/proofs++++++++++++++++++96.27+2842792
Dec 28 03:44:43 Starting+examples/cost
Dec 28 05:44:18 Finished+examples/cost+++++++++++++++++++++++++++++++++++++7174.34+8931760
Dec 28 05:44:18 Starting+examples/lpr_checker
Dec 28 05:45:58 Finished+examples/lpr_checker++++++++++++++++++++++++++++++99.38+942636
Dec 28 05:45:58 Starting+examples/lpr_checker/array
Dec 28 06:49:10 Finished+examples/lpr_checker/array++++++++++++++++++++++++3790.14+6389112
Dec 28 06:49:10 Starting+examples/lpr_checker/array/compilation
Dec 28 09:42:26 Finished+examples/lpr_checker/array/compilation++++++++++++10395.24+37536320
Dec 28 09:42:26 Starting+examples/lpr_checker/array/compilation/proofs
Dec 28 09:44:55 Finished+examples/lpr_checker/array/compilation/proofs+++++149.23+7506072
Dec 28 09:44:56 Starting+examples/opentheory
Dec 28 10:05:03 Finished+examples/opentheory+++++++++++++++++++++++++++++++1207.52+4226736
Dec 28 10:05:04 Starting+examples/opentheory
Dec 28 10:05:06 Finished+examples/opentheory+++++++++++++++++++++++++++++++2.53+34208
Dec 28 10:05:07 Starting+examples/opentheory/compilation
Dec 28 11:29:22 Finished+examples/opentheory/compilation+++++++++++++++++++5054.71+45645112
Dec 28 11:29:22 Starting+examples/opentheory/compilation/proofs
Dec 28 11:30:53 Finished+examples/opentheory/compilation/proofs++++++++++++90.73+4043360
Dec 28 11:30:53 Starting+examples/opentheory/compilation/ag32
Dec 28 12:53:29 Finished+examples/opentheory/compilation/ag32++++++++++++++4955.31+29706624
Dec 28 12:53:29 Starting+examples/opentheory/compilation/ag32/proofs
Dec 28 12:56:52 Finished+examples/opentheory/compilation/ag32/proofs+++++++202.87+3724180
Dec 28 12:56:53 Starting+examples/sat_encodings
Dec 28 13:00:43 Finished+examples/sat_encodings++++++++++++++++++++++++++++229.94+837560
Dec 28 13:00:43 Starting+examples/sat_encodings/case_studies
Dec 28 13:04:00 Finished+examples/sat_encodings/case_studies+++++++++++++++197.06+895472
Dec 28 13:04:01 Starting+examples/sat_encodings/translation
Dec 28 13:15:21 Finished+examples/sat_encodings/translation++++++++++++++++680.35+3832576
Dec 28 13:15:21 Starting+examples/sat_encodings/translation/compilation
Dec 28 14:42:34 Finished+examples/sat_encodings/translation/compilation++++5232.52+24368372
Dec 28 14:42:35 Starting+translator/okasaki-examples
Dec 28 14:51:51 Finished+translator/okasaki-examples+++++++++++++++++++++++556.17+1969604
Dec 28 14:51:52 Starting+translator/other-examples
Dec 28 14:55:31 Finished+translator/other-examples+++++++++++++++++++++++++219.46+1740916
Dec 28 14:55:31 Starting+compiler/parsing/tests
Dec 28 14:56:37 Finished+compiler/parsing/tests++++++++++++++++++++++++++++65.41+817924
Dec 28 14:56:37 Starting+compiler/inference/tests
Dec 28 15:12:50 Finished+compiler/inference/tests++++++++++++++++++++++++++972.35+3791872
Dec 28 15:12:50 Starting+compiler/bootstrap/translation
Dec 28 20:47:32 Finished+compiler/bootstrap/translation++++++++++++++++++++20080.96+26687932
Dec 28 20:47:32 Starting+unverified/sexpr-bootstrap/x64/64
Dec 28 21:07:23 Finished+unverified/sexpr-bootstrap/x64/64+++++++++++++++++1189.95+9972604
Dec 28 21:07:23 Starting+unverified/sexpr-bootstrap/x64/32
Dec 28 21:24:29 Finished+unverified/sexpr-bootstrap/x64/32+++++++++++++++++1025.70+8364584
Dec 28 21:24:29 Starting+compiler/benchmarks
Dec 28 21:24:34 Finished+compiler/benchmarks+++++++++++++++++++++++++++++++4.31+34208
Dec 28 21:24:34 Starting+compiler/bootstrap/compilation/x64/64
Dec 30 02:33:38 Finished+compiler/bootstrap/compilation/x64/64+++++++++++++104943.22+108869496
Dec 30 02:33:38 Starting+compiler/bootstrap/compilation/x64/64/proofs
Dec 30 02:38:21 Finished+compiler/bootstrap/compilation/x64/64/proofs++++++282.55+15398340
Dec 30 02:38:21 Starting+compiler/bootstrap/compilation/x64/32
Dec 31 02:09:51 Finished+compiler/bootstrap/compilation/x64/32+++++++++++++84688.66+107935740
Dec 31 02:09:51 Starting+compiler/bootstrap/compilation/x64/32/proofs
Dec 31 02:14:42 Finished+compiler/bootstrap/compilation/x64/32/proofs++++++290.41+12648664
Dec 31 02:14:42 Starting+compiler/bootstrap/compilation/ag32/32
Jan 01 03:05:43 Finished+compiler/bootstrap/compilation/ag32/32++++++++++++89460.14+110636824
Jan 01 03:05:43 Starting+compiler/bootstrap/compilation/ag32/32/proofs
Jan 01 03:26:05 Finished+compiler/bootstrap/compilation/ag32/32/proofs+++++1221.39+47235268
Jan 01 03:26:05 SUCCESS