CakeML Regression Test

Job 1156

CakeML:3a8cdd942237e58c14d85d24f8d9997cac1784b4
  Merge pull request #718 from CakeML/lpr [Jan 16 12:30:11]
HOL:b219f4bb4132ea21f42769a8edf7e3abde4cc48d
  emacs-mode: some indentation tweaks [Jan 22 06:44:58]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 23 17:55:56 Claimed job
Jan 23 17:55:58 Reusing HOL
Jan 23 17:56:51 Starting developers
Jan 23 17:56:55 Finished developers                                               4s  95MB
Jan 23 17:56:56 Starting developers/bin
Jan 23 17:57:03 Finished developers/bin                                           7s   1GB
Jan 23 17:57:04 Starting semantics/ffi
Jan 23 17:57:14 Finished semantics/ffi                                           10s 228MB
Jan 23 17:57:14 Starting semantics
Jan 23 17:58:37 Finished semantics                                             1m22s   1GB
Jan 23 17:58:37 Starting semantics/proofs
Jan 23 18:02:04 Finished semantics/proofs                                      3m26s 998MB
Jan 23 18:02:05 Starting semantics/alt_semantics
Jan 23 18:02:13 Finished semantics/alt_semantics                                  8s 264MB
Jan 23 18:02:13 Starting semantics/alt_semantics/proofs
Jan 23 18:04:22 Finished semantics/alt_semantics/proofs                        2m08s 761MB
Jan 23 18:04:22 Starting basis/pure
Jan 23 18:05:11 Finished basis/pure                                              49s 892MB
Jan 23 18:05:12 Starting translator
Jan 23 18:07:50 Finished translator                                            2m38s   1GB
Jan 23 18:07:50 Starting compiler/parsing
Jan 23 18:09:02 Finished compiler/parsing                                      1m11s   2GB
Jan 23 18:09:02 Starting characteristic
Jan 23 18:15:02 Finished characteristic                                        5m59s   2GB
Jan 23 18:15:02 Starting translator/monadic
Jan 23 18:16:39 Finished translator/monadic                                    1m36s   1GB
Jan 23 18:16:39 Starting basis
Jan 23 18:51:52 Finished basis                                                35m12s  20GB
Jan 23 18:51:52 Starting compiler/inference
Jan 23 18:54:05 Finished compiler/inference                                    2m13s   1GB
Jan 23 18:54:06 Starting compiler/backend/reg_alloc
Jan 23 18:55:09 Finished compiler/backend/reg_alloc                            1m02s   1GB
Jan 23 18:55:09 Starting compiler/backend/gc
Jan 23 18:58:25 Finished compiler/backend/gc                                   3m16s   2GB
Jan 23 18:58:25 Starting compiler/backend
Jan 23 19:03:00 Finished compiler/backend                                      4m34s   3GB
Jan 23 19:03:00 Starting compiler/encoders/asm
Jan 23 19:03:23 Finished compiler/encoders/asm                                   22s 968MB
Jan 23 19:03:24 Starting compiler/encoders/x64
Jan 23 19:03:50 Finished compiler/encoders/x64                                   25s 757MB
Jan 23 19:03:50 Starting compiler/encoders/arm7
Jan 23 19:04:39 Finished compiler/encoders/arm7                                  48s 741MB
Jan 23 19:04:39 Starting compiler/encoders/arm8
Jan 23 19:04:52 Finished compiler/encoders/arm8                                  12s 901MB
Jan 23 19:04:52 Starting compiler/encoders/mips
Jan 23 19:05:10 Finished compiler/encoders/mips                                  17s   1GB
Jan 23 19:05:10 Starting compiler/encoders/riscv
Jan 23 19:05:25 Finished compiler/encoders/riscv                                 14s 785MB
Jan 23 19:05:25 Starting compiler/encoders/ag32
Jan 23 19:05:43 Finished compiler/encoders/ag32                                  18s 565MB
Jan 23 19:05:44 Starting compiler/backend/x64
Jan 23 19:06:02 Finished compiler/backend/x64                                    18s   1GB
Jan 23 19:06:03 Starting compiler/backend/arm7
Jan 23 19:06:23 Finished compiler/backend/arm7                                   20s   1GB
Jan 23 19:06:23 Starting compiler/backend/arm8
Jan 23 19:06:42 Finished compiler/backend/arm8                                   18s   1GB
Jan 23 19:06:42 Starting compiler/backend/mips
Jan 23 19:07:02 Finished compiler/backend/mips                                   19s   1GB
Jan 23 19:07:02 Starting compiler/backend/riscv
Jan 23 19:07:21 Finished compiler/backend/riscv                                  18s   1GB
Jan 23 19:07:21 Starting compiler/backend/ag32
Jan 23 19:08:33 Finished compiler/backend/ag32                                 1m11s 971MB
Jan 23 19:08:33 Starting compiler/parsing/proofs
Jan 23 19:14:21 Finished compiler/parsing/proofs                               5m47s 942MB
Jan 23 19:14:21 Starting compiler/inference/proofs
Jan 23 19:17:26 Finished compiler/inference/proofs                             3m05s   1GB
Jan 23 19:17:26 Starting compiler/backend/semantics
Jan 23 19:17:38 FAILED: compiler/backend/semantics
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
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 $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Starting work on README.md
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
README.md                                       real:    0s  user:    0s     OK
Starting work on wordSemTheory
backendPropsTheory                              real:    9s  user:    8sFAIL<1>
 Saved theorem _____ "oracle_monotonic_subset"
 Saved theorem _____ "oracle_monotonic_shift_subset"
 Saved theorem _____ "oracle_monotonic_shift_seq"
 Saved theorem _____ "oracle_monotonic_DISJOINT_init"
 error in quse /home/cake/oven/regression/cakeml-1156/compiler/backend/semantics/backendPropsScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1156/compiler/backend/semantics/backendPropsScript : Fail "Static Errors"
 Saved definition __ "is_state_oracle_def"
 /home/cake/oven/regression/cakeml-1156/compiler/backend/semantics/backendPropsScript.sml:177: error: Value or constructor (ADD_1_SUC) has not been declared in structure sptreeTheory
 Found near [sptreeTheory.ADD_1_SUC]
 Uncaught exception: Fail "Static Errors"
closSemTheory                                                           M-KILLED
flatSemTheory                                                           M-KILLED
wordSemTheory                                                           M-KILLED