Job 1850

CakeML:1ba4cc0596199c911715e5fd992cca4bee9981f8
  Fix bug in translator proofs [Apr 06 11:19:35]
#865 (Iced_cake)
Merging into:4317d3f1cb4cafc7b1ea154c0e89e4dcae2700ba
  Update COPYING [Apr 04 06:16:57]
HOL:6d938663389537576efe0d6e2eeee81911702d3d
  Extend COPYRIGHT into 2022 [Apr 03 23:12:02]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Apr 07 02:55:55 Claimed job
Apr 07 02:56:00 Building HOL
Apr 07 03:05:39 Starting developers
Apr 07 03:05:40 Finished developers                                               1s  36MB
Apr 07 03:05:40 Starting developers/bin
Apr 07 03:05:47 Finished developers/bin                                           6s   1GB
Apr 07 03:05:47 Starting semantics/ffi
Apr 07 03:05:57 Finished semantics/ffi                                            9s 257MB
Apr 07 03:05:57 Starting semantics
Apr 07 03:08:35 Finished semantics                                             2m38s   1GB
Apr 07 03:08:35 Starting semantics/proofs
Apr 07 03:15:38 Finished semantics/proofs                                      7m03s   1GB
Apr 07 03:15:38 Starting semantics/alt_semantics
Apr 07 03:16:08 Finished semantics/alt_semantics                                 29s 522MB
Apr 07 03:16:08 Starting semantics/alt_semantics/proofs
Apr 07 03:29:46 Finished semantics/alt_semantics/proofs                       13m38s   1GB
Apr 07 03:29:46 Starting basis/pure
Apr 07 03:32:53 Finished basis/pure                                            3m06s 899MB
Apr 07 03:32:53 Starting translator
Apr 07 03:36:36 Finished translator                                            3m42s   1GB
Apr 07 03:36:36 Starting compiler/parsing
Apr 07 03:38:08 Finished compiler/parsing                                      1m31s   5GB
Apr 07 03:38:08 Starting characteristic
Apr 07 03:45:10 Finished characteristic                                        6m59s   1GB
Apr 07 03:45:10 Starting translator/monadic
Apr 07 03:47:13 Finished translator/monadic                                    2m02s   1GB
Apr 07 03:47:13 Starting basis
Apr 07 04:38:35 Finished basis                                                51m21s  25GB
Apr 07 04:38:35 Starting compiler/inference
Apr 07 04:40:11 Finished compiler/inference                                    1m36s   1GB
Apr 07 04:40:11 Starting compiler/backend/reg_alloc
Apr 07 04:41:57 Finished compiler/backend/reg_alloc                            1m44s   2GB
Apr 07 04:41:57 Starting compiler/backend/gc
Apr 07 04:46:26 Finished compiler/backend/gc                                   4m26s   1GB
Apr 07 04:46:28 Starting compiler/backend
Apr 07 04:52:18 Finished compiler/backend                                      5m49s   2GB
Apr 07 04:52:18 Starting compiler/encoders/asm
Apr 07 04:52:49 Finished compiler/encoders/asm                                   30s 779MB
Apr 07 04:52:49 Starting compiler/encoders/x64
Apr 07 04:53:56 Finished compiler/encoders/x64                                 1m07s 843MB
Apr 07 04:53:56 Starting compiler/encoders/arm7
Apr 07 04:56:07 Finished compiler/encoders/arm7                                2m10s   1GB
Apr 07 04:56:07 Starting compiler/encoders/arm8
Apr 07 04:56:50 Finished compiler/encoders/arm8                                  43s 667MB
Apr 07 04:56:50 Starting compiler/encoders/arm8_asl
Apr 07 07:09:22 Finished compiler/encoders/arm8_asl                         2h12m31s  44GB
Apr 07 07:09:22 Starting compiler/encoders/mips
Apr 07 07:10:54 Finished compiler/encoders/mips                                1m31s   1GB
Apr 07 07:10:54 Starting compiler/encoders/riscv
Apr 07 07:12:43 Finished compiler/encoders/riscv                               1m48s   1GB
Apr 07 07:12:43 Starting compiler/encoders/ag32
Apr 07 07:13:05 Finished compiler/encoders/ag32                                  21s 862MB
Apr 07 07:13:05 Starting compiler/backend/x64
Apr 07 07:13:28 Finished compiler/backend/x64                                    23s   1GB
Apr 07 07:13:28 Starting compiler/backend/arm7
Apr 07 07:13:52 Finished compiler/backend/arm7                                   24s   1GB
Apr 07 07:13:52 Starting compiler/backend/arm8
Apr 07 07:14:15 Finished compiler/backend/arm8                                   22s   1GB
Apr 07 07:14:15 Starting compiler/backend/mips
Apr 07 07:14:38 Finished compiler/backend/mips                                   22s   1GB
Apr 07 07:14:38 Starting compiler/backend/riscv
Apr 07 07:15:01 Finished compiler/backend/riscv                                  22s   1GB
Apr 07 07:15:01 Starting compiler/backend/ag32
Apr 07 07:16:29 Finished compiler/backend/ag32                                 1m27s   1GB
Apr 07 07:16:29 Starting compiler/parsing/proofs
Apr 07 07:20:11 Finished compiler/parsing/proofs                               3m42s   1GB
Apr 07 07:20:11 Starting compiler/inference/proofs
Apr 07 07:22:55 Finished compiler/inference/proofs                             2m43s   1GB
Apr 07 07:22:56 Starting compiler/backend/semantics
Apr 07 07:54:37 Finished compiler/backend/semantics                           31m41s   2GB
Apr 07 07:54:37 Starting compiler/backend/reg_alloc/proofs
Apr 07 07:58:11 Finished compiler/backend/reg_alloc/proofs                     3m34s 811MB
Apr 07 07:58:12 Starting compiler/backend/proofs
Apr 07 08:11:17 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)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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/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)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanned 48 directories
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 (17s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                              compiler/backend/proofs (29s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                                                 compiler/backend/proofs (22s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                               compiler/backend/proofs (80s)     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                                           compiler/backend/proofs (28s)     OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                                               compiler/backend/proofs (98s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                              compiler/backend/proofs (23s)     OK
Starting work on bvl_inlineProofTheory
bvi_tailrecProofTheory                                                             compiler/backend/proofs(173s)     OK
Starting work on clos_fvsProofTheory
bvl_inlineProofTheory                                                              compiler/backend/proofs (36s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                                                                compiler/backend/proofs (19s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                              compiler/backend/proofs (14s)     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                                             compiler/backend/proofs(138s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                                                              compiler/backend/proofs (21s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                                                                 compiler/backend/proofs (24s)     OK
Starting work on clos_mtiProofTheory
clos_callProofTheory                                                               compiler/backend/proofs(165s)     OK
Starting work on clos_numberProofTheory
clos_ticksProofTheory                                                              compiler/backend/proofs (27s)     OK
Starting work on clos_knownProofTheory
clos_numberProofTheory                                                             compiler/backend/proofs (28s)     OK
Starting work on bvl_jumpProofTheory
clos_mtiProofTheory                                                                compiler/backend/proofs (36s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                                                                compiler/backend/proofs (13s)     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                                               compiler/backend/proofs (57s)     OK
Starting work on word_gcFunctionsTheory
bvl_to_bviProofTheory                                                              compiler/backend/proofs(184s)     OK
Starting work on word_allocProofTheory
word_gcFunctionsTheory                                                             compiler/backend/proofs (42s)     OK
Starting work on data_to_word_memoryProofTheory
clos_knownProofTheory                                                              compiler/backend/proofs(135s)     OK
Starting work on clos_to_bvlProofTheory
word_bignumProofTheory                                                             compiler/backend/proofs(213s)     OK
Starting work on word_instProofTheory
word_instProofTheory                                                               compiler/backend/proofs (56s)     OK
Starting work on word_removeProofTheory
word_removeProofTheory                                                             compiler/backend/proofs (35s)     OK
Starting work on word_depthProofTheory
clos_to_bvlProofTheory                                                             compiler/backend/proofs(208s)     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                                                            compiler/backend/proofs (45s)     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                                                              compiler/backend/proofs (64s)     OK
Starting work on lab_filterProofTheory
lab_filterProofTheory                                                              compiler/backend/proofs (66s)     OK
Starting work on stack_removeProofTheory
flat_to_closProofTheory                                                            compiler/backend/proofs (85s)     OK
Starting work on source_evalProofTheory
source_evalProofTheory                                                             compiler/backend/proofs (23s)FAIL<1>
   SOME ((refs'',s.ffi),Rval (Loc (LENGTH refs'))) 
   LIST_REL (sv_rel (v_rel orac_s')) (s.refs  [Varray (x1::v47)]) refs''
 
 Failed to prove theorem do_app_sim.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/cug/hk324/cml-regression/cakeml-1850/compiler/backend/proofs/source_evalProofScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/cug/hk324/cml-regression/cakeml-1850/compiler/backend/proofs/source_evalProofScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
word_allocProofTheory                                                              compiler/backend/proofs(404s)MKILLED
data_to_word_memoryProofTheory                                                     compiler/backend/proofs(382s)MKILLED
stack_removeProofTheory                                                            compiler/backend/proofs (26s)MKILLED