Job 1824

CakeML:be5529e04744d8535196ec7c045b7f76663db302
  Prevent the pattern parser from taking apart alias [Mar 14 15:36:24]
#868 (candle-pattern-fix)
Merging into:9bc73fcc84ed3d9932f534e5c512abd1ee8dc774
  Fix a broken proof [Mar 14 08:42:31]
HOL:9ef02c741e59da2e5b90512fc92aa8194c043623
  Fix Holmakefiles for Tamarack example; further modernise port-full [Mar 07 23:09:46]
Machine:oven3+4.19.67.1.amd64-smp+

Mar 14 21:38:39 Claimed job
Mar 14 21:38:44 Reusing+HOL
Mar 14 21:39:42 Starting+developers
Mar 14 21:39:51 Finished+developers++++++++++++++++++++++++++++++++++++++++8.73+141480
Mar 14 21:39:51 Starting+developers/bin
Mar 14 21:40:05 Finished+developers/bin++++++++++++++++++++++++++++++++++++14.28+1253700
Mar 14 21:40:05 Starting+semantics/ffi
Mar 14 21:40:34 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++28.70+234740
Mar 14 21:40:35 Starting+semantics
Mar 14 21:44:28 Finished+semantics+++++++++++++++++++++++++++++++++++++++++233.56+1024784
Mar 14 21:44:29 Starting+semantics/proofs
Mar 14 21:52:24 Finished+semantics/proofs++++++++++++++++++++++++++++++++++474.99+1182112
Mar 14 21:52:24 Starting+semantics/alt_semantics
Mar 14 21:53:04 Finished+semantics/alt_semantics+++++++++++++++++++++++++++39.84+481704
Mar 14 21:53:04 Starting+semantics/alt_semantics/proofs
Mar 14 21:58:29 Finished+semantics/alt_semantics/proofs++++++++++++++++++++324.65+1289540
Mar 14 21:58:29 Starting+basis/pure
Mar 14 22:00:41 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++131.65+1285536
Mar 14 22:00:41 Starting+translator
Mar 14 22:07:04 Finished+translator++++++++++++++++++++++++++++++++++++++++383.02+1417012
Mar 14 22:07:05 Starting+compiler/parsing
Mar 14 22:09:56 Finished+compiler/parsing++++++++++++++++++++++++++++++++++170.88+2514544
Mar 14 22:09:56 Starting+characteristic
Mar 14 22:23:12 Finished+characteristic++++++++++++++++++++++++++++++++++++795.82+2204612
Mar 14 22:23:12 Starting+translator/monadic
Mar 14 22:27:17 Finished+translator/monadic++++++++++++++++++++++++++++++++244.21+1565388
Mar 14 22:27:17 Starting+basis
Mar 15 00:09:52 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6154.89+14234256
Mar 15 00:09:52 Starting+compiler/inference
Mar 15 00:12:41 Finished+compiler/inference++++++++++++++++++++++++++++++++168.16+1286824
Mar 15 00:12:41 Starting+compiler/backend/reg_alloc
Mar 15 00:15:48 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++187.41+1735300
Mar 15 00:15:49 Starting+compiler/backend/gc
Mar 15 00:24:12 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++502.69+2026032
Mar 15 00:24:12 Starting+compiler/backend
Mar 15 00:34:54 Finished+compiler/backend++++++++++++++++++++++++++++++++++642.59+2020808
Mar 15 00:34:55 Starting+compiler/encoders/asm
Mar 15 00:35:59 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++64.25+738932
Mar 15 00:35:59 Starting+compiler/encoders/x64
Mar 15 00:37:04 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++64.75+803048
Mar 15 00:37:04 Starting+compiler/encoders/arm7
Mar 15 00:39:07 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++122.62+840564
Mar 15 00:39:07 Starting+compiler/encoders/arm8
Mar 15 00:39:43 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++35.30+763848
Mar 15 00:39:43 Starting+compiler/encoders/arm8_asl
Mar 15 00:46:31 Finished+compiler/encoders/arm8_asl++++++++++++++++++++++++407.51+1143340
Mar 15 00:46:31 Starting+compiler/encoders/mips
Mar 15 00:47:17 Finished+compiler/encoders/mips++++++++++++++++++++++++++++45.73+1516028
Mar 15 00:47:17 Starting+compiler/encoders/riscv
Mar 15 00:47:58 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++41.01+794120
Mar 15 00:47:58 Starting+compiler/encoders/ag32
Mar 15 00:48:49 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++50.18+658496
Mar 15 00:48:49 Starting+compiler/backend/x64
Mar 15 00:49:38 Finished+compiler/backend/x64++++++++++++++++++++++++++++++49.16+1340032
Mar 15 00:49:39 Starting+compiler/backend/arm7
Mar 15 00:50:32 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++53.42+1579984
Mar 15 00:50:32 Starting+compiler/backend/arm8
Mar 15 00:51:22 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++49.14+1444252
Mar 15 00:51:22 Starting+compiler/backend/mips
Mar 15 00:52:11 Finished+compiler/backend/mips+++++++++++++++++++++++++++++48.51+1474764
Mar 15 00:52:11 Starting+compiler/backend/riscv
Mar 15 00:52:58 Finished+compiler/backend/riscv++++++++++++++++++++++++++++46.80+1147780
Mar 15 00:52:58 Starting+compiler/backend/ag32
Mar 15 00:55:52 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++174.25+1847360
Mar 15 00:55:53 Starting+compiler/parsing/proofs
Mar 15 01:04:07 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++494.05+1299700
Mar 15 01:04:07 Starting+compiler/inference/proofs
Mar 15 01:09:51 Finished+compiler/inference/proofs+++++++++++++++++++++++++343.72+1155968
Mar 15 01:09:51 Starting+compiler/backend/semantics
Mar 15 02:12:22 Finished+compiler/backend/semantics++++++++++++++++++++++++3749.84+2630260
Mar 15 02:12:23 Starting+compiler/backend/reg_alloc/proofs
Mar 15 02:20:13 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++470.69+1010440
Mar 15 02:20:14 Starting+compiler/backend/proofs
Mar 15 03:59:57 Finished+compiler/backend/proofs+++++++++++++++++++++++++++5982.82+19802604
Mar 15 03:59:57 Starting+compiler/backend/serialiser
Mar 15 04:03:14 Finished+compiler/backend/serialiser+++++++++++++++++++++++196.42+2447508
Mar 15 04:03:14 Starting+compiler/encoders/x64/proofs
Mar 15 04:24:37 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1283.15+5395164
Mar 15 04:24:37 Starting+compiler/encoders/arm7/proofs
Mar 15 04:53:49 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1751.02+3667324
Mar 15 04:53:49 Starting+compiler/encoders/arm8/proofs
Mar 15 05:09:15 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++925.24+1455576
Mar 15 05:09:15 Starting+compiler/encoders/arm8_asl/proofs
Mar 15 05:45:09 Finished+compiler/encoders/arm8_asl/proofs+++++++++++++++++2153.75+2423444
Mar 15 05:45:10 Starting+compiler/encoders/mips/proofs
Mar 15 06:08:08 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1377.95+2447668
Mar 15 06:08:08 Starting+compiler/encoders/riscv/proofs
Mar 15 06:28:12 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1202.46+1388084
Mar 15 06:28:12 Starting+compiler/encoders/ag32/proofs
Mar 15 06:34:00 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++347.56+852520
Mar 15 06:34:00 Starting+compiler/backend/x64/proofs
Mar 15 06:35:00 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++60.26+1553948
Mar 15 06:35:00 Starting+compiler/backend/arm7/proofs
Mar 15 06:36:03 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++62.35+2350872
Mar 15 06:36:03 Starting+compiler/backend/arm8/proofs
Mar 15 06:37:00 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++56.98+1409836
Mar 15 06:37:01 Starting+compiler/backend/arm8_asl
Mar 15 06:37:52 Finished+compiler/backend/arm8_asl+++++++++++++++++++++++++51.37+1781212
Mar 15 06:37:52 Starting+compiler/backend/mips/proofs
Mar 15 06:38:52 Finished+compiler/backend/mips/proofs++++++++++++++++++++++59.79+1598892
Mar 15 06:38:52 Starting+compiler/backend/riscv/proofs
Mar 15 06:39:53 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++60.00+1649376
Mar 15 06:39:53 Starting+compiler/backend/ag32/proofs
Mar 15 07:09:00 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1746.67+2583756
Mar 15 07:09:00 Starting+compiler/proofs
Mar 15 07:13:22 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++262.13+3171360
Mar 15 07:13:22 Starting+candle/set-theory
Mar 15 07:14:34 Finished+candle/set-theory+++++++++++++++++++++++++++++++++71.13+1046584
Mar 15 07:14:34 Starting+candle/syntax-lib
Mar 15 07:15:05 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++30.37+541080
Mar 15 07:15:05 Starting+candle/standard/syntax
Mar 15 07:19:36 Finished+candle/standard/syntax++++++++++++++++++++++++++++271.34+996052
Mar 15 07:19:36 Starting+candle/standard/semantics
Mar 15 07:23:40 Finished+candle/standard/semantics+++++++++++++++++++++++++242.90+1279072
Mar 15 07:23:40 Starting+candle/standard/monadic
Mar 15 07:27:42 Finished+candle/standard/monadic+++++++++++++++++++++++++++242.29+1893240
Mar 15 07:27:42 Starting+candle/standard/ml_kernel
Mar 15 07:40:40 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++777.66+2917484
Mar 15 07:40:41 Starting+candle/overloading/syntax
Mar 15 07:47:31 Finished+candle/overloading/syntax+++++++++++++++++++++++++409.98+1428368
Mar 15 07:47:31 Starting+candle/overloading/semantics
Mar 15 08:13:20 Finished+candle/overloading/semantics++++++++++++++++++++++1549.23+2525100
Mar 15 08:13:21 Starting+candle/overloading/monadic
Mar 15 08:18:47 Finished+candle/overloading/monadic++++++++++++++++++++++++325.61+1630080
Mar 15 08:18:47 Starting+candle/overloading/ml_kernel
Mar 15 08:33:44 Finished+candle/overloading/ml_kernel++++++++++++++++++++++896.99+3714128
Mar 15 08:33:44 Starting+candle/overloading/ml_checker
Mar 15 08:39:15 Finished+candle/overloading/ml_checker+++++++++++++++++++++330.59+3098308
Mar 15 08:39:15 Starting+candle/prover
Mar 15 08:56:55 Finished+candle/prover+++++++++++++++++++++++++++++++++++++1059.51+2941060
Mar 15 08:56:56 Starting+pancake
Mar 15 09:04:32 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++456.33+4437688
Mar 15 09:04:32 Starting+pancake/ffi
Mar 15 09:04:33 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.78+32156
Mar 15 09:04:33 Starting+pancake/semantics
Mar 15 09:09:44 Finished+pancake/semantics+++++++++++++++++++++++++++++++++310.01+1180736
Mar 15 09:09:44 Starting+pancake/proofs
Mar 15 09:36:32 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1607.98+5917532
Mar 15 09:36:32 Starting+characteristic/examples
Mar 15 09:39:29 Finished+characteristic/examples+++++++++++++++++++++++++++176.70+3197820
Mar 15 09:39:29 Starting+tutorial/solutions
Mar 15 10:16:11 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2201.35+9346408
Mar 15 10:16:11 Starting+translator/monadic/examples
Mar 15 10:23:09 Finished+translator/monadic/examples+++++++++++++++++++++++417.29+2894444
Mar 15 10:23:09 Starting+examples
Mar 15 10:41:08 Finished+examples++++++++++++++++++++++++++++++++++++++++++1078.68+3842516
Mar 15 10:41:08 Starting+examples/compilation/x64
Mar 15 16:15:53 Finished+examples/compilation/x64++++++++++++++++++++++++++20084.13+26298052
Mar 15 16:15:53 Starting+examples/compilation/x64/proofs
Mar 15 16:20:48 Finished+examples/compilation/x64/proofs+++++++++++++++++++294.99+3138472
Mar 15 16:20:48 Starting+examples/compilation/ag32
Mar 15 17:39:02 Finished+examples/compilation/ag32+++++++++++++++++++++++++4693.58+9019004
Mar 15 17:39:02 Starting+examples/compilation/ag32/proofs
Mar 15 17:40:55 Finished+examples/compilation/ag32/proofs++++++++++++++++++112.87+3858384
Mar 15 17:40:56 Starting+examples/cost
Mar 15 19:39:49 Finished+examples/cost+++++++++++++++++++++++++++++++++++++7133.44+9170288
Mar 15 19:39:50 Starting+examples/lpr_checker
Mar 15 19:42:01 Finished+examples/lpr_checker++++++++++++++++++++++++++++++131.42+994804
Mar 15 19:42:01 Starting+examples/lpr_checker/array
Mar 15 20:46:39 Finished+examples/lpr_checker/array++++++++++++++++++++++++3877.65+5539588
Mar 15 20:46:40 Starting+examples/lpr_checker/array/compilation
Mar 15 23:42:28 Finished+examples/lpr_checker/array/compilation++++++++++++10547.39+33487648
Mar 15 23:42:28 Starting+examples/lpr_checker/array/compilation/proofs
Mar 15 23:45:23 Finished+examples/lpr_checker/array/compilation/proofs+++++174.99+7728780
Mar 15 23:45:23 Starting+examples/opentheory
Mar 16 00:06:33 Finished+examples/opentheory+++++++++++++++++++++++++++++++1269.34+5815716
Mar 16 00:06:33 Starting+examples/opentheory
Mar 16 00:06:37 Finished+examples/opentheory+++++++++++++++++++++++++++++++2.89+34948
Mar 16 00:06:37 Starting+examples/opentheory/compilation
Mar 16 01:39:00 Finished+examples/opentheory/compilation+++++++++++++++++++5543.34+34644620
Mar 16 01:39:01 Starting+examples/opentheory/compilation/proofs
Mar 16 01:41:19 Finished+examples/opentheory/compilation/proofs++++++++++++138.29+3608220
Mar 16 01:41:19 Starting+examples/opentheory/compilation/ag32
Mar 16 03:08:51 Finished+examples/opentheory/compilation/ag32++++++++++++++5249.95+32114172
Mar 16 03:08:51 Starting+examples/opentheory/compilation/ag32/proofs
Mar 16 03:12:37 Finished+examples/opentheory/compilation/ag32/proofs+++++++226.02+6439228
Mar 16 03:12:37 Starting+examples/sat_encodings
Mar 16 03:16:56 Finished+examples/sat_encodings++++++++++++++++++++++++++++258.97+930348
Mar 16 03:16:57 Starting+examples/sat_encodings/case_studies
Mar 16 03:20:39 Finished+examples/sat_encodings/case_studies+++++++++++++++222.42+722992
Mar 16 03:20:40 Starting+examples/sat_encodings/translation
Mar 16 03:32:27 Finished+examples/sat_encodings/translation++++++++++++++++706.92+3494052
Mar 16 03:32:27 Starting+examples/sat_encodings/translation/compilation
Mar 16 05:01:12 Finished+examples/sat_encodings/translation/compilation++++5324.68+23134368
Mar 16 05:01:12 Starting+translator/okasaki-examples
Mar 16 05:10:59 Finished+translator/okasaki-examples+++++++++++++++++++++++586.29+1965856
Mar 16 05:10:59 Starting+translator/other-examples
Mar 16 05:12:37 Finished+translator/other-examples+++++++++++++++++++++++++98.50+1327076
Mar 16 05:12:38 Starting+compiler/parsing/tests
Mar 16 05:13:46 Finished+compiler/parsing/tests++++++++++++++++++++++++++++68.01+652608
Mar 16 05:13:46 Starting+compiler/inference/tests
Mar 16 05:29:32 Finished+compiler/inference/tests++++++++++++++++++++++++++946.11+4362464
Mar 16 05:29:33 Starting+compiler/printing/test
Mar 16 05:37:06 Finished+compiler/printing/test++++++++++++++++++++++++++++453.77+3438636
Mar 16 05:37:07 Starting+compiler/repl
Mar 16 06:01:38 Finished+compiler/repl+++++++++++++++++++++++++++++++++++++1471.49+8538120
Mar 16 06:01:39 Starting+compiler/bootstrap/translation
Mar 16 14:35:50 Finished+compiler/bootstrap/translation++++++++++++++++++++30851.04+39434600
Mar 16 14:35:50 Starting+unverified/sexpr-bootstrap/x64/64
Mar 16 14:58:20 Finished+unverified/sexpr-bootstrap/x64/64+++++++++++++++++1349.22+12222672
Mar 16 14:58:20 Starting+unverified/sexpr-bootstrap/x64/32
Mar 16 15:16:35 Finished+unverified/sexpr-bootstrap/x64/32+++++++++++++++++1095.23+10709564
Mar 16 15:16:36 Starting+compiler/benchmarks
Mar 16 15:16:41 Finished+compiler/benchmarks+++++++++++++++++++++++++++++++5.25+47748
Mar 16 15:16:41 Starting+compiler/bootstrap/compilation/x64/64
Mar 18 06:22:59 Finished+compiler/bootstrap/compilation/x64/64+++++++++++++140777.01+108799036
Mar 18 06:22:59 Starting+compiler/bootstrap/compilation/x64/64/proofs
Mar 18 07:02:52 Finished+compiler/bootstrap/compilation/x64/64/proofs++++++2392.77+35039288
Mar 18 07:02:52 Starting+compiler/bootstrap/compilation/x64/32
Mar 19 08:17:42 Finished+compiler/bootstrap/compilation/x64/32+++++++++++++90888.99+78555880
Mar 19 08:17:42 Starting+compiler/bootstrap/compilation/x64/32/proofs
Mar 19 08:24:59 Finished+compiler/bootstrap/compilation/x64/32/proofs++++++436.58+18701924
Mar 19 08:24:59 Starting+compiler/bootstrap/compilation/ag32/32
Mar 20 11:03:36 Finished+compiler/bootstrap/compilation/ag32/32++++++++++++95915.94+96090712
Mar 20 11:03:36 Starting+compiler/bootstrap/compilation/ag32/32/proofs
Mar 20 11:29:24 Finished+compiler/bootstrap/compilation/ag32/32/proofs+++++1547.44+62825456
Mar 20 11:29:24 SUCCESS