Overview

Job 2897

CakeML:37518565be94bc14dc08fcd0968751ddc6a967ee
  Remove dead code from xletauto
#1200 (xletautodeadcode)
Merging into:438ba42d07076a8f14c147c24a56b265ce72accd
  Merge pull request #1199 from CakeML/wordLang_multiret
HOL:8f40aff08a2753e965a7f4d2ebde5c91c5fc14d0
  [emacs-mode] Fix trace-toggling given change in 284560503f
Machine:lammmington

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               3s 199MB
 Starting developers/bin
 Finished developers/bin                                           4s 592MB
 Starting misc
 Finished misc                                                    55s   1GB
 Starting compiler/proofs
 FAILED: compiler/proofs
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanned 91 directories
Starting work on NTpropertiesTheory
Starting work on simpleSexpTheory
Starting work on balanced_mapTheory
Starting work on FormalLangTheory
FormalLangTheory                         examples/formal-languages  (2s)     OK
Finished $(HOLDIR)/examples/formal-languages [#theories: 1]            (2.100s) 
Starting work on charsetTheory
NTpropertiesTheory          examples/formal-languages/context-free  (4s)     OK
Starting work on vec_mapTheory
simpleSexpTheory            examples/formal-languages/context-free  (5s)     OK
Starting work on simpleSexpPEGTheory
vec_mapTheory                    examples/formal-languages/regular  (1s)     OK
Starting work on temporalTheory
simpleSexpPEGTheory         examples/formal-languages/context-free  (3s)     OK
Starting work on simpleSexpParseTheory
temporalTheory                  examples/machine-code/hoare-triple  (3s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 1]   (3.050s) 
Starting work on ffiTheory
charsetTheory                    examples/formal-languages/regular  (8s)     OK
Starting work on regexpTheory
ffiTheory                                            semantics/ffi  (7s)     OK
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1]                     (7.380s) 
Starting work on fpValTreeTheory
fpValTreeTheory                                          semantics  (1s)     OK
Starting work on fpOptTheory
simpleSexpParseTheory       examples/formal-languages/context-free (10s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 4] (23.780s) 
Starting work on namespaceTheory
namespaceTheory                                          semantics  (2s)     OK
Starting work on realOpsTheory
realOpsTheory                                            semantics  (1s)     OK
Starting work on tokensTheory
fpOptTheory                                              semantics  (4s)     OK
Starting work on fpSemTheory
regexpTheory                     examples/formal-languages/regular (14s)     OK
Starting work on mllistTheory
fpSemTheory                                              semantics  (1s)     OK
Starting work on astTheory
tokensTheory                                             semantics  (3s)     OK
Starting work on gramTheory
mllistTheory                                            basis/pure  (2s)     OK
Starting work on tokenUtilsTheory
astTheory                                                semantics  (7s)     OK
Starting work on semanticPrimitivesTheory
gramTheory                                               semantics  (7s)     OK
Starting work on lexer_funTheory
tokenUtilsTheory                                         semantics  (7s)     OK
Starting work on cmlPtreeConversionTheory
cmlPtreeConversionTheory                                 semantics (20s)     OK
Starting work on mlstringTheory
semanticPrimitivesTheory                                 semantics (34s)     OK
Starting work on evaluateTheory
mlstringTheory                                          basis/pure (11s)     OK
Starting work on typeSystemTheory
lexer_funTheory                                          semantics (39s)     OK
Starting work on mlintTheory
evaluateTheory                                           semantics  (5s)     OK
Starting work on mloptionTheory
balanced_mapTheory                           examples/balanced_bst (79s)     OK
Starting work on osetTheory
mloptionTheory                                          basis/pure  (2s)     OK
Starting work on mlmapTheory
mlintTheory                                             basis/pure  (7s)     OK
Starting work on mlratTheory
osetTheory                                   examples/balanced_bst  (4s)     OK
Finished $(HOLDIR)/examples/balanced_bst [#theories: 2]               (83.980s) 
Starting work on regexp_mapTheory
mlmapTheory                                             basis/pure  (4s)     OK
Starting work on mlsetTheory
mlratTheory                                             basis/pure  (3s)     OK
Starting work on typeDecToPPTheory
mlsetTheory                                             basis/pure  (2s)     OK
Starting work on astPropsTheory
regexp_mapTheory                 examples/formal-languages/regular  (3s)     OK
Starting work on regexp_compilerTheory
typeSystemTheory                                         semantics (12s)     OK
Starting work on primTypesTheory
astPropsTheory                                    semantics/proofs  (1s)     OK
Starting work on gramPropsTheory
typeDecToPPTheory                                       basis/pure  (2s)     OK
Starting work on namespacePropsTheory
primTypesTheory                                          semantics  (2s)     OK
Starting work on semanticsTheory
semanticsTheory                                          semantics  (4s)     OK
Finished $(CAKEMLDIR)/semantics [#theories: 16]                      (156.920s) 
Starting work on fpOptPropsTheory
namespacePropsTheory                              semantics/proofs  (5s)     OK
Starting work on semanticPrimitivesPropsTheory
fpOptPropsTheory                                  semantics/proofs  (5s)     OK
Starting work on fpSemPropsTheory
regexp_compilerTheory            examples/formal-languages/regular (14s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 5]   (41.890s) 
Starting work on mlvectorTheory
gramPropsTheory                                   semantics/proofs (14s)     OK
Starting work on typeSoundInvariantsTheory
mlvectorTheory                                          basis/pure  (4s)     OK
Starting work on mlprettyprinterTheory
typeSoundInvariantsTheory                         semantics/proofs  (4s)     OK
Starting work on cmlPEGTheory
mlprettyprinterTheory                                   basis/pure  (7s)     OK
Finished $(CAKEMLDIR)/basis/pure [#theories: 10]                      (49.730s) 
Starting work on fromSexpTheory
semanticPrimitivesPropsTheory                     semantics/proofs (30s)     OK
Starting work on typeSysPropsTheory
typeSysPropsTheory                                semantics/proofs (20s)     OK
Starting work on primSemEnvTheory
primSemEnvTheory                                  semantics/proofs  (7s)     OK
Starting work on weakeningTheory
weakeningTheory                                   semantics/proofs  (5s)     OK
Starting work on lexer_implTheory
cmlPEGTheory                                      compiler/parsing (62s)     OK
Starting work on cmlParseTheory
cmlParseTheory                                    compiler/parsing  (8s)     OK
Starting work on cfFFITypeTheory
cfFFITypeTheory                                     characteristic  (4s)     OK
Starting work on ml_monadBaseTheory
fpSemPropsTheory                                  semantics/proofs (90s)     OK
Starting work on evaluatePropsTheory
fromSexpTheory                                    compiler/parsing (72s)     OK
Starting work on MarshallingTheory
MarshallingTheory                                            basis  (3s)     OK
Starting work on spt_closureTheory
ml_monadBaseTheory                   translator/monadic/monad_base (15s)     OK
Finished $(CAKEMLDIR)/translator/monadic/monad_base [#theories: 1]    (15.520s) 
Starting work on multiwordTheory
spt_closureTheory                              examples/algorithms  (1s)     OK
Finished $(HOLDIR)/examples/algorithms [#theories: 1]                  (1.640s) 
Starting work on pattern_commonTheory
lexer_implTheory                                  compiler/parsing (39s)     OK
Finished $(CAKEMLDIR)/compiler/parsing [#theories: 4]                (182.390s) 
Starting work on reg_allocTheory
pattern_commonTheory             compiler/backend/pattern_matching  (8s)     OK
Starting work on pattern_semanticsTheory
pattern_semanticsTheory          compiler/backend/pattern_matching (12s)     OK
Starting work on pattern_compTheory
multiwordTheory                    examples/machine-code/multiword (25s)     OK
Starting work on mc_multiwordTheory
reg_allocTheory                         compiler/backend/reg_alloc (37s)     OK
Starting work on linear_scanTheory
pattern_compTheory               compiler/backend/pattern_matching (14s)     OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3] (36.660s) 
Starting work on parmoveTheory
mc_multiwordTheory                 examples/machine-code/multiword (34s)     OK
Finished $(HOLDIR)/examples/machine-code/multiword [#theories: 2]     (60.340s) 
Finished $(HOLDIR)/examples/l3-machine-code/common                     (0.000s) 
Starting work on asmTheory
parmoveTheory                           compiler/backend/reg_alloc (21s)     OK
Starting work on backend_commonTheory
evaluatePropsTheory                               semantics/proofs (82s)     OK
Starting work on typeSoundTheory
backend_commonTheory                              compiler/backend  (3s)     OK
Starting work on evaluate_decTheory
linear_scanTheory                       compiler/backend/reg_alloc (32s)     OK
Finished $(CAKEMLDIR)/compiler/backend/reg_alloc [#theories: 3]       (91.380s) 
Starting work on closLangTheory
evaluate_decTheory                                      translator  (6s)     OK
Starting work on ml_progTheory
asmTheory                                    compiler/encoders/asm (10s)     OK
Starting work on asmSemTheory
closLangTheory                                    compiler/backend  (7s)     OK
Starting work on bviTheory
bviTheory                                         compiler/backend  (2s)     OK
Starting work on dataLangTheory
asmSemTheory                                 compiler/encoders/asm (10s)     OK
Starting work on asmPropsTheory
dataLangTheory                                    compiler/backend  (3s)     OK
Starting work on data_liveTheory
ml_progTheory                                           translator (13s)     OK
Starting work on ml_translatorTheory
data_liveTheory                                   compiler/backend  (5s)     OK
Starting work on cfHeapsBaseTheory
asmPropsTheory                               compiler/encoders/asm (15s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/asm [#theories: 3]            (36.400s) 
Starting work on data_simpTheory
data_simpTheory                                   compiler/backend  (2s)     OK
Starting work on data_spaceTheory
cfHeapsBaseTheory                                   characteristic (16s)     OK
Starting work on clFFITheory
data_spaceTheory                                  compiler/backend  (6s)     OK
Starting work on runtimeFFITheory
clFFITheory                                                  basis  (5s)     OK
Starting work on fsFFITheory
runtimeFFITheory                                             basis  (4s)     OK
Starting work on bvi_to_dataTheory
fsFFITheory                                                  basis  (9s)     OK
Starting work on fsFFIPropsTheory
bvi_to_dataTheory                                 compiler/backend (19s)     OK
Starting work on bvi_letTheory
bvi_letTheory                                     compiler/backend  (4s)     OK
Starting work on bvi_tailrecTheory
ml_translatorTheory                                     translator (56s)     OK
Starting work on ml_optimiseTheory
ml_optimiseTheory                                       translator (14s)     OK
Starting work on ml_pmatchTheory
fsFFIPropsTheory                                             basis (40s)     OK
Starting work on bvlTheory
bvlTheory                                         compiler/backend  (2s)     OK
Starting work on bvl_constTheory
ml_pmatchTheory                                         translator (11s)     OK
Starting work on std_preludeTheory
bvi_tailrecTheory                                 compiler/backend (27s)     OK
Starting work on cfHeapsTheory
std_preludeTheory                                       translator (13s)     OK
Finished $(CAKEMLDIR)/translator [#theories: 6]                      (116.140s) 
Starting work on db_varsTheory
cfHeapsTheory                                       characteristic (11s)     OK
Starting work on cfStoreTheory
db_varsTheory                                     compiler/backend  (2s)     OK
Starting work on bvl_jumpTheory
bvl_jumpTheory                                    compiler/backend  (2s)     OK
Starting work on clos_annotateTheory
clos_annotateTheory                               compiler/backend  (6s)     OK
Starting work on clos_callTheory
bvl_constTheory                                   compiler/backend (26s)     OK
Starting work on bvl_handleTheory
cfStoreTheory                                       characteristic (15s)     OK
Starting work on cfNormaliseTheory
clos_callTheory                                   compiler/backend  (6s)     OK
Starting work on clos_fvsTheory
clos_fvsTheory                                    compiler/backend  (2s)     OK
Starting work on clos_letopTheory
clos_letopTheory                                  compiler/backend  (3s)     OK
Starting work on clos_opTheory
cfNormaliseTheory                                   characteristic (12s)     OK
Starting work on cfAppTheory
bvl_handleTheory                                  compiler/backend (18s)     OK
Starting work on bvl_inlineTheory
bvl_inlineTheory                                  compiler/backend  (6s)     OK
Starting work on bvl_to_bviTheory
clos_opTheory                                     compiler/backend (15s)     OK
Starting work on clos_ticksTheory
typeSoundTheory                                   semantics/proofs(166s)     OK
Starting work on semanticsPropsTheory
clos_ticksTheory                                  compiler/backend  (2s)     OK
Starting work on clos_knownTheory
semanticsPropsTheory                              semantics/proofs  (6s)     OK
Finished $(CAKEMLDIR)/semantics/proofs [#theories: 13]               (442.040s) 
Starting work on clos_mtiTheory
cfAppTheory                                         characteristic (21s)     OK
Starting work on cfTheory
clos_mtiTheory                                    compiler/backend  (4s)     OK
Starting work on clos_numberTheory
clos_numberTheory                                 compiler/backend  (2s)     OK
Starting work on stackLangTheory
stackLangTheory                                   compiler/backend  (5s)     OK
Starting work on wordLangTheory
clos_knownTheory                                  compiler/backend (20s)     OK
Starting work on clos_to_bvlTheory
wordLangTheory                                    compiler/backend (10s)     OK
Starting work on word_bignumTheory
bvl_to_bviTheory                                  compiler/backend (38s)     OK
Starting work on word_depthTheory
word_depthTheory                                  compiler/backend  (7s)     OK
Starting work on word_allocTheory
word_bignumTheory                                 compiler/backend (29s)     OK
Starting work on word_copyTheory
word_copyTheory                                   compiler/backend  (6s)     OK
Starting work on word_cseTheory
clos_to_bvlTheory                                 compiler/backend (47s)     OK
Starting work on word_instTheory
word_cseTheory                                    compiler/backend  (9s)     OK
Starting work on word_removeTheory
word_removeTheory                                 compiler/backend  (7s)     OK
Starting work on word_simpTheory
cfTheory                                            characteristic (90s)     OK
Starting work on cfTacticsTheory
word_instTheory                                   compiler/backend (26s)     OK
Starting work on xcfTheory
xcfTheory                                           characteristic  (4s)     OK
Starting work on word_unreachTheory
word_simpTheory                                   compiler/backend (17s)     OK
Starting work on clos_interpTheory
cfTacticsTheory                                     characteristic (12s)     OK
Starting work on cfDivTheory
word_unreachTheory                                compiler/backend  (4s)     OK
Starting work on cfLetAutoTheory
clos_interpTheory                                 compiler/backend (16s)     OK
Starting work on cfMainTheory
cfLetAutoTheory                                     characteristic (18s)     OK
Starting work on ml_monad_translatorBaseTheory
word_allocTheory                                  compiler/backend (87s)     OK
Starting work on word_to_wordTheory
word_to_wordTheory                                compiler/backend  (4s)     OK
Starting work on data_to_wordTheory
cfMainTheory                                        characteristic (16s)     OK
Starting work on flatLangTheory
ml_monad_translatorBaseTheory                   translator/monadic (18s)     OK
Starting work on ml_monad_translatorTheory
flatLangTheory                                    compiler/backend  (8s)     OK
Starting work on flat_to_closTheory
flat_to_closTheory                                compiler/backend (10s)     OK
Starting work on jsonLangTheory
jsonLangTheory                                    compiler/backend  (3s)     OK
Starting work on labLangTheory
labLangTheory                                     compiler/backend  (2s)     OK
Starting work on lab_filterTheory
lab_filterTheory                                  compiler/backend  (2s)     OK
Starting work on lab_to_targetTheory
lab_to_targetTheory                               compiler/backend (12s)     OK
Starting work on str_treeTheory
str_treeTheory                                    compiler/backend  (3s)     OK
Starting work on displayLangTheory
ml_monad_translatorTheory                       translator/monadic (37s)     OK
Starting work on cfMonadTheory
displayLangTheory                                 compiler/backend  (2s)     OK
Starting work on flat_elimTheory
data_to_wordTheory                                compiler/backend (53s)     OK
Starting work on flat_patternTheory
flat_patternTheory                                compiler/backend  (7s)     OK
Starting work on source_letTheory
flat_elimTheory                                   compiler/backend  (8s)     OK
Starting work on source_to_flatTheory
source_letTheory                                  compiler/backend  (3s)     OK
Starting work on source_to_sourceTheory
source_to_sourceTheory                            compiler/backend  (2s)     OK
Starting work on stack_allocTheory
cfMonadTheory                                   translator/monadic (17s)     OK
Finished $(CAKEMLDIR)/translator/monadic [#theories: 3]               (74.100s) 
Starting work on stack_namesTheory
source_to_flatTheory                              compiler/backend  (9s)     OK
Starting work on presLangTheory
stack_namesTheory                                 compiler/backend  (8s)     OK
Starting work on stack_rawcallTheory
stack_allocTheory                                 compiler/backend (21s)     OK
Starting work on stack_removeTheory
presLangTheory                                    compiler/backend (23s)     OK
Starting work on word_to_stackTheory
stack_removeTheory                                compiler/backend  (7s)     OK
Starting work on exportTheory
cfDivTheory                                         characteristic(129s)     OK
Finished $(CAKEMLDIR)/characteristic [#theories: 12]                 (352.980s) 
Starting work on RuntimeProgTheory
exportTheory                                      compiler/backend  (4s)     OK
Starting work on word_elimTheory
word_elimTheory                                   compiler/backend  (3s)     OK
Starting work on ag32Theory
word_to_stackTheory                               compiler/backend (14s)     OK
Starting work on export_ag32Theory
ag32Theory                                  compiler/encoders/ag32  (8s)     OK
Starting work on ag32_targetTheory
stack_rawcallTheory                               compiler/backend (34s)     OK
Starting work on stack_to_labTheory
export_ag32Theory                            compiler/backend/ag32  (9s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/lib                        (0.000s) 
Starting work on armTheory
RuntimeProgTheory                                            basis (21s)     OK
Starting work on OptionProgTheory
ag32_targetTheory                           compiler/encoders/ag32 (12s)     OK
Starting work on RuntimeProofTheory
OptionProgTheory                                             basis  (9s)     OK
Starting work on ListProgTheory
stack_to_labTheory                                compiler/backend (21s)     OK
Starting work on backendTheory
RuntimeProofTheory                                           basis (22s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/ag32 [#theories: 2]           (20.930s) 
Finished $(HOLDIR)/examples/machine-code/decompiler                    (0.000s) 
Starting work on l3-heap
l3-heap                                   examples/l3-machine-code (20s)     OK
Finished $(HOLDIR)/examples/l3-machine-code                           (20.210s) 
Starting work on export_arm7Theory
armTheory                       examples/l3-machine-code/arm/model (48s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/arm/model [#theories: 1]  (48.120s) 
Starting work on arm-heap
backendTheory                                     compiler/backend (27s)     OK
Starting work on backend_passesTheory
export_arm7Theory                            compiler/backend/arm7  (9s)     OK
Starting work on ag32_configTheory
ListProgTheory                                               basis (41s)     OK
Starting work on VectorProgTheory
arm-heap                         examples/l3-machine-code/arm/step (37s)     OK
Starting work on ListProofTheory
backend_passesTheory                              compiler/backend (16s)     OK
Finished $(CAKEMLDIR)/compiler/backend [#theories: 65]               (835.950s) 
Starting work on arm_stepTheory
ag32_configTheory                            compiler/backend/ag32 (19s)     OK
Finished $(CAKEMLDIR)/compiler/backend/ag32 [#theories: 2]            (28.270s) 
Starting work on arm8Theory
arm_stepTheory                   examples/l3-machine-code/arm/step (15s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/arm/step [#theories: 1]   (53.110s) 
Starting work on arm7_targetTheory
VectorProgTheory                                             basis (28s)     OK
Starting work on StringProgTheory
ListProofTheory                                              basis (20s)     OK
Starting work on export_arm8Theory
arm8Theory                     examples/l3-machine-code/arm8/model (18s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/arm8/model [#theories: 1] (18.640s) 
Starting work on arm8-heap
export_arm8Theory                            compiler/backend/arm8  (9s)     OK
Starting work on mipsTheory
arm7_targetTheory                           compiler/encoders/arm7 (14s)     OK
Starting work on arm7_eval_encodeTheory
arm8-heap                       examples/l3-machine-code/arm8/step (16s)     OK
Starting work on arm8_stepTheory
arm8_stepTheory                 examples/l3-machine-code/arm8/step  (4s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/arm8/step [#theories: 1]  (20.940s) 
Starting work on arm8_targetTheory
StringProgTheory                                             basis (32s)     OK
Starting work on mlbasicsProgTheory
arm8_targetTheory                           compiler/encoders/arm8 (13s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/arm8 [#theories: 1]           (13.870s) 
Starting work on arm8_configTheory
arm7_eval_encodeTheory                      compiler/encoders/arm7 (38s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/arm7 [#theories: 2]           (52.820s) 
Starting work on arm7_configTheory
arm8_configTheory                            compiler/backend/arm8 (18s)     OK
Finished $(CAKEMLDIR)/compiler/backend/arm8 [#theories: 2]            (28.460s) 
Starting work on export_mipsTheory
mipsTheory                     examples/l3-machine-code/mips/model (53s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/mips/model [#theories: 1] (53.300s) 
Starting work on mips-heap
mlbasicsProgTheory                                           basis (32s)     OK
Starting work on IntProgTheory
export_mipsTheory                            compiler/backend/mips  (9s)     OK
Starting work on riscvTheory
mips-heap                       examples/l3-machine-code/mips/step (25s)     OK
Starting work on mips_stepTheory
arm7_configTheory                            compiler/backend/arm7 (21s)     OK
Finished $(CAKEMLDIR)/compiler/backend/arm7 [#theories: 2]            (31.240s) 
Starting work on export_riscvTheory
export_riscvTheory                          compiler/backend/riscv  (9s)     OK
Starting work on x64Theory
mips_stepTheory                 examples/l3-machine-code/mips/step (13s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/mips/step [#theories: 1]  (39.250s) 
Starting work on mips_targetTheory
IntProgTheory                                                basis (31s)     OK
Starting work on PrettyPrinterProgTheory
x64Theory                       examples/l3-machine-code/x64/model (17s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/x64/model [#theories: 1]  (17.730s) 
Starting work on x64-heap
mips_targetTheory                           compiler/encoders/mips (17s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/mips [#theories: 1]           (17.370s) 
Starting work on mips_configTheory
x64-heap                         examples/l3-machine-code/x64/step (11s)     OK
Starting work on x64_stepTheory
PrettyPrinterProgTheory                                      basis (20s)     OK
Starting work on RatProgTheory
riscvTheory                   examples/l3-machine-code/riscv/model (56s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/riscv/model [#theories: 1] (56.180s) 
Starting work on riscv-heap
x64_stepTheory                   examples/l3-machine-code/x64/step (16s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/x64/step [#theories: 1]   (28.300s) 
Starting work on x64_targetTheory
riscv-heap                     examples/l3-machine-code/riscv/step (13s)     OK
Starting work on riscv_stepTheory
mips_configTheory                            compiler/backend/mips (19s)     OK
Finished $(CAKEMLDIR)/compiler/backend/mips [#theories: 2]            (29.740s) 
Starting work on export_x64Theory
export_x64Theory                              compiler/backend/x64 (10s)     OK
Starting work on commonUnifTheory
commonUnifTheory        examples/algorithms/unification/triangular  (0s)     OK
Finished $(HOLDIR)/examples/algorithms/unification/triangular [#theories: 1] (0.650s) 
Starting work on cpsTheory
cpsTheory                                    src/transfer/examples  (0s)     OK
Starting work on fmspTheory
x64_targetTheory                             compiler/encoders/x64 (14s)     OK
Starting work on x64_eval_encodeTheory
fmspTheory                                   src/transfer/examples  (1s)     OK
Finished $(HOLDIR)/src/transfer/examples [#theories: 2]                (1.840s) 
Starting work on termTheory
termTheory  examples/algorithms/unification/triangular/first-order  (0s)     OK
Starting work on substTheory
substTheory examples/algorithms/unification/triangular/first-order  (3s)     OK
Starting work on walkTheory
walkTheory  examples/algorithms/unification/triangular/first-order  (2s)     OK
Starting work on walkstarTheory
walkstarTheory ...es/algorithms/unification/triangular/first-order  (1s)     OK
Starting work on collapseTheory
riscv_stepTheory               examples/l3-machine-code/riscv/step (27s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/riscv/step [#theories: 1] (40.490s) 
Starting work on riscv_targetTheory
collapseTheory ...es/algorithms/unification/triangular/first-order  (1s)     OK
Starting work on unifDefTheory
x64_eval_encodeTheory                        compiler/encoders/x64 (12s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/x64 [#theories: 2]            (27.010s) 
Starting work on x64_configTheory
unifDefTheory ...les/algorithms/unification/triangular/first-order  (3s)     OK
Starting work on unifPropsTheory
unifPropsTheory ...s/algorithms/unification/triangular/first-order  (3s)     OK
Finished $(HOLDIR)/examples/algorithms/unification/triangular/first-order [#theories: 7] (15.910s) 
Starting work on rmfmapTheory
RatProgTheory                                                basis (41s)     OK
Starting work on CharProgTheory
rmfmapTheory ...hms/unification/triangular/first-order/compilation  (1s)     OK
Starting work on tcallUnifTheory
tcallUnifTheory .../unification/triangular/first-order/compilation  (5s)     OK
Finished $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation [#theories: 2] (7.240s) 
Starting work on infer_tTheory
riscv_targetTheory                         compiler/encoders/riscv (14s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/riscv [#theories: 1]          (14.780s) 
Starting work on riscv_configTheory
x64_configTheory                              compiler/backend/x64 (18s)     OK
Finished $(CAKEMLDIR)/compiler/backend/x64 [#theories: 2]             (28.970s) 
Starting work on crepLangTheory
infer_tTheory                                   compiler/inference (11s)     OK
Starting work on unifyTheory
crepLangTheory                                             pancake  (8s)     OK
Starting work on crep_arithTheory
crep_arithTheory                                           pancake  (2s)     OK
Starting work on loopLangTheory
riscv_configTheory                          compiler/backend/riscv (19s)     OK
Finished $(CAKEMLDIR)/compiler/backend/riscv [#theories: 2]           (28.990s) 
Starting work on panLangTheory
CharProgTheory                                               basis (28s)     OK
Starting work on Word64ProgTheory
loopLangTheory                                             pancake  (6s)     OK
Starting work on loop_callTheory
loop_callTheory                                            pancake  (2s)     OK
Starting work on loop_liveTheory
panLangTheory                                              pancake  (8s)     OK
Starting work on loop_removeTheory
unifyTheory                                     compiler/inference (18s)FAIL<1>
 Saved theorem _______ "kcwalkstarl_thm"
 Saved theorem _______ "datatype_kclkont"
 Saved theorem _______ "kclkont_11"
 Saved theorem _______ "kclkont_distinct"
 Saved theorem _______ "kclkont_nchotomy"
 Saved theorem _______ "kclkont_Axiom"
 Saved theorem _______ "kclkont_induction"
 Saved theorem _______ "kclkont_case_cong"
 Saved theorem _______ "kclkont_case_eq"
 <<HOL message: Defined type: "kclkont">>
 Saved definition ____ "apply_kclkont_def"
 Saved induction _____ "apply_kclkont_ind"
 Saved definition ____ "dfkcwalkstarl_def"
 Saved theorem _______ "apply_kclkont5"
 Saved theorem _______ "apply_kclkont_thm"
 Saved theorem _______ "dfkcwalkstarl_thm"
 Saved definition ____ "kcwalkstarwl_def"
 Saved theorem _______ "kcwalkstarwl_thm"
 Saved theorem _______ "dfkcwalkstarl_removed"
 Saved theorem _______ "apply_kclkont_ID"
 Saved theorem _______ "cwalkstar_to_dfkcwalkstarl"
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 Saved definition ____ "star_kwork_def"
 Saved induction _____ "star_kwork_ind"
 Saved definition ____ "star_workbag_def"
 Saved theorem _______ "FINITE_star_kwork"
 Saved theorem _______ "FINITE_star_workbag"
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 Saved definition ____ "isCONSk_def"
 Saved induction _____ "isCONSk_ind"
 Saved definition ____ "kcwalkstarwlR_def"
 Saved theorem _______ "WF_kcwalkstarwlR"
 Saved definition ____ "kcwalkstarwl_code_def"
 Saved theorem _______ "kcwalkstarwl_preserves_precond"
 Proof of 
 
 x y.
   ((v,its,k). cwfs s) x  kcwalkstarwl_code s x = INL y 
   kcwalkstarwlR s y x
 
 failed.
 Failed to prove theorem kcwalkstarwl_ensures_decrease.
 
 Exception raised at Tactical.FIRST_LT:
 No goal on which tactic succeeds
 error in quse /scratch/cakeml/regression3/cakeml-2897/compiler/inference/unifyScript.sml : HOL_ERR {message = "No goal on which tactic succeeds", origin_function = "FIRST_LT", origin_structure = "Tactical", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression3/cakeml-2897/compiler/inference/unifyScript : HOL_ERR {message = "No goal on which tactic succeeds", origin_function = "FIRST_LT", origin_structure = "Tactical", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression3/HOL-8f40aff08a2753e965a7f4d2ebde5c91c5fc14d0/src/prekernel/Feedback.sml:124: HOL_ERR {message = "No goal on which tactic succeeds", origin_function = "FIRST_LT", origin_structure = "Tactical", source_location = Loc_Unknown}
 Full log: /scratch/cakeml/regression3/cakeml-2897/compiler/inference/.hol/logs/unifyTheory
Word64ProgTheory                                             basis  (8s)MKILLED
loop_liveTheory                                            pancake  (3s)MKILLED
loop_removeTheory                                          pancake  (2s)MKILLED