Job 1717

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:af01322db66662cdba8bcd13dd1e0fa76d818bfa
  Proper names for theorems. [Jan 14 05:47:46]
Machine:oven3+4.19.67.1.amd64-smp+

Jan 16 21:01:20 Claimed job
Jan 16 21:01:25 Building+HOL
Jan 16 21:21:02 Starting+developers
Jan 16 21:21:10 Finished+developers++++++++++++++++++++++++++++++++++++++++8.20+164080
Jan 16 21:21:11 Starting+developers/bin
Jan 16 21:21:21 Finished+developers/bin++++++++++++++++++++++++++++++++++++9.55+675824
Jan 16 21:21:21 Starting+semantics/ffi
Jan 16 21:21:41 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++20.28+238016
Jan 16 21:21:41 Starting+semantics
Jan 16 21:24:59 Finished+semantics+++++++++++++++++++++++++++++++++++++++++197.44+1499432
Jan 16 21:24:59 Starting+semantics/proofs
Jan 16 21:32:51 Finished+semantics/proofs++++++++++++++++++++++++++++++++++471.90+1541496
Jan 16 21:32:52 Starting+semantics/alt_semantics
Jan 16 21:33:18 Finished+semantics/alt_semantics+++++++++++++++++++++++++++26.26+394612
Jan 16 21:33:18 Starting+semantics/alt_semantics/proofs
Jan 16 21:38:40 Finished+semantics/alt_semantics/proofs++++++++++++++++++++321.69+968260
Jan 16 21:38:40 Starting+basis/pure
Jan 16 21:44:53 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++372.87+712992
Jan 16 21:44:54 Starting+translator
Jan 16 21:50:45 Finished+translator++++++++++++++++++++++++++++++++++++++++350.94+1748240
Jan 16 21:50:45 Starting+compiler/parsing
Jan 16 21:53:26 Finished+compiler/parsing++++++++++++++++++++++++++++++++++160.58+2728320
Jan 16 21:53:26 Starting+characteristic
Jan 16 22:05:28 Finished+characteristic++++++++++++++++++++++++++++++++++++721.89+2061664
Jan 16 22:05:28 Starting+translator/monadic
Jan 16 22:08:55 Finished+translator/monadic++++++++++++++++++++++++++++++++207.19+1534260
Jan 16 22:08:56 Starting+basis
Jan 16 23:50:06 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6069.15+21895224
Jan 16 23:50:07 Starting+compiler/inference
Jan 16 23:52:46 Finished+compiler/inference++++++++++++++++++++++++++++++++159.53+1609208
Jan 16 23:52:47 Starting+compiler/backend/reg_alloc
Jan 16 23:54:50 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++123.39+1279636
Jan 16 23:54:50 Starting+compiler/backend/gc
Jan 17 00:01:41 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++410.34+1978640
Jan 17 00:01:41 Starting+compiler/backend
Jan 17 00:10:37 Finished+compiler/backend++++++++++++++++++++++++++++++++++535.83+2515996
Jan 17 00:10:37 Starting+compiler/encoders/asm
Jan 17 00:11:29 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++51.40+579940
Jan 17 00:11:29 Starting+compiler/encoders/x64
Jan 17 00:13:48 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++138.40+746292
Jan 17 00:13:48 Starting+compiler/encoders/arm7
Jan 17 00:18:17 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++268.53+1458044
Jan 17 00:18:17 Starting+compiler/encoders/arm8
Jan 17 00:19:40 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++83.19+904100
Jan 17 00:19:40 Starting+compiler/encoders/mips
Jan 17 00:22:56 Finished+compiler/encoders/mips++++++++++++++++++++++++++++195.89+1158512
Jan 17 00:22:57 Starting+compiler/encoders/riscv
Jan 17 00:26:41 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++224.08+1125320
Jan 17 00:26:41 Starting+compiler/encoders/ag32
Jan 17 00:27:24 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++42.56+644220
Jan 17 00:27:24 Starting+compiler/backend/x64
Jan 17 00:28:07 Finished+compiler/backend/x64++++++++++++++++++++++++++++++42.42+1295896
Jan 17 00:28:07 Starting+compiler/backend/arm7
Jan 17 00:28:52 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++44.85+1663128
Jan 17 00:28:52 Starting+compiler/backend/arm8
Jan 17 00:29:35 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++42.57+1376220
Jan 17 00:29:35 Starting+compiler/backend/mips
Jan 17 00:30:18 Finished+compiler/backend/mips+++++++++++++++++++++++++++++42.73+1451752
Jan 17 00:30:18 Starting+compiler/backend/riscv
Jan 17 00:31:03 Finished+compiler/backend/riscv++++++++++++++++++++++++++++44.84+1441116
Jan 17 00:31:04 Starting+compiler/backend/ag32
Jan 17 00:33:28 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++144.52+1765560
Jan 17 00:33:28 Starting+compiler/parsing/proofs
Jan 17 00:41:47 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++498.70+1247576
Jan 17 00:41:48 Starting+compiler/inference/proofs
Jan 17 00:47:03 Finished+compiler/inference/proofs+++++++++++++++++++++++++315.22+969492
Jan 17 00:47:03 Starting+compiler/backend/semantics
Jan 17 01:49:32 Finished+compiler/backend/semantics++++++++++++++++++++++++3748.89+2093772
Jan 17 01:49:33 Starting+compiler/backend/reg_alloc/proofs
Jan 17 01:57:29 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++476.65+903436
Jan 17 01:57:30 Starting+compiler/backend/proofs
Jan 17 03:39:08 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6096.66+23329812
Jan 17 03:39:09 Starting+compiler/backend/serialiser
Jan 17 03:41:35 Finished+compiler/backend/serialiser+++++++++++++++++++++++145.98+1305092
Jan 17 03:41:35 Starting+compiler/encoders/x64/proofs
Jan 17 04:03:15 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1300.37+4664024
Jan 17 04:03:16 Starting+compiler/encoders/arm7/proofs
Jan 17 04:32:42 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1766.00+5617068
Jan 17 04:32:42 Starting+compiler/encoders/arm8/proofs
Jan 17 04:48:03 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++920.30+1610296
Jan 17 04:48:03 Starting+compiler/encoders/mips/proofs
Jan 17 05:10:11 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1328.20+2712468
Jan 17 05:10:12 Starting+compiler/encoders/riscv/proofs
Jan 17 05:30:15 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1203.25+1174612
Jan 17 05:30:15 Starting+compiler/encoders/ag32/proofs
Jan 17 05:36:01 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++345.77+1049928
Jan 17 05:36:01 Starting+compiler/backend/x64/proofs
Jan 17 05:36:51 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++49.28+1568068
Jan 17 05:36:51 Starting+compiler/backend/arm7/proofs
Jan 17 05:37:46 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++54.50+1706220
Jan 17 05:37:46 Starting+compiler/backend/arm8/proofs
Jan 17 05:38:37 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++50.71+1577220
Jan 17 05:38:37 Starting+compiler/backend/mips/proofs
Jan 17 05:39:27 Finished+compiler/backend/mips/proofs++++++++++++++++++++++49.76+1232364
Jan 17 05:39:27 Starting+compiler/backend/riscv/proofs
Jan 17 05:40:18 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++50.80+1782192
Jan 17 05:40:18 Starting+compiler/backend/ag32/proofs
Jan 17 06:08:26 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1687.08+2469044
Jan 17 06:08:26 Starting+compiler/proofs
Jan 17 06:12:36 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++249.76+3298388
Jan 17 06:12:36 Starting+candle/set-theory
Jan 17 06:13:35 Finished+candle/set-theory+++++++++++++++++++++++++++++++++58.74+684844
Jan 17 06:13:35 Starting+candle/syntax-lib
Jan 17 06:13:59 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++23.14+687608
Jan 17 06:13:59 Starting+candle/standard/syntax
Jan 17 06:17:48 Finished+candle/standard/syntax++++++++++++++++++++++++++++228.79+995076
Jan 17 06:17:48 Starting+candle/standard/semantics
Jan 17 06:21:30 Finished+candle/standard/semantics+++++++++++++++++++++++++221.71+1337984
Jan 17 06:21:30 Starting+candle/standard/monadic
Jan 17 06:24:55 Finished+candle/standard/monadic+++++++++++++++++++++++++++204.25+1055624
Jan 17 06:24:55 Starting+candle/standard/ml_kernel
Jan 17 06:39:07 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++851.95+3204888
Jan 17 06:39:07 Starting+candle/overloading/syntax
Jan 17 06:45:34 Finished+candle/overloading/syntax+++++++++++++++++++++++++386.62+1036160
Jan 17 06:45:34 Starting+candle/overloading/semantics
Jan 17 07:10:50 Finished+candle/overloading/semantics++++++++++++++++++++++1514.92+2956304
Jan 17 07:10:50 Starting+candle/prover
Jan 17 07:27:41 Finished+candle/prover+++++++++++++++++++++++++++++++++++++1010.54+3807988
Jan 17 07:27:41 Starting+pancake
Jan 17 07:31:50 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++249.51+2854444
Jan 17 07:31:51 Starting+pancake/ffi
Jan 17 07:31:51 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.47+7796
Jan 17 07:31:52 Starting+pancake/semantics
Jan 17 07:36:47 Finished+pancake/semantics+++++++++++++++++++++++++++++++++295.09+1597748
Jan 17 07:36:47 Starting+pancake/proofs
Jan 17 08:02:51 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1564.17+6776804
Jan 17 08:02:52 Starting+characteristic/examples
Jan 17 08:05:49 Finished+characteristic/examples+++++++++++++++++++++++++++177.11+3124764
Jan 17 08:05:49 Starting+tutorial/solutions
Jan 17 08:41:36 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2146.28+13858704
Jan 17 08:41:36 Starting+translator/monadic/examples
Jan 17 08:47:22 Finished+translator/monadic/examples+++++++++++++++++++++++345.55+2792564
Jan 17 08:47:22 Starting+examples
Jan 17 08:48:47 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 (24s)     OK
Starting work on printingTheory
printingTheory                                                                                                                                                                                               examples/bootstrap  (8s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]                                                                                                                                                                (24.234s) 
Starting work on lcsTheory
parsingTheory                                                                                                                                                                                                examples/bootstrap (39s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                                                                                                                                                                               (54.216s) 
Starting work on divTheory
lcsTheory                                                                                                                                                                                                              examples (25s)     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-1717/examples/diffScript.sml : Fail "Static Errors"
 error in load /root/regression/cakeml-1717/examples/diffScript : Fail "Static Errors"
 Saved theorem _______ "tokens_append_right_strlit"
 /root/regression/cakeml-1717/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 (77s)MKILLED
catProgTheory                                                                                                                                                                                                          examples (78s)MKILLED
divTheory                                                                                                                                                                                                              examples (30s)MKILLED