Job 1823

CakeML:6ea4b61bbb6d25815c5b016af56ce83fbb3660f2
  Merge remote-tracking branch 'origin/master' into array-fixed [Mar 13 10:13:34]
#867 (array-fixed)
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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 14 10:35:05 Claimed job
Mar 14 10:35:07 Reusing HOL
Mar 14 10:35:48 Starting developers
Mar 14 10:35:54 Finished developers                                               4s  75MB
Mar 14 10:35:54 Starting developers/bin
Mar 14 10:36:01 Finished developers/bin                                           6s   1GB
Mar 14 10:36:01 Starting semantics/ffi
Mar 14 10:36:13 Finished semantics/ffi                                           12s 213MB
Mar 14 10:36:14 Starting semantics
Mar 14 10:38:33 Finished semantics                                             2m19s 810MB
Mar 14 10:38:33 Starting semantics/proofs
Mar 14 10:43:13 Finished semantics/proofs                                      4m40s   3GB
Mar 14 10:43:14 Starting semantics/alt_semantics
Mar 14 10:43:33 Finished semantics/alt_semantics                                 18s 468MB
Mar 14 10:43:33 Starting semantics/alt_semantics/proofs
Mar 14 10:46:16 Finished semantics/alt_semantics/proofs                        2m42s   1GB
Mar 14 10:46:16 Starting basis/pure
Mar 14 21:57:57 Resuming basis/pure
Mar 14 21:58:20 Finished basis/pure                                              22s 264MB
Mar 14 21:58:20 Starting translator
Mar 14 22:01:58 Finished translator                                            3m37s 984MB
Mar 14 22:01:58 Starting compiler/parsing
Mar 14 22:03:52 Finished compiler/parsing                                      1m53s 811MB
Mar 14 22:03:53 Starting characteristic
Mar 14 22:11:36 Finished characteristic                                        7m42s   1GB
Mar 14 22:11:36 Starting translator/monadic
Mar 14 22:14:15 Finished translator/monadic                                    2m38s 587MB
Mar 14 22:14:15 Starting basis
Mar 14 23:13:50 Finished basis                                                59m34s   3GB
Mar 14 23:13:50 Starting compiler/inference
Mar 14 23:15:24 Finished compiler/inference                                    1m33s   1GB
Mar 14 23:15:24 Starting compiler/backend/reg_alloc
Mar 14 23:17:30 Finished compiler/backend/reg_alloc                            2m05s   1GB
Mar 14 23:17:30 Starting compiler/backend/gc
Mar 14 23:22:51 Finished compiler/backend/gc                                   5m20s   1GB
Mar 14 23:22:51 Starting compiler/backend
Mar 14 23:30:15 Finished compiler/backend                                      7m23s   1GB
Mar 14 23:30:16 Starting compiler/encoders/asm
Mar 14 23:30:49 Finished compiler/encoders/asm                                   32s 695MB
Mar 14 23:30:49 Starting compiler/encoders/x64
Mar 14 23:31:22 Finished compiler/encoders/x64                                   32s 856MB
Mar 14 23:31:22 Starting compiler/encoders/arm7
Mar 14 23:32:21 Finished compiler/encoders/arm7                                  58s 771MB
Mar 14 23:32:21 Starting compiler/encoders/arm8
Mar 14 23:32:40 Finished compiler/encoders/arm8                                  18s 787MB
Mar 14 23:32:40 Starting compiler/encoders/arm8_asl
Mar 14 23:35:44 Finished compiler/encoders/arm8_asl                            3m03s   1GB
Mar 14 23:35:44 Starting compiler/encoders/mips
Mar 14 23:36:07 Finished compiler/encoders/mips                                  23s   1GB
Mar 14 23:36:08 Starting compiler/encoders/riscv
Mar 14 23:36:29 Finished compiler/encoders/riscv                                 21s 792MB
Mar 14 23:36:29 Starting compiler/encoders/ag32
Mar 14 23:36:54 Finished compiler/encoders/ag32                                  24s 807MB
Mar 14 23:36:54 Starting compiler/backend/x64
Mar 14 23:37:18 Finished compiler/backend/x64                                    23s   1GB
Mar 14 23:37:18 Starting compiler/backend/arm7
Mar 14 23:37:43 Finished compiler/backend/arm7                                   24s   1GB
Mar 14 23:37:43 Starting compiler/backend/arm8
Mar 14 23:38:09 Finished compiler/backend/arm8                                   25s   1GB
Mar 14 23:38:09 Starting compiler/backend/mips
Mar 14 23:38:32 Finished compiler/backend/mips                                   22s 975MB
Mar 14 23:38:32 Starting compiler/backend/riscv
Mar 14 23:38:56 Finished compiler/backend/riscv                                  23s   1GB
Mar 14 23:38:56 Starting compiler/backend/ag32
Mar 14 23:40:32 Finished compiler/backend/ag32                                 1m36s   1GB
Mar 14 23:40:33 Starting compiler/parsing/proofs
Mar 14 23:44:46 Finished compiler/parsing/proofs                               4m13s   1GB
Mar 14 23:44:46 Starting compiler/inference/proofs
Mar 14 23:47:48 Finished compiler/inference/proofs                             3m01s   1GB
Mar 14 23:47:48 Starting compiler/backend/semantics
Mar 15 00:26:01 Finished compiler/backend/semantics                           38m13s   1GB
Mar 15 00:26:01 Starting compiler/backend/reg_alloc/proofs
Mar 15 00:30:06 Finished compiler/backend/reg_alloc/proofs                     4m05s 836MB
Mar 15 00:30:06 Starting compiler/backend/proofs
Mar 15 01:41:13 Finished compiler/backend/proofs                            1h11m05s   4GB
Mar 15 01:41:14 Starting compiler/backend/serialiser
Mar 15 01:43:17 Finished compiler/backend/serialiser                           2m03s   1GB
Mar 15 01:43:17 Starting compiler/encoders/x64/proofs
Mar 15 01:55:45 Finished compiler/encoders/x64/proofs                         12m27s   1GB
Mar 15 01:55:45 Starting compiler/encoders/arm7/proofs
Mar 15 02:12:22 Finished compiler/encoders/arm7/proofs                        16m36s   1GB
Mar 15 02:12:23 Starting compiler/encoders/arm8/proofs
Mar 15 02:20:48 Finished compiler/encoders/arm8/proofs                         8m25s 807MB
Mar 15 02:20:48 Starting compiler/encoders/arm8_asl/proofs
Mar 15 02:39:01 Finished compiler/encoders/arm8_asl/proofs                    18m12s   1GB
Mar 15 02:39:01 Starting compiler/encoders/mips/proofs
Mar 15 02:51:05 Finished compiler/encoders/mips/proofs                        12m03s 984MB
Mar 15 02:51:06 Starting compiler/encoders/riscv/proofs
Mar 15 03:01:49 Finished compiler/encoders/riscv/proofs                       10m42s 591MB
Mar 15 03:01:49 Starting compiler/encoders/ag32/proofs
Mar 15 03:04:53 Finished compiler/encoders/ag32/proofs                         3m03s 494MB
Mar 15 03:04:53 Starting compiler/backend/x64/proofs
Mar 15 03:05:44 Finished compiler/backend/x64/proofs                             50s 763MB
Mar 15 03:05:44 Starting compiler/backend/arm7/proofs
Mar 15 03:06:24 Finished compiler/backend/arm7/proofs                            40s 954MB
Mar 15 03:06:24 Starting compiler/backend/arm8/proofs
Mar 15 03:06:55 Finished compiler/backend/arm8/proofs                            30s   1GB
Mar 15 03:06:55 Starting compiler/backend/arm8_asl
Mar 15 03:07:20 Finished compiler/backend/arm8_asl                               24s   1GB
Mar 15 03:07:20 Starting compiler/backend/mips/proofs
Mar 15 03:07:51 Finished compiler/backend/mips/proofs                            30s   1GB
Mar 15 03:07:51 Starting compiler/backend/riscv/proofs
Mar 15 03:08:37 Finished compiler/backend/riscv/proofs                           45s 791MB
Mar 15 03:08:37 Starting compiler/backend/ag32/proofs
Mar 15 03:24:57 Finished compiler/backend/ag32/proofs                         16m19s   1GB
Mar 15 03:24:58 Starting compiler/proofs
Mar 15 03:28:04 Finished compiler/proofs                                       3m05s   2GB
Mar 15 03:28:04 Starting candle/set-theory
Mar 15 03:28:43 Finished candle/set-theory                                       39s 637MB
Mar 15 03:28:44 Starting candle/syntax-lib
Mar 15 03:28:58 Finished candle/syntax-lib                                       14s 628MB
Mar 15 03:28:59 Starting candle/standard/syntax
Mar 15 03:31:19 Finished candle/standard/syntax                                2m19s   1GB
Mar 15 03:31:19 Starting candle/standard/semantics
Mar 15 03:33:26 Finished candle/standard/semantics                             2m06s   1GB
Mar 15 03:33:26 Starting candle/standard/monadic
Mar 15 03:35:40 Finished candle/standard/monadic                               2m14s   1GB
Mar 15 03:35:41 Starting candle/standard/ml_kernel
Mar 15 03:43:24 Finished candle/standard/ml_kernel                             7m43s   2GB
Mar 15 03:43:25 Starting candle/overloading/syntax
Mar 15 03:47:06 Finished candle/overloading/syntax                             3m40s   1GB
Mar 15 03:47:06 Starting candle/overloading/semantics
Mar 15 04:00:06 Finished candle/overloading/semantics                         12m58s   2GB
Mar 15 04:00:06 Starting candle/overloading/monadic
Mar 15 04:03:00 Finished candle/overloading/monadic                            2m54s   1GB
Mar 15 04:03:00 Starting candle/overloading/ml_kernel
Mar 15 04:11:46 Finished candle/overloading/ml_kernel                          8m45s   1GB
Mar 15 04:11:46 Starting candle/overloading/ml_checker
Mar 15 04:14:54 Finished candle/overloading/ml_checker                         3m07s   1GB
Mar 15 04:14:54 Starting candle/prover
Mar 15 04:25:10 Finished candle/prover                                        10m15s   1GB
Mar 15 04:25:10 Starting pancake
Mar 15 04:29:59 Finished pancake                                               4m49s   2GB
Mar 15 04:30:00 Starting pancake/ffi
Mar 15 04:30:00 Finished pancake/ffi                                              0s  17MB
Mar 15 04:30:01 Starting pancake/semantics
Mar 15 04:33:04 Finished pancake/semantics                                     3m03s   1GB
Mar 15 04:33:05 Starting pancake/proofs
Mar 15 04:48:43 Finished pancake/proofs                                       15m37s   2GB
Mar 15 04:48:43 Starting characteristic/examples
Mar 15 04:50:39 Finished characteristic/examples                               1m55s 762MB
Mar 15 04:50:39 Starting tutorial/solutions
Mar 15 05:10:38 Finished tutorial/solutions                                   19m55s   6GB
Mar 15 05:10:38 Starting translator/monadic/examples
Mar 15 05:15:36 Finished translator/monadic/examples                           4m57s   2GB
Mar 15 05:15:36 Starting examples
Mar 15 05:29:58 Finished examples                                             14m21s   3GB
Mar 15 05:29:58 Starting examples/compilation/x64
Mar 15 08:41:26 Finished examples/compilation/x64                           3h11m25s   5GB
Mar 15 08:41:26 Starting examples/compilation/x64/proofs
Mar 15 08:45:24 Finished examples/compilation/x64/proofs                       3m57s   2GB
Mar 15 08:45:24 Starting examples/compilation/ag32
Mar 15 09:29:30 Finished examples/compilation/ag32                            44m05s   5GB
Mar 15 09:29:30 Starting examples/compilation/ag32/proofs
Mar 15 09:31:37 Finished examples/compilation/ag32/proofs                      2m07s   1GB
Mar 15 09:31:38 Starting examples/cost
Mar 15 10:47:05 Finished examples/cost                                      1h15m26s   3GB
Mar 15 10:47:05 Starting examples/lpr_checker
Mar 15 10:48:29 Finished examples/lpr_checker                                  1m23s   1GB
Mar 15 10:48:29 Starting examples/lpr_checker/array
Mar 15 11:23:16 Finished examples/lpr_checker/array                           34m46s   3GB
Mar 15 11:23:16 Starting examples/lpr_checker/array/compilation
Mar 15 13:25:56 Finished examples/lpr_checker/array/compilation             2h02m39s   6GB
Mar 15 13:25:57 Starting examples/lpr_checker/array/compilation/proofs
Mar 15 13:28:36 Finished examples/lpr_checker/array/compilation/proofs         2m39s   2GB
Mar 15 13:28:36 Starting examples/opentheory
Mar 15 13:40:59 Finished examples/opentheory                                  12m22s   2GB
Mar 15 13:41:00 Starting examples/opentheory
Mar 15 13:41:02 Finished examples/opentheory                                      1s  18MB
Mar 15 13:41:02 Starting examples/opentheory/compilation
Mar 15 14:42:14 Finished examples/opentheory/compilation                    1h01m11s   5GB
Mar 15 14:42:14 Starting examples/opentheory/compilation/proofs
Mar 15 14:43:42 Finished examples/opentheory/compilation/proofs                1m27s   3GB
Mar 15 14:43:42 Starting examples/opentheory/compilation/ag32
Mar 15 15:40:10 Finished examples/opentheory/compilation/ag32                 56m28s   4GB
Mar 15 15:40:11 Starting examples/opentheory/compilation/ag32/proofs
Mar 15 15:43:01 Finished examples/opentheory/compilation/ag32/proofs           2m49s   2GB
Mar 15 15:43:01 Starting examples/sat_encodings
Mar 15 15:45:28 Finished examples/sat_encodings                                2m26s 928MB
Mar 15 15:45:28 Starting examples/sat_encodings/case_studies
Mar 15 15:47:37 Finished examples/sat_encodings/case_studies                   2m08s 721MB
Mar 15 15:47:37 Starting examples/sat_encodings/translation
Mar 15 15:55:18 Finished examples/sat_encodings/translation                    7m40s   1GB
Mar 15 15:55:18 Starting examples/sat_encodings/translation/compilation
Mar 15 17:03:53 Finished examples/sat_encodings/translation/compilation     1h08m34s   5GB
Mar 15 17:03:53 Starting translator/okasaki-examples
Mar 15 17:09:46 Finished translator/okasaki-examples                           5m53s   1GB
Mar 15 17:09:46 Starting translator/other-examples
Mar 15 17:10:56 Finished translator/other-examples                             1m09s   1GB
Mar 15 17:10:56 Starting compiler/parsing/tests
Mar 15 17:11:31 Finished compiler/parsing/tests                                  34s 656MB
Mar 15 17:11:31 Starting compiler/inference/tests
Mar 15 17:20:09 Finished compiler/inference/tests                              8m37s   4GB
Mar 15 17:20:10 Starting compiler/printing/test
Mar 15 17:24:42 Finished compiler/printing/test                                4m31s   1GB
Mar 15 17:24:42 Starting compiler/repl
Mar 15 17:40:13 Finished compiler/repl                                        15m30s   4GB
Mar 15 17:40:13 Starting compiler/bootstrap/translation
Mar 15 23:01:06 Finished compiler/bootstrap/translation                     5h20m52s   8GB
Mar 15 23:01:06 Starting unverified/sexpr-bootstrap/x64/64
Mar 15 23:13:02 Finished unverified/sexpr-bootstrap/x64/64                    11m55s   8GB
Mar 15 23:13:02 Starting unverified/sexpr-bootstrap/x64/32
Mar 15 23:23:48 Finished unverified/sexpr-bootstrap/x64/32                    10m45s   8GB
Mar 15 23:23:48 Starting compiler/benchmarks
Mar 15 23:23:55 Finished compiler/benchmarks                                      7s  29MB
Mar 15 23:23:55 Starting compiler/bootstrap/compilation/x64/64
Mar 18 13:56:12 FAILED: compiler/bootstrap/compilation/x64/64
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)/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)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/ocaml[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/candle/prover[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanned 90 directories
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                                           (0s)     OK
cake-sexpr-32                                                     (281s)     OK
cake-sexpr-64                                                     (287s)     OK
to_dataBootstrapTheory                                            (158m)     OK
Starting work on to_lab_x64BootstrapTheory
to_lab_x64BootstrapTheory                                          (44h)     OK
Starting work on cake.S
cake.S                                                            (949m)FAIL<1>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL message: Created theory "x64Bootstrap">>
           lab_to_target eval: runtime: 15h10m30s,    gctime: 12h15m58s,     systime: 10m28s.
           lab_to_target real: 18h10m29s
           lab_to_target size: 143909427
 Warning - Unable to increase stack - interrupting thread
 error in quse /home/cake/oven/regression/cakeml-1823/compiler/bootstrap/compilation/x64/64/x64BootstrapScript.sml : Interrupt
 error in load /home/cake/oven/regression/cakeml-1823/compiler/bootstrap/compilation/x64/64/x64BootstrapScript : Interrupt
 Uncaught exception: Interrupt