Job 1714

CakeML:4136ae455d57fa0446d68d1cac373f6add4fc932
  Automatic readme updates [Jan 16 02:47:45]
#856 (printing)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
  Merge pull request #852 from CakeML/tidy-up [Jan 05 17:40:32]
HOL:6b1dbc7559064a70fabbe71836947411103b499e
  Fix INCLUDES for src/coalgebras [Jan 07 05:56:33]
Machine:oven3+4.19.67.1.amd64-smp+

Jan 16 04:12:31 Claimed job
Jan 16 04:12:34 Reusing+HOL
Jan 16 04:13:26 Starting+developers
Jan 16 04:13:35 Finished+developers++++++++++++++++++++++++++++++++++++++++8.18+131892
Jan 16 04:13:35 Starting+developers/bin
Jan 16 04:13:45 Finished+developers/bin++++++++++++++++++++++++++++++++++++9.64+680244
Jan 16 04:13:45 Starting+semantics/ffi
Jan 16 04:14:05 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++19.97+239080
Jan 16 04:14:05 Starting+semantics
Jan 16 04:16:59 Finished+semantics+++++++++++++++++++++++++++++++++++++++++173.29+1199344
Jan 16 04:16:59 Starting+semantics/proofs
Jan 16 04:24:34 Finished+semantics/proofs++++++++++++++++++++++++++++++++++454.70+1017804
Jan 16 04:24:34 Starting+semantics/alt_semantics
Jan 16 04:25:00 Finished+semantics/alt_semantics+++++++++++++++++++++++++++25.61+425376
Jan 16 04:25:00 Starting+semantics/alt_semantics/proofs
Jan 16 04:30:10 Finished+semantics/alt_semantics/proofs++++++++++++++++++++309.86+1071452
Jan 16 04:30:11 Starting+basis/pure
Jan 16 04:31:57 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++106.07+840308
Jan 16 04:31:57 Starting+translator
Jan 16 04:37:51 Finished+translator++++++++++++++++++++++++++++++++++++++++353.46+1801016
Jan 16 04:37:51 Starting+compiler/parsing
Jan 16 04:40:28 Finished+compiler/parsing++++++++++++++++++++++++++++++++++157.08+1887816
Jan 16 04:40:29 Starting+characteristic
Jan 16 04:52:39 Finished+characteristic++++++++++++++++++++++++++++++++++++730.75+1678028
Jan 16 04:52:40 Starting+translator/monadic
Jan 16 04:56:09 Finished+translator/monadic++++++++++++++++++++++++++++++++208.69+1686272
Jan 16 04:56:09 Starting+basis
Jan 16 06:36:46 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6036.66+16845388
Jan 16 06:36:46 Starting+compiler/inference
Jan 16 06:39:13 Finished+compiler/inference++++++++++++++++++++++++++++++++146.20+1113420
Jan 16 06:39:13 Starting+compiler/backend/reg_alloc
Jan 16 06:41:17 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++124.24+1330512
Jan 16 06:41:18 Starting+compiler/backend/gc
Jan 16 06:47:51 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++392.71+1983272
Jan 16 06:47:51 Starting+compiler/backend
Jan 16 06:56:51 Finished+compiler/backend++++++++++++++++++++++++++++++++++540.41+2489676
Jan 16 06:56:52 Starting+compiler/encoders/asm
Jan 16 06:57:42 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++50.46+636884
Jan 16 06:57:43 Starting+compiler/encoders/x64
Jan 16 06:58:41 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++58.63+994604
Jan 16 06:58:42 Starting+compiler/encoders/arm7
Jan 16 07:00:35 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++113.68+774000
Jan 16 07:00:36 Starting+compiler/encoders/arm8
Jan 16 07:01:05 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++29.05+924692
Jan 16 07:01:05 Starting+compiler/encoders/mips
Jan 16 07:01:43 Finished+compiler/encoders/mips++++++++++++++++++++++++++++37.54+1268336
Jan 16 07:01:43 Starting+compiler/encoders/riscv
Jan 16 07:02:15 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++32.07+851032
Jan 16 07:02:15 Starting+compiler/encoders/ag32
Jan 16 07:02:58 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++42.19+588640
Jan 16 07:02:58 Starting+compiler/backend/x64
Jan 16 07:03:43 Finished+compiler/backend/x64++++++++++++++++++++++++++++++44.84+1437732
Jan 16 07:03:43 Starting+compiler/backend/arm7
Jan 16 07:04:29 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++45.51+1502552
Jan 16 07:04:29 Starting+compiler/backend/arm8
Jan 16 07:05:12 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++42.41+1385716
Jan 16 07:05:12 Starting+compiler/backend/mips
Jan 16 07:05:54 Finished+compiler/backend/mips+++++++++++++++++++++++++++++41.54+1569104
Jan 16 07:05:54 Starting+compiler/backend/riscv
Jan 16 07:06:40 Finished+compiler/backend/riscv++++++++++++++++++++++++++++45.39+1535088
Jan 16 07:06:40 Starting+compiler/backend/ag32
Jan 16 07:09:04 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++143.84+1413304
Jan 16 07:09:04 Starting+compiler/parsing/proofs
Jan 16 07:17:22 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++497.39+1036876
Jan 16 07:17:22 Starting+compiler/inference/proofs
Jan 16 07:22:52 Finished+compiler/inference/proofs+++++++++++++++++++++++++330.39+1240420
Jan 16 07:22:53 Starting+compiler/backend/semantics
Jan 16 08:24:29 Finished+compiler/backend/semantics++++++++++++++++++++++++3696.35+2996824
Jan 16 08:24:29 Starting+compiler/backend/reg_alloc/proofs
Jan 16 08:31:55 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++444.94+958264
Jan 16 08:31:55 Starting+compiler/backend/proofs
Jan 16 10:12:34 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6037.97+14914964
Jan 16 10:12:34 Starting+compiler/backend/serialiser
Jan 16 10:15:02 Finished+compiler/backend/serialiser+++++++++++++++++++++++148.04+1833252
Jan 16 10:15:02 Starting+compiler/encoders/x64/proofs
Jan 16 10:36:37 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1294.17+4749920
Jan 16 10:36:37 Starting+compiler/encoders/arm7/proofs
Jan 16 11:06:25 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1787.60+3768456
Jan 16 11:06:25 Starting+compiler/encoders/arm8/proofs
Jan 16 11:21:40 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++914.66+1784476
Jan 16 11:21:40 Starting+compiler/encoders/mips/proofs
Jan 16 11:44:41 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1381.18+2654552
Jan 16 11:44:42 Starting+compiler/encoders/riscv/proofs
Jan 16 12:05:02 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1220.11+1295920
Jan 16 12:05:02 Starting+compiler/encoders/ag32/proofs
Jan 16 12:10:40 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++337.35+940188
Jan 16 12:10:40 Starting+compiler/backend/x64/proofs
Jan 16 12:11:31 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++51.04+1449452
Jan 16 12:11:31 Starting+compiler/backend/arm7/proofs
Jan 16 12:12:26 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++54.43+1710700
Jan 16 12:12:26 Starting+compiler/backend/arm8/proofs
Jan 16 12:13:17 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++51.32+1607400
Jan 16 12:13:18 Starting+compiler/backend/mips/proofs
Jan 16 12:14:13 Finished+compiler/backend/mips/proofs++++++++++++++++++++++54.96+1203804
Jan 16 12:14:13 Starting+compiler/backend/riscv/proofs
Jan 16 12:15:02 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++49.03+1383144
Jan 16 12:15:02 Starting+compiler/backend/ag32/proofs
Jan 16 12:41:53 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1609.87+2723532
Jan 16 12:41:54 Starting+compiler/proofs
Jan 16 12:45:39 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++225.72+2880380
Jan 16 12:45:40 Starting+candle/set-theory
Jan 16 12:46:38 Finished+candle/set-theory+++++++++++++++++++++++++++++++++58.63+738464
Jan 16 12:46:39 Starting+candle/syntax-lib
Jan 16 12:47:03 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++23.91+658464
Jan 16 12:47:03 Starting+candle/standard/syntax
Jan 16 12:50:58 Finished+candle/standard/syntax++++++++++++++++++++++++++++235.05+1155480
Jan 16 12:50:58 Starting+candle/standard/semantics
Jan 16 12:54:45 Finished+candle/standard/semantics+++++++++++++++++++++++++226.81+1070860
Jan 16 12:54:46 Starting+candle/standard/monadic
Jan 16 12:58:08 Finished+candle/standard/monadic+++++++++++++++++++++++++++201.87+1720200
Jan 16 12:58:08 Starting+candle/standard/ml_kernel
Jan 16 13:12:03 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++835.26+4184836
Jan 16 13:12:03 Starting+candle/overloading/syntax
Jan 16 13:18:24 Finished+candle/overloading/syntax+++++++++++++++++++++++++380.14+1455588
Jan 16 13:18:24 Starting+candle/overloading/semantics
Jan 16 13:43:52 Finished+candle/overloading/semantics++++++++++++++++++++++1527.46+2160068
Jan 16 13:43:52 Starting+candle/prover
Jan 16 14:00:29 Finished+candle/prover+++++++++++++++++++++++++++++++++++++996.81+3323164
Jan 16 14:00:30 Starting+pancake
Jan 16 14:04:28 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++238.27+2738176
Jan 16 14:04:28 Starting+pancake/ffi
Jan 16 14:04:29 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.45+7564
Jan 16 14:04:29 Starting+pancake/semantics
Jan 16 14:09:23 Finished+pancake/semantics+++++++++++++++++++++++++++++++++294.35+1144236
Jan 16 14:09:24 Starting+pancake/proofs
Jan 16 14:35:14 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1550.20+6905824
Jan 16 14:35:14 Starting+characteristic/examples
Jan 16 14:38:11 Finished+characteristic/examples+++++++++++++++++++++++++++176.40+3304976
Jan 16 14:38:11 Starting+tutorial/solutions
Jan 16 15:13:55 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2143.97+14858896
Jan 16 15:13:56 Starting+translator/monadic/examples
Jan 16 15:19:46 Finished+translator/monadic/examples+++++++++++++++++++++++350.25+3550040
Jan 16 15:19:46 Starting+examples
Jan 16 15:21:14 FAILED:+examples
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
README.md                                                                                                                                                                                                              examples  (0s)     OK
Starting work on catProgTheory
source_valuesTheory                                                                                                                                                                                          examples/bootstrap  (4s)     OK
Starting work on source_syntaxTheory
source_syntaxTheory                                                                                                                                                                                          examples/bootstrap  (1s)     OK
Starting work on parsingTheory
regexp_parserTheory                                                                                                                                                                           examples/formal-languages/regular (25s)     OK
Starting work on printingTheory
printingTheory                                                                                                                                                                                               examples/bootstrap  (9s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]                                                                                                                                                                (25.974s) 
Starting work on lcsTheory
parsingTheory                                                                                                                                                                                                examples/bootstrap (43s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                                                                                                                                                                               (59.748s) 
Starting work on divTheory
lcsTheory                                                                                                                                                                                                              examples (23s)     OK
Starting work on diffTheory
diffTheory                                                                                                                                                                                                             examples (18s)FAIL<1>
 Saved definition ____ "patch_alg_def"
 Saved definition ____ "patch_alg_offs_def"
 Saved theorem _______ "string_concat_empty"
 Saved theorem _______ "tokens_append_strlit"
 error in quse /root/regression/cakeml-1714/examples/diffScript.sml : Fail "Static Errors"
 error in load /root/regression/cakeml-1714/examples/diffScript : Fail "Static Errors"
 Saved theorem _______ "tokens_append_right_strlit"
 /root/regression/cakeml-1714/examples/diffScript.sml:271: error: Value or constructor (zero_pad_def) has not been declared
 Found near [zero_pad_def]
 Uncaught exception: Fail "Static Errors"
quicksortProgTheory                                                                                                                                                                                                    examples (78s)MKILLED
catProgTheory                                                                                                                                                                                                          examples (78s)MKILLED
divTheory                                                                                                                                                                                                              examples (26s)MKILLED