Job 1683

CakeML:1589eaddef9881edeb4243e653a0f7f5a66c87f3
  Var exp is no longer primed [Dec 11 15:27:00]
HOL:c51de550191d516cb9dfe47c6a1e866b232f2c96
  Remove another use of .. that causes grammar precedence problems [Dec 09 23:13:20]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Dec 11 15:30:59 Claimed job
Dec 11 15:31:03 Reusing HOL
Dec 11 15:31:40 Starting developers
Dec 11 15:31:45 Finished developers                                               4s 128MB
Dec 11 15:31:45 Starting developers/bin
Dec 11 15:31:51 Finished developers/bin                                           6s   1GB
Dec 11 15:31:51 Starting semantics/ffi
Dec 11 15:31:59 Finished semantics/ffi                                            8s 216MB
Dec 11 15:31:59 Starting semantics
Dec 11 15:33:21 Finished semantics                                             1m21s   1GB
Dec 11 15:33:21 Starting semantics/proofs
Dec 11 15:36:56 Finished semantics/proofs                                      3m33s   1GB
Dec 11 15:36:56 Starting semantics/alt_semantics
Dec 11 15:37:06 Finished semantics/alt_semantics                                 10s 341MB
Dec 11 15:37:07 Starting semantics/alt_semantics/proofs
Dec 11 15:39:31 Finished semantics/alt_semantics/proofs                        2m24s   1GB
Dec 11 15:39:31 Starting basis/pure
Dec 11 15:40:21 Finished basis/pure                                              49s 693MB
Dec 11 15:40:21 Starting translator
Dec 11 15:43:07 Finished translator                                            2m46s   1GB
Dec 11 15:43:07 Starting compiler/parsing
Dec 11 15:44:20 Finished compiler/parsing                                      1m12s   3GB
Dec 11 15:44:20 Starting characteristic
Dec 11 15:50:01 Finished characteristic                                        5m40s   2GB
Dec 11 15:50:02 Starting translator/monadic
Dec 11 15:51:44 Finished translator/monadic                                    1m41s   1GB
Dec 11 15:51:44 Starting basis
Dec 11 16:37:14 Finished basis                                                45m28s  18GB
Dec 11 16:37:14 Starting compiler/inference
Dec 11 16:38:19 Finished compiler/inference                                    1m04s   1GB
Dec 11 16:38:19 Starting compiler/backend/reg_alloc
Dec 11 16:39:24 Finished compiler/backend/reg_alloc                            1m04s   1GB
Dec 11 16:39:24 Starting compiler/backend/gc
Dec 11 16:42:38 Finished compiler/backend/gc                                   3m13s   2GB
Dec 11 16:42:38 Starting compiler/backend
Dec 11 16:47:04 Finished compiler/backend                                      4m25s   2GB
Dec 11 16:47:04 Starting compiler/encoders/asm
Dec 11 16:47:27 Finished compiler/encoders/asm                                   22s 690MB
Dec 11 16:47:27 Starting compiler/encoders/x64
Dec 11 16:47:52 Finished compiler/encoders/x64                                   24s 786MB
Dec 11 16:47:52 Starting compiler/encoders/arm7
Dec 11 16:48:42 Finished compiler/encoders/arm7                                  50s   1GB
Dec 11 16:48:43 Starting compiler/encoders/arm8
Dec 11 16:48:56 Finished compiler/encoders/arm8                                  13s 935MB
Dec 11 16:48:56 Starting compiler/encoders/mips
Dec 11 16:49:14 Finished compiler/encoders/mips                                  17s   1GB
Dec 11 16:49:14 Starting compiler/encoders/riscv
Dec 11 16:49:29 Finished compiler/encoders/riscv                                 15s 856MB
Dec 11 16:49:30 Starting compiler/encoders/ag32
Dec 11 16:49:48 Finished compiler/encoders/ag32                                  18s 879MB
Dec 11 16:49:48 Starting compiler/backend/x64
Dec 11 16:50:07 Finished compiler/backend/x64                                    18s   1GB
Dec 11 16:50:07 Starting compiler/backend/arm7
Dec 11 16:50:28 Finished compiler/backend/arm7                                   21s   1GB
Dec 11 16:50:28 Starting compiler/backend/arm8
Dec 11 16:50:48 Finished compiler/backend/arm8                                   19s   1GB
Dec 11 16:50:48 Starting compiler/backend/mips
Dec 11 16:51:08 Finished compiler/backend/mips                                   19s   1GB
Dec 11 16:51:08 Starting compiler/backend/riscv
Dec 11 16:51:28 Finished compiler/backend/riscv                                  19s   1GB
Dec 11 16:51:28 Starting compiler/backend/ag32
Dec 11 16:52:35 Finished compiler/backend/ag32                                 1m06s   1GB
Dec 11 16:52:35 Starting compiler/parsing/proofs
Dec 11 16:56:13 Finished compiler/parsing/proofs                               3m37s   1GB
Dec 11 16:56:13 Starting compiler/inference/proofs
Dec 11 16:58:34 Finished compiler/inference/proofs                             2m20s 984MB
Dec 11 16:58:34 Starting compiler/backend/semantics
Dec 11 17:26:46 Finished compiler/backend/semantics                           28m11s   2GB
Dec 11 17:26:46 Starting compiler/backend/reg_alloc/proofs
Dec 11 17:30:13 Finished compiler/backend/reg_alloc/proofs                     3m27s   1GB
Dec 11 17:30:13 Starting compiler/backend/proofs
Dec 11 18:25:52 FAILED: compiler/backend/proofs
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Finished $(CAKEMLDIR)/misc                                                                                     (0.000s) 
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
data_simpProofTheory                                                               compiler/backend/proofs (13s)     OK
Starting work on data_spaceProofTheory
data_spaceProofTheory                                                              compiler/backend/proofs (23s)     OK
Starting work on bvl_constProofTheory
data_liveProofTheory                                                               compiler/backend/proofs (66s)     OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                                                               compiler/backend/proofs (89s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                              compiler/backend/proofs (17s)     OK
Starting work on bvl_inlineProofTheory
bvi_tailrecProofTheory                                                             compiler/backend/proofs(162s)     OK
Starting work on bvi_letProofTheory
bvl_inlineProofTheory                                                              compiler/backend/proofs (28s)     OK
Starting work on clos_annotateProofTheory
bvi_letProofTheory                                                                 compiler/backend/proofs (16s)     OK
Starting work on bvl_to_bviProofTheory
bvi_to_dataProofTheory                                                             compiler/backend/proofs(121s)     OK
Starting work on clos_callProofTheory
clos_annotateProofTheory                                                           compiler/backend/proofs (23s)     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                                                                compiler/backend/proofs (14s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                              compiler/backend/proofs  (9s)     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                                                              compiler/backend/proofs (16s)     OK
Starting work on clos_opProofTheory
clos_opProofTheory                                                                 compiler/backend/proofs (19s)     OK
Starting work on clos_ticksProofTheory
clos_ticksProofTheory                                                              compiler/backend/proofs (21s)     OK
Starting work on clos_knownProofTheory
clos_callProofTheory                                                               compiler/backend/proofs(147s)     OK
Starting work on clos_mtiProofTheory
bvl_to_bviProofTheory                                                              compiler/backend/proofs(168s)     OK
Starting work on clos_numberProofTheory
clos_mtiProofTheory                                                                compiler/backend/proofs (29s)     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                                                             compiler/backend/proofs (21s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                                                                compiler/backend/proofs  (8s)     OK
Starting work on word_bignumProofTheory
clos_knownProofTheory                                                              compiler/backend/proofs(121s)     OK
Starting work on clos_to_bvlProofTheory
word_simpProofTheory                                                               compiler/backend/proofs (48s)     OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory                                                             compiler/backend/proofs (28s)     OK
Starting work on data_to_word_memoryProofTheory
word_bignumProofTheory                                                             compiler/backend/proofs(183s)     OK
Starting work on word_allocProofTheory
clos_to_bvlProofTheory                                                             compiler/backend/proofs(179s)     OK
Starting work on word_instProofTheory
word_instProofTheory                                                               compiler/backend/proofs (47s)     OK
Starting work on word_removeProofTheory
word_removeProofTheory                                                             compiler/backend/proofs (27s)     OK
Starting work on word_depthProofTheory
word_depthProofTheory                                                              compiler/backend/proofs (60s)     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                                                            compiler/backend/proofs (37s)     OK
Starting work on flat_to_closProofTheory
flat_to_closProofTheory                                                            compiler/backend/proofs (72s)     OK
Starting work on lab_filterProofTheory
lab_filterProofTheory                                                              compiler/backend/proofs (53s)     OK
Starting work on stack_removeProofTheory
data_to_word_memoryProofTheory                                                     compiler/backend/proofs(579s)     OK
Starting work on source_evalProofTheory
source_evalProofTheory                                                             compiler/backend/proofs (59s)     OK
Starting work on flat_elimProofTheory
word_allocProofTheory                                                              compiler/backend/proofs(552s)     OK
Starting work on word_to_wordProofTheory
flat_elimProofTheory                                                               compiler/backend/proofs (32s)     OK
Starting work on source_to_flatProofTheory
stack_removeProofTheory                                                            compiler/backend/proofs(228s)     OK
Starting work on lab_to_targetProofTheory
word_to_wordProofTheory                                                            compiler/backend/proofs (50s)     OK
Starting work on data_to_word_gcProofTheory
source_to_flatProofTheory                                                          compiler/backend/proofs (97s)     OK
Starting work on stack_allocProofTheory
lab_to_targetProofTheory                                                           compiler/backend/proofs(205s)     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                                                             compiler/backend/proofs (28s)     OK
Starting work on stack_rawcallProofTheory
data_to_word_gcProofTheory                                                         compiler/backend/proofs(224s)     OK
Starting work on data_to_word_bignumProofTheory
stack_rawcallProofTheory                                                           compiler/backend/proofs (59s)     OK
Starting work on word_to_stackProofTheory
data_to_word_bignumProofTheory                                                     compiler/backend/proofs(202s)     OK
Starting work on data_to_word_assignProofTheory
stack_allocProofTheory                                                             compiler/backend/proofs(402s)     OK
Starting work on word_elimProofTheory
word_elimProofTheory                                                               compiler/backend/proofs (78s)     OK
data_to_word_assignProofTheory                                                     compiler/backend/proofs (17m)     OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                                                            compiler/backend/proofs(249s)     OK
word_to_stackProofTheory                                                           compiler/backend/proofs (25m)     OK
Starting work on stack_to_labProofTheory
stack_to_labProofTheory                                                            compiler/backend/proofs(299s)     OK
Starting work on backendProofTheory
backendProofTheory                                                                 compiler/backend/proofs (69s)FAIL<1>
    installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names ffi
      (heap_regs c.stack_conf.reg_names) mc ms 
    machine_sem mc ffi ms 
    extend_with_resource_limit'
      (is_safe_for_space ffi c prog (read_limits c mc ms))
      (semantics_prog s env prog))
 
 failed.
 Failed to prove theorem compile_correct'.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 3165) (THEN1 on line 3176) (THEN1 on line 3183) (THEN1 on line 3268) (THEN1 on line 3353) (THEN1 on line 3390) (THEN1 on line 3593) (THEN1 on line 3623) (THEN1 on line 3633) (THEN1 on line 3712)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
README.md                                                                          compiler/backend/proofs  (0s)MKILLED