Job 1682

CakeML:c3690f80386409010c5998f08a26b8dea26e8b7a
  Merge pull request #849 from CakeML/delete_terminationTheory [Dec 11 07:42:47]
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 07:46:30 Claimed job
Dec 11 07:46:37 Building HOL
Dec 11 07:55:59 Starting developers
Dec 11 07:56:03 Finished developers                                               4s 114MB
Dec 11 07:56:03 Starting developers/bin
Dec 11 07:56:10 Finished developers/bin                                           6s   1GB
Dec 11 07:56:10 Starting semantics/ffi
Dec 11 07:56:18 Finished semantics/ffi                                            8s 212MB
Dec 11 07:56:18 Starting semantics
Dec 11 07:57:50 Finished semantics                                             1m31s   1GB
Dec 11 07:57:50 Starting semantics/proofs
Dec 11 08:01:25 Finished semantics/proofs                                      3m35s   1GB
Dec 11 08:01:25 Starting semantics/alt_semantics
Dec 11 08:01:36 Finished semantics/alt_semantics                                 10s 363MB
Dec 11 08:01:36 Starting semantics/alt_semantics/proofs
Dec 11 08:04:00 Finished semantics/alt_semantics/proofs                        2m23s 795MB
Dec 11 08:04:00 Starting basis/pure
Dec 11 08:06:50 Finished basis/pure                                            2m50s 925MB
Dec 11 08:06:51 Starting translator
Dec 11 08:09:37 Finished translator                                            2m46s   1GB
Dec 11 08:09:37 Starting compiler/parsing
Dec 11 08:10:50 Finished compiler/parsing                                      1m12s   2GB
Dec 11 08:10:50 Starting characteristic
Dec 11 08:16:31 Finished characteristic                                        5m40s   2GB
Dec 11 08:16:31 Starting translator/monadic
Dec 11 08:18:12 Finished translator/monadic                                    1m40s   1GB
Dec 11 08:18:12 Starting basis
Dec 11 09:03:26 Finished basis                                                45m12s  19GB
Dec 11 09:03:26 Starting compiler/inference
Dec 11 09:04:40 Finished compiler/inference                                    1m13s 984MB
Dec 11 09:04:40 Starting compiler/backend/reg_alloc
Dec 11 09:05:46 Finished compiler/backend/reg_alloc                            1m05s   1GB
Dec 11 09:05:46 Starting compiler/backend/gc
Dec 11 09:09:11 Finished compiler/backend/gc                                   3m25s   1GB
Dec 11 09:09:11 Starting compiler/backend
Dec 11 09:13:39 Finished compiler/backend                                      4m27s   2GB
Dec 11 09:13:39 Starting compiler/encoders/asm
Dec 11 09:14:01 Finished compiler/encoders/asm                                   22s 720MB
Dec 11 09:14:01 Starting compiler/encoders/x64
Dec 11 09:15:02 Finished compiler/encoders/x64                                 1m00s 887MB
Dec 11 09:15:02 Starting compiler/encoders/arm7
Dec 11 09:17:00 Finished compiler/encoders/arm7                                1m57s   1GB
Dec 11 09:17:00 Starting compiler/encoders/arm8
Dec 11 09:17:37 Finished compiler/encoders/arm8                                  36s 934MB
Dec 11 09:17:37 Starting compiler/encoders/mips
Dec 11 09:19:02 Finished compiler/encoders/mips                                1m25s   1GB
Dec 11 09:19:02 Starting compiler/encoders/riscv
Dec 11 09:20:44 Finished compiler/encoders/riscv                               1m42s   1GB
Dec 11 09:20:45 Starting compiler/encoders/ag32
Dec 11 09:21:02 Finished compiler/encoders/ag32                                  17s 648MB
Dec 11 09:21:02 Starting compiler/backend/x64
Dec 11 09:21:22 Finished compiler/backend/x64                                    19s   1GB
Dec 11 09:21:22 Starting compiler/backend/arm7
Dec 11 09:21:42 Finished compiler/backend/arm7                                   20s   1GB
Dec 11 09:21:43 Starting compiler/backend/arm8
Dec 11 09:22:02 Finished compiler/backend/arm8                                   18s   1GB
Dec 11 09:22:02 Starting compiler/backend/mips
Dec 11 09:22:21 Finished compiler/backend/mips                                   19s   1GB
Dec 11 09:22:21 Starting compiler/backend/riscv
Dec 11 09:22:41 Finished compiler/backend/riscv                                  20s   1GB
Dec 11 09:22:41 Starting compiler/backend/ag32
Dec 11 09:23:49 Finished compiler/backend/ag32                                 1m07s   1GB
Dec 11 09:23:49 Starting compiler/parsing/proofs
Dec 11 09:27:29 Finished compiler/parsing/proofs                               3m40s   1GB
Dec 11 09:27:29 Starting compiler/inference/proofs
Dec 11 09:29:51 Finished compiler/inference/proofs                             2m21s   1GB
Dec 11 09:29:51 Starting compiler/backend/semantics
Dec 11 09:57:24 Finished compiler/backend/semantics                           27m32s   2GB
Dec 11 09:57:24 Starting compiler/backend/reg_alloc/proofs
Dec 11 10:00:48 Finished compiler/backend/reg_alloc/proofs                     3m23s   1GB
Dec 11 10:00:48 Starting compiler/backend/proofs
Dec 11 10:10:42 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
README.md                                                                          compiler/backend/proofs  (1s)     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                                                               compiler/backend/proofs (13s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                              compiler/backend/proofs (25s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                                                 compiler/backend/proofs (17s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                               compiler/backend/proofs (66s)     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                                           compiler/backend/proofs (24s)     OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                                               compiler/backend/proofs (93s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                              compiler/backend/proofs (18s)     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                                                              compiler/backend/proofs (28s)     OK
Starting work on clos_fvsProofTheory
bvi_tailrecProofTheory                                                             compiler/backend/proofs(164s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                                                                compiler/backend/proofs (14s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                              compiler/backend/proofs (10s)     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                                             compiler/backend/proofs(125s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                                                              compiler/backend/proofs (16s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                                                                 compiler/backend/proofs (20s)     OK
Starting work on clos_mtiProofTheory
clos_ticksProofTheory                                                              compiler/backend/proofs (22s)     OK
Starting work on clos_knownProofTheory
clos_callProofTheory                                                               compiler/backend/proofs(154s)     OK
Starting work on clos_numberProofTheory
clos_mtiProofTheory                                                                compiler/backend/proofs (31s)     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                                                             compiler/backend/proofs (23s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                                                                compiler/backend/proofs  (9s)     OK
Starting work on word_bignumProofTheory
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
bvl_to_bviProofTheory                                                              compiler/backend/proofs(172s)     OK
Starting work on word_allocProofTheory
clos_knownProofTheory                                                              compiler/backend/proofs(124s)     OK
Starting work on clos_to_bvlProofTheory
word_bignumProofTheory                                                             compiler/backend/proofs(187s)     OK
Starting work on word_instProofTheory
word_instProofTheory                                                               compiler/backend/proofs (48s)     OK
Starting work on word_removeProofTheory
word_removeProofTheory                                                             compiler/backend/proofs (27s)     OK
Starting work on word_depthProofTheory
clos_to_bvlProofTheory                                                             compiler/backend/proofs(189s)     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                                                            compiler/backend/proofs (37s)     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                                                              compiler/backend/proofs (58s)FAIL<1>
 res  SOME Error  subspt funs s.code 
 option_le s1.stack_max
   (OPTION_MAP2 MAX s.stack_max
      (OPTION_MAP2 $+ s.locals_size
         (OPTION_MAP2 $+ (stack_size s.stack)
            (max_depth s.stack_size (full_call_graph dest funs)))))
 
 failed.
 Failed to prove theorem max_depth_Call_SOME.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 851)", origin_function = "THEN1", origin_structure = "Tactical"}
data_to_word_memoryProofTheory                                                     compiler/backend/proofs(251s)MKILLED
word_allocProofTheory                                                              compiler/backend/proofs(245s)MKILLED
flat_to_closProofTheory                                                            compiler/backend/proofs  (4s)MKILLED