Job 1278

CakeML:e0c6a81ec7bea54528f530a25c6bec6b70bc6bdd
  Remove last mention of non-existent SORTED_APPEND_IFF [Jun 17 09:02:12]
HOL:511e4a42e7cb57caffe27cfa441825baa744d7ec
  Update src for strip_binop change [Jun 13 04:34:39]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jun 17 09:05:08 Claimed job
Jun 17 09:05:14 Reusing HOL
Jun 17 09:06:01 Starting developers
Jun 17 09:06:05 Finished developers                                               4s 100MB
Jun 17 09:06:05 Starting developers/bin
Jun 17 09:06:13 Finished developers/bin                                           8s   1GB
Jun 17 09:06:14 Starting semantics/ffi
Jun 17 09:06:26 Finished semantics/ffi                                           12s 213MB
Jun 17 09:06:26 Starting semantics
Jun 17 09:07:59 Finished semantics                                             1m32s   1GB
Jun 17 09:07:59 Starting semantics/proofs
Jun 17 09:11:46 Finished semantics/proofs                                      3m46s   1GB
Jun 17 09:11:46 Starting semantics/alt_semantics
Jun 17 09:11:56 Finished semantics/alt_semantics                                  9s 312MB
Jun 17 09:11:56 Starting semantics/alt_semantics/proofs
Jun 17 09:14:19 Finished semantics/alt_semantics/proofs                        2m22s 754MB
Jun 17 09:14:19 Starting basis/pure
Jun 17 09:15:14 Finished basis/pure                                              55s 670MB
Jun 17 09:15:14 Starting translator
Jun 17 09:18:14 Finished translator                                            2m59s   1GB
Jun 17 09:18:14 Starting compiler/parsing
Jun 17 09:19:40 Finished compiler/parsing                                      1m25s   2GB
Jun 17 09:19:40 Starting characteristic
Jun 17 09:26:16 Finished characteristic                                        6m35s   1GB
Jun 17 09:26:16 Starting translator/monadic
Jun 17 09:28:00 Finished translator/monadic                                    1m44s   1GB
Jun 17 09:28:00 Starting basis
Jun 17 10:04:50 Finished basis                                                36m49s  15GB
Jun 17 10:04:50 Starting compiler/inference
Jun 17 10:06:00 Finished compiler/inference                                    1m09s 931MB
Jun 17 10:06:00 Starting compiler/backend/reg_alloc
Jun 17 10:07:12 Finished compiler/backend/reg_alloc                            1m11s   1GB
Jun 17 10:07:12 Starting compiler/backend/gc
Jun 17 10:11:05 Finished compiler/backend/gc                                   3m52s   2GB
Jun 17 10:11:05 Starting compiler/backend
Jun 17 10:16:35 Finished compiler/backend                                      5m29s   3GB
Jun 17 10:16:35 Starting compiler/encoders/asm
Jun 17 10:17:00 Finished compiler/encoders/asm                                   24s 933MB
Jun 17 10:17:00 Starting compiler/encoders/x64
Jun 17 10:17:27 Finished compiler/encoders/x64                                   27s 830MB
Jun 17 10:17:28 Starting compiler/encoders/arm7
Jun 17 10:18:22 Finished compiler/encoders/arm7                                  54s 676MB
Jun 17 10:18:23 Starting compiler/encoders/arm8
Jun 17 10:18:37 Finished compiler/encoders/arm8                                  14s 854MB
Jun 17 10:18:37 Starting compiler/encoders/mips
Jun 17 10:18:56 Finished compiler/encoders/mips                                  18s   1GB
Jun 17 10:18:56 Starting compiler/encoders/riscv
Jun 17 10:19:13 Finished compiler/encoders/riscv                                 15s 864MB
Jun 17 10:19:13 Starting compiler/encoders/ag32
Jun 17 10:19:33 Finished compiler/encoders/ag32                                  19s 746MB
Jun 17 10:19:33 Starting compiler/backend/x64
Jun 17 10:19:52 Finished compiler/backend/x64                                    18s 925MB
Jun 17 10:19:52 Starting compiler/backend/arm7
Jun 17 10:20:14 Finished compiler/backend/arm7                                   21s   1GB
Jun 17 10:20:14 Starting compiler/backend/arm8
Jun 17 10:20:34 Finished compiler/backend/arm8                                   20s   1GB
Jun 17 10:20:34 Starting compiler/backend/mips
Jun 17 10:20:56 Finished compiler/backend/mips                                   21s   1GB
Jun 17 10:20:56 Starting compiler/backend/riscv
Jun 17 10:21:18 Finished compiler/backend/riscv                                  21s   1GB
Jun 17 10:21:18 Starting compiler/backend/ag32
Jun 17 10:22:37 Finished compiler/backend/ag32                                 1m18s   1GB
Jun 17 10:22:37 Starting compiler/parsing/proofs
Jun 17 10:28:39 Finished compiler/parsing/proofs                               6m02s 965MB
Jun 17 10:28:39 Starting compiler/inference/proofs
Jun 17 10:31:25 Finished compiler/inference/proofs                             2m45s   1GB
Jun 17 10:31:25 Starting compiler/backend/semantics
Jun 17 11:05:34 Finished compiler/backend/semantics                           34m07s   2GB
Jun 17 11:05:34 Starting compiler/backend/reg_alloc/proofs
Jun 17 11:09:26 Finished compiler/backend/reg_alloc/proofs                     3m52s   1GB
Jun 17 11:09:26 Starting compiler/backend/proofs
Jun 17 12:16:59 Finished compiler/backend/proofs                            1h07m31s  15GB
Jun 17 12:16:59 Starting compiler/encoders/x64/proofs
Jun 17 12:27:35 Finished compiler/encoders/x64/proofs                         10m35s   4GB
Jun 17 12:27:35 Starting compiler/encoders/arm7/proofs
Jun 17 12:41:50 Finished compiler/encoders/arm7/proofs                        14m14s   2GB
Jun 17 12:41:50 Starting compiler/encoders/arm8/proofs
Jun 17 12:48:59 Finished compiler/encoders/arm8/proofs                         7m09s   1GB
Jun 17 12:49:00 Starting compiler/encoders/mips/proofs
Jun 17 12:59:54 Finished compiler/encoders/mips/proofs                        10m54s   2GB
Jun 17 12:59:55 Starting compiler/encoders/riscv/proofs
Jun 17 13:09:34 Finished compiler/encoders/riscv/proofs                        9m38s   1GB
Jun 17 13:09:34 Starting compiler/encoders/ag32/proofs
Jun 17 13:12:25 Finished compiler/encoders/ag32/proofs                         2m50s 999MB
Jun 17 13:12:25 Starting compiler/backend/x64/proofs
Jun 17 13:12:48 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 17 13:12:48 Starting compiler/backend/arm7/proofs
Jun 17 13:13:11 Finished compiler/backend/arm7/proofs                            23s   1GB
Jun 17 13:13:12 Starting compiler/backend/arm8/proofs
Jun 17 13:13:33 Finished compiler/backend/arm8/proofs                            21s 789MB
Jun 17 13:13:34 Starting compiler/backend/mips/proofs
Jun 17 13:13:56 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 17 13:13:57 Starting compiler/backend/riscv/proofs
Jun 17 13:14:18 Finished compiler/backend/riscv/proofs                           21s   1GB
Jun 17 13:14:18 Starting compiler/backend/ag32/proofs
Jun 17 13:28:45 Finished compiler/backend/ag32/proofs                         14m26s   2GB
Jun 17 13:28:45 Starting compiler/proofs
Jun 17 13:30:24 Finished compiler/proofs                                       1m39s   3GB
Jun 17 13:30:24 Starting candle/set-theory
Jun 17 13:30:56 Finished candle/set-theory                                       31s 713MB
Jun 17 13:30:56 Starting candle/syntax-lib
Jun 17 13:31:08 Finished candle/syntax-lib                                       11s 708MB
Jun 17 13:31:08 Starting candle/standard/syntax
Jun 17 13:33:08 Finished candle/standard/syntax                                2m00s   1GB
Jun 17 13:33:09 Starting candle/standard/semantics
Jun 17 13:35:02 Finished candle/standard/semantics                             1m53s 945MB
Jun 17 13:35:02 Starting candle/standard/monadic
Jun 17 13:36:55 Finished candle/standard/monadic                               1m52s   1GB
Jun 17 13:36:55 Starting candle/standard/ml_kernel
Jun 17 13:42:59 Finished candle/standard/ml_kernel                             6m03s   3GB
Jun 17 13:42:59 Starting candle/standard/opentheory
Jun 17 13:53:14 Finished candle/standard/opentheory                           10m15s   4GB
Jun 17 13:53:14 Starting candle/standard/opentheory/compilation
Jun 17 14:27:33 Finished candle/standard/opentheory/compilation               34m18s  20GB
Jun 17 14:27:33 Starting candle/standard/opentheory/compilation/proofs
Jun 17 14:28:35 Finished candle/standard/opentheory/compilation/proofs         1m02s   1GB
Jun 17 14:28:35 Starting candle/overloading/syntax
Jun 17 14:32:02 Finished candle/overloading/syntax                             3m26s 942MB
Jun 17 14:32:02 Starting candle/overloading/semantics
Jun 17 14:39:47 Finished candle/overloading/semantics                          7m44s   3GB
Jun 17 14:39:47 Starting characteristic/examples
Jun 17 14:41:10 Finished characteristic/examples                               1m22s   2GB
Jun 17 14:41:10 Starting tutorial/solutions
Jun 17 14:56:55 Finished tutorial/solutions                                   15m44s   7GB
Jun 17 14:56:55 Starting translator/monadic/examples
Jun 17 15:00:48 Finished translator/monadic/examples                           3m53s   2GB
Jun 17 15:00:48 Starting examples
Jun 17 15:11:15 Finished examples                                             10m26s   4GB
Jun 17 15:11:15 Starting examples/compilation/x64
Jun 17 17:39:28 Finished examples/compilation/x64                           2h28m11s  15GB
Jun 17 17:39:28 Starting examples/compilation/x64/proofs
Jun 17 17:41:21 Finished examples/compilation/x64/proofs                       1m52s   2GB
Jun 17 17:41:21 Starting examples/compilation/ag32
Jun 17 18:15:08 Finished examples/compilation/ag32                            33m47s   5GB
Jun 17 18:15:08 Starting examples/compilation/ag32/proofs
Jun 17 18:16:03 Finished examples/compilation/ag32/proofs                        54s   2GB
Jun 17 18:16:03 Starting examples/cost
Jun 17 19:10:10 Finished examples/cost                                        54m07s   7GB
Jun 17 19:10:11 Starting examples/lpr_checker
Jun 17 19:14:19 Finished examples/lpr_checker                                  4m08s   3GB
Jun 17 19:14:19 Starting examples/lpr_checker/compilation
Jun 17 19:33:56 Finished examples/lpr_checker/compilation                     19m36s   9GB
Jun 17 19:33:56 Starting examples/lpr_checker/compilation/proofs
Jun 17 19:35:04 Finished examples/lpr_checker/compilation/proofs               1m07s   1GB
Jun 17 19:35:04 Starting examples/lpr_checker/array
Jun 17 19:46:15 Finished examples/lpr_checker/array                           11m11s   2GB
Jun 17 19:46:15 Starting examples/lpr_checker/array/compilation
Jun 17 20:06:09 Finished examples/lpr_checker/array/compilation               19m53s  12GB
Jun 17 20:06:10 Starting examples/lpr_checker/array/compilation/proofs
Jun 17 20:07:02 Finished examples/lpr_checker/array/compilation/proofs           52s   3GB
Jun 17 20:07:03 Starting translator/okasaki-examples
Jun 17 20:07:15 FAILED: translator/okasaki-examples
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Starting work on BankersQueueTheory
Starting work on BatchedQueueTheory
Starting work on okasaki_miscTheory
Starting work on HoodMelvilleQueueTheory
okasaki_miscTheory                              real:   10s  user:    9sFAIL<1>
 Saved theorem _____ "list_to_bag_append"
 error in quse /home/cake/oven/regression/cakeml-1278/translator/okasaki-examples/okasaki_miscScript.sml : HOL_ERR {message = "No match (THEN1 on line 108)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 error in load /home/cake/oven/regression/cakeml-1278/translator/okasaki-examples/okasaki_miscScript : HOL_ERR {message = "No match (THEN1 on line 108)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 Saved theorem _____ "list_to_bag_perm"
 Proof of 
 
 R l. transitive R  SORTED R l  SORTED (x y. R y x) (REVERSE l)
 
 failed.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 108)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
BankersQueueTheory                                                      M-KILLED
BatchedQueueTheory                                                      M-KILLED
HoodMelvilleQueueTheory                                                 M-KILLED