CakeML:741ac48b85efa0a158d4d1241e53cab7ca8d1de4
Remove more stray timeLang files
#1161 (untime)
Merging into:3d7e93912298b606a2c046ad9ccea824c08e7528
remove stray comment in #1157
HOL:cf4347f8d871d793c021d04fe2bdc677c7149183
Add UNCURRY_CONST
Machine:pavlova
Claimed job
Building HOL
Starting developers
Finished developers 3s 127MB
Starting developers/bin
Finished developers/bin 4s 592MB
Starting misc
Finished misc 57s 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/ring/src
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 92 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.090s)
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.140s)
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.540s)
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.050s)
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 (18s) OK
Starting work on mlstringTheory
mlstringTheory basis/pure (12s) OK
Starting work on mlintTheory
semanticPrimitivesTheory semantics (35s) OK
Starting work on evaluateTheory
lexer_funTheory semantics (40s) OK
Starting work on typeSystemTheory
evaluateTheory semantics (5s) OK
Starting work on mloptionTheory
mlintTheory basis/pure (7s) OK
Starting work on mlratTheory
mloptionTheory basis/pure (2s) OK
Starting work on typeDecToPPTheory
typeDecToPPTheory basis/pure (2s) OK
Starting work on astPropsTheory
mlratTheory basis/pure (3s) OK
Starting work on gramPropsTheory
astPropsTheory semantics/proofs (1s) OK
Starting work on namespacePropsTheory
typeSystemTheory semantics (12s) OK
Starting work on primTypesTheory
namespacePropsTheory semantics/proofs (5s) OK
Starting work on fpOptPropsTheory
primTypesTheory semantics (2s) OK
Starting work on semanticsTheory
fpOptPropsTheory semantics/proofs (5s) OK
Starting work on fpSemPropsTheory
semanticsTheory semantics (4s) OK
Finished $(CAKEMLDIR)/semantics [#theories: 16] (156.880s)
Starting work on semanticPrimitivesPropsTheory
gramPropsTheory semantics/proofs (14s) OK
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory semantics/proofs (4s) OK
Starting work on cmlPEGTheory
balanced_mapTheory examples/balanced_bst(134s) OK
Starting work on osetTheory
semanticPrimitivesPropsTheory semantics/proofs (36s) OK
Starting work on mlmapTheory
osetTheory examples/balanced_bst (4s) OK
Finished $(HOLDIR)/examples/balanced_bst [#theories: 2] (139.190s)
Starting work on regexp_mapTheory
mlmapTheory basis/pure (4s) OK
Starting work on mlsetTheory
regexp_mapTheory examples/formal-languages/regular (3s) OK
Starting work on regexp_compilerTheory
mlsetTheory basis/pure (2s) OK
Starting work on typeSysPropsTheory
regexp_compilerTheory examples/formal-languages/regular (14s) OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 5] (41.700s)
Starting work on mlvectorTheory
mlvectorTheory basis/pure (4s) OK
Starting work on mlprettyprinterTheory
typeSysPropsTheory semantics/proofs (20s) OK
Starting work on primSemEnvTheory
cmlPEGTheory compiler/parsing (62s) OK
Starting work on weakeningTheory
mlprettyprinterTheory basis/pure (7s) OK
Finished $(CAKEMLDIR)/basis/pure [#theories: 10] (50.580s)
Starting work on cmlParseTheory
primSemEnvTheory semantics/proofs (7s) OK
Starting work on fromSexpTheory
weakeningTheory semantics/proofs (5s) OK
Starting work on lexer_implTheory
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
ml_monadBaseTheory translator/monadic/monad_base (15s) OK
Finished $(CAKEMLDIR)/translator/monadic/monad_base [#theories: 1] (15.510s)
Starting work on MarshallingTheory
MarshallingTheory basis (3s) OK
Starting work on spt_closureTheory
spt_closureTheory examples/algorithms (1s) OK
Finished $(HOLDIR)/examples/algorithms [#theories: 1] (1.600s)
Starting work on multiwordTheory
lexer_implTheory compiler/parsing (44s) OK
Starting work on pattern_commonTheory
pattern_commonTheory compiler/backend/pattern_matching (9s) OK
Starting work on pattern_semanticsTheory
multiwordTheory examples/machine-code/multiword (25s) OK
Starting work on mc_multiwordTheory
pattern_semanticsTheory compiler/backend/pattern_matching (13s) OK
Starting work on pattern_compTheory
fromSexpTheory compiler/parsing (69s) OK
Finished $(CAKEMLDIR)/compiler/parsing [#theories: 4] (184.620s)
Starting work on reg_allocTheory
pattern_compTheory compiler/backend/pattern_matching (15s) OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3] (38.740s)
Starting work on parmoveTheory
evaluatePropsTheory semantics/proofs (82s) OK
Starting work on typeSoundTheory
mc_multiwordTheory examples/machine-code/multiword (35s) OK
Starting work on evaluate_decTheory
evaluate_decTheory translator (6s) OK
Starting work on ml_progTheory
parmoveTheory compiler/backend/reg_alloc (22s) OK
Finished $(HOLDIR)/examples/machine-code/multiword [#theories: 2] (61.770s)
Finished $(HOLDIR)/examples/l3-machine-code/common (0.000s)
Starting work on asmTheory
reg_allocTheory compiler/backend/reg_alloc (37s) OK
Starting work on linear_scanTheory
ml_progTheory translator (12s) OK
Starting work on ml_translatorTheory
asmTheory compiler/encoders/asm (11s) OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory characteristic (15s) OK
Starting work on clFFITheory
clFFITheory basis (4s) OK
Starting work on runtimeFFITheory
linear_scanTheory compiler/backend/reg_alloc (31s) OK
Starting work on fsFFITheory
runtimeFFITheory basis (4s) OK
Finished $(CAKEMLDIR)/compiler/backend/reg_alloc [#theories: 3] (90.850s)
Starting work on asmSemTheory
fsFFITheory basis (9s) OK
Starting work on fsFFIPropsTheory
asmSemTheory compiler/encoders/asm (11s) OK
Starting work on asmPropsTheory
ml_translatorTheory translator (54s) OK
Starting work on ml_optimiseTheory
asmPropsTheory compiler/encoders/asm (15s) OK
Starting work on ml_pmatchTheory
ml_optimiseTheory translator (14s) OK
Finished $(CAKEMLDIR)/compiler/encoders/asm [#theories: 3] (38.750s)
Starting work on backend_commonTheory
backend_commonTheory compiler/backend (4s) OK
Starting work on closLangTheory
ml_pmatchTheory translator (11s) OK
Starting work on std_preludeTheory
closLangTheory compiler/backend (7s) OK
Starting work on cfHeapsTheory
fsFFIPropsTheory basis (40s) OK
Starting work on bviTheory
bviTheory compiler/backend (2s) OK
Starting work on dataLangTheory
dataLangTheory compiler/backend (3s) OK
Starting work on data_liveTheory
std_preludeTheory translator (13s) OK
Finished $(CAKEMLDIR)/translator [#theories: 6] (113.460s)
Starting work on data_simpTheory
data_simpTheory compiler/backend (2s) OK
Starting work on data_spaceTheory
data_liveTheory compiler/backend (5s) OK
Starting work on bvi_letTheory
cfHeapsTheory characteristic (11s) OK
Starting work on cfStoreTheory
bvi_letTheory compiler/backend (3s) OK
Starting work on bvi_tailrecTheory
data_spaceTheory compiler/backend (5s) OK
Starting work on bvi_to_dataTheory
cfStoreTheory characteristic (15s) OK
Starting work on cfNormaliseTheory
bvi_to_dataTheory compiler/backend (19s) OK
Starting work on bvlTheory
bvlTheory compiler/backend (2s) OK
Starting work on bvl_constTheory
cfNormaliseTheory characteristic (13s) OK
Starting work on cfAppTheory
bvi_tailrecTheory compiler/backend (30s) OK
Starting work on db_varsTheory
db_varsTheory compiler/backend (2s) OK
Starting work on bvl_jumpTheory
bvl_jumpTheory compiler/backend (2s) OK
Starting work on clos_annotateTheory
typeSoundTheory semantics/proofs(164s) OK
Starting work on semanticsPropsTheory
clos_annotateTheory compiler/backend (6s) OK
Starting work on clos_callTheory
semanticsPropsTheory semantics/proofs (6s) OK
Finished $(CAKEMLDIR)/semantics/proofs [#theories: 13] (447.640s)
Starting work on clos_fvsTheory
cfAppTheory characteristic (21s) OK
Starting work on cfTheory
clos_callTheory compiler/backend (6s) OK
Starting work on clos_letopTheory
clos_fvsTheory compiler/backend (2s) OK
Starting work on clos_opTheory
clos_letopTheory compiler/backend (3s) OK
Starting work on clos_ticksTheory
bvl_constTheory compiler/backend (26s) OK
Starting work on bvl_handleTheory
clos_ticksTheory compiler/backend (2s) OK
Starting work on clos_mtiTheory
clos_mtiTheory compiler/backend (4s) OK
Starting work on clos_numberTheory
clos_numberTheory compiler/backend (2s) OK
Starting work on stackLangTheory
clos_opTheory compiler/backend (14s) OK
Starting work on clos_knownTheory
stackLangTheory compiler/backend (6s) OK
Starting work on wordLangTheory
bvl_handleTheory compiler/backend (18s) OK
Starting work on bvl_inlineTheory
wordLangTheory compiler/backend (10s) OK
Starting work on word_bignumTheory
bvl_inlineTheory compiler/backend (6s) OK
Starting work on bvl_to_bviTheory
clos_knownTheory compiler/backend (20s) OK
Starting work on clos_to_bvlTheory
word_bignumTheory compiler/backend (27s) OK
Starting work on word_depthTheory
word_depthTheory compiler/backend (4s) OK
Starting work on word_allocTheory
bvl_to_bviTheory compiler/backend (37s) OK
Starting work on word_copyTheory
word_copyTheory compiler/backend (6s) OK
Starting work on word_cseTheory
word_cseTheory compiler/backend (9s) OK
Starting work on word_instTheory
clos_to_bvlTheory compiler/backend (47s) OK
Starting work on word_removeTheory
cfTheory characteristic (90s) OK
Starting work on cfTacticsTheory
word_removeTheory compiler/backend (7s) OK
Starting work on xcfTheory
xcfTheory characteristic (4s) OK
Starting work on word_simpTheory
cfTacticsTheory characteristic (12s) OK
Starting work on cfDivTheory
word_instTheory compiler/backend (26s) OK
Starting work on cfLetAutoTheory
word_simpTheory compiler/backend (17s) OK
Starting work on cfMainTheory
word_allocTheory compiler/backend (71s) OK
Starting work on word_unreachTheory
cfMainTheory characteristic (17s) OK
Starting work on clos_interpTheory
cfLetAutoTheory characteristic (19s) OK
Starting work on ml_monad_translatorBaseTheory
word_unreachTheory compiler/backend (4s) OK
Starting work on word_to_wordTheory
word_to_wordTheory compiler/backend (4s) OK
Starting work on data_to_wordTheory
clos_interpTheory compiler/backend (16s) OK
Starting work on flatLangTheory
ml_monad_translatorBaseTheory translator/monadic (20s) 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 (3s) OK
Starting work on lab_filterTheory
lab_filterTheory compiler/backend (2s) OK
Starting work on lab_to_targetTheory
data_to_wordTheory compiler/backend (50s) OK
Starting work on str_treeTheory
lab_to_targetTheory compiler/backend (12s) OK
Starting work on flat_elimTheory
ml_monad_translatorTheory translator/monadic (38s) OK
Starting work on cfMonadTheory
str_treeTheory compiler/backend (3s) OK
Starting work on displayLangTheory
displayLangTheory compiler/backend (2s) OK
Starting work on flat_patternTheory
flat_elimTheory compiler/backend (7s) OK
Starting work on source_letTheory
source_letTheory compiler/backend (3s) OK
Starting work on source_to_sourceTheory
flat_patternTheory compiler/backend (7s) OK
Starting work on source_to_flatTheory
source_to_sourceTheory compiler/backend (2s) OK
Starting work on stack_allocTheory
cfMonadTheory translator/monadic (19s) OK
Finished $(CAKEMLDIR)/translator/monadic [#theories: 3] (78.440s)
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
cfDivTheory characteristic(133s) OK
Finished $(CAKEMLDIR)/characteristic [#theories: 12] (358.980s)
Starting work on RuntimeProgTheory
stack_allocTheory compiler/backend (21s) OK
Starting work on stack_removeTheory
stack_removeTheory compiler/backend (6s) OK
Starting work on word_to_stackTheory
presLangTheory compiler/backend (23s) OK
Starting work on exportTheory
exportTheory compiler/backend (4s) OK
Starting work on word_elimTheory
RuntimeProgTheory basis (20s) OK
Starting work on OptionProgTheory
word_elimTheory compiler/backend (3s) OK
Starting work on RuntimeProofTheory
word_to_stackTheory compiler/backend (13s) OK
Starting work on ag32Theory
OptionProgTheory basis (9s) OK
Starting work on ListProgTheory
stack_rawcallTheory compiler/backend (33s) OK
Starting work on stack_to_labTheory
ag32Theory compiler/encoders/ag32 (8s) OK
Starting work on ag32_targetTheory
RuntimeProofTheory basis (21s) OK
Starting work on export_ag32Theory
ag32_targetTheory compiler/encoders/ag32 (12s) OK
Finished $(CAKEMLDIR)/compiler/encoders/ag32 [#theories: 2] (21.780s)
Finished $(HOLDIR)/examples/l3-machine-code/lib (0.000s)
Starting work on armTheory
export_ag32Theory compiler/backend/ag32 (9s) OK
Finished $(HOLDIR)/examples/machine-code/decompiler (0.000s)
Starting work on l3-heap
stack_to_labTheory compiler/backend (21s) OK
Starting work on backendTheory
l3-heap examples/l3-machine-code (19s) OK
Finished $(HOLDIR)/examples/l3-machine-code (19.100s)
Starting work on export_arm7Theory
ListProgTheory basis (42s) OK
Starting work on VectorProgTheory
export_arm7Theory compiler/backend/arm7 (10s) OK
Starting work on ListProofTheory
backendTheory compiler/backend (26s) OK
Starting work on backend_passesTheory
ListProofTheory basis (20s) OK
Starting work on ag32_configTheory
armTheory examples/l3-machine-code/arm/model (48s) OK
Finished $(HOLDIR)/examples/l3-machine-code/arm/model [#theories: 1] (48.250s)
Starting work on arm-heap
backend_passesTheory compiler/backend (15s) OK
Finished $(CAKEMLDIR)/compiler/backend [#theories: 65] (808.270s)
Starting work on arm8Theory
VectorProgTheory basis (28s) OK
Starting work on StringProgTheory
arm-heap examples/l3-machine-code/arm/step (46s) OK
Starting work on arm_stepTheory
ag32_configTheory compiler/backend/ag32 (18s) OK
Finished $(CAKEMLDIR)/compiler/backend/ag32 [#theories: 2] (28.200s)
Starting work on export_arm8Theory
arm8Theory examples/l3-machine-code/arm8/model (19s) OK
Finished $(HOLDIR)/examples/l3-machine-code/arm8/model [#theories: 1] (19.140s)
Starting work on arm8-heap
arm8-heap examples/l3-machine-code/arm8/step (18s) OK
Starting work on arm8_stepTheory
export_arm8Theory compiler/backend/arm8 (10s) OK
Starting work on mipsTheory
arm_stepTheory examples/l3-machine-code/arm/step (16s) OK
Finished $(HOLDIR)/examples/l3-machine-code/arm/step [#theories: 1] (62.970s)
Starting work on arm7_targetTheory
arm8_stepTheory examples/l3-machine-code/arm8/step (4s) OK
Finished $(HOLDIR)/examples/l3-machine-code/arm8/step [#theories: 1] (23.040s)
Starting work on arm8_targetTheory
StringProgTheory basis (34s) OK
Starting work on mlbasicsProgTheory
arm7_targetTheory compiler/encoders/arm7 (14s) OK
Starting work on arm7_eval_encodeTheory
arm8_targetTheory compiler/encoders/arm8 (14s) OK
Finished $(CAKEMLDIR)/compiler/encoders/arm8 [#theories: 1] (14.230s)
Starting work on arm8_configTheory
arm8_configTheory compiler/backend/arm8 (20s) OK
Finished $(CAKEMLDIR)/compiler/backend/arm8 [#theories: 2] (31.480s)
Starting work on export_mipsTheory
mlbasicsProgTheory basis (32s) OK
Starting work on IntProgTheory
mipsTheory examples/l3-machine-code/mips/model (52s) OK
Finished $(HOLDIR)/examples/l3-machine-code/mips/model [#theories: 1] (52.170s)
Starting work on mips-heap
export_mipsTheory compiler/backend/mips (10s) OK
Starting work on riscvTheory
arm7_eval_encodeTheory compiler/encoders/arm7 (39s) OK
Finished $(CAKEMLDIR)/compiler/encoders/arm7 [#theories: 2] (53.610s)
Starting work on arm7_configTheory
mips-heap examples/l3-machine-code/mips/step (19s) OK
Starting work on mips_stepTheory
mips_stepTheory examples/l3-machine-code/mips/step (13s) OK
Finished $(HOLDIR)/examples/l3-machine-code/mips/step [#theories: 1] (33.810s)
Starting work on mips_targetTheory
IntProgTheory basis (31s) OK
Starting work on PrettyPrinterProgTheory
arm7_configTheory compiler/backend/arm7 (20s) OK
Finished $(CAKEMLDIR)/compiler/backend/arm7 [#theories: 2] (31.270s)
Starting work on export_riscvTheory
export_riscvTheory compiler/backend/riscv (10s) OK
Starting work on x64Theory
mips_targetTheory compiler/encoders/mips (17s) OK
Finished $(CAKEMLDIR)/compiler/encoders/mips [#theories: 1] (17.190s)
Starting work on mips_configTheory
PrettyPrinterProgTheory basis (20s) OK
Starting work on RatProgTheory
riscvTheory examples/l3-machine-code/riscv/model (57s) OK
Finished $(HOLDIR)/examples/l3-machine-code/riscv/model [#theories: 1] (57.700s)
Starting work on riscv-heap
x64Theory examples/l3-machine-code/x64/model (19s) OK
Finished $(HOLDIR)/examples/l3-machine-code/x64/model [#theories: 1] (19.120s)
Starting work on x64-heap
riscv-heap examples/l3-machine-code/riscv/step (14s) OK
Starting work on riscv_stepTheory
mips_configTheory compiler/backend/mips (21s) OK
Finished $(CAKEMLDIR)/compiler/backend/mips [#theories: 2] (31.830s)
Starting work on export_x64Theory
x64-heap examples/l3-machine-code/x64/step (12s) OK
Starting work on x64_stepTheory
export_x64Theory compiler/backend/x64 (11s) OK
Starting work on commonUnifTheory
commonUnifTheory examples/algorithms/unification/triangular (0s) OK
Finished $(HOLDIR)/examples/algorithms/unification/triangular [#theories: 1] (0.660s)
Starting work on cpsTheory
cpsTheory src/transfer/examples (0s) OK
Starting work on fmspTheory
fmspTheory src/transfer/examples (1s) OK
Finished $(HOLDIR)/src/transfer/examples [#theories: 2] (1.740s)
Starting work on termTheory
termTheory examples/algorithms/unification/triangular/first-order (1s) OK
Starting work on substTheory
x64_stepTheory examples/l3-machine-code/x64/step (16s) OK
Finished $(HOLDIR)/examples/l3-machine-code/x64/step [#theories: 1] (29.370s)
Starting work on x64_targetTheory
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 (2s) OK
Starting work on collapseTheory
RatProgTheory basis (41s) OK
Starting work on CharProgTheory
riscv_stepTheory examples/l3-machine-code/riscv/step (26s) OK
Finished $(HOLDIR)/examples/l3-machine-code/riscv/step [#theories: 1] (41.830s)
Starting work on riscv_targetTheory
collapseTheory ...es/algorithms/unification/triangular/first-order (1s) OK
Starting work on unifDefTheory
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] (16.050s)
Starting work on rmfmapTheory
x64_targetTheory compiler/encoders/x64 (14s) OK
Starting work on x64_eval_encodeTheory
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.020s)
Starting work on infer_tTheory
riscv_targetTheory compiler/encoders/riscv (15s) OK
Finished $(CAKEMLDIR)/compiler/encoders/riscv [#theories: 1] (15.080s)
Starting work on riscv_configTheory
x64_eval_encodeTheory compiler/encoders/x64 (13s) OK
Finished $(CAKEMLDIR)/compiler/encoders/x64 [#theories: 2] (27.460s)
Starting work on x64_configTheory
CharProgTheory basis (26s) OK
Starting work on Word64ProgTheory
infer_tTheory compiler/inference (12s) OK
Starting work on unifyTheory
riscv_configTheory compiler/backend/riscv (20s) OK
Finished $(CAKEMLDIR)/compiler/backend/riscv [#theories: 2] (30.280s)
Starting work on crepLangTheory
x64_configTheory compiler/backend/x64 (18s) OK
Finished $(CAKEMLDIR)/compiler/backend/x64 [#theories: 2] (30.380s)
Starting work on loopLangTheory
crepLangTheory pancake (8s) OK
Starting work on crep_arithTheory
crep_arithTheory pancake (2s) OK
Starting work on panLangTheory
loopLangTheory pancake (6s) OK
Starting work on loop_callTheory
loop_callTheory pancake (2s) OK
Starting work on loop_liveTheory
Word64ProgTheory basis (29s) OK
Starting work on Word8ProgTheory
loop_liveTheory pancake (4s) OK
Starting work on crep_to_loopTheory
panLangTheory pancake (7s) OK
Starting work on loop_removeTheory
unifyTheory compiler/inference (31s) OK
Starting work on inferTheory
loop_removeTheory pancake (3s) OK
Starting work on loop_to_wordTheory
crep_to_loopTheory pancake (4s) OK
Starting work on panStaticTheory
loop_to_wordTheory pancake (4s) OK
Starting work on pan_commonTheory
pan_commonTheory pancake (1s) OK
Starting work on pan_simpTheory
panStaticTheory pancake (6s) OK
Starting work on pan_to_crepTheory
pan_simpTheory pancake (5s) OK
Starting work on panLexerTheory
pan_to_crepTheory pancake (5s) OK
Starting work on pan_to_wordTheory
pan_to_wordTheory pancake (2s) OK
Starting work on pan_to_targetTheory
panLexerTheory pancake/parser (6s) OK
Starting work on panPEGTheory
pan_to_targetTheory pancake (6s) OK
Starting work on pan_passesTheory
Word8ProgTheory basis (27s) OK
Starting work on Word8ArrayProgTheory
pan_passesTheory pancake (15s) OK
Finished $(CAKEMLDIR)/pancake [#theories: 16] (90.650s)
Starting work on gc_sharedTheory
panPEGTheory pancake/parser (25s) OK
Starting work on panPtreeConversionTheory
Word8ArrayProgTheory basis (26s) OK
Starting work on ArrayProgTheory
inferTheory compiler/inference (52s) OK
Starting work on Word8ArrayProofTheory
gc_sharedTheory compiler/backend/gc (15s) OK
Starting work on inferPropsTheory
panPtreeConversionTheory pancake/parser (12s) OK
Finished $(CAKEMLDIR)/pancake/parser [#theories: 3] (44.340s)
Starting work on copying_gcTheory
copying_gcTheory compiler/backend/gc (14s) OK
Starting work on gen_gcTheory
Word8ArrayProofTheory basis (33s) OK
Starting work on reg_allocProofTheory
gen_gcTheory compiler/backend/gc (28s) OK
Starting work on gen_gc_partialTheory
inferPropsTheory compiler/inference (64s) OK
Finished $(CAKEMLDIR)/compiler/inference [#theories: 4] (161.100s)
Starting work on backendPropsTheory
backendPropsTheory compiler/backend/semantics (4s) OK
Starting work on closSemTheory
ArrayProgTheory basis (74s) OK
Starting work on ArrayProofTheory
closSemTheory compiler/backend/semantics (14s) OK
Starting work on MapProgTheory
reg_allocProofTheory compiler/backend/reg_alloc/proofs (54s) OK
Starting work on linear_scanProofTheory
ArrayProofTheory basis (59s) OK
Starting work on bvlSemTheory
bvlSemTheory compiler/backend/semantics (10s) OK
Starting work on bviSemTheory
MapProgTheory basis (57s) OK
Starting work on SetProgTheory
gen_gc_partialTheory compiler/backend/gc (96s) OK
Starting work on gc_combinedTheory
bviSemTheory compiler/backend/semantics (8s) OK
Starting work on bvlPropsTheory
gc_combinedTheory compiler/backend/gc (12s) OK
Finished $(CAKEMLDIR)/compiler/backend/gc [#theories: 5] (167.260s)
Starting work on closPropsTheory
SetProgTheory basis (56s) OK
Starting work on HashtableProgTheory
bvlPropsTheory compiler/backend/semantics (63s) OK
Starting work on bviPropsTheory
linear_scanProofTheory compiler/backend/reg_alloc/proofs(139s) OK
Finished $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs [#theories: 2] (193.880s)
Starting work on dataSemTheory
bviPropsTheory compiler/backend/semantics (35s) OK
Starting work on flatSemTheory
HashtableProgTheory basis (52s) OK
Starting work on CommandLineProgTheory
flatSemTheory compiler/backend/semantics (16s) OK
Starting work on flatPropsTheory
dataSemTheory compiler/backend/semantics (56s) OK
Starting work on dataPropsTheory
CommandLineProgTheory basis (38s) OK
Starting work on CommandLineProofTheory
flatPropsTheory compiler/backend/semantics (45s) OK
Starting work on DoubleProgTheory
closPropsTheory compiler/backend/semantics(163s) OK
Starting work on wordSemTheory
CommandLineProofTheory basis (65s) OK
Starting work on wordConvsTheory
wordSemTheory compiler/backend/semantics (42s) OK
Starting work on targetSemTheory
targetSemTheory compiler/backend/semantics (8s) OK
Starting work on labSemTheory
wordConvsTheory compiler/backend/semantics (15s) OK
Starting work on targetPropsTheory
DoubleProgTheory basis (60s) OK
Starting work on MarshallingProgTheory
labSemTheory compiler/backend/semantics (15s) OK
Starting work on labPropsTheory
targetPropsTheory compiler/backend/semantics (22s) OK
Starting work on stackSemTheory
MarshallingProgTheory basis (46s) OK
Starting work on TextIOProgTheory
stackSemTheory compiler/backend/semantics (26s) OK
Starting work on stackPropsTheory
labPropsTheory compiler/backend/semantics (90s) OK
Starting work on wordPropsTheory
TextIOProgTheory basis(163s) OK
Starting work on TextIOProofTheory
wordPropsTheory compiler/backend/semantics(269s) OK
Starting work on bvi_tailrecProofTheory
bvi_tailrecProofTheory compiler/backend/proofs(127s) OK
Starting work on bvl_constProofTheory
bvl_constProofTheory compiler/backend/proofs (70s) OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory compiler/backend/proofs (16s) OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory compiler/backend/proofs (19s) OK
Starting work on bvi_letProofTheory
bvi_letProofTheory compiler/backend/proofs (10s) OK
Starting work on bvl_to_bviProofTheory
bvl_to_bviProofTheory compiler/backend/proofs(142s) OK
Starting work on clos_annotateProofTheory
clos_annotateProofTheory compiler/backend/proofs (18s) OK
Starting work on clos_callProofTheory
clos_callProofTheory compiler/backend/proofs(124s) OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory compiler/backend/proofs (8s) OK
Starting work on clos_interpProofTheory
clos_interpProofTheory compiler/backend/proofs (24s) OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory compiler/backend/proofs (4s) OK
Starting work on clos_letopProofTheory
clos_letopProofTheory compiler/backend/proofs (9s) OK
Starting work on clos_opProofTheory
clos_opProofTheory compiler/backend/proofs (17s) OK
Starting work on clos_ticksProofTheory
clos_ticksProofTheory compiler/backend/proofs (14s) OK
Starting work on clos_knownProofTheory
clos_knownProofTheory compiler/backend/proofs (88s) OK
Starting work on clos_mtiProofTheory
dataPropsTheory compiler/backend/semantics (21m) OK
Starting work on data_liveProofTheory
data_liveProofTheory compiler/backend/proofs (62s) OK
Starting work on data_simpProofTheory
data_simpProofTheory compiler/backend/proofs (9s) OK
Starting work on data_spaceProofTheory
data_spaceProofTheory compiler/backend/proofs (19s) OK
Starting work on bvi_to_dataProofTheory
bvi_to_dataProofTheory compiler/backend/proofs (95s) OK
Starting work on clos_numberProofTheory
clos_numberProofTheory compiler/backend/proofs (15s) OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory compiler/backend/proofs (3s) OK
Starting work on clos_constantProofTheory
clos_constantProofTheory compiler/backend/proofs (18s) OK
Starting work on word_simpProofTheory
word_simpProofTheory compiler/backend/proofs (48s) OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory compiler/backend/proofs (17s) OK
Starting work on data_to_word_memoryProofTheory
data_to_word_memoryProofTheory compiler/backend/proofs(577s) OK
Starting work on word_bignumProofTheory
word_bignumProofTheory compiler/backend/proofs (44s)FAIL<1>
runtime: 0.27988s, gctime: 0.00000s, systime: 0.00397s.
derive_corr_thm mc_copy_over Saved theorem _______ "mc_copy_over_corr_thm"
runtime: 0.35342s, gctime: 0.03416s, systime: 0.00000s.
derive_corr_thm mc_div0 Saved theorem _______ "mc_div0_corr_thm"
runtime: 0.66768s, gctime: 0.06652s, systime: 0.01586s.
derive_corr_thm mc_single_div Saved theorem _______ "mc_single_div_corr_thm"
runtime: 0.25082s, gctime: 0.00450s, systime: 0.00013s.
derive_corr_thm mc_simple_div Saved theorem _______ "mc_simple_div_corr_thm"
runtime: 0.56217s, gctime: 0.05216s, systime: 0.01596s.
derive_corr_thm mc_div1 Saved theorem _______ "mc_div1_corr_thm"
runtime: 1.5s, gctime: 0.08216s, systime: 0.03201s.
derive_corr_thm mc_calc_d Saved theorem _______ "mc_calc_d_corr_thm"
runtime: 0.27031s, gctime: 0.00403s, systime: 0.00000s.
derive_corr_thm mc_single_mul_add Proof of
(let
r0 = s.regs ' 0;
r1 = s.regs ' 1;
r2 = s.regs ' 2;
r3 = s.regs ' 3
in
0 FDOM s.regs 1 FDOM s.regs 2 FDOM s.regs 3 FDOM s.regs
mc_single_mul_add_pre (r0,r1,r2,r3))
mc_single_mul_add_raw s =
INR
(let
r0 = s.regs ' 0;
r1 = s.regs ' 1;
r2 = s.regs ' 2;
r3 = s.regs ' 3;
(r0,r1,r2,r3) = mc_single_mul_add (r0,r1,r2,r3)
in
delete_vars [4]
(reg_write 0 (SOME r0)
(reg_write 1 (SOME r1)
(reg_write 2 (SOME r2) (reg_write 3 (SOME r3) s)))))
mc_single_mul_add_raw_pre s
failed.
First unsolved sub-goal is
SND
(single_add_word (FST (single_mul (s.regs ' 0) (s.regs ' 2) 0w))
(s.regs ' 1) 0w) = 1w
runtime: 0.63475s, gctime: 0.06191s, systime: 0.02790s.
runtime: 5.8s, gctime: 0.39287s, systime: 0.11995s.
error in quse /scratch/cakeml/regression/cakeml-2813/compiler/backend/proofs/word_bignumProofScript.sml : HOL_ERR {message = "derive_corr_thm failed", origin_function = "failwith", origin_structure = "??", source_location = Loc_Unknown}
error in load /scratch/cakeml/regression/cakeml-2813/compiler/backend/proofs/word_bignumProofScript : HOL_ERR {message = "derive_corr_thm failed", origin_function = "failwith", origin_structure = "??", source_location = Loc_Unknown}
Uncaught exception at /scratch/cakeml/regression/HOL-cf4347f8d871d793c021d04fe2bdc677c7149183/src/prekernel/Feedback.sml:131: HOL_ERR {message = "derive_corr_thm failed", origin_function = "failwith", origin_structure = "??", source_location = Loc_Unknown}
stackPropsTheory compiler/backend/semantics (32m)MKILLED
TextIOProofTheory basis (31m)MKILLED
clos_mtiProofTheory compiler/backend/proofs (17m)MKILLED