CakeML Regression Test

Job 1733

CakeML:a02d88700551743195a7a79ca60b98d42002b65e
  Printer test now passes [Jan 23 13:11:59]
#856 (printing)
Merging into:fe46ca072678de42c6fdfc32f40eafeb917dab02
  Fix proof broken by HOL changes making more rewrites automatic [Jan 20 00:31:55]
HOL:74f42248dbc44958d90a69acf52b5902e11e6683
  Provide more automatic rewrites about positivity of u.l.p constants [Jan 20 23:50:06]
Machine:oven3+4.19.67.1.amd64-smp+

Jan 23 21:08:44 Claimed job
Jan 23 21:08:57 Building+HOL
Jan 23 21:28:38 Starting+developers
Jan 23 21:28:46 Finished+developers++++++++++++++++++++++++++++++++++++++++8.11+166020
Jan 23 21:28:47 Starting+developers/bin
Jan 23 21:28:57 Finished+developers/bin++++++++++++++++++++++++++++++++++++10.61+682456
Jan 23 21:28:57 Starting+semantics/ffi
Jan 23 21:29:21 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++23.77+234632
Jan 23 21:29:22 Starting+semantics
Jan 23 21:32:43 Finished+semantics+++++++++++++++++++++++++++++++++++++++++201.40+1123380
Jan 23 21:32:44 Starting+semantics/proofs
Jan 23 21:40:34 Finished+semantics/proofs++++++++++++++++++++++++++++++++++470.44+1364964
Jan 23 21:40:34 Starting+semantics/alt_semantics
Jan 23 21:41:04 Finished+semantics/alt_semantics+++++++++++++++++++++++++++29.62+386712
Jan 23 21:41:04 Starting+semantics/alt_semantics/proofs
Jan 23 21:46:27 Finished+semantics/alt_semantics/proofs++++++++++++++++++++322.04+1005888
Jan 23 21:46:27 Starting+basis/pure
Jan 23 21:52:49 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++381.41+870964
Jan 23 21:52:49 Starting+translator
Jan 23 21:58:49 Finished+translator++++++++++++++++++++++++++++++++++++++++360.39+1528620
Jan 23 21:58:50 Starting+compiler/parsing
Jan 23 22:01:39 Finished+compiler/parsing++++++++++++++++++++++++++++++++++169.12+3563544
Jan 23 22:01:39 Starting+characteristic
Jan 23 22:14:09 Finished+characteristic++++++++++++++++++++++++++++++++++++750.06+1861200
Jan 23 22:14:10 Starting+translator/monadic
Jan 23 22:17:53 Finished+translator/monadic++++++++++++++++++++++++++++++++223.18+1838116
Jan 23 22:17:53 Starting+basis
Jan 24 00:01:16 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6202.67+16379452
Jan 24 00:01:16 Starting+compiler/inference
Jan 24 00:04:03 Finished+compiler/inference++++++++++++++++++++++++++++++++165.91+1255204
Jan 24 00:04:03 Starting+compiler/backend/reg_alloc
Jan 24 00:06:08 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++124.59+1545088
Jan 24 00:06:08 Starting+compiler/backend/gc
Jan 24 00:13:22 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++433.71+2086964
Jan 24 00:13:22 Starting+compiler/backend
Jan 24 00:23:24 Finished+compiler/backend++++++++++++++++++++++++++++++++++602.30+2698120
Jan 24 00:23:25 Starting+compiler/encoders/asm
Jan 24 00:24:18 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++53.31+630932
Jan 24 00:24:18 Starting+compiler/encoders/x64
Jan 24 00:26:39 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++140.82+1004552
Jan 24 00:26:39 Starting+compiler/encoders/arm7
Jan 24 00:31:06 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++266.27+1506636
Jan 24 00:31:06 Starting+compiler/encoders/arm8
Jan 24 00:32:37 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++90.42+709288
Jan 24 00:32:37 Starting+compiler/encoders/mips
Jan 24 00:35:56 Finished+compiler/encoders/mips++++++++++++++++++++++++++++198.71+1270356
Jan 24 00:35:56 Starting+compiler/encoders/riscv
Jan 24 00:39:39 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++223.12+831252
Jan 24 00:39:40 Starting+compiler/encoders/ag32
Jan 24 00:40:24 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++44.17+707284
Jan 24 00:40:24 Starting+compiler/backend/x64
Jan 24 00:41:10 Finished+compiler/backend/x64++++++++++++++++++++++++++++++45.18+1322808
Jan 24 00:41:10 Starting+compiler/backend/arm7
Jan 25 07:42:31 Resuming+compiler/backend/arm7
Jan 25 07:42:56 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++24.47+563284
Jan 25 07:42:56 Starting+compiler/backend/arm8
Jan 25 07:43:44 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++47.57+1473248
Jan 25 07:43:44 Starting+compiler/backend/mips
Jan 25 07:44:33 Finished+compiler/backend/mips+++++++++++++++++++++++++++++48.80+1431988
Jan 25 07:44:33 Starting+compiler/backend/riscv
Jan 25 07:45:18 Finished+compiler/backend/riscv++++++++++++++++++++++++++++44.62+1489340
Jan 25 07:45:18 Starting+compiler/backend/ag32
Jan 25 07:47:49 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++150.78+1381236
Jan 25 07:47:49 Starting+compiler/parsing/proofs
Jan 25 07:56:18 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++508.57+1261312
Jan 25 07:56:18 Starting+compiler/inference/proofs
Jan 25 08:01:41 Finished+compiler/inference/proofs+++++++++++++++++++++++++322.10+1054484
Jan 25 08:01:41 Starting+compiler/backend/semantics
Jan 25 09:03:52 Finished+compiler/backend/semantics++++++++++++++++++++++++3731.03+1974240
Jan 25 09:03:52 Starting+compiler/backend/reg_alloc/proofs
Jan 25 09:11:44 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++471.98+837016
Jan 25 09:11:45 Starting+compiler/backend/proofs
Jan 25 10:53:26 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6100.92+18029332
Jan 25 10:53:26 Starting+compiler/backend/serialiser
Jan 25 10:56:24 Finished+compiler/backend/serialiser+++++++++++++++++++++++177.09+2404644
Jan 25 10:56:24 Starting+compiler/encoders/x64/proofs
Jan 25 11:18:03 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1298.88+6225644
Jan 25 11:18:03 Starting+compiler/encoders/arm7/proofs
Jan 25 11:47:10 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1746.26+3343224
Jan 25 11:47:10 Starting+compiler/encoders/arm8/proofs
Jan 25 12:02:48 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++937.47+1651420
Jan 25 12:02:48 Starting+compiler/encoders/mips/proofs
Jan 25 12:25:11 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1342.83+2777404
Jan 25 12:25:11 Starting+compiler/encoders/riscv/proofs
Jan 25 12:45:07 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1195.71+1409244
Jan 25 12:45:07 Starting+compiler/encoders/ag32/proofs
Jan 25 12:50:58 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++350.70+870588
Jan 25 12:50:58 Starting+compiler/backend/x64/proofs
Jan 25 12:51:55 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++56.35+1571788
Jan 25 12:51:55 Starting+compiler/backend/arm7/proofs
Jan 25 12:52:50 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++55.00+1321632
Jan 25 12:52:51 Starting+compiler/backend/arm8/proofs
Jan 25 12:53:44 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++53.42+1360532
Jan 25 12:53:44 Starting+compiler/backend/mips/proofs
Jan 25 12:54:45 Finished+compiler/backend/mips/proofs++++++++++++++++++++++60.98+1560712
Jan 25 12:54:46 Starting+compiler/backend/riscv/proofs
Jan 25 12:55:44 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++58.47+1591056
Jan 25 12:55:45 Starting+compiler/backend/ag32/proofs
Jan 25 13:24:20 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1715.19+2551724
Jan 25 13:24:20 Starting+compiler/proofs
Jan 25 13:29:07 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++286.63+4764192
Jan 25 13:29:07 Starting+candle/set-theory
Jan 25 13:30:08 Finished+candle/set-theory+++++++++++++++++++++++++++++++++60.35+784336
Jan 25 13:30:08 Starting+candle/syntax-lib
Jan 25 13:30:33 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++25.10+660344
Jan 25 13:30:34 Starting+candle/standard/syntax
Jan 25 13:34:32 Finished+candle/standard/syntax++++++++++++++++++++++++++++237.96+953052
Jan 25 13:34:32 Starting+candle/standard/semantics
Jan 25 13:38:31 Finished+candle/standard/semantics+++++++++++++++++++++++++238.99+1493556
Jan 25 13:38:31 Starting+candle/standard/monadic
Jan 25 13:41:56 Finished+candle/standard/monadic+++++++++++++++++++++++++++204.82+1622952
Jan 25 13:41:57 Starting+candle/standard/ml_kernel
Jan 25 13:56:18 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++861.24+3373888
Jan 25 13:56:18 Starting+candle/overloading/syntax
Jan 25 14:03:07 Finished+candle/overloading/syntax+++++++++++++++++++++++++408.31+1410240
Jan 25 14:03:07 Starting+candle/overloading/semantics
Jan 25 14:28:48 Finished+candle/overloading/semantics++++++++++++++++++++++1539.59+2691892
Jan 25 14:28:48 Starting+candle/prover
Jan 25 14:46:54 Finished+candle/prover+++++++++++++++++++++++++++++++++++++1085.52+3241528
Jan 25 14:46:54 Starting+pancake
Jan 25 14:52:22 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++328.12+1913560
Jan 25 14:52:22 Starting+pancake/ffi
Jan 25 14:52:23 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.75+30776
Jan 25 14:52:24 Starting+pancake/semantics
Jan 25 14:57:44 Finished+pancake/semantics+++++++++++++++++++++++++++++++++320.33+1320740
Jan 25 14:57:44 Starting+pancake/proofs
Jan 25 15:23:30 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1545.57+5671888
Jan 25 15:23:30 Starting+characteristic/examples
Jan 25 15:26:38 Finished+characteristic/examples+++++++++++++++++++++++++++187.10+3299388
Jan 25 15:26:38 Starting+tutorial/solutions
Jan 25 16:03:08 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2189.98+9077432
Jan 25 16:03:09 Starting+translator/monadic/examples
Jan 25 16:09:23 Finished+translator/monadic/examples+++++++++++++++++++++++374.08+2742628
Jan 25 16:09:23 Starting+examples
Jan 25 16:28:27 Finished+examples++++++++++++++++++++++++++++++++++++++++++1144.05+4066408
Jan 25 16:28:28 Starting+examples/compilation/x64
Jan 25 22:08:19 Finished+examples/compilation/x64++++++++++++++++++++++++++20391.06+26164908
Jan 25 22:08:19 Starting+examples/compilation/x64/proofs
Jan 25 22:12:29 Finished+examples/compilation/x64/proofs+++++++++++++++++++249.60+3359548
Jan 25 22:12:29 Starting+examples/compilation/ag32
Jan 25 23:32:42 Finished+examples/compilation/ag32+++++++++++++++++++++++++4812.08+10079108
Jan 25 23:32:42 Starting+examples/compilation/ag32/proofs
Jan 25 23:34:33 Finished+examples/compilation/ag32/proofs++++++++++++++++++110.43+3085020
Jan 25 23:34:33 Starting+examples/cost
Jan 26 01:32:31 Finished+examples/cost+++++++++++++++++++++++++++++++++++++7076.89+8322228
Jan 26 01:32:31 Starting+examples/lpr_checker
Jan 26 01:34:28 Finished+examples/lpr_checker++++++++++++++++++++++++++++++116.66+653076
Jan 26 01:34:28 Starting+examples/lpr_checker/array
Jan 26 02:38:39 Finished+examples/lpr_checker/array++++++++++++++++++++++++3850.65+7003096
Jan 26 02:38:39 Starting+examples/lpr_checker/array/compilation
Jan 26 05:46:58 Finished+examples/lpr_checker/array/compilation++++++++++++11297.36+38217584
Jan 26 05:46:58 Starting+examples/lpr_checker/array/compilation/proofs
Jan 26 05:49:47 Finished+examples/lpr_checker/array/compilation/proofs+++++168.63+6772168
Jan 26 05:49:47 Starting+examples/opentheory
Jan 26 06:11:48 Finished+examples/opentheory+++++++++++++++++++++++++++++++1320.79+4065068
Jan 26 06:11:48 Starting+examples/opentheory
Jan 26 06:11:51 Finished+examples/opentheory+++++++++++++++++++++++++++++++2.85+32512
Jan 26 06:11:52 Starting+examples/opentheory/compilation
Jan 26 07:41:44 Finished+examples/opentheory/compilation+++++++++++++++++++5392.32+34145580
Jan 26 07:41:44 Starting+examples/opentheory/compilation/proofs
Jan 26 07:43:32 Finished+examples/opentheory/compilation/proofs++++++++++++106.91+4883764
Jan 26 07:43:32 Starting+examples/opentheory/compilation/ag32
Jan 26 09:19:43 Finished+examples/opentheory/compilation/ag32++++++++++++++5770.66+53286976
Jan 26 09:19:44 Starting+examples/opentheory/compilation/ag32/proofs
Jan 26 09:23:27 Finished+examples/opentheory/compilation/ag32/proofs+++++++223.18+6592912
Jan 26 09:23:27 Starting+examples/sat_encodings
Jan 26 09:27:48 Finished+examples/sat_encodings++++++++++++++++++++++++++++260.19+916360
Jan 26 09:27:48 Starting+examples/sat_encodings/case_studies
Jan 26 09:31:25 Finished+examples/sat_encodings/case_studies+++++++++++++++217.06+758884
Jan 26 09:31:25 Starting+examples/sat_encodings/translation
Jan 26 09:43:57 Finished+examples/sat_encodings/translation++++++++++++++++751.03+4732464
Jan 26 09:43:57 Starting+examples/sat_encodings/translation/compilation
Jan 26 11:13:40 Finished+examples/sat_encodings/translation/compilation++++5382.11+22876976
Jan 26 11:13:40 Starting+translator/okasaki-examples
Jan 26 11:23:11 Finished+translator/okasaki-examples+++++++++++++++++++++++570.71+2275080
Jan 26 11:23:11 Starting+translator/other-examples
Jan 26 11:26:52 Finished+translator/other-examples+++++++++++++++++++++++++220.14+1896588
Jan 26 11:26:52 Starting+compiler/parsing/tests
Jan 26 11:27:59 Finished+compiler/parsing/tests++++++++++++++++++++++++++++67.22+538324
Jan 26 11:28:00 Starting+compiler/inference/tests
Jan 26 11:47:35 Finished+compiler/inference/tests++++++++++++++++++++++++++1175.39+6626724
Jan 26 11:47:35 Starting+compiler/bootstrap/translation
Jan 26 17:36:36 Finished+compiler/bootstrap/translation++++++++++++++++++++20940.64+28131092
Jan 26 17:36:37 Starting+unverified/sexpr-bootstrap/x64/64
Jan 26 17:57:49 Finished+unverified/sexpr-bootstrap/x64/64+++++++++++++++++1272.63+10026184
Jan 26 17:57:50 Starting+unverified/sexpr-bootstrap/x64/32
Jan 26 18:16:01 Finished+unverified/sexpr-bootstrap/x64/32+++++++++++++++++1091.51+8889236
Jan 26 18:16:01 Starting+compiler/benchmarks
Jan 26 18:16:06 Finished+compiler/benchmarks+++++++++++++++++++++++++++++++4.77+50680
Jan 26 18:16:07 Starting+compiler/bootstrap/compilation/x64/64
Jan 27 22:47:04 Finished+compiler/bootstrap/compilation/x64/64+++++++++++++102656.96+74166792
Jan 27 22:47:04 Starting+compiler/bootstrap/compilation/x64/64/proofs
Jan 27 22:52:12 Finished+compiler/bootstrap/compilation/x64/64/proofs++++++307.05+16219564
Jan 27 22:52:12 Starting+compiler/bootstrap/compilation/x64/32
Jan 28 23:30:19 Finished+compiler/bootstrap/compilation/x64/32+++++++++++++88686.51+90625680
Jan 28 23:30:19 Starting+compiler/bootstrap/compilation/x64/32/proofs
Jan 28 23:35:07 Finished+compiler/bootstrap/compilation/x64/32/proofs++++++286.98+14971352
Jan 28 23:35:07 Starting+compiler/bootstrap/compilation/ag32/32
Jan 30 04:34:46 Finished+compiler/bootstrap/compilation/ag32/32++++++++++++104378.93+110444504
Jan 30 04:34:46 Starting+compiler/bootstrap/compilation/ag32/32/proofs
Jan 30 04:57:04 Finished+compiler/bootstrap/compilation/ag32/32/proofs+++++1337.30+40810740
Jan 30 04:57:04 SUCCESS