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