Job 1724

CakeML:04809afe3c23bf2711ab2493d03930bb6c6a2ff7
  Make ref references in opentheory less fragile [Jan 18 14:50:09]
#856 (printing)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
  Merge pull request #852 from CakeML/tidy-up [Jan 05 17:40:32]
HOL:0e74a42a431c508b13c303f1ef44290a2ba31e2c
  Fix typo in documentation of SRULE [Jan 17 23:32:45]
Machine:oven3+4.19.67.1.amd64-smp+

Jan 18 21:06:27 Claimed job
Jan 18 21:06:36 Building+HOL
Jan 18 21:26:22 Starting+developers
Jan 18 21:26:29 Finished+developers++++++++++++++++++++++++++++++++++++++++7.79+147896
Jan 18 21:26:30 Starting+developers/bin
Jan 18 21:26:39 Finished+developers/bin++++++++++++++++++++++++++++++++++++9.55+678256
Jan 18 21:26:40 Starting+semantics/ffi
Jan 18 21:27:00 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++20.58+238432
Jan 18 21:27:01 Starting+semantics
Jan 18 21:30:19 Finished+semantics+++++++++++++++++++++++++++++++++++++++++198.33+1294396
Jan 18 21:30:19 Starting+semantics/proofs
Jan 18 21:38:09 Finished+semantics/proofs++++++++++++++++++++++++++++++++++469.52+1413840
Jan 18 21:38:09 Starting+semantics/alt_semantics
Jan 18 21:38:35 Finished+semantics/alt_semantics+++++++++++++++++++++++++++25.69+380748
Jan 18 21:38:35 Starting+semantics/alt_semantics/proofs
Jan 18 21:43:52 Finished+semantics/alt_semantics/proofs++++++++++++++++++++316.46+1051896
Jan 18 21:43:52 Starting+basis/pure
Jan 18 21:50:13 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++380.33+866460
Jan 18 21:50:13 Starting+translator
Jan 18 21:56:05 Finished+translator++++++++++++++++++++++++++++++++++++++++351.01+1723852
Jan 18 21:56:05 Starting+compiler/parsing
Jan 18 21:58:48 Finished+compiler/parsing++++++++++++++++++++++++++++++++++162.85+2073820
Jan 18 21:58:48 Starting+characteristic
Jan 18 22:10:42 Finished+characteristic++++++++++++++++++++++++++++++++++++713.29+2083508
Jan 18 22:10:42 Starting+translator/monadic
Jan 18 22:14:11 Finished+translator/monadic++++++++++++++++++++++++++++++++209.02+1438180
Jan 18 22:14:11 Starting+basis
Jan 18 23:57:36 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6204.72+16267904
Jan 18 23:57:36 Starting+compiler/inference
Jan 19 00:00:17 Finished+compiler/inference++++++++++++++++++++++++++++++++160.05+1028360
Jan 19 00:00:17 Starting+compiler/backend/reg_alloc
Jan 19 00:02:21 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++124.07+1241424
Jan 19 00:02:21 Starting+compiler/backend/gc
Jan 19 00:09:21 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++419.20+2453240
Jan 19 00:09:21 Starting+compiler/backend
Jan 19 00:18:10 Finished+compiler/backend++++++++++++++++++++++++++++++++++528.50+2099880
Jan 19 00:18:10 Starting+compiler/encoders/asm
Jan 19 00:19:01 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++50.96+719852
Jan 19 00:19:01 Starting+compiler/encoders/x64
Jan 19 00:21:18 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++136.06+602028
Jan 19 00:21:18 Starting+compiler/encoders/arm7
Jan 19 00:25:52 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++274.24+1742692
Jan 19 00:25:53 Starting+compiler/encoders/arm8
Jan 19 00:27:17 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++83.78+920228
Jan 19 00:27:17 Starting+compiler/encoders/mips
Jan 19 00:30:29 Finished+compiler/encoders/mips++++++++++++++++++++++++++++192.34+1234180
Jan 19 00:30:30 Starting+compiler/encoders/riscv
Jan 19 00:34:17 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++227.50+763476
Jan 19 00:34:17 Starting+compiler/encoders/ag32
Jan 19 00:34:58 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++40.39+663572
Jan 19 00:34:58 Starting+compiler/backend/x64
Jan 19 00:35:39 Finished+compiler/backend/x64++++++++++++++++++++++++++++++40.84+1446516
Jan 19 00:35:40 Starting+compiler/backend/arm7
Jan 19 00:36:27 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++47.60+1199732
Jan 19 00:36:28 Starting+compiler/backend/arm8
Jan 19 00:37:07 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++39.63+1528724
Jan 19 00:37:08 Starting+compiler/backend/mips
Jan 19 00:37:50 Finished+compiler/backend/mips+++++++++++++++++++++++++++++41.88+1549532
Jan 19 00:37:50 Starting+compiler/backend/riscv
Jan 19 00:38:32 Finished+compiler/backend/riscv++++++++++++++++++++++++++++42.30+1408468
Jan 19 00:38:33 Starting+compiler/backend/ag32
Jan 19 00:40:59 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++145.77+1450540
Jan 19 00:40:59 Starting+compiler/parsing/proofs
Jan 19 00:49:17 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++497.89+1257308
Jan 19 00:49:17 Starting+compiler/inference/proofs
Jan 19 00:54:29 Finished+compiler/inference/proofs+++++++++++++++++++++++++311.90+978312
Jan 19 00:54:29 Starting+compiler/backend/semantics
Jan 19 01:55:45 Finished+compiler/backend/semantics++++++++++++++++++++++++3675.30+3345144
Jan 19 01:55:45 Starting+compiler/backend/reg_alloc/proofs
Jan 19 02:03:03 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++437.65+1041092
Jan 19 02:03:03 Starting+compiler/backend/proofs
Jan 19 03:44:26 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6082.07+23211852
Jan 19 03:44:26 Starting+compiler/backend/serialiser
Jan 19 03:46:59 Finished+compiler/backend/serialiser+++++++++++++++++++++++152.91+1999488
Jan 19 03:46:59 Starting+compiler/encoders/x64/proofs
Jan 19 04:08:31 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1291.82+5053976
Jan 19 04:08:31 Starting+compiler/encoders/arm7/proofs
Jan 19 04:37:57 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1765.85+3547856
Jan 19 04:37:58 Starting+compiler/encoders/arm8/proofs
Jan 19 04:53:10 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++911.17+1522580
Jan 19 04:53:10 Starting+compiler/encoders/mips/proofs
Jan 19 05:16:01 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1370.44+2169808
Jan 19 05:16:01 Starting+compiler/encoders/riscv/proofs
Jan 19 05:36:14 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1212.89+1469124
Jan 19 05:36:14 Starting+compiler/encoders/ag32/proofs
Jan 19 05:42:05 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++350.77+840004
Jan 19 05:42:05 Starting+compiler/backend/x64/proofs
Jan 19 05:42:55 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++49.66+1628592
Jan 19 05:42:56 Starting+compiler/backend/arm7/proofs
Jan 19 05:43:45 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++49.05+1101432
Jan 19 05:43:45 Starting+compiler/backend/arm8/proofs
Jan 19 05:44:36 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++50.79+1646308
Jan 19 05:44:36 Starting+compiler/backend/mips/proofs
Jan 19 05:45:27 Finished+compiler/backend/mips/proofs++++++++++++++++++++++50.47+1216860
Jan 19 05:45:27 Starting+compiler/backend/riscv/proofs
Jan 19 05:46:16 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++49.11+1488708
Jan 19 05:46:16 Starting+compiler/backend/ag32/proofs
Jan 19 06:13:51 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1654.61+2784016
Jan 19 06:13:52 Starting+compiler/proofs
Jan 19 06:18:13 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++260.99+4348220
Jan 19 06:18:13 Starting+candle/set-theory
Jan 19 06:19:11 Finished+candle/set-theory+++++++++++++++++++++++++++++++++57.86+717860
Jan 19 06:19:11 Starting+candle/syntax-lib
Jan 19 06:19:35 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++23.47+652436
Jan 19 06:19:35 Starting+candle/standard/syntax
Jan 19 06:23:28 Finished+candle/standard/syntax++++++++++++++++++++++++++++232.58+1262224
Jan 19 06:23:28 Starting+candle/standard/semantics
Jan 19 06:27:20 Finished+candle/standard/semantics+++++++++++++++++++++++++231.22+1328852
Jan 19 06:27:20 Starting+candle/standard/monadic
Jan 19 06:30:40 Finished+candle/standard/monadic+++++++++++++++++++++++++++199.85+1669636
Jan 19 06:30:40 Starting+candle/standard/ml_kernel
Jan 19 06:44:44 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++843.26+3366828
Jan 19 06:44:44 Starting+candle/overloading/syntax
Jan 19 06:51:05 Finished+candle/overloading/syntax+++++++++++++++++++++++++380.93+1317668
Jan 19 06:51:05 Starting+candle/overloading/semantics
Jan 19 07:17:01 Finished+candle/overloading/semantics++++++++++++++++++++++1555.22+2591476
Jan 19 07:17:01 Starting+candle/prover
Jan 19 07:33:37 Finished+candle/prover+++++++++++++++++++++++++++++++++++++996.23+3310148
Jan 19 07:33:38 Starting+pancake
Jan 19 07:37:37 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++239.50+2900472
Jan 19 07:37:38 Starting+pancake/ffi
Jan 19 07:37:38 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.47+7508
Jan 19 07:37:38 Starting+pancake/semantics
Jan 19 07:42:31 Finished+pancake/semantics+++++++++++++++++++++++++++++++++292.84+1136076
Jan 19 07:42:32 Starting+pancake/proofs
Jan 19 08:07:41 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1508.82+4122228
Jan 19 08:07:41 Starting+characteristic/examples
Jan 19 08:10:38 Finished+characteristic/examples+++++++++++++++++++++++++++177.01+2874852
Jan 19 08:10:38 Starting+tutorial/solutions
Jan 19 08:46:09 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2130.07+9767772
Jan 19 08:46:09 Starting+translator/monadic/examples
Jan 19 08:52:00 Finished+translator/monadic/examples+++++++++++++++++++++++350.92+3334960
Jan 19 08:52:00 Starting+examples
Jan 19 09:10:22 Finished+examples++++++++++++++++++++++++++++++++++++++++++1101.75+4004788
Jan 19 09:10:22 Starting+examples/compilation/x64
Jan 19 14:40:27 Finished+examples/compilation/x64++++++++++++++++++++++++++19804.73+27040348
Jan 19 14:40:28 Starting+examples/compilation/x64/proofs
Jan 19 14:44:01 Finished+examples/compilation/x64/proofs+++++++++++++++++++213.36+3570384
Jan 19 14:44:01 Starting+examples/compilation/ag32
Jan 19 16:02:28 Finished+examples/compilation/ag32+++++++++++++++++++++++++4705.55+10141592
Jan 19 16:02:28 Starting+examples/compilation/ag32/proofs
Jan 19 16:04:04 Finished+examples/compilation/ag32/proofs++++++++++++++++++95.00+4075260
Jan 19 16:04:04 Starting+examples/cost
Jan 19 18:02:03 Finished+examples/cost+++++++++++++++++++++++++++++++++++++7078.82+8049764
Jan 19 18:02:03 Starting+examples/lpr_checker
Jan 19 18:03:52 Finished+examples/lpr_checker++++++++++++++++++++++++++++++108.30+733612
Jan 19 18:03:52 Starting+examples/lpr_checker/array
Jan 19 19:08:08 Finished+examples/lpr_checker/array++++++++++++++++++++++++3854.59+6874608
Jan 19 19:08:08 Starting+examples/lpr_checker/array/compilation
Jan 19 22:19:27 Finished+examples/lpr_checker/array/compilation++++++++++++11478.83+50022544
Jan 19 22:19:27 Starting+examples/lpr_checker/array/compilation/proofs
Jan 19 22:22:12 Finished+examples/lpr_checker/array/compilation/proofs+++++164.09+7565344
Jan 19 22:22:12 Starting+examples/opentheory
Jan 19 22:44:33 Finished+examples/opentheory+++++++++++++++++++++++++++++++1341.06+5159168
Jan 19 22:44:33 Starting+examples/opentheory
Jan 19 22:44:36 Finished+examples/opentheory+++++++++++++++++++++++++++++++2.54+34060
Jan 19 22:44:36 Starting+examples/opentheory/compilation
Jan 20 00:15:09 Finished+examples/opentheory/compilation+++++++++++++++++++5432.28+39280368
Jan 20 00:15:09 Starting+examples/opentheory/compilation/proofs
Jan 20 00:16:40 Finished+examples/opentheory/compilation/proofs++++++++++++90.39+3578832
Jan 20 00:16:40 Starting+examples/opentheory/compilation/ag32
Jan 20 01:41:14 Finished+examples/opentheory/compilation/ag32++++++++++++++5073.84+30448832
Jan 20 01:41:14 Starting+examples/opentheory/compilation/ag32/proofs
Jan 20 01:44:44 Finished+examples/opentheory/compilation/ag32/proofs+++++++210.07+6206608
Jan 20 01:44:45 Starting+examples/sat_encodings
Jan 20 01:48:33 Finished+examples/sat_encodings++++++++++++++++++++++++++++228.57+754644
Jan 20 01:48:34 Starting+examples/sat_encodings/case_studies
Jan 20 01:52:04 Finished+examples/sat_encodings/case_studies+++++++++++++++210.32+984372
Jan 20 01:52:04 Starting+examples/sat_encodings/translation
Jan 20 02:03:50 Finished+examples/sat_encodings/translation++++++++++++++++705.40+4059428
Jan 20 02:03:50 Starting+examples/sat_encodings/translation/compilation
Jan 20 03:32:39 Finished+examples/sat_encodings/translation/compilation++++5328.80+24473808
Jan 20 03:32:40 Starting+translator/okasaki-examples
Jan 20 03:41:57 Finished+translator/okasaki-examples+++++++++++++++++++++++557.12+1982472
Jan 20 03:41:57 Starting+translator/other-examples
Jan 20 03:45:35 Finished+translator/other-examples+++++++++++++++++++++++++217.43+1402840
Jan 20 03:45:35 Starting+compiler/parsing/tests
Jan 20 03:46:37 Finished+compiler/parsing/tests++++++++++++++++++++++++++++61.64+668140
Jan 20 03:46:37 Starting+compiler/inference/tests
Jan 20 04:05:24 Finished+compiler/inference/tests++++++++++++++++++++++++++1126.43+6602888
Jan 20 04:05:24 Starting+compiler/bootstrap/translation
Jan 20 09:45:39 Finished+compiler/bootstrap/translation++++++++++++++++++++20414.62+25390328
Jan 20 09:45:39 Starting+unverified/sexpr-bootstrap/x64/64
Jan 20 10:06:34 Finished+unverified/sexpr-bootstrap/x64/64+++++++++++++++++1254.79+9503948
Jan 20 10:06:34 Starting+unverified/sexpr-bootstrap/x64/32
Jan 20 10:24:36 Finished+unverified/sexpr-bootstrap/x64/32+++++++++++++++++1081.12+8370968
Jan 20 10:24:36 Starting+compiler/benchmarks
Jan 20 10:24:40 Finished+compiler/benchmarks+++++++++++++++++++++++++++++++4.40+33568
Jan 20 10:24:40 Starting+compiler/bootstrap/compilation/x64/64
Jan 21 15:11:09 Finished+compiler/bootstrap/compilation/x64/64+++++++++++++103588.21+82789752
Jan 21 15:11:09 Starting+compiler/bootstrap/compilation/x64/64/proofs
Jan 21 15:16:08 Finished+compiler/bootstrap/compilation/x64/64/proofs++++++298.39+17780708
Jan 21 15:16:08 Starting+compiler/bootstrap/compilation/x64/32
Jan 22 17:37:45 Finished+compiler/bootstrap/compilation/x64/32+++++++++++++94896.29+109988900
Jan 22 17:37:45 Starting+compiler/bootstrap/compilation/x64/32/proofs
Jan 22 17:42:07 Finished+compiler/bootstrap/compilation/x64/32/proofs++++++261.52+15570724
Jan 22 17:42:07 Starting+compiler/bootstrap/compilation/ag32/32
Jan 23 20:17:37 Finished+compiler/bootstrap/compilation/ag32/32++++++++++++95727.94+111906676
Jan 23 20:17:37 Starting+compiler/bootstrap/compilation/ag32/32/proofs
Jan 23 21:08:43 Finished+compiler/bootstrap/compilation/ag32/32/proofs+++++3065.44+56434980
Jan 23 21:08:43 SUCCESS