CakeML Regression Test

Job 684

CakeML:169cd272829fec7fc43468193f1efcb5b0bb9d34
  Add header file for compcert compatibility [Jan 15 18:49:54]
#604 (master)
Merging into:901708feeaa4cd0a8263ec24d39144eeb1f6d15d
  Merge pull request #599 from CakeML/lem-readme [Jan 14 09:15:32]
HOL:1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42
  Add selftest for sorting_compset [Jan 15 02:02:25]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 16 14:47:09 Claimed job
Jan 16 14:47:35 Building HOL
Jan 16 14:56:55 Starting developers
Jan 16 14:56:57 Finished developers                                               2s  20MB
Jan 16 14:56:58 Starting developers/bin
Jan 16 14:58:08 Finished developers/bin                                        1m08s 916MB
Jan 16 14:58:08 Starting semantics/ffi
Jan 16 14:58:47 Finished semantics/ffi                                           37s 324MB
Jan 16 14:58:47 Starting semantics
Jan 16 15:00:26 Finished semantics                                             1m37s   1GB
Jan 16 15:00:26 Starting semantics/proofs
Jan 16 15:03:48 Finished semantics/proofs                                      3m21s   1GB
Jan 16 15:03:49 Starting basis/pure
Jan 16 15:07:28 Finished basis/pure                                            3m38s 702MB
Jan 16 15:07:29 Starting translator
Jan 16 15:09:10 Finished translator                                            1m40s   1GB
Jan 16 15:09:10 Starting compiler/parsing
Jan 16 15:10:16 Finished compiler/parsing                                      1m04s   1GB
Jan 16 15:10:16 Starting characteristic
Jan 16 15:13:38 Finished characteristic                                        3m20s   2GB
Jan 16 15:13:38 Starting translator/monadic
Jan 16 15:15:08 Finished translator/monadic                                    1m29s   1GB
Jan 16 15:15:09 Starting basis
Jan 16 15:31:23 Finished basis                                                16m13s   2GB
Jan 16 15:31:23 Starting compiler/inference
Jan 16 15:33:21 Finished compiler/inference                                    1m57s   1GB
Jan 16 15:33:22 Starting compiler/backend/reg_alloc
Jan 16 15:34:15 Finished compiler/backend/reg_alloc                              52s   1GB
Jan 16 15:34:15 Starting compiler/backend/gc
Jan 16 15:43:18 Finished compiler/backend/gc                                   9m01s   1GB
Jan 16 15:43:18 Starting compiler/backend
Jan 16 15:43:21 Finished compiler/backend                                         2s  16MB
Jan 16 15:43:22 Starting compiler/encoders/asm
Jan 16 15:43:24 Finished compiler/encoders/asm                                    1s  15MB
Jan 16 15:43:24 Starting compiler/encoders/x64
Jan 16 15:44:26 Finished compiler/encoders/x64                                 1m00s 858MB
Jan 16 15:44:26 Starting compiler/encoders/arm6
Jan 16 15:46:20 Finished compiler/encoders/arm6                                1m52s   1GB
Jan 16 15:46:20 Starting compiler/encoders/arm8
Jan 16 15:46:52 Finished compiler/encoders/arm8                                  31s 511MB
Jan 16 15:46:53 Starting compiler/encoders/mips
Jan 16 15:47:59 Finished compiler/encoders/mips                                1m05s   1GB
Jan 16 15:47:59 Starting compiler/encoders/riscv
Jan 16 15:49:07 Finished compiler/encoders/riscv                               1m07s 803MB
Jan 16 15:49:08 Starting compiler/encoders/ag32
Jan 16 15:49:26 Finished compiler/encoders/ag32                                  17s 789MB
Jan 16 15:49:26 Starting compiler/backend/x64
Jan 16 15:49:44 Finished compiler/backend/x64                                    17s 771MB
Jan 16 15:49:45 Starting compiler/backend/arm6
Jan 16 15:50:06 Finished compiler/backend/arm6                                   20s   1GB
Jan 16 15:50:06 Starting compiler/backend/arm8
Jan 16 15:50:25 Finished compiler/backend/arm8                                   17s   1GB
Jan 16 15:50:26 Starting compiler/backend/mips
Jan 16 15:50:45 Finished compiler/backend/mips                                   19s   1GB
Jan 16 15:50:46 Starting compiler/backend/riscv
Jan 16 15:51:05 Finished compiler/backend/riscv                                  18s 811MB
Jan 16 15:51:05 Starting compiler/backend/ag32
Jan 16 15:52:19 Finished compiler/backend/ag32                                 1m12s   1GB
Jan 16 15:52:19 Starting compiler/parsing/proofs
Jan 16 15:58:27 Finished compiler/parsing/proofs                               6m06s   1GB
Jan 16 15:58:27 Starting compiler/inference/proofs
Jan 16 16:01:21 Finished compiler/inference/proofs                             2m53s   1GB
Jan 16 16:01:22 Starting compiler/backend/semantics
Jan 16 16:06:43 FAILED: compiler/backend/semantics
]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-684/basis/pure]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-684/basis/pure]0;Holmake: ~/oven/regression/cakeml-684/misc]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-684/misc]0;Holmake: ~/oven/regression/cakeml-684/developers]0;Holmake: ~/oven/regression/cakeml-684/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-684/misc]0;Holmake: ~/oven/regression/cakeml-684/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-684/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-684/misc]0;Holmake: ~/oven/regression/cakeml-684/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-684/basis/pure]0;Holmake: ~/oven/regression/cakeml-684/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-684/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-684/semantics]0;Holmake: ~/oven/regression/cakeml-684/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-684/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-684/semantics]0;Holmake: ~/oven/regression/cakeml-684/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-684/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-684/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-684/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-684/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-684/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-684/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/semantics
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
Starting work on wordSemTheory
backendPropsTheory                                                           OK
Starting work on patSemTheory
flatSemTheory                                                                OK
Starting work on flatPropsTheory
closSemTheory                                                                OK
Starting work on bvlSemTheory
patSemTheory                                                                 OK
Starting work on closPropsTheory
bvlSemTheory                                                                 OK
Starting work on bviSemTheory
wordSemTheory                                                                OK
Starting work on dataSemTheory
bviSemTheory                                                                 OK
Starting work on targetSemTheory
dataSemTheory                                                                OK
Starting work on dataPropsTheory
flatPropsTheory                                                              OK
Starting work on patPropsTheory
targetSemTheory                                                              OK
Starting work on labSemTheory
labSemTheory                                                                 OK
Starting work on labPropsTheory
patPropsTheory                                                               OK
Starting work on stackSemTheory
stackSemTheory                                                               OK
Starting work on stackPropsTheory
labPropsTheory                                                               OK
Starting work on targetPropsTheory
targetPropsTheory                                                            OK
Starting work on wordPropsTheory
stackPropsTheory                                                             OK
Starting work on README.md
README.md                                                                    OK
dataPropsTheory                                                              OK
closPropsTheory                                                              OK
Starting work on bvlPropsTheory
wordPropsTheory                                                     FAILED! <1>
     locals_rel temp s t  EVERY (x. x < temp) ls 
     locals_rel temp (alist_insert ls vs s) (alist_insert ls vs t)
 
 failed.
 First unsolved sub-goal is
 
 lookup x (alist_insert [] vs s) = lookup x (alist_insert [] vs t)
 
 Failed to prove theorem locals_rel_alist_insert.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
bvlPropsTheory                                                         M-KILLED