CakeML Regression Test

Job 1275

CakeML:b8bdd1f7605321c03123d6e9b61c29ab779d663a
  Fix another SORTED_APPEND issue [Jun 16 14:38:41]
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 18:42:40 Claimed job
Jun 16 18:42:42 Reusing HOL
Jun 16 18:43:30 Starting developers
Jun 16 18:43:35 Finished developers                                               4s  95MB
Jun 16 18:43:35 Starting developers/bin
Jun 16 18:43:43 Finished developers/bin                                           7s   1GB
Jun 16 18:43:43 Starting semantics/ffi
Jun 16 18:43:56 Finished semantics/ffi                                           12s 213MB
Jun 16 18:43:56 Starting semantics
Jun 16 18:45:30 Finished semantics                                             1m33s   1GB
Jun 16 18:45:30 Starting semantics/proofs
Jun 16 18:49:15 Finished semantics/proofs                                      3m45s 922MB
Jun 16 18:49:15 Starting semantics/alt_semantics
Jun 16 18:49:25 Finished semantics/alt_semantics                                  9s 274MB
Jun 16 18:49:26 Starting semantics/alt_semantics/proofs
Jun 16 18:51:49 Finished semantics/alt_semantics/proofs                        2m23s 766MB
Jun 16 18:51:49 Starting basis/pure
Jun 16 18:52:44 Finished basis/pure                                              54s 775MB
Jun 16 18:52:44 Starting translator
Jun 16 18:55:45 Finished translator                                            3m00s   1GB
Jun 16 18:55:45 Starting compiler/parsing
Jun 16 18:57:09 Finished compiler/parsing                                      1m24s   2GB
Jun 16 18:57:09 Starting characteristic
Jun 16 19:03:48 Finished characteristic                                        6m38s   1GB
Jun 16 19:03:49 Starting translator/monadic
Jun 16 19:05:34 Finished translator/monadic                                    1m45s   1GB
Jun 16 19:05:34 Starting basis
Jun 16 19:42:10 Finished basis                                                36m35s  12GB
Jun 16 19:42:10 Starting compiler/inference
Jun 16 19:43:19 Finished compiler/inference                                    1m08s   1GB
Jun 16 19:43:19 Starting compiler/backend/reg_alloc
Jun 16 19:44:31 Finished compiler/backend/reg_alloc                            1m11s   1GB
Jun 16 19:44:31 Starting compiler/backend/gc
Jun 16 19:48:26 Finished compiler/backend/gc                                   3m54s   2GB
Jun 16 19:48:26 Starting compiler/backend
Jun 16 19:53:58 Finished compiler/backend                                      5m32s   4GB
Jun 16 19:53:58 Starting compiler/encoders/asm
Jun 16 19:54:22 Finished compiler/encoders/asm                                   24s 718MB
Jun 16 19:54:23 Starting compiler/encoders/x64
Jun 16 19:54:51 Finished compiler/encoders/x64                                   27s 831MB
Jun 16 19:54:51 Starting compiler/encoders/arm7
Jun 16 19:55:44 Finished compiler/encoders/arm7                                  53s 732MB
Jun 16 19:55:45 Starting compiler/encoders/arm8
Jun 16 19:55:59 Finished compiler/encoders/arm8                                  14s 635MB
Jun 16 19:55:59 Starting compiler/encoders/mips
Jun 16 19:56:18 Finished compiler/encoders/mips                                  19s   1GB
Jun 16 19:56:18 Starting compiler/encoders/riscv
Jun 16 19:56:34 Finished compiler/encoders/riscv                                 15s 964MB
Jun 16 19:56:35 Starting compiler/encoders/ag32
Jun 16 19:56:54 Finished compiler/encoders/ag32                                  19s 613MB
Jun 16 19:56:54 Starting compiler/backend/x64
Jun 16 19:57:13 Finished compiler/backend/x64                                    18s 910MB
Jun 16 19:57:13 Starting compiler/backend/arm7
Jun 16 19:57:35 Finished compiler/backend/arm7                                   21s   1GB
Jun 16 19:57:36 Starting compiler/backend/arm8
Jun 16 19:57:56 Finished compiler/backend/arm8                                   20s   1GB
Jun 16 19:57:56 Starting compiler/backend/mips
Jun 16 19:58:15 Finished compiler/backend/mips                                   18s 957MB
Jun 16 19:58:16 Starting compiler/backend/riscv
Jun 16 19:58:36 Finished compiler/backend/riscv                                  20s   1GB
Jun 16 19:58:36 Starting compiler/backend/ag32
Jun 16 19:59:54 Finished compiler/backend/ag32                                 1m17s   1GB
Jun 16 19:59:55 Starting compiler/parsing/proofs
Jun 16 20:06:03 Finished compiler/parsing/proofs                               6m07s 882MB
Jun 16 20:06:03 Starting compiler/inference/proofs
Jun 16 20:08:48 Finished compiler/inference/proofs                             2m44s   1GB
Jun 16 20:08:48 Starting compiler/backend/semantics
Jun 16 20:42:56 Finished compiler/backend/semantics                           34m07s   1GB
Jun 16 20:42:56 Starting compiler/backend/reg_alloc/proofs
Jun 16 20:46:54 Finished compiler/backend/reg_alloc/proofs                     3m58s   1GB
Jun 16 20:46:54 Starting compiler/backend/proofs
Jun 16 21:55:11 Finished compiler/backend/proofs                            1h08m16s  15GB
Jun 16 21:55:11 Starting compiler/encoders/x64/proofs
Jun 16 22:05:54 Finished compiler/encoders/x64/proofs                         10m43s   5GB
Jun 16 22:05:54 Starting compiler/encoders/arm7/proofs
Jun 16 22:20:24 Finished compiler/encoders/arm7/proofs                        14m29s   3GB
Jun 16 22:20:24 Starting compiler/encoders/arm8/proofs
Jun 16 22:27:38 Finished compiler/encoders/arm8/proofs                         7m13s   1GB
Jun 16 22:27:38 Starting compiler/encoders/mips/proofs
Jun 16 22:38:37 Finished compiler/encoders/mips/proofs                        10m58s   2GB
Jun 16 22:38:37 Starting compiler/encoders/riscv/proofs
Jun 16 22:48:10 Finished compiler/encoders/riscv/proofs                        9m33s   1GB
Jun 16 22:48:11 Starting compiler/encoders/ag32/proofs
Jun 16 22:51:04 Finished compiler/encoders/ag32/proofs                         2m52s 602MB
Jun 16 22:51:04 Starting compiler/backend/x64/proofs
Jun 16 22:51:27 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 16 22:51:27 Starting compiler/backend/arm7/proofs
Jun 16 22:51:49 Finished compiler/backend/arm7/proofs                            22s   1GB
Jun 16 22:51:49 Starting compiler/backend/arm8/proofs
Jun 16 22:52:11 Finished compiler/backend/arm8/proofs                            21s   1GB
Jun 16 22:52:11 Starting compiler/backend/mips/proofs
Jun 16 22:52:33 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 16 22:52:34 Starting compiler/backend/riscv/proofs
Jun 16 22:52:56 Finished compiler/backend/riscv/proofs                           22s   1GB
Jun 16 22:52:56 Starting compiler/backend/ag32/proofs
Jun 16 23:07:24 Finished compiler/backend/ag32/proofs                         14m28s   2GB
Jun 16 23:07:24 Starting compiler/proofs
Jun 16 23:09:07 Finished compiler/proofs                                       1m42s   3GB
Jun 16 23:09:07 Starting candle/set-theory
Jun 16 23:09:38 Finished candle/set-theory                                       30s   1GB
Jun 16 23:09:38 Starting candle/syntax-lib
Jun 16 23:09:50 Finished candle/syntax-lib                                       11s 691MB
Jun 16 23:09:50 Starting candle/standard/syntax
Jun 16 23:11:51 Finished candle/standard/syntax                                2m00s 984MB
Jun 16 23:11:51 Starting candle/standard/semantics
Jun 16 23:13:47 Finished candle/standard/semantics                             1m55s   1GB
Jun 16 23:13:47 Starting candle/standard/monadic
Jun 16 23:15:41 Finished candle/standard/monadic                               1m53s   1GB
Jun 16 23:15:41 Starting candle/standard/ml_kernel
Jun 16 23:21:43 Finished candle/standard/ml_kernel                             6m01s   5GB
Jun 16 23:21:43 Starting candle/standard/opentheory
Jun 16 23:32:01 Finished candle/standard/opentheory                           10m18s   4GB
Jun 16 23:32:02 Starting candle/standard/opentheory/compilation
Jun 17 00:06:22 Finished candle/standard/opentheory/compilation               34m19s  26GB
Jun 17 00:06:22 Starting candle/standard/opentheory/compilation/proofs
Jun 17 00:07:31 Finished candle/standard/opentheory/compilation/proofs         1m08s   2GB
Jun 17 00:07:32 Starting candle/overloading/syntax
Jun 17 00:10:55 Finished candle/overloading/syntax                             3m22s   1GB
Jun 17 00:10:55 Starting candle/overloading/semantics
Jun 17 00:18:36 Finished candle/overloading/semantics                          7m40s   2GB
Jun 17 00:18:36 Starting characteristic/examples
Jun 17 00:19:59 Finished characteristic/examples                               1m22s   2GB
Jun 17 00:19:59 Starting tutorial/solutions
Jun 17 00:35:29 Finished tutorial/solutions                                   15m29s  12GB
Jun 17 00:35:29 Starting translator/monadic/examples
Jun 17 00:38:08 FAILED: translator/monadic/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 README.md
Starting work on array_global_stateProgTheory
Starting work on array_local_stateProgTheory
Starting work on array_searchProgTheory
README.md                                       real:    0s  user:    0s     OK
Starting work on doubleProgTheory
doubleProgTheory                                real:   37s  user:   35s     OK
Starting work on exceptionProgTheory
array_searchProgTheory                          real:   43s  user:   41s     OK
Starting work on exception_arity_testProgTheory
array_global_stateProgTheory                    real:   49s  user:   47s     OK
Starting work on fibProgTheory
array_local_stateProgTheory                     real:   73s  user:   70s     OK
Starting work on floyd_warshallProgTheory
exceptionProgTheory                             real:   38s  user:   37s     OK
Starting work on helloProgTheory
exception_arity_testProgTheory                  real:   41s  user:   39s     OK
Starting work on poly_array_sortProgTheory
fibProgTheory                                   real:   59s  user:   57s     OK
Starting work on ref_stateProgTheory
floyd_warshallProgTheory                        real:   53s  user:   51s     OK
Starting work on runProgTheory
helloProgTheory                                 real:   66s  user:   63s     OK
Starting work on test_assumProgTheory
ref_stateProgTheory                             real:   36s  user:   34s     OK
Starting work on test_precondProgTheory
poly_array_sortProgTheory                       real:   73s  user:   70sFAIL<1>
 Saved definition __ "array_get_aux_def"
 Saved induction ___ "array_get_aux_ind"
 Saved definition __ "array_get_def"
 Saved theorem _____ "array_get_aux_Success"
 Saved theorem _____ "array_get_Success"
 /home/cake/oven/regression/cakeml-1275/translator/monadic/examples/poly_array_sortProgScript.sml:890: error: Value or constructor (SORTED_APPEND_IFF) has not been declared
 Found near [SORTED_APPEND_IFF]
 error in quse /home/cake/oven/regression/cakeml-1275/translator/monadic/examples/poly_array_sortProgScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1275/translator/monadic/examples/poly_array_sortProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
runProgTheory                                                           M-KILLED
test_assumProgTheory                                                    M-KILLED
test_precondProgTheory                                                  M-KILLED