CakeML Regression Test

Job 1269

CakeML:befff2fc13548ac6a8addb6bc8b55c523567a333
  Update compiler backend proofs changes to HOL [Jun 15 11:03:37]
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 15 11:20:01 Claimed job
Jun 15 11:20:04 Reusing HOL
Jun 15 11:20:50 Starting developers
Jun 15 11:20:54 Finished developers                                               4s  81MB
Jun 15 11:20:54 Starting developers/bin
Jun 15 11:21:02 Finished developers/bin                                           7s   1GB
Jun 15 11:21:02 Starting semantics/ffi
Jun 15 11:21:14 Finished semantics/ffi                                           11s 238MB
Jun 15 11:21:15 Starting semantics
Jun 15 11:22:48 Finished semantics                                             1m32s   1GB
Jun 15 11:22:48 Starting semantics/proofs
Jun 15 11:26:31 Finished semantics/proofs                                      3m42s   1GB
Jun 15 11:26:31 Starting semantics/alt_semantics
Jun 15 11:26:41 Finished semantics/alt_semantics                                  9s 269MB
Jun 15 11:26:41 Starting semantics/alt_semantics/proofs
Jun 15 11:29:03 Finished semantics/alt_semantics/proofs                        2m21s 734MB
Jun 15 11:29:04 Starting basis/pure
Jun 15 11:29:59 Finished basis/pure                                              55s 827MB
Jun 15 11:29:59 Starting translator
Jun 15 11:32:55 Finished translator                                            2m56s   1GB
Jun 15 11:32:56 Starting compiler/parsing
Jun 15 11:34:19 Finished compiler/parsing                                      1m23s   2GB
Jun 15 11:34:19 Starting characteristic
Jun 15 11:40:50 Finished characteristic                                        6m30s   2GB
Jun 15 11:40:50 Starting translator/monadic
Jun 15 11:42:37 Finished translator/monadic                                    1m46s   1GB
Jun 15 11:42:37 Starting basis
Jun 15 12:19:20 Finished basis                                                36m43s  12GB
Jun 15 12:19:20 Starting compiler/inference
Jun 15 12:20:30 Finished compiler/inference                                    1m08s   1GB
Jun 15 12:20:30 Starting compiler/backend/reg_alloc
Jun 15 12:21:41 Finished compiler/backend/reg_alloc                            1m11s   1GB
Jun 15 12:21:41 Starting compiler/backend/gc
Jun 15 12:25:36 Finished compiler/backend/gc                                   3m54s   2GB
Jun 15 12:25:36 Starting compiler/backend
Jun 15 12:31:07 Finished compiler/backend                                      5m30s   3GB
Jun 15 12:31:07 Starting compiler/encoders/asm
Jun 15 12:31:31 Finished compiler/encoders/asm                                   24s 884MB
Jun 15 12:31:31 Starting compiler/encoders/x64
Jun 15 12:31:59 Finished compiler/encoders/x64                                   27s 842MB
Jun 15 12:31:59 Starting compiler/encoders/arm7
Jun 15 12:32:52 Finished compiler/encoders/arm7                                  53s 766MB
Jun 15 12:32:52 Starting compiler/encoders/arm8
Jun 15 12:33:07 Finished compiler/encoders/arm8                                  13s 600MB
Jun 15 12:33:07 Starting compiler/encoders/mips
Jun 15 12:33:25 Finished compiler/encoders/mips                                  18s   1GB
Jun 15 12:33:26 Starting compiler/encoders/riscv
Jun 15 12:33:42 Finished compiler/encoders/riscv                                 16s 864MB
Jun 15 12:33:42 Starting compiler/encoders/ag32
Jun 15 12:34:01 Finished compiler/encoders/ag32                                  19s 647MB
Jun 15 12:34:01 Starting compiler/backend/x64
Jun 15 12:34:22 Finished compiler/backend/x64                                    20s   1GB
Jun 15 12:34:22 Starting compiler/backend/arm7
Jun 15 12:34:44 Finished compiler/backend/arm7                                   21s   1GB
Jun 15 12:34:44 Starting compiler/backend/arm8
Jun 15 12:35:03 Finished compiler/backend/arm8                                   18s   1GB
Jun 15 12:35:03 Starting compiler/backend/mips
Jun 15 12:35:23 Finished compiler/backend/mips                                   19s   1GB
Jun 15 12:35:23 Starting compiler/backend/riscv
Jun 15 12:35:45 Finished compiler/backend/riscv                                  21s   1GB
Jun 15 12:35:45 Starting compiler/backend/ag32
Jun 15 12:37:04 Finished compiler/backend/ag32                                 1m18s   1GB
Jun 15 12:37:04 Starting compiler/parsing/proofs
Jun 15 12:43:10 Finished compiler/parsing/proofs                               6m05s   1GB
Jun 15 12:43:10 Starting compiler/inference/proofs
Jun 15 12:45:54 Finished compiler/inference/proofs                             2m42s 926MB
Jun 15 12:45:54 Starting compiler/backend/semantics
Jun 15 13:20:10 Finished compiler/backend/semantics                           34m15s   2GB
Jun 15 13:20:10 Starting compiler/backend/reg_alloc/proofs
Jun 15 13:24:02 Finished compiler/backend/reg_alloc/proofs                     3m52s 832MB
Jun 15 13:24:02 Starting compiler/backend/proofs
Jun 15 14:31:40 Finished compiler/backend/proofs                            1h07m37s  18GB
Jun 15 14:31:40 Starting compiler/encoders/x64/proofs
Jun 15 14:42:22 Finished compiler/encoders/x64/proofs                         10m41s   4GB
Jun 15 14:42:22 Starting compiler/encoders/arm7/proofs
Jun 15 14:56:35 Finished compiler/encoders/arm7/proofs                        14m13s   3GB
Jun 15 14:56:36 Starting compiler/encoders/arm8/proofs
Jun 15 15:03:49 Finished compiler/encoders/arm8/proofs                         7m13s   1GB
Jun 15 15:03:49 Starting compiler/encoders/mips/proofs
Jun 15 15:14:43 Finished compiler/encoders/mips/proofs                        10m53s   2GB
Jun 15 15:14:43 Starting compiler/encoders/riscv/proofs
Jun 15 15:24:20 Finished compiler/encoders/riscv/proofs                        9m36s   1GB
Jun 15 15:24:21 Starting compiler/encoders/ag32/proofs
Jun 15 15:27:14 Finished compiler/encoders/ag32/proofs                         2m53s 666MB
Jun 15 15:27:14 Starting compiler/backend/x64/proofs
Jun 15 15:27:36 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 15 15:27:36 Starting compiler/backend/arm7/proofs
Jun 15 15:27:59 Finished compiler/backend/arm7/proofs                            22s   1GB
Jun 15 15:27:59 Starting compiler/backend/arm8/proofs
Jun 15 15:28:21 Finished compiler/backend/arm8/proofs                            21s   1GB
Jun 15 15:28:21 Starting compiler/backend/mips/proofs
Jun 15 15:28:43 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 15 15:28:43 Starting compiler/backend/riscv/proofs
Jun 15 15:29:06 Finished compiler/backend/riscv/proofs                           22s   1GB
Jun 15 15:29:06 Starting compiler/backend/ag32/proofs
Jun 15 15:43:20 Finished compiler/backend/ag32/proofs                         14m12s   2GB
Jun 15 15:43:20 Starting compiler/proofs
Jun 15 15:45:20 Finished compiler/proofs                                       1m59s   3GB
Jun 15 15:45:20 Starting candle/set-theory
Jun 15 15:45:51 Finished candle/set-theory                                       31s 867MB
Jun 15 15:45:51 Starting candle/syntax-lib
Jun 15 15:46:03 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-1269/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-1269/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"}