Job 1336

CakeML:aed4cf53de006242fd0045168e342cff29d27373
  tweak basis_ffi.c to avoid warnings from -Wall [Sep 08 08:52:54]
#749 (update_basis)
Merging into:ce8a04cfea6a1cde3a0e1522d40c67d10fbeb4ff
  Merge pull request #750 from arolle/master [Sep 08 14:08:03]
HOL:88de89b34812af401d9d2e112d6f2d895ee06bc2
  Get new quote-filter test to also work under Moscow ML [Sep 09 04:11:33]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Sep 12 00:03:27 Claimed job
Sep 12 00:03:35 Building HOL
Sep 12 00:16:43 Starting developers
Sep 12 00:16:46 Finished developers                                               2s  94MB
Sep 12 00:16:46 Starting developers/bin
Sep 12 00:16:52 Finished developers/bin                                           6s   1GB
Sep 12 00:16:52 Starting semantics/ffi
Sep 12 00:17:03 Finished semantics/ffi                                           10s 327MB
Sep 12 00:17:03 Starting semantics
Sep 12 00:18:37 Finished semantics                                             1m33s   1GB
Sep 12 00:18:37 Starting semantics/proofs
Sep 12 00:21:56 Finished semantics/proofs                                      3m18s   2GB
Sep 12 00:21:56 Starting semantics/alt_semantics
Sep 12 00:22:04 Finished semantics/alt_semantics                                  8s 451MB
Sep 12 00:22:04 Starting semantics/alt_semantics/proofs
Sep 12 00:24:05 Finished semantics/alt_semantics/proofs                        2m00s   1GB
Sep 12 00:24:05 Starting basis/pure
Sep 12 00:26:44 Finished basis/pure                                            2m38s   1GB
Sep 12 00:26:44 Starting translator
Sep 12 00:29:23 Finished translator                                            2m38s   2GB
Sep 12 00:29:23 Starting compiler/parsing
Sep 12 00:30:33 Finished compiler/parsing                                      1m10s   3GB
Sep 12 00:30:33 Starting characteristic
Sep 12 00:36:18 Finished characteristic                                        5m44s   3GB
Sep 12 00:36:18 Starting translator/monadic
Sep 12 00:37:57 Finished translator/monadic                                    1m38s   1GB
Sep 12 00:37:57 Starting basis
Sep 12 01:10:48 Finished basis                                                32m50s  39GB
Sep 12 01:10:48 Starting compiler/inference
Sep 12 01:11:58 Finished compiler/inference                                    1m09s   1GB
Sep 12 01:11:58 Starting compiler/backend/reg_alloc
Sep 12 01:13:06 Finished compiler/backend/reg_alloc                            1m07s   2GB
Sep 12 01:13:06 Starting compiler/backend/gc
Sep 12 01:16:36 Finished compiler/backend/gc                                   3m29s   3GB
Sep 12 01:16:36 Starting compiler/backend
Sep 12 01:21:32 Finished compiler/backend                                      4m55s   4GB
Sep 12 01:21:32 Starting compiler/encoders/asm
Sep 12 01:21:54 Finished compiler/encoders/asm                                   22s   1GB
Sep 12 01:21:54 Starting compiler/encoders/x64
Sep 12 01:22:54 Finished compiler/encoders/x64                                   59s   1GB
Sep 12 01:22:54 Starting compiler/encoders/arm7
Sep 12 01:24:41 Finished compiler/encoders/arm7                                1m46s   1GB
Sep 12 01:24:41 Starting compiler/encoders/arm8
Sep 12 01:25:18 Finished compiler/encoders/arm8                                  37s   1GB
Sep 12 01:25:19 Starting compiler/encoders/mips
Sep 12 01:26:31 Finished compiler/encoders/mips                                1m12s   1GB
Sep 12 01:26:31 Starting compiler/encoders/riscv
Sep 12 01:27:58 Finished compiler/encoders/riscv                               1m26s   1GB
Sep 12 01:27:58 Starting compiler/encoders/ag32
Sep 12 01:28:16 Finished compiler/encoders/ag32                                  18s   1GB
Sep 12 01:28:16 Starting compiler/backend/x64
Sep 12 01:28:35 Finished compiler/backend/x64                                    18s   1GB
Sep 12 01:28:36 Starting compiler/backend/arm7
Sep 12 01:28:56 Finished compiler/backend/arm7                                   20s   1GB
Sep 12 01:28:56 Starting compiler/backend/arm8
Sep 12 01:29:15 Finished compiler/backend/arm8                                   18s   1GB
Sep 12 01:29:15 Starting compiler/backend/mips
Sep 12 01:29:35 Finished compiler/backend/mips                                   19s   1GB
Sep 12 01:29:35 Starting compiler/backend/riscv
Sep 12 01:29:55 Finished compiler/backend/riscv                                  19s   1GB
Sep 12 01:29:55 Starting compiler/backend/ag32
Sep 12 01:31:06 Finished compiler/backend/ag32                                 1m10s   2GB
Sep 12 01:31:06 Starting compiler/parsing/proofs
Sep 12 01:33:15 Finished compiler/parsing/proofs                               2m08s   1GB
Sep 12 01:33:15 Starting compiler/inference/proofs
Sep 12 01:35:33 Finished compiler/inference/proofs                             2m17s   1GB
Sep 12 01:35:33 Starting compiler/backend/semantics
Sep 12 02:01:18 Finished compiler/backend/semantics                           25m44s   2GB
Sep 12 02:01:18 Starting compiler/backend/reg_alloc/proofs
Sep 12 02:04:33 Finished compiler/backend/reg_alloc/proofs                     3m14s   1GB
Sep 12 02:04:33 Starting compiler/backend/proofs
Sep 12 02:55:28 Finished compiler/backend/proofs                              50m54s  30GB
Sep 12 02:55:28 Starting compiler/encoders/x64/proofs
Sep 12 03:04:57 Finished compiler/encoders/x64/proofs                          9m28s   6GB
Sep 12 03:04:57 Starting compiler/encoders/arm7/proofs
Sep 12 03:17:16 Finished compiler/encoders/arm7/proofs                        12m18s   8GB
Sep 12 03:17:16 Starting compiler/encoders/arm8/proofs
Sep 12 03:23:34 Finished compiler/encoders/arm8/proofs                         6m17s   3GB
Sep 12 03:23:34 Starting compiler/encoders/mips/proofs
Sep 12 03:33:18 Finished compiler/encoders/mips/proofs                         9m44s   3GB
Sep 12 03:33:19 Starting compiler/encoders/riscv/proofs
Sep 12 03:41:20 Finished compiler/encoders/riscv/proofs                        8m00s   3GB
Sep 12 03:41:20 Starting compiler/encoders/ag32/proofs
Sep 12 03:43:40 Finished compiler/encoders/ag32/proofs                         2m19s   1GB
Sep 12 03:43:40 Starting compiler/backend/x64/proofs
Sep 12 03:44:00 Finished compiler/backend/x64/proofs                             20s   1GB
Sep 12 03:44:00 Starting compiler/backend/arm7/proofs
Sep 12 03:44:23 Finished compiler/backend/arm7/proofs                            22s   2GB
Sep 12 03:44:23 Starting compiler/backend/arm8/proofs
Sep 12 03:44:42 Finished compiler/backend/arm8/proofs                            18s   1GB
Sep 12 03:44:42 Starting compiler/backend/mips/proofs
Sep 12 03:45:02 Finished compiler/backend/mips/proofs                            19s   1GB
Sep 12 03:45:03 Starting compiler/backend/riscv/proofs
Sep 12 03:45:24 Finished compiler/backend/riscv/proofs                           21s   2GB
Sep 12 03:45:24 Starting compiler/backend/ag32/proofs
Sep 12 03:57:19 Finished compiler/backend/ag32/proofs                         11m53s   4GB
Sep 12 03:57:19 Starting compiler/proofs
Sep 12 03:59:10 Finished compiler/proofs                                       1m50s   5GB
Sep 12 03:59:10 Starting candle/set-theory
Sep 12 03:59:39 Finished candle/set-theory                                       29s 968MB
Sep 12 03:59:39 Starting candle/syntax-lib
Sep 12 03:59:51 Finished candle/syntax-lib                                       11s 846MB
Sep 12 03:59:51 Starting candle/standard/syntax
Sep 12 04:01:42 Finished candle/standard/syntax                                1m51s   1GB
Sep 12 04:01:43 Starting candle/standard/semantics
Sep 12 04:03:25 Finished candle/standard/semantics                             1m42s   2GB
Sep 12 04:03:25 Starting candle/standard/monadic
Sep 12 04:05:06 Finished candle/standard/monadic                               1m41s   2GB
Sep 12 04:05:06 Starting candle/standard/ml_kernel
Sep 12 04:10:13 Finished candle/standard/ml_kernel                             5m06s   7GB
Sep 12 04:10:14 Starting candle/overloading/syntax
Sep 12 04:13:21 Finished candle/overloading/syntax                             3m06s   2GB
Sep 12 04:13:21 Starting candle/overloading/semantics
Sep 12 04:23:52 Finished candle/overloading/semantics                         10m31s   4GB
Sep 12 04:23:52 Starting characteristic/examples
Sep 12 04:25:06 Finished characteristic/examples                               1m13s   4GB
Sep 12 04:25:06 Starting tutorial/solutions
Sep 12 04:39:41 Finished tutorial/solutions                                   14m34s  11GB
Sep 12 04:39:41 Starting translator/monadic/examples
Sep 12 04:42:57 Finished translator/monadic/examples                           3m15s   4GB
Sep 12 04:42:57 Starting examples
Sep 12 04:51:17 Finished examples                                              8m19s   6GB
Sep 12 04:51:17 Starting examples/compilation/x64
Sep 12 07:01:12 Finished examples/compilation/x64                           2h09m54s  26GB
Sep 12 07:01:12 Starting examples/compilation/x64/proofs
Sep 12 07:02:58 Finished examples/compilation/x64/proofs                       1m45s   3GB
Sep 12 07:02:58 Starting examples/compilation/ag32
Sep 15 14:47:37 Resuming examples/compilation/ag32
Sep 15 14:47:39 Finished examples/compilation/ag32                                1s 147MB
Sep 15 14:47:39 Starting examples/compilation/ag32/proofs
Sep 15 14:48:23 Finished examples/compilation/ag32/proofs                        44s   4GB
Sep 15 14:48:24 Starting examples/cost
Sep 15 15:33:12 Finished examples/cost                                        44m48s  16GB
Sep 15 15:33:12 Starting examples/lpr_checker
Sep 15 15:36:51 Finished examples/lpr_checker                                  3m38s   4GB
Sep 15 15:36:51 Starting examples/lpr_checker/compilation
Sep 15 15:53:56 Finished examples/lpr_checker/compilation                     17m04s  11GB
Sep 15 15:53:56 Starting examples/lpr_checker/compilation/proofs
Sep 15 15:54:35 Finished examples/lpr_checker/compilation/proofs                 39s   3GB
Sep 15 15:54:35 Starting examples/lpr_checker/array
Sep 15 16:06:58 Finished examples/lpr_checker/array                           12m22s   5GB
Sep 15 16:06:58 Starting examples/lpr_checker/array/compilation
Sep 15 16:25:02 Finished examples/lpr_checker/array/compilation               18m04s  21GB
Sep 15 16:25:02 Starting examples/lpr_checker/array/compilation/proofs
Sep 15 16:25:52 Finished examples/lpr_checker/array/compilation/proofs           48s   4GB
Sep 15 16:25:52 Starting examples/opentheory
Sep 15 16:34:49 Finished examples/opentheory                                   8m56s   6GB
Sep 15 16:34:49 Starting examples/opentheory
Sep 15 16:34:50 Finished examples/opentheory                                      0s  98MB
Sep 15 16:34:50 Starting examples/opentheory/compilation
Sep 15 17:06:06 Finished examples/opentheory/compilation                      31m16s  29GB
Sep 15 17:06:07 Starting examples/opentheory/compilation/proofs
Sep 15 17:06:46 Finished examples/opentheory/compilation/proofs                  38s   3GB
Sep 15 17:06:46 Starting examples/opentheory/compilation/ag32
Sep 15 17:38:27 Finished examples/opentheory/compilation/ag32                 31m41s  25GB
Sep 15 17:38:28 Starting examples/opentheory/compilation/ag32/proofs
Sep 15 17:39:56 Finished examples/opentheory/compilation/ag32/proofs           1m28s   6GB
Sep 15 17:39:56 Starting translator/okasaki-examples
Sep 15 17:44:05 Finished translator/okasaki-examples                           4m08s   2GB
Sep 15 17:44:05 Starting translator/other-examples
Sep 15 17:46:03 Finished translator/other-examples                             1m57s   2GB
Sep 15 17:46:03 Starting compiler/parsing/tests
Sep 15 17:46:27 Finished compiler/parsing/tests                                  23s 629MB
Sep 15 17:46:27 Starting compiler/inference/tests
Sep 15 17:50:43 Finished compiler/inference/tests                              4m15s   6GB
Sep 15 17:50:43 Starting compiler/bootstrap/translation
Sep 15 20:24:02 Finished compiler/bootstrap/translation                     2h33m18s  48GB
Sep 15 20:24:02 Starting unverified/sexpr-bootstrap/x64/64
Sep 15 20:33:56 Finished unverified/sexpr-bootstrap/x64/64                     9m53s   8GB
Sep 15 20:33:56 Starting unverified/sexpr-bootstrap/x64/32
Sep 15 20:41:43 Finished unverified/sexpr-bootstrap/x64/32                     7m46s   8GB
Sep 15 20:41:43 Starting compiler/benchmarks
Sep 15 21:19:49 Finished compiler/benchmarks                                  38m05s   2GB
Sep 15 21:19:49 Starting compiler/bootstrap/compilation/x64/64
Sep 16 11:00:43 FAILED: compiler/bootstrap/compilation/x64/64
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/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[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/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[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/bootstrap/translation[0m
Starting work on README.md
Starting work on to_dataBootstrapTheory
README.md                                                                     real:    0s  user:    0s     OK
to_dataBootstrapTheory                                                        real: 3645s  user: 3626s     OK
Starting work on to_lab_x64BootstrapTheory
to_lab_x64BootstrapTheory                                                     real:  759m  user: 1537m     OK
Starting work on cake.S
cake.S                                                                        real:   65s  user:   57sFAIL<1>
      (...) => ... ... |
      ... => ... |
      ...
 /home/myreen/regression/cakeml-1336/compiler/compilationLib.sml:187: warning: Pattern is not exhaustive.
 Found near
   val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 Run out of store - interrupting threads
 Failed to recover - exiting