Overview

Job 1853

CakeML:bda8728644fe57011f006f9dd2ea4946a3844f98
  Merge branch 'master' into Iced_cake
#865 (Iced_cake)
Merging into:746be7b61665e6297b7ce29f70b74eec6efc7a79
  Merge pull request #873 from CakeML/issue871
HOL:bf3e59ba99decc59cfe5a28a6d45dfea3e058afc
  Add a timeout on regression build attempts
Machine:oven3

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               9s  91MB
 Starting developers/bin
 Finished developers/bin                                          13s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           24s 247MB
 Starting semantics
 Finished semantics                                             5m20s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                     15m24s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                               1m01s 534MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                       25m27s   1GB
 Starting basis/pure
 Finished basis/pure                                            6m29s 950MB
 Starting translator
 Finished translator                                            7m57s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m55s   3GB
 Starting characteristic
 Finished characteristic                                       14m39s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    4m16s   1GB
 Starting basis
 Finished basis                                              1h51m50s  13GB
 Starting compiler/inference
 Finished compiler/inference                                    3m27s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            3m15s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   8m51s   2GB
 Starting compiler/backend
 Finished compiler/backend                                     11m27s   2GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                 1m06s 778MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 2m32s 940MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                4m43s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                1m33s   1GB
 Starting compiler/encoders/arm8_asl
 Finished compiler/encoders/arm8_asl                         4h11m36s  43GB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                3m23s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               3m51s 824MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  48s 698MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    46s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   53s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   46s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   51s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  49s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 2m59s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               8m29s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             6m08s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                         1h11m30s   3GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     7m47s   1GB
 Starting compiler/backend/proofs
 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  (2s)     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                                                                                                                                                         compiler/backend/proofs (35s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                                                                                                                        compiler/backend/proofs (61s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                                                                                                                                           compiler/backend/proofs (42s)     OK
Starting work on clos_annotateProofTheory
clos_annotateProofTheory                                                                                                                                                     compiler/backend/proofs (57s)     OK
Starting work on clos_callProofTheory
data_liveProofTheory                                                                                                                                                         compiler/backend/proofs(173s)     OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                                                                                                                                                         compiler/backend/proofs(203s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                                                                                                                        compiler/backend/proofs (41s)     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                                                                                                                                                        compiler/backend/proofs (69s)     OK
Starting work on clos_fvsProofTheory
bvi_tailrecProofTheory                                                                                                                                                       compiler/backend/proofs(369s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                                                                                                                                                          compiler/backend/proofs (37s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                                                                                                                        compiler/backend/proofs (25s)     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                                                                                                                                       compiler/backend/proofs(268s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                                                                                                                                                        compiler/backend/proofs (38s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                                                                                                                                                           compiler/backend/proofs (48s)     OK
Starting work on clos_mtiProofTheory
clos_callProofTheory                                                                                                                                                         compiler/backend/proofs(327s)     OK
Starting work on clos_numberProofTheory
clos_ticksProofTheory                                                                                                                                                        compiler/backend/proofs (51s)     OK
Starting work on clos_knownProofTheory
clos_numberProofTheory                                                                                                                                                       compiler/backend/proofs (57s)     OK
Starting work on bvl_jumpProofTheory
clos_mtiProofTheory                                                                                                                                                          compiler/backend/proofs (68s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                                                                                                                                                          compiler/backend/proofs (24s)     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                                                                                                                                         compiler/backend/proofs(112s)     OK
Starting work on word_gcFunctionsTheory
bvl_to_bviProofTheory                                                                                                                                                        compiler/backend/proofs(372s)     OK
Starting work on word_allocProofTheory
word_gcFunctionsTheory                                                                                                                                                       compiler/backend/proofs (75s)     OK
Starting work on data_to_word_memoryProofTheory
clos_knownProofTheory                                                                                                                                                        compiler/backend/proofs(262s)     OK
Starting work on clos_to_bvlProofTheory
word_bignumProofTheory                                                                                                                                                       compiler/backend/proofs(409s)     OK
Starting work on word_instProofTheory
word_instProofTheory                                                                                                                                                         compiler/backend/proofs(109s)     OK
Starting work on word_removeProofTheory
word_removeProofTheory                                                                                                                                                       compiler/backend/proofs (65s)     OK
Starting work on word_depthProofTheory
clos_to_bvlProofTheory                                                                                                                                                       compiler/backend/proofs(401s)     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                                                                                                                                                      compiler/backend/proofs (93s)     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                                                                                                                                                        compiler/backend/proofs(129s)     OK
Starting work on lab_filterProofTheory
lab_filterProofTheory                                                                                                                                                        compiler/backend/proofs(132s)     OK
Starting work on stack_removeProofTheory
flat_to_closProofTheory                                                                                                                                                      compiler/backend/proofs(174s)     OK
Starting work on source_evalProofTheory
source_evalProofTheory                                                                                                                                                       compiler/backend/proofs(180s)     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                                                                                                                                                         compiler/backend/proofs (84s)     OK
Starting work on source_to_flatProofTheory
word_allocProofTheory                                                                                                                                                        compiler/backend/proofs (19m)     OK
Starting work on word_to_wordProofTheory
stack_removeProofTheory                                                                                                                                                      compiler/backend/proofs(535s)     OK
Starting work on lab_to_targetProofTheory
source_to_flatProofTheory                                                                                                                                                    compiler/backend/proofs(276s)     OK
Starting work on stack_allocProofTheory
word_to_wordProofTheory                                                                                                                                                      compiler/backend/proofs(118s)     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                                                                                                                                                       compiler/backend/proofs (69s)     OK
Starting work on stack_rawcallProofTheory
data_to_word_memoryProofTheory                                                                                                                                               compiler/backend/proofs (22m)     OK
Starting work on data_to_word_gcProofTheory
stack_rawcallProofTheory                                                                                                                                                     compiler/backend/proofs(155s)     OK
Starting work on word_to_stackProofTheory
lab_to_targetProofTheory                                                                                                                                                     compiler/backend/proofs(493s)     OK
Starting work on word_elimProofTheory
data_to_word_gcProofTheory                                                                                                                                                   compiler/backend/proofs(524s)     OK
Starting work on data_to_word_bignumProofTheory
word_elimProofTheory                                                                                                                                                         compiler/backend/proofs(174s)     OK
stack_allocProofTheory                                                                                                                                                       compiler/backend/proofs(955s)     OK
data_to_word_bignumProofTheory                                                                                                                                               compiler/backend/proofs(472s)     OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory                                                                                                                                                     compiler/backend/proofs (47m)     OK
Starting work on stack_to_labProofTheory
data_to_word_assignProofTheory                                                                                                                                               compiler/backend/proofs (38m)     OK
Starting work on data_to_wordProofTheory
stack_to_labProofTheory                                                                                                                                                      compiler/backend/proofs(701s)     OK
data_to_wordProofTheory                                                                                                                                                      compiler/backend/proofs(518s)     OK
Starting work on backendProofTheory
backendProofTheory                                                                                                                                                           compiler/backend/proofs(323s)     OK
Starting work on backend_itreeProofTheory
backend_itreeProofTheory                                                                                                                                                     compiler/backend/proofs (62s)FAIL<1>
 First unsolved sub-goal is
 
 <|refs := []; next_type_stamp := 2; next_exn_stamp := 4; eval_state := NONE;
   fp_state :=
     <|rws := []; opts := (x. []); choices := 0; canOpt := Strict;
       real_sem := F|> |> =
 <|refs := []; next_type_stamp := 2; next_exn_stamp := 4; eval_state := NONE|>
 
 Failed to prove theorem start_dstate.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}