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"}