CakeML Regression Test

Job 1155

CakeML:343fb5a57700571bb7c4b396c3fc9426d9763710
  Add LenEq and improve TagLenEq; and update proofs [Jan 23 09:01:09]
#720 (flat-to-clos)
Merging into: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 15:14:28 Claimed job
Jan 23 15:14:35 Building HOL
Jan 23 15:25:57 Starting developers
Jan 23 15:26:02 Finished developers                                               4s  97MB
Jan 23 15:26:02 Starting developers/bin
Jan 23 15:26:10 Finished developers/bin                                           7s   1GB
Jan 23 15:26:10 Starting semantics/ffi
Jan 23 15:26:20 Finished semantics/ffi                                           10s 233MB
Jan 23 15:26:20 Starting semantics
Jan 23 15:27:52 Finished semantics                                             1m31s   1GB
Jan 23 15:27:53 Starting semantics/proofs
Jan 23 15:31:21 Finished semantics/proofs                                      3m27s   1GB
Jan 23 15:31:21 Starting semantics/alt_semantics
Jan 23 15:31:29 Finished semantics/alt_semantics                                  8s 294MB
Jan 23 15:31:29 Starting semantics/alt_semantics/proofs
Jan 23 15:33:39 Finished semantics/alt_semantics/proofs                        2m09s 820MB
Jan 23 15:33:40 Starting basis/pure
Jan 23 15:36:44 Finished basis/pure                                            3m03s 840MB
Jan 23 15:36:44 Starting translator
Jan 23 15:39:23 Finished translator                                            2m39s   1GB
Jan 23 15:39:23 Starting compiler/parsing
Jan 23 15:40:34 Finished compiler/parsing                                      1m10s   2GB
Jan 23 15:40:34 Starting characteristic
Jan 23 15:46:31 Finished characteristic                                        5m56s   1GB
Jan 23 15:46:31 Starting translator/monadic
Jan 23 15:48:07 Finished translator/monadic                                    1m35s   1GB
Jan 23 15:48:07 Starting basis
Jan 23 16:23:32 Finished basis                                                35m25s  13GB
Jan 23 16:23:33 Starting compiler/inference
Jan 23 16:25:52 Finished compiler/inference                                    2m19s   2GB
Jan 23 16:25:52 Starting compiler/backend/reg_alloc
Jan 23 16:26:55 Finished compiler/backend/reg_alloc                            1m01s   1GB
Jan 23 16:26:55 Starting compiler/backend/gc
Jan 23 16:30:24 Finished compiler/backend/gc                                   3m29s   2GB
Jan 23 16:30:24 Starting compiler/backend
Jan 23 16:34:57 Finished compiler/backend                                      4m32s   3GB
Jan 23 16:34:57 Starting compiler/encoders/asm
Jan 23 16:35:19 Finished compiler/encoders/asm                                   21s 701MB
Jan 23 16:35:19 Starting compiler/encoders/x64
Jan 23 16:36:18 Finished compiler/encoders/x64                                   58s 948MB
Jan 23 16:36:18 Starting compiler/encoders/arm7
Jan 23 16:38:06 Finished compiler/encoders/arm7                                1m47s   1GB
Jan 23 16:38:06 Starting compiler/encoders/arm8
Jan 23 16:38:41 Finished compiler/encoders/arm8                                  34s 653MB
Jan 23 16:38:41 Starting compiler/encoders/mips
Jan 23 16:39:54 Finished compiler/encoders/mips                                1m12s   1GB
Jan 23 16:39:54 Starting compiler/encoders/riscv
Jan 23 16:41:21 Finished compiler/encoders/riscv                               1m26s   1GB
Jan 23 16:41:21 Starting compiler/encoders/ag32
Jan 23 16:41:39 Finished compiler/encoders/ag32                                  17s 711MB
Jan 23 16:41:39 Starting compiler/backend/x64
Jan 23 16:41:57 Finished compiler/backend/x64                                    18s   1GB
Jan 23 16:41:58 Starting compiler/backend/arm7
Jan 23 16:42:18 Finished compiler/backend/arm7                                   20s   1GB
Jan 23 16:42:18 Starting compiler/backend/arm8
Jan 23 16:42:37 Finished compiler/backend/arm8                                   18s   1GB
Jan 23 16:42:37 Starting compiler/backend/mips
Jan 23 16:42:57 Finished compiler/backend/mips                                   19s   1GB
Jan 23 16:42:57 Starting compiler/backend/riscv
Jan 23 16:43:16 Finished compiler/backend/riscv                                  18s   1GB
Jan 23 16:43:16 Starting compiler/backend/ag32
Jan 23 16:44:26 Finished compiler/backend/ag32                                 1m09s   1GB
Jan 23 16:44:26 Starting compiler/parsing/proofs
Jan 23 16:50:20 Finished compiler/parsing/proofs                               5m53s 924MB
Jan 23 16:50:20 Starting compiler/inference/proofs
Jan 23 16:53:25 Finished compiler/inference/proofs                             3m04s 950MB
Jan 23 16:53:25 Starting compiler/backend/semantics
Jan 23 17:24:12 Finished compiler/backend/semantics                           30m45s   2GB
Jan 23 17:24:12 Starting compiler/backend/reg_alloc/proofs
Jan 23 17:27:48 Finished compiler/backend/reg_alloc/proofs                     3m35s 965MB
Jan 23 17:27:48 Starting compiler/backend/proofs
Jan 23 17:55:55 FAILED: compiler/backend/proofs
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)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
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
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Starting work on reachable_sptProofTheory
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md                                       real:    1s  user:    0s     OK
Starting work on data_simpProofTheory
reachable_sptProofTheory                        real:   12s  user:   11s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   14s  user:   13s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   29s  user:   27s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   19s  user:   17s     OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                            real:   51s  user:   50s     OK
Starting work on bvl_handleProofTheory
data_liveProofTheory                            real:   72s  user:   71s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   27s  user:   26s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   20s  user:   19s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   33s  user:   32s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   17s  user:   16s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   11s  user:   10s     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                           real:   18s  user:   17s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  192s  user:  189s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   25s  user:   24s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  139s  user:  136s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   35s  user:   34s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  182s  user:  179s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                          real:   25s  user:   24s     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                             real:   10s  user:    9s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   54s  user:   53s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  134s  user:  132s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   27s  user:   26s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  195s  user:  191s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  215s  user:  210s     OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory                          real:  215s  user:  210s     OK
Starting work on word_removeProofTheory
word_instProofTheory                            real:   51s  user:   49s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   29s  user:   28s     OK
Starting work on flat_patternProofTheory
word_depthProofTheory                           real:   69s  user:   68s     OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory                         real:   49s  user:   48s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   59s  user:   57s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   62s  user:   60s     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                            real:   67s  user:   65s     OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory                       real:  107s  user:  105s     OK
Starting work on stack_allocProofTheory
stack_removeProofTheory                         real:  269s  user:  264s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  624s  user:  616s     OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                         real:   67s  user:   65s     OK
Starting work on stack_namesProofTheory
data_to_word_memoryProofTheory                  real:  746s  user:  738s     OK
Starting work on data_to_word_gcProofTheory
stack_namesProofTheory                          real:   32s  user:   31s     OK
Starting work on stack_rawcallProofTheory
stack_rawcallProofTheory                        real:   72s  user:   70s     OK
Starting work on word_to_stackProofTheory
lab_to_targetProofTheory                        real:  242s  user:  237s     OK
Starting work on word_elimProofTheory
stack_allocProofTheory                          real:  429s  user:  423s     OK
word_elimProofTheory                            real:  127s  user:  125s     OK
data_to_word_gcProofTheory                      real:  247s  user:  242s     OK
Starting work on data_to_word_bignumProofTheory
data_to_word_bignumProofTheory                  real:  272s  user:  269s     OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory                        real:  498s  user:  490sFAIL<1>
 Saved theorem _____ "comp_FFI_correct"
 Saved theorem _____ "compile_prog_stack_size"
 Proved triviality _ "SUB_SUB_SUB_MAX"
 Proved triviality _ "MAX_LE"
 Saved theorem _____ "stack_rel_stack_size"
 /home/cake/oven/regression/cakeml-1155/compiler/backend/proofs/word_to_stackProofScript.sml:7138: error: Value or constructor (EL_CONS_IF) has not been declared
 Found near [EL_CONS_IF, PRE_SUB1]
 error in quse /home/cake/oven/regression/cakeml-1155/compiler/backend/proofs/word_to_stackProofScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1155/compiler/backend/proofs/word_to_stackProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
data_to_word_assignProofTheory                                          M-KILLED