Job 1277

CakeML:cb9f2476e1d1e45f23b8c76e1276570a31572866
  spell and use strtoul correctly [Jun 15 11:44:12]
#738 (export_update)
Merging into: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:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 17 09:02:24 Claimed job
Jun 17 09:02:29 Reusing HOL
Jun 17 09:02:34 Starting developers
Jun 17 09:02:34 Finished developers                                               0s  29MB
Jun 17 09:02:35 Starting developers/bin
Jun 17 09:02:41 Finished developers/bin                                           6s   1GB
Jun 17 09:02:41 Starting semantics/ffi
Jun 17 09:02:50 Finished semantics/ffi                                            8s 276MB
Jun 17 09:02:50 Starting semantics
Jun 17 09:04:11 Finished semantics                                             1m20s   1GB
Jun 17 09:04:11 Starting semantics/proofs
Jun 17 09:07:24 Finished semantics/proofs                                      3m12s   1GB
Jun 17 09:07:24 Starting semantics/alt_semantics
Jun 17 09:07:32 Finished semantics/alt_semantics                                  7s 292MB
Jun 17 09:07:32 Starting semantics/alt_semantics/proofs
Jun 17 09:09:36 Finished semantics/alt_semantics/proofs                        2m03s 811MB
Jun 17 09:09:36 Starting basis/pure
Jun 17 09:10:24 Finished basis/pure                                              47s 753MB
Jun 17 09:10:24 Starting translator
Jun 17 09:12:56 Finished translator                                            2m31s   1GB
Jun 17 09:12:56 Starting compiler/parsing
Jun 17 09:14:02 Finished compiler/parsing                                      1m06s   2GB
Jun 17 09:14:03 Starting characteristic
Jun 17 09:19:47 Finished characteristic                                        5m44s   1GB
Jun 17 09:19:47 Starting translator/monadic
Jun 17 09:21:21 Finished translator/monadic                                    1m34s   1GB
Jun 17 09:21:21 Starting basis
Jun 17 09:52:16 Finished basis                                                30m51s  17GB
Jun 17 09:52:16 Starting compiler/inference
Jun 17 09:53:17 Finished compiler/inference                                    1m00s   1GB
Jun 17 09:53:17 Starting compiler/backend/reg_alloc
Jun 17 09:54:20 Finished compiler/backend/reg_alloc                            1m02s   1GB
Jun 17 09:54:20 Starting compiler/backend/gc
Jun 17 09:57:32 Finished compiler/backend/gc                                   3m12s   2GB
Jun 17 09:57:33 Starting compiler/backend
Jun 17 10:02:05 Finished compiler/backend                                      4m31s   4GB
Jun 17 10:02:05 Starting compiler/encoders/asm
Jun 17 10:02:26 Finished compiler/encoders/asm                                   20s 827MB
Jun 17 10:02:26 Starting compiler/encoders/x64
Jun 17 10:02:50 Finished compiler/encoders/x64                                   23s 849MB
Jun 17 10:02:50 Starting compiler/encoders/arm7
Jun 17 10:03:37 Finished compiler/encoders/arm7                                  46s 691MB
Jun 17 10:03:37 Starting compiler/encoders/arm8
Jun 17 10:03:49 Finished compiler/encoders/arm8                                  12s 919MB
Jun 17 10:03:49 Starting compiler/encoders/mips
Jun 17 10:04:06 Finished compiler/encoders/mips                                  16s 948MB
Jun 17 10:04:07 Starting compiler/encoders/riscv
Jun 17 10:04:20 Finished compiler/encoders/riscv                                 13s 815MB
Jun 17 10:04:20 Starting compiler/encoders/ag32
Jun 17 10:04:37 Finished compiler/encoders/ag32                                  16s 882MB
Jun 17 10:04:37 Starting compiler/backend/x64
Jun 17 10:04:55 Finished compiler/backend/x64                                    18s   1GB
Jun 17 10:04:55 Starting compiler/backend/arm7
Jun 17 10:05:15 Finished compiler/backend/arm7                                   19s   1GB
Jun 17 10:05:15 Starting compiler/backend/arm8
Jun 17 10:05:33 Finished compiler/backend/arm8                                   18s   1GB
Jun 17 10:05:34 Starting compiler/backend/mips
Jun 17 10:05:52 Finished compiler/backend/mips                                   18s   1GB
Jun 17 10:05:52 Starting compiler/backend/riscv
Jun 17 10:06:11 Finished compiler/backend/riscv                                  18s   1GB
Jun 17 10:06:11 Starting compiler/backend/ag32
Jun 17 10:07:18 Finished compiler/backend/ag32                                 1m07s 998MB
Jun 17 10:07:18 Starting compiler/parsing/proofs
Jun 17 10:12:58 Finished compiler/parsing/proofs                               5m39s   1GB
Jun 17 10:12:58 Starting compiler/inference/proofs
Jun 17 10:15:20 Finished compiler/inference/proofs                             2m21s   1GB
Jun 17 10:15:20 Starting compiler/backend/semantics
Jun 17 10:42:51 Finished compiler/backend/semantics                           27m30s   2GB
Jun 17 10:42:51 Starting compiler/backend/reg_alloc/proofs
Jun 17 10:46:07 Finished compiler/backend/reg_alloc/proofs                     3m15s 976MB
Jun 17 10:46:07 Starting compiler/backend/proofs
Jun 17 11:38:51 Finished compiler/backend/proofs                              52m43s  19GB
Jun 17 11:38:51 Starting compiler/encoders/x64/proofs
Jun 17 11:48:01 Finished compiler/encoders/x64/proofs                          9m10s   5GB
Jun 17 11:48:02 Starting compiler/encoders/arm7/proofs
Jun 17 12:00:29 Finished compiler/encoders/arm7/proofs                        12m27s   3GB
Jun 17 12:00:29 Starting compiler/encoders/arm8/proofs
Jun 17 12:06:53 Finished compiler/encoders/arm8/proofs                         6m22s   1GB
Jun 17 12:06:53 Starting compiler/encoders/mips/proofs
Jun 17 12:16:34 Finished compiler/encoders/mips/proofs                         9m41s   2GB
Jun 17 12:16:34 Starting compiler/encoders/riscv/proofs
Jun 17 12:25:04 Finished compiler/encoders/riscv/proofs                        8m29s   1GB
Jun 17 12:25:05 Starting compiler/encoders/ag32/proofs
Jun 17 12:27:33 Finished compiler/encoders/ag32/proofs                         2m28s 732MB
Jun 17 12:27:33 Starting compiler/backend/x64/proofs
Jun 17 12:27:53 Finished compiler/backend/x64/proofs                             19s   1GB
Jun 17 12:27:53 Starting compiler/backend/arm7/proofs
Jun 17 12:28:14 Finished compiler/backend/arm7/proofs                            21s   1GB
Jun 17 12:28:14 Starting compiler/backend/arm8/proofs
Jun 17 12:28:33 Finished compiler/backend/arm8/proofs                            18s   1GB
Jun 17 12:28:33 Starting compiler/backend/mips/proofs
Jun 17 12:28:54 Finished compiler/backend/mips/proofs                            20s   1GB
Jun 17 12:28:54 Starting compiler/backend/riscv/proofs
Jun 17 12:29:14 Finished compiler/backend/riscv/proofs                           19s   1GB
Jun 17 12:29:14 Starting compiler/backend/ag32/proofs
Jun 17 12:41:47 Finished compiler/backend/ag32/proofs                         12m32s   2GB
Jun 17 12:41:48 Starting compiler/proofs
Jun 17 12:43:16 Finished compiler/proofs                                       1m27s   3GB
Jun 17 12:43:16 Starting candle/set-theory
Jun 17 12:43:43 Finished candle/set-theory                                       26s 759MB
Jun 17 12:43:43 Starting candle/syntax-lib
Jun 17 12:43:54 Finished candle/syntax-lib                                       10s 485MB
Jun 17 12:43:54 Starting candle/standard/syntax
Jun 17 12:45:40 Finished candle/standard/syntax                                1m46s 947MB
Jun 17 12:45:40 Starting candle/standard/semantics
Jun 17 12:47:20 Finished candle/standard/semantics                             1m39s   1GB
Jun 17 12:47:20 Starting candle/standard/monadic
Jun 17 12:48:58 Finished candle/standard/monadic                               1m37s   1GB
Jun 17 12:48:58 Starting candle/standard/ml_kernel
Jun 17 12:54:12 Finished candle/standard/ml_kernel                             5m14s   5GB
Jun 17 12:54:13 Starting candle/standard/opentheory
Jun 17 13:02:56 Finished candle/standard/opentheory                            8m43s   4GB
Jun 17 13:02:56 Starting candle/standard/opentheory/compilation
Jun 17 13:35:00 Finished candle/standard/opentheory/compilation               32m03s  17GB
Jun 17 13:35:00 Starting candle/standard/opentheory/compilation/proofs
Jun 17 13:35:37 Finished candle/standard/opentheory/compilation/proofs           36s   3GB
Jun 17 13:35:37 Starting candle/overloading/syntax
Jun 17 13:38:37 Finished candle/overloading/syntax                             2m59s   1GB
Jun 17 13:38:37 Starting candle/overloading/semantics
Jun 17 13:45:27 Finished candle/overloading/semantics                          6m49s   2GB
Jun 17 13:45:27 Starting characteristic/examples
Jun 17 13:46:40 Finished characteristic/examples                               1m12s   2GB
Jun 17 13:46:40 Starting tutorial/solutions
Jun 17 14:00:44 Finished tutorial/solutions                                   14m03s   8GB
Jun 17 14:00:44 Starting translator/monadic/examples
Jun 17 14:03:54 Finished translator/monadic/examples                           3m09s   2GB
Jun 17 14:03:54 Starting examples
Jun 17 14:12:05 Finished examples                                              8m10s   3GB
Jun 17 14:12:05 Starting examples/compilation/x64
Jun 17 16:23:58 Finished examples/compilation/x64                           2h11m52s  15GB
Jun 17 16:23:59 Starting examples/compilation/x64/proofs
Jun 17 16:25:31 Finished examples/compilation/x64/proofs                       1m32s   3GB
Jun 17 16:25:31 Starting examples/compilation/ag32
Jun 17 16:55:56 Finished examples/compilation/ag32                            30m24s   6GB
Jun 17 16:55:56 Starting examples/compilation/ag32/proofs
Jun 17 16:56:38 Finished examples/compilation/ag32/proofs                        41s   2GB
Jun 17 16:56:38 Starting examples/cost
Jun 17 17:43:06 Finished examples/cost                                        46m27s   6GB
Jun 17 17:43:06 Starting examples/lpr_checker
Jun 17 17:46:42 Finished examples/lpr_checker                                  3m35s   2GB
Jun 17 17:46:42 Starting examples/lpr_checker/compilation
Jun 17 18:03:53 Finished examples/lpr_checker/compilation                     17m11s  10GB
Jun 17 18:03:54 Starting examples/lpr_checker/compilation/proofs
Jun 17 18:04:29 Finished examples/lpr_checker/compilation/proofs                 34s   2GB
Jun 17 18:04:29 Starting examples/lpr_checker/array
Jun 17 18:14:10 Finished examples/lpr_checker/array                            9m40s   3GB
Jun 17 18:14:10 Starting examples/lpr_checker/array/compilation
Jun 17 18:32:21 Finished examples/lpr_checker/array/compilation               18m10s  10GB
Jun 17 18:32:21 Starting examples/lpr_checker/array/compilation/proofs
Jun 17 18:33:10 Finished examples/lpr_checker/array/compilation/proofs           48s   3GB
Jun 17 18:33:10 Starting translator/okasaki-examples
Jun 17 18:33:20 FAILED: translator/okasaki-examples
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
Starting work on BankersQueueTheory
Starting work on BatchedQueueTheory
Starting work on okasaki_miscTheory
Starting work on HoodMelvilleQueueTheory
okasaki_miscTheory                                                                                                                                  real:    8s  user:    8sFAIL<1>
 Saved theorem _____ "list_to_bag_append"
 Saved theorem _____ "list_to_bag_perm"
 Proof of 
 
 R l. transitive R  SORTED R l  SORTED (x y. R y x) (REVERSE l)
 
 failed.
 error in quse /home/myreen/regression/cakeml-1277/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/myreen/regression/cakeml-1277/translator/okasaki-examples/okasaki_miscScript : HOL_ERR {message = "No match (THEN1 on line 108)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 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