Job 1271

CakeML:cb9f2476e1d1e45f23b8c76e1276570a31572866
  spell and use strtoul correctly [Jun 15 11:44:12]
#738 (export_update)
Merging into:a22b1d936ee75ea1ad3389494d24a3ee85f700f0
  Fix examples for changes in HOL [Jun 15 13:41:25]
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 16 06:20:14 Claimed job
Jun 16 06:20:20 Reusing HOL
Jun 16 06:21:07 Starting developers
Jun 16 06:21:11 Finished developers                                               4s  91MB
Jun 16 06:21:11 Starting developers/bin
Jun 16 06:21:19 Finished developers/bin                                           7s   1GB
Jun 16 06:21:19 Starting semantics/ffi
Jun 16 06:21:32 Finished semantics/ffi                                           11s 243MB
Jun 16 06:21:32 Starting semantics
Jun 16 06:23:07 Finished semantics                                             1m35s   1GB
Jun 16 06:23:07 Starting semantics/proofs
Jun 16 06:26:54 Finished semantics/proofs                                      3m46s   1GB
Jun 16 06:26:54 Starting semantics/alt_semantics
Jun 16 06:27:04 Finished semantics/alt_semantics                                 10s 278MB
Jun 16 06:27:04 Starting semantics/alt_semantics/proofs
Jun 16 06:29:26 Finished semantics/alt_semantics/proofs                        2m21s 836MB
Jun 16 06:29:26 Starting basis/pure
Jun 16 06:30:21 Finished basis/pure                                              54s 838MB
Jun 16 06:30:22 Starting translator
Jun 16 06:33:19 Finished translator                                            2m57s   1GB
Jun 16 06:33:20 Starting compiler/parsing
Jun 16 06:34:45 Finished compiler/parsing                                      1m25s   3GB
Jun 16 06:34:45 Starting characteristic
Jun 16 06:41:17 Finished characteristic                                        6m31s   1GB
Jun 16 06:41:17 Starting translator/monadic
Jun 16 06:43:03 Finished translator/monadic                                    1m45s   2GB
Jun 16 06:43:03 Starting basis
Jun 16 07:19:54 Finished basis                                                36m50s  15GB
Jun 16 07:19:54 Starting compiler/inference
Jun 16 07:21:02 Finished compiler/inference                                    1m08s   1GB
Jun 16 07:21:02 Starting compiler/backend/reg_alloc
Jun 16 07:22:14 Finished compiler/backend/reg_alloc                            1m11s   1GB
Jun 16 07:22:14 Starting compiler/backend/gc
Jun 16 07:26:07 Finished compiler/backend/gc                                   3m52s   2GB
Jun 16 07:26:07 Starting compiler/backend
Jun 16 07:31:39 Finished compiler/backend                                      5m31s   3GB
Jun 16 07:31:39 Starting compiler/encoders/asm
Jun 16 07:32:03 Finished compiler/encoders/asm                                   24s 729MB
Jun 16 07:32:03 Starting compiler/encoders/x64
Jun 16 07:32:32 Finished compiler/encoders/x64                                   28s 971MB
Jun 16 07:32:32 Starting compiler/encoders/arm7
Jun 16 07:33:26 Finished compiler/encoders/arm7                                  53s   1GB
Jun 16 07:33:26 Starting compiler/encoders/arm8
Jun 16 07:33:40 Finished compiler/encoders/arm8                                  13s 697MB
Jun 16 07:33:40 Starting compiler/encoders/mips
Jun 16 07:33:59 Finished compiler/encoders/mips                                  19s   1GB
Jun 16 07:33:59 Starting compiler/encoders/riscv
Jun 16 07:34:16 Finished compiler/encoders/riscv                                 15s 812MB
Jun 16 07:34:16 Starting compiler/encoders/ag32
Jun 16 07:34:35 Finished compiler/encoders/ag32                                  19s 785MB
Jun 16 07:34:35 Starting compiler/backend/x64
Jun 16 07:34:56 Finished compiler/backend/x64                                    20s   1GB
Jun 16 07:34:56 Starting compiler/backend/arm7
Jun 16 07:35:18 Finished compiler/backend/arm7                                   21s   1GB
Jun 16 07:35:18 Starting compiler/backend/arm8
Jun 16 07:35:39 Finished compiler/backend/arm8                                   20s   1GB
Jun 16 07:35:39 Starting compiler/backend/mips
Jun 16 07:36:00 Finished compiler/backend/mips                                   20s   1GB
Jun 16 07:36:00 Starting compiler/backend/riscv
Jun 16 07:36:19 Finished compiler/backend/riscv                                  19s   1GB
Jun 16 07:36:20 Starting compiler/backend/ag32
Jun 16 07:37:38 Finished compiler/backend/ag32                                 1m18s   1GB
Jun 16 07:37:39 Starting compiler/parsing/proofs
Jun 16 07:43:47 Finished compiler/parsing/proofs                               6m07s   1GB
Jun 16 07:43:47 Starting compiler/inference/proofs
Jun 16 07:46:34 Finished compiler/inference/proofs                             2m47s   1GB
Jun 16 07:46:34 Starting compiler/backend/semantics
Jun 16 08:21:22 Finished compiler/backend/semantics                           34m47s   2GB
Jun 16 08:21:22 Starting compiler/backend/reg_alloc/proofs
Jun 16 08:25:19 Finished compiler/backend/reg_alloc/proofs                     3m56s 829MB
Jun 16 08:25:19 Starting compiler/backend/proofs
Jun 16 09:32:36 Finished compiler/backend/proofs                            1h07m16s  16GB
Jun 16 09:32:36 Starting compiler/encoders/x64/proofs
Jun 16 09:43:19 Finished compiler/encoders/x64/proofs                         10m42s   4GB
Jun 16 09:43:19 Starting compiler/encoders/arm7/proofs
Jun 16 09:57:40 Finished compiler/encoders/arm7/proofs                        14m21s   2GB
Jun 16 09:57:40 Starting compiler/encoders/arm8/proofs
Jun 16 10:04:57 Finished compiler/encoders/arm8/proofs                         7m16s   1GB
Jun 16 10:04:57 Starting compiler/encoders/mips/proofs
Jun 16 10:16:01 Finished compiler/encoders/mips/proofs                        11m03s   2GB
Jun 16 10:16:01 Starting compiler/encoders/riscv/proofs
Jun 16 10:25:37 Finished compiler/encoders/riscv/proofs                        9m35s   1GB
Jun 16 10:25:37 Starting compiler/encoders/ag32/proofs
Jun 16 10:28:32 Finished compiler/encoders/ag32/proofs                         2m54s 628MB
Jun 16 10:28:32 Starting compiler/backend/x64/proofs
Jun 16 10:28:55 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 16 10:28:55 Starting compiler/backend/arm7/proofs
Jun 16 10:29:18 Finished compiler/backend/arm7/proofs                            22s 902MB
Jun 16 10:29:18 Starting compiler/backend/arm8/proofs
Jun 16 10:29:40 Finished compiler/backend/arm8/proofs                            21s   1GB
Jun 16 10:29:40 Starting compiler/backend/mips/proofs
Jun 16 10:30:03 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 16 10:30:03 Starting compiler/backend/riscv/proofs
Jun 16 10:30:25 Finished compiler/backend/riscv/proofs                           22s   1GB
Jun 16 10:30:26 Starting compiler/backend/ag32/proofs
Jun 16 10:44:31 Finished compiler/backend/ag32/proofs                         14m05s   2GB
Jun 16 10:44:31 Starting compiler/proofs
Jun 16 10:46:09 Finished compiler/proofs                                       1m37s   2GB
Jun 16 10:46:09 Starting candle/set-theory
Jun 16 10:46:41 Finished candle/set-theory                                       31s   1GB
Jun 16 10:46:41 Starting candle/syntax-lib
Jun 16 10:46:53 FAILED: candle/syntax-lib
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
Starting work on README.md
Starting work on holSyntaxLibTheory
README.md                                       real:    0s  user:    0s     OK
holSyntaxLibTheory                              real:   10s  user:    9sFAIL<1>
 No match (THEN1 on line 301) (THEN1 on line 304)
 error in quse /home/cake/oven/regression/cakeml-1271/candle/syntax-lib/holSyntaxLibScript.sml : HOL_ERR {message = "No match (THEN1 on line 301) (THEN1 on line 304)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 error in load /home/cake/oven/regression/cakeml-1271/candle/syntax-lib/holSyntaxLibScript : HOL_ERR {message = "No match (THEN1 on line 301) (THEN1 on line 304)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 Proof of 
 
 ls. SORTED $< (STRING_SORT ls)
 
 failed.
 Failed to prove theorem STRING_SORT_SORTED.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 301) (THEN1 on line 304)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}