CakeML:884d9e5b3e1234942ba3b303cbbecdbb0a795650
Translate word-amount shifts and use them for Word8/Word64 basis shifts
#1500 (var-len-shifts)
Merging into:c377badec962935396e0da1b357dcf943cfb4814
Merge pull request #1499 from CakeML/clean-misc
HOL:dfff742b1f89a43e9c1812a146e9a40d4c4d89fc
Avoid Q.prove in Lib
Machine:timtam
Claimed job
Reusing HOL
Starting developers
Finished developers 50s 1GB
Starting developers/bin
Finished developers/bin 8s 1GB
Starting misc
Finished misc 46s 1GB
Starting compiler/proofs
FAILED: compiler/proofs
HOLORIG=/scratch/cakeml/regression2/cakeml-3543/compiler/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/src/TeX
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)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/ocaml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
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)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/proofs
Scanning $(CAKEMLDIR)/examples/deflate
Scanning $(CAKEMLDIR)/examples/deflate/translation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation/tests
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/translator/monadic/examples
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(HOLDIR)/examples/Crypto/RSA
Scanning $(HOLDIR)/examples/miller/ho_prover
Scanning $(HOLDIR)/examples/miller/subtypes
Scanning $(HOLDIR)/examples/miller/formalize
Scanning $(HOLDIR)/examples/miller/groups
Scanning $(HOLDIR)/examples/probability/legacy
Scanning $(HOLDIR)/examples/miller/prob
Scanning $(HOLDIR)/examples/miller/miller
Scanning $(CAKEMLDIR)/translator/other-examples
Scanning $(CAKEMLDIR)/translator/other-examples/auxiliary
Scanning $(CAKEMLDIR)/tutorial
Scanning $(CAKEMLDIR)/unverified
Scanning $(CAKEMLDIR)/unverified/front-end
Scanning $(CAKEMLDIR)/unverified/hol-light-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/lib
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/tests
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32
Scanning $(candle_overloading)/ml_checker
Scanning $(candle_overloading)/ml_kernel
Scanning $(candle_overloading)/monadic
Scanning $(candle_overloading)/semantics
Scanning $(candle_overloading)/syntax
Scanning $(cnf)/array
Scanning $(cnf)/dist
Scanning $(cnf)/dist/array
Scanning $(cnf)/dist/array/compilation
Scanning $(cnf)/dist/array/compilation/proofs
Scanning $(cnf)/lrup
Scanning $(cnf)/lrup/array
Scanning $(cnf)/lrup/array/compilation
Scanning $(cnf)/lrup/array/compilation/proofs
Scanning $(cnf)/xlrup
Scanning $(cnf)/xlrup/array
Scanning $(cnf)/xlrup/array/compilation
Scanning $(cnf)/xlrup/array/compilation/proofs
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(lpr_checker)/array/compilation/proofsARM8
Scanning $(opentheory)/compilation
Scanning $(opentheory)/compilation/ag32
Scanning $(opentheory)/compilation/ag32/proofs
Scanning $(opentheory)/compilation/proofs
Scanning $(pseudo_bool)/array
Scanning $(pseudo_bool)/array/compilation
Scanning $(pseudo_bool)/array/compilation/proofs
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/cnf_encoding/array
Scanning $(pseudo_bool)/cnf_encoding/array/compilation
Scanning $(pseudo_bool)/cnf_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/cp_encoding
Scanning $(pseudo_bool)/cp_encoding/array
Scanning $(pseudo_bool)/cp_encoding/array/compilation
Scanning $(pseudo_bool)/cp_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/graph_encoding
Scanning $(pseudo_bool)/graph_encoding/array
Scanning $(pseudo_bool)/graph_encoding/array/compilation
Scanning $(pseudo_bool)/graph_encoding/array/compilation/proofs
Scanning $(sat_encodings)/case_studies
Scanning $(sat_encodings)/demo
Scanning $(sat_encodings)/translation
Scanning $(sat_encodings)/translation/compilation
Scanning $(scpog_checker)/array
Scanning $(scpog_checker)/array/compilation
Scanning $(scpog_checker)/array/compilation/proofs
Scanning $(xlrup_checker)/array
Scanning $(xlrup_checker)/array/compilation
Scanning $(xlrup_checker)/array/compilation/proofs
Scanned 302 directories
Building 319 theory files
Starting work on MarshallingTheory
Starting work on mllistTheory
Starting work on mlmapTheory
Starting work on mloptionTheory
mloptionTheory basis/pure (2s) [318] OK
Starting work on mlsetTheory
MarshallingTheory basis (3s) [317] OK
Starting work on db_varsTheory
mllistTheory basis/pure (4s) [316] OK
Starting work on mlstringTheory
mlmapTheory basis/pure (5s) [315] OK
Starting work on mlvectorTheory
mlsetTheory basis/pure (3s) [314] OK
Starting work on gc_sharedTheory
db_varsTheory compiler/backend (2s) [313] OK
Starting work on pattern_commonTheory
mlvectorTheory basis/pure (8s) [312] OK
Starting work on parmoveTheory
pattern_commonTheory compiler/backend/pattern_matching (11s) [311] OK
Starting work on backendPropsTheory
mlstringTheory basis/pure (15s) [310] OK
Starting work on mlintTheory
gc_sharedTheory compiler/backend/gc (15s) [309] OK
Starting work on mlsexpTheory
backendPropsTheory compiler/backend/semantics (4s) [308] OK
Starting work on cfFFITypeTheory
cfFFITypeTheory characteristic (5s) [307] OK
Starting work on backend_commonTheory
mlintTheory basis/pure (8s) [306] OK
Starting work on mlprettyprinterTheory
mlsexpTheory basis/pure (9s) [305] OK
Starting work on mlratTheory
parmoveTheory compiler/backend/reg_alloc (22s) [304] OK
Starting work on jsonLangTheory
mlratTheory basis/pure (4s) [303] OK
Starting work on exportTheory
backend_commonTheory compiler/backend (7s) [302] OK
Starting work on copying_gcTheory
mlprettyprinterTheory basis/pure (9s) [301] OK
Starting work on gen_gcTheory
Finished basis/pure [#theories: 10] (71.230s)
jsonLangTheory compiler/backend (3s) [300] OK
Starting work on displayLangTheory
displayLangTheory compiler/backend (2s) [299] OK
Starting work on ag32Theory
exportTheory compiler/backend (6s) [298] OK
Starting work on export_ag32Theory
copying_gcTheory compiler/backend/gc (15s) [297] OK
Starting work on export_arm7Theory
ag32Theory compiler/encoders/ag32 (10s) [296] OK
Starting work on export_arm8Theory
export_ag32Theory compiler/backend/ag32 (13s) [295] OK
Starting work on export_mipsTheory
export_arm7Theory compiler/backend/arm7 (12s) [294] OK
Starting work on export_riscvTheory
export_arm8Theory compiler/backend/arm8 (12s) [293] OK
Starting work on export_x64Theory
gen_gcTheory compiler/backend/gc (28s) [292] OK
Starting work on gen_gc_partialTheory
export_mipsTheory compiler/backend/mips (12s) [291] OK
Starting work on README.md
README.md compiler/proofs (0s) OK
Starting work on pan_commonTheory
pan_commonTheory pancake (1s) [290] OK
Starting work on panLexerTheory
export_riscvTheory compiler/backend/riscv (12s) [289] OK
Starting work on namespaceTheory
panLexerTheory pancake/parser (8s) [288] OK
Starting work on panPEGTheory
export_x64Theory compiler/backend/x64 (13s) [287] OK
Starting work on tokensTheory
namespaceTheory semantics (2s) [286] OK
Starting work on astTheory
tokensTheory semantics (4s) [285] OK
Starting work on lexer_funTheory
astTheory semantics (6s) [284] OK
Starting work on flatLangTheory
flatLangTheory compiler/backend (4s) [283] OK
Starting work on flat_elimTheory
lexer_funTheory semantics (12s) [282] OK
Starting work on asmTheory
flat_elimTheory compiler/backend (8s) [281] OK
Starting work on typeDecToPPTheory
asmTheory compiler/encoders/asm (12s) [280] OK
Starting work on stackLangTheory
typeDecToPPTheory compiler/printing (10s) [279] OK
Starting work on labLangTheory
labLangTheory compiler/backend (3s) [278] OK
Starting work on lab_filterTheory
stackLangTheory compiler/backend (7s) [277] OK
Starting work on wordLangTheory
lab_filterTheory compiler/backend (3s) [276] OK
Starting work on stack_namesTheory
panPEGTheory pancake/parser (44s) [275] OK
Starting work on stack_removeTheory
wordLangTheory compiler/backend (10s) [274] OK
Starting work on word_bignumTheory
stack_namesTheory compiler/backend (9s) [273] OK
Starting work on word_depthTheory
stack_removeTheory compiler/backend (9s) [272] OK
Starting work on word_cseTheory
word_depthTheory compiler/backend (6s) [271] OK
Starting work on word_instTheory
gen_gc_partialTheory compiler/backend/gc (80s) [270] OK
Starting work on word_removeTheory
word_cseTheory compiler/backend (13s) [269] OK
Starting work on word_simpTheory
word_removeTheory compiler/backend (9s) [268] OK
Starting work on word_unreachTheory
word_unreachTheory compiler/backend (6s) [267] OK
Starting work on word_elimTheory
word_bignumTheory compiler/backend (32s) [266] OK
Starting work on asmSemTheory
word_elimTheory compiler/backend (4s) [265] OK
Starting work on panLangTheory
Finished compiler/printing [#theories: 1] (10.980s)
word_simpTheory compiler/backend (20s) [264] OK
Starting work on fpSemTheory
fpSemTheory semantics (2s) [263] OK
Starting work on closLangTheory
word_instTheory compiler/backend (32s) [262] OK
Starting work on fromSexpTheory
panLangTheory pancake (11s) [261] OK
Starting work on crepLangTheory
asmSemTheory compiler/encoders/asm (13s) [260] OK
Starting work on asmPropsTheory
closLangTheory compiler/backend (5s) [259] OK
Starting work on bviTheory
bviTheory compiler/backend (3s) [258] OK
Starting work on dataLangTheory
crepLangTheory pancake (6s) [257] OK
Starting work on bvi_inlineTheory
dataLangTheory compiler/backend (3s) [256] OK
Starting work on data_liveTheory
data_liveTheory compiler/backend (7s) [255] OK
Starting work on data_simpTheory
asmPropsTheory compiler/encoders/asm (17s) [254] OK
Starting work on data_spaceTheory
data_simpTheory compiler/backend (3s) [253] OK
Starting work on bvi_letTheory
bvi_letTheory compiler/backend (5s) [252] OK
Starting work on bvi_tailrecTheory
data_spaceTheory compiler/backend (7s) [251] OK
Starting work on bvi_to_dataTheory
bvi_inlineTheory compiler/backend (20s) [250] OK
Starting work on bvi_tmcTheory
bvi_tmcTheory compiler/backend (10s) [249] OK
Starting work on bvlTheory
bvlTheory compiler/backend (3s) [248] OK
Starting work on bvl_constTheory
fromSexpTheory compiler/parsing (48s) [247] OK
Starting work on bvl_jumpTheory
bvl_jumpTheory compiler/backend (3s) [246] OK
Starting work on clos_annotateTheory
bvi_to_dataTheory compiler/backend (25s) [245] OK
Starting work on clos_callTheory
clos_annotateTheory compiler/backend (7s) [244] OK
Starting work on clos_fvsTheory
bvi_tailrecTheory compiler/backend (33s) [243] OK
Starting work on clos_letopTheory
clos_fvsTheory compiler/backend (4s) [242] OK
Starting work on clos_opTheory
clos_callTheory compiler/backend (8s) [241] OK
Starting work on clos_ticksTheory
clos_letopTheory compiler/backend (4s) [240] OK
Starting work on clos_mtiTheory
clos_ticksTheory compiler/backend (3s) [239] OK
Starting work on clos_numberTheory
clos_numberTheory compiler/backend (3s) [238] OK
Starting work on clos_interpTheory
clos_mtiTheory compiler/backend (5s) [237] OK
Starting work on ag32_targetTheory
Finished compiler/encoders/asm [#theories: 3] (43.120s)
bvl_constTheory compiler/backend (27s) [236] OK
Starting work on bvl_handleTheory
clos_opTheory compiler/backend (17s) [235] OK
Starting work on clos_knownTheory
ag32_targetTheory compiler/encoders/ag32 (15s) [234] OK
Starting work on arm7_targetTheory
Finished compiler/encoders/ag32 [#theories: 2] (25.530s)
clos_interpTheory compiler/backend (18s) [233] OK
Starting work on flat_to_closTheory
bvl_handleTheory compiler/backend (23s) [232] OK
Starting work on bvl_inlineTheory
flat_to_closTheory compiler/backend (11s) [231] OK
Starting work on arm8_targetTheory
clos_knownTheory compiler/backend (22s) [230] OK
Starting work on clos_to_bvlTheory
arm7_targetTheory compiler/encoders/arm7 (18s) [229] OK
Starting work on arm7_eval_encodeTheory
bvl_inlineTheory compiler/backend (8s) [228] OK
Starting work on bvl_to_bviTheory
arm8_targetTheory compiler/encoders/arm8 (17s) [227] OK
Starting work on mips_targetTheory
Finished compiler/encoders/arm8 [#theories: 1] (17.210s)
mips_targetTheory compiler/encoders/mips (19s) [226] OK
Starting work on riscv_targetTheory
arm7_eval_encodeTheory compiler/encoders/arm7 (41s) [225] OK
Starting work on x64_targetTheory
Finished compiler/encoders/arm7 [#theories: 2] (60.060s)
bvl_to_bviTheory compiler/backend (41s) [224] OK
Starting work on crep_arithTheory
crep_arithTheory pancake (4s) [223] OK
Starting work on crep_inlineTheory
clos_to_bvlTheory compiler/backend (52s) [222] OK
Starting work on loopLangTheory
riscv_targetTheory compiler/encoders/riscv (18s) [221] OK
Starting work on newsTheory
crep_inlineTheory pancake (7s) [220] OK
Starting work on panStaticTheory
newsTheory pancake (2s) [219] OK
Starting work on pan_globalsTheory
loopLangTheory pancake (6s) [218] OK
Starting work on loop_callTheory
x64_targetTheory compiler/encoders/x64 (18s) [217] OK
Starting work on x64_eval_encodeTheory
loop_callTheory pancake (3s) [216] OK
Starting work on loop_liveTheory
pan_globalsTheory pancake (6s) [215] OK
Starting work on loop_to_wordTheory
loop_liveTheory pancake (6s) [214] OK
Starting work on crep_to_loopTheory
loop_to_wordTheory pancake (6s) [213] OK
Starting work on pan_to_crepTheory
panStaticTheory pancake (18s) [212] OK
Starting work on pan_simpTheory
crep_to_loopTheory pancake (7s) [211] OK
Starting work on pan_structsTheory
pan_to_crepTheory pancake (7s) [210] OK
Starting work on panPtreeConversionTheory
x64_eval_encodeTheory compiler/encoders/x64 (16s) [209] OK
Starting work on lexer_implTheory
Finished compiler/encoders/x64 [#theories: 2] (34.360s)
pan_structsTheory pancake (5s) [208] OK
Starting work on gramTheory
pan_simpTheory pancake (8s) [207] OK
Starting work on pan_to_wordTheory
pan_to_wordTheory pancake (3s) [206] OK
Starting work on tokenUtilsTheory
gramTheory semantics (11s) [205] OK
Starting work on ffiTheory
panPtreeConversionTheory pancake/parser (19s) [204] OK
Starting work on gramPropsTheory
Finished pancake/parser [#theories: 3] (72.370s)
tokenUtilsTheory semantics (10s) [203] OK
Starting work on cmlPEGTheory
ffiTheory semantics/ffi (8s) [202] OK
Starting work on cmlPtreeConversionTheory
gramPropsTheory semantics/proofs (12s) [201] OK
Starting work on lab_to_targetTheory
Finished semantics/ffi [#theories: 1] (8.700s)
lexer_implTheory compiler/parsing (40s) [200] OK
Starting work on wordSemTheory
lab_to_targetTheory compiler/backend (12s) [199] OK
Starting work on semanticPrimitivesTheory
cmlPtreeConversionTheory semantics (26s) [198] OK
Starting work on cmlNTPropsTheory
cmlNTPropsTheory compiler/parsing/proofs (16s) [197] OK
Starting work on namespacePropsTheory
semanticPrimitivesTheory semantics (25s) [196] OK
Starting work on pattern_semanticsTheory
Finished compiler/encoders/mips [#theories: 1] (19.410s)
namespacePropsTheory semantics/proofs (6s) [195] OK
Starting work on evaluateTheory
Finished compiler/encoders/riscv [#theories: 1] (18.380s)
evaluateTheory semantics (6s) [194] OK
Starting work on source_letTheory
pattern_semanticsTheory compiler/backend/pattern_matching (14s) [193] OK
Starting work on pattern_exhTheory
source_letTheory compiler/backend (4s) [192] OK
Starting work on source_to_sourceTheory
source_to_sourceTheory compiler/backend (2s) [191] OK
Starting work on typeSystemTheory
wordSemTheory compiler/backend/semantics (51s) [190] OK
Starting work on stackSemTheory
cmlPEGTheory compiler/parsing (84s) [189] OK
Starting work on cmlParseTheory
pattern_exhTheory compiler/backend/pattern_matching (19s) [188] OK
Starting work on pattern_compTheory
typeSystemTheory semantics (15s) [187] OK
Starting work on pegSoundTheory
cmlParseTheory compiler/parsing (11s) [186] OK
Starting work on infer_tTheory
Finished compiler/parsing [#theories: 4] (185.190s)
stackSemTheory compiler/backend/semantics (27s) [185] OK
Starting work on stackPropsTheory
pattern_compTheory compiler/backend/pattern_matching (16s) [184] OK
Starting work on flat_patternTheory
Finished compiler/backend/pattern_matching [#theories: 4] (61.570s)
infer_tTheory compiler/inference (14s) [183] OK
Starting work on unifyTheory
flat_patternTheory compiler/backend (8s) [182] OK
Starting work on source_to_flatTheory
source_to_flatTheory compiler/backend (12s) [181] OK
Starting work on presLangTheory
unifyTheory compiler/inference (30s) [180] OK
Starting work on primTypesTheory
primTypesTheory semantics (2s) [179] OK
Starting work on semanticsTheory
pegSoundTheory compiler/parsing/proofs (57s) [178] OK
Starting work on pegCompleteTheory
semanticsTheory semantics (5s) [177] OK
Starting work on semanticPrimitivesPropsTheory
Finished semantics [#theories: 13] (131.770s)
presLangTheory compiler/backend (30s) [176] OK
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory semantics/proofs (5s) [175] OK
Starting work on ml_monadBaseTheory
semanticPrimitivesPropsTheory semantics/proofs (27s) [174] OK
Starting work on closSemTheory
ml_monadBaseTheory translator/monadic/monad_base (18s) [173] OK
Starting work on flatSemTheory
stackPropsTheory compiler/backend/semantics (82s) [172] OK
Starting work on stack_namesProofTheory
flatSemTheory compiler/backend/semantics (19s) [171] OK
Starting work on evaluatePropsTheory
closSemTheory compiler/backend/semantics (29s) [170] OK
Starting work on clos_constantProofTheory
stack_namesProofTheory compiler/backend/proofs (34s) [169] OK
Starting work on bvlSemTheory
clos_constantProofTheory compiler/backend/proofs (16s) [168] OK
Starting work on closPropsTheory
pegCompleteTheory compiler/parsing/proofs (90s) [167] OK
Starting work on parserProofTheory
bvlSemTheory compiler/backend/semantics (17s) [166] OK
Starting work on bviSemTheory
parserProofTheory compiler/parsing/proofs (15s) [165] OK
Starting work on bvlPropsTheory
bviSemTheory compiler/backend/semantics (19s) [164] OK
Starting work on typeSysPropsTheory
Finished compiler/parsing/proofs [#theories: 4] (179.540s)
evaluatePropsTheory semantics/proofs (66s) [163] OK
Starting work on source_evalProofTheory
typeSysPropsTheory semantics/proofs (14s) [162] OK
Starting work on flatPropsTheory
bvlPropsTheory compiler/backend/semantics (50s) [161] OK
Starting work on bvl_constProofTheory
flatPropsTheory compiler/backend/semantics (38s) [160] OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory compiler/backend/proofs (4s) [159] OK
Starting work on bviPropsTheory
bvl_constProofTheory compiler/backend/proofs (25s) [158] OK
Starting work on bvl_handleProofTheory
closPropsTheory compiler/backend/semantics(104s) [157] OK
Starting work on clos_annotateProofTheory
source_evalProofTheory compiler/backend/proofs (67s) [156] OK
Starting work on clos_callProofTheory
bvl_handleProofTheory compiler/backend/proofs (16s) [155] OK
Starting work on bvl_inlineProofTheory
clos_annotateProofTheory compiler/backend/proofs (21s) [154] OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory compiler/backend/proofs (13s) [153] OK
Starting work on clos_interpProofTheory
bvl_inlineProofTheory compiler/backend/proofs (20s) [152] OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory compiler/backend/proofs (5s) [151] OK
Starting work on clos_letopProofTheory
clos_letopProofTheory compiler/backend/proofs (15s) [150] OK
Starting work on clos_opProofTheory
clos_interpProofTheory compiler/backend/proofs (28s) [149] OK
Starting work on clos_ticksProofTheory
bviPropsTheory compiler/backend/semantics (80s) [148] OK
Starting work on clos_mtiProofTheory
clos_opProofTheory compiler/backend/proofs (17s) [147] OK
Starting work on clos_numberProofTheory
clos_ticksProofTheory compiler/backend/proofs (19s) [146] OK
Starting work on clos_knownProofTheory
clos_mtiProofTheory compiler/backend/proofs (25s) [145] OK
Starting work on source_letProofTheory
clos_numberProofTheory compiler/backend/proofs (16s) [144] OK
Starting work on bvi_inlineProofTheory
source_letProofTheory compiler/backend/proofs (9s) [143] OK
Starting work on bvi_tailrecProofTheory
clos_callProofTheory compiler/backend/proofs(116s) [142] OK
Starting work on bvi_tmcProofTheory
bvi_inlineProofTheory compiler/backend/proofs (39s) [141] OK
Starting work on bvi_letProofTheory
bvi_letProofTheory compiler/backend/proofs (9s) [140] OK
Starting work on source_to_sourceProofTheory
source_to_sourceProofTheory compiler/backend/proofs (4s) [139] OK
Starting work on flat_patternProofTheory
flat_patternProofTheory compiler/backend/proofs (27s) [138] OK
Starting work on flat_to_closProofTheory
clos_knownProofTheory compiler/backend/proofs (93s) [137] OK
Starting work on clos_to_bvlProofTheory
bvi_tmcProofTheory compiler/backend/proofs(112s) [136] OK
Starting work on flat_elimProofTheory
bvi_tailrecProofTheory compiler/backend/proofs(137s) [135] OK
Starting work on bvl_to_bviProofTheory
flat_to_closProofTheory compiler/backend/proofs (84s) [134] OK
Starting work on targetSemTheory
flat_elimProofTheory compiler/backend/proofs (26s) [133] OK
Starting work on source_to_flatProofTheory
targetSemTheory compiler/backend/semantics (10s) [132] OK
Starting work on labSemTheory
labSemTheory compiler/backend/semantics (17s) [131] OK
Starting work on targetPropsTheory
clos_to_bvlProofTheory compiler/backend/proofs(135s) [130] OK
Starting work on primSemEnvTheory
primSemEnvTheory semantics/proofs (8s) [129] OK
Starting work on weakeningTheory
targetPropsTheory compiler/backend/semantics (30s) [128] OK
Starting work on evaluate_decTheory
weakeningTheory semantics/proofs (7s) [127] OK
Starting work on typeSoundTheory
evaluate_decTheory translator (7s) [126] OK
Starting work on ml_progTheory
ml_progTheory translator (12s) [125] OK
Starting work on cfHeapsBaseTheory
source_to_flatProofTheory compiler/backend/proofs (84s) [124] OK
Starting work on ml_translatorTheory
cfHeapsBaseTheory characteristic (16s) [123] OK
Starting work on clFFITheory
clFFITheory basis (6s) [122] OK
Starting work on runtimeFFITheory
runtimeFFITheory basis (5s) [121] OK
Starting work on fsFFITheory
fsFFITheory basis (10s) [120] OK
Starting work on fsFFIPropsTheory
ml_translatorTheory translator (42s) [119] OK
Starting work on ml_optimiseTheory
bvl_to_bviProofTheory compiler/backend/proofs(162s) [118] OK
Starting work on ml_pmatchTheory
ml_optimiseTheory translator (13s) [117] OK
Starting work on inferTheory
typeSoundTheory semantics/proofs (87s) [116] OK
Starting work on semanticsPropsTheory
ml_pmatchTheory translator (13s) [115] OK
Starting work on cfHeapsTheory
semanticsPropsTheory semantics/proofs (7s) [114] OK
Starting work on stack_removeProofTheory
Finished semantics/proofs [#theories: 10] (244.610s)
fsFFIPropsTheory basis (42s) [113] OK
Starting work on labPropsTheory
cfHeapsTheory characteristic (14s) [112] OK
Starting work on cfStoreTheory
cfStoreTheory characteristic (18s) [111] OK
Starting work on cfNormaliseTheory
inferTheory compiler/inference (56s) [110] OK
Starting work on inferPropsTheory
cfNormaliseTheory characteristic (15s) [109] OK
Starting work on cfAppTheory
cfAppTheory characteristic (22s) [108] OK
Starting work on cfTheory
inferPropsTheory compiler/inference (54s) [107] OK
Starting work on envRelTheory
Finished compiler/inference [#theories: 4] (156.640s)
labPropsTheory compiler/backend/semantics(101s) [106] OK
Starting work on lab_filterProofTheory
envRelTheory compiler/inference/proofs (26s) [105] OK
Starting work on infer_eCompleteTheory
cfTheory characteristic (76s) [104] OK
Starting work on cfTacticsTheory
cfTacticsTheory characteristic (14s) [103] OK
Starting work on xcfTheory
infer_eCompleteTheory compiler/inference/proofs (40s) [102] OK
Starting work on infer_eSoundTheory
lab_filterProofTheory compiler/backend/proofs (55s) [101] OK
Starting work on type_dCanonTheory
xcfTheory characteristic (5s) [100] OK
Starting work on cfLetAutoTheory
cfLetAutoTheory characteristic (22s) [99] OK
Starting work on cfMainTheory
infer_eSoundTheory compiler/inference/proofs (34s) [98] OK
Starting work on type_eDetermTheory
type_dCanonTheory compiler/inference/proofs (31s) [97] OK
Starting work on std_preludeTheory
cfMainTheory characteristic (19s) [96] OK
Starting work on ml_monad_translatorBaseTheory
std_preludeTheory translator (16s) [95] OK
Starting work on cfDivTheory
Finished translator [#theories: 6] (104.560s)
type_eDetermTheory compiler/inference/proofs (16s) [94] OK
Starting work on inferCompleteTheory
stack_removeProofTheory compiler/backend/proofs(233s) [93] OK
Starting work on lab_to_targetProofTheory
ml_monad_translatorBaseTheory translator/monadic (23s) [92] OK
Starting work on inferSoundTheory
inferCompleteTheory compiler/inference/proofs (23s) [91] OK
Starting work on ml_monad_translatorTheory
inferSoundTheory compiler/inference/proofs (21s) [90] OK
Starting work on reg_allocTheory
Finished compiler/inference/proofs [#theories: 7] (194.710s)
Finished translator/monadic/monad_base [#theories: 1] (18.110s)
ml_monad_translatorTheory translator/monadic (42s) [89] OK
Starting work on cfMonadTheory
reg_allocTheory compiler/backend/reg_alloc (39s) [88] OK
Starting work on word_copyTheory
cfMonadTheory translator/monadic (21s) [87] OK
Starting work on linear_scanTheory
word_copyTheory compiler/backend (7s) [86] OK
Starting work on reg_allocProofTheory
cfDivTheory characteristic(104s) [85] OK
Starting work on RuntimeProgTheory
Finished characteristic [#theories: 12] (335.540s)
RuntimeProgTheory basis (24s) [84] OK
Starting work on OptionProgTheory
linear_scanTheory compiler/backend/reg_alloc (35s) [83] OK
Starting work on RuntimeProofTheory
OptionProgTheory basis (11s) [82] OK
Starting work on ListProgTheory
reg_allocProofTheory compiler/backend/reg_alloc/proofs (54s) [81] OK
Starting work on word_allocTheory
Finished compiler/backend/reg_alloc [#theories: 3] (98.110s)
RuntimeProofTheory basis (25s) [80] OK
Starting work on linear_scanProofTheory
ListProgTheory basis (43s) [79] OK
Starting work on VectorProgTheory
VectorProgTheory basis (32s) [78] OK
Starting work on StringProgTheory
word_allocTheory compiler/backend(100s) [77] OK
Starting work on ListProofTheory
StringProgTheory basis (37s) [76] OK
Starting work on mlbasicsProgTheory
linear_scanProofTheory compiler/backend/reg_alloc/proofs(115s) [75] OK
Starting work on word_to_wordTheory
word_to_wordTheory compiler/backend (5s) [74] OK
Starting work on data_to_wordTheory
ListProofTheory basis (24s) [73] OK
Starting work on word_to_stackTheory
word_to_stackTheory compiler/backend (18s) [72] OK
Starting work on wordConvsTheory
Finished compiler/backend/reg_alloc/proofs [#theories: 2] (170.030s)
mlbasicsProgTheory basis (36s) [71] OK
Starting work on IntProgTheory
wordConvsTheory compiler/backend/semantics (29s) [70] OK
Starting work on wordConvsProofTheory
IntProgTheory basis (34s) [69] OK
Starting work on PrettyPrinterProgTheory
data_to_wordTheory compiler/backend (66s) [68] OK
Starting work on stack_allocTheory
PrettyPrinterProgTheory basis (24s) [67] OK
Starting work on RatProgTheory
stack_allocTheory compiler/backend (26s) [66] OK
Starting work on stack_rawcallTheory
RatProgTheory basis (42s) [65] OK
Starting work on CharProgTheory
stack_rawcallTheory compiler/backend (40s) [64] OK
Starting work on stack_to_labTheory
wordConvsProofTheory compiler/backend/proofs(105s) [63] OK
Starting work on gc_combinedTheory
CharProgTheory basis (32s) [62] OK
Starting work on Word64ProgTheory
stack_to_labTheory compiler/backend (28s) [61] OK
Starting work on backendTheory
gc_combinedTheory compiler/backend/gc (15s) [60] OK
Starting work on stack_rawcallProofTheory
Finished compiler/backend/gc [#theories: 5] (156.560s)
backendTheory compiler/backend (23s) [59] OK
Starting work on backend_passesTheory
Word64ProgTheory basis (33s) [58] OK
Starting work on Word8ProgTheory
backend_passesTheory compiler/backend (20s) [57] OK
Starting work on ag32_configTheory
Finished compiler/backend [#theories: 66] (1011.150s)
Word8ProgTheory basis (33s) [56] OK
Starting work on Word8ArrayProgTheory
stack_rawcallProofTheory compiler/backend/proofs (58s) [55] OK
Starting work on arm7_configTheory
ag32_configTheory compiler/backend/ag32 (21s) [54] OK
Starting work on arm8_configTheory
Finished compiler/backend/ag32 [#theories: 2] (34.830s)
arm7_configTheory compiler/backend/arm7 (23s) [53] OK
Starting work on mips_configTheory
Finished compiler/backend/arm7 [#theories: 2] (36.400s)
arm8_configTheory compiler/backend/arm8 (23s) [52] OK
Starting work on riscv_configTheory
Finished compiler/backend/arm8 [#theories: 2] (35.680s)
Word8ArrayProgTheory basis (32s) [51] OK
Starting work on ArrayProgTheory
mips_configTheory compiler/backend/mips (25s) [50] OK
Starting work on Word8ArrayProofTheory
riscv_configTheory compiler/backend/riscv (25s) [49] OK
Starting work on dataSemTheory
Finished compiler/backend/mips [#theories: 2] (37.710s)
Finished compiler/backend/riscv [#theories: 2] (37.810s)
Word8ArrayProofTheory basis (35s) [48] OK
Starting work on wordPropsTheory
lab_to_targetProofTheory compiler/backend/proofs(607s) [47] OK
Starting work on x64_configTheory
x64_configTheory compiler/backend/x64 (24s) [46] OK
Starting work on pan_to_targetTheory
Finished compiler/backend/x64 [#theories: 2] (37.620s)
ArrayProgTheory basis (90s) [45] OK
Starting work on ArrayProofTheory
pan_to_targetTheory pancake (10s) [44] OK
Starting work on MapProgTheory
dataSemTheory compiler/backend/semantics (73s) [43] OK
Starting work on dataPropsTheory
ArrayProofTheory basis (52s) [42] OK
Starting work on pan_passesTheory
MapProgTheory basis (58s) [41] OK
Starting work on SetProgTheory
pan_passesTheory pancake (22s) [40] OK
Finished pancake [#theories: 19] (148.540s)
Finished translator/monadic [#theories: 3] (87.200s)
SetProgTheory basis (56s) [39] OK
Starting work on HashtableProgTheory
wordPropsTheory compiler/backend/semantics(205s) [38] OK
Starting work on word_simpProofTheory
Starting work on word_bignumProofTheory
HashtableProgTheory basis (66s) [37] OK
Starting work on CommandLineProgTheory
word_simpProofTheory compiler/backend/proofs (56s) [36] OK
Starting work on word_gcFunctionsTheory
CommandLineProgTheory basis (47s) [35] OK
Starting work on CommandLineProofTheory
word_gcFunctionsTheory compiler/backend/proofs (19s) [34] OK
Starting work on DoubleProgTheory
CommandLineProofTheory basis (51s) [33] OK
Starting work on word_depthProofTheory
word_bignumProofTheory compiler/backend/proofs(126s) [32] OK
Starting work on word_allocProofTheory
DoubleProgTheory basis (81s) [31] OK
Starting work on MarshallingProgTheory
MarshallingProgTheory basis (49s) [30] OK
Starting work on TextIOProgTheory
word_depthProofTheory compiler/backend/proofs(144s) [29] OK
Starting work on word_copyProofTheory
word_copyProofTheory compiler/backend/proofs (27s) [28] OK
Starting work on word_cseProofTheory
dataPropsTheory compiler/backend/semantics(533s) [27] OK
Starting work on word_elimProofTheory
TextIOProgTheory basis(187s) [26] OK
Starting work on TextIOProofTheory
word_elimProofTheory compiler/backend/proofs (57s) [25] OK
Starting work on word_instProofTheory
word_cseProofTheory compiler/backend/proofs(152s) [24] OK
Starting work on word_removeProofTheory
word_removeProofTheory compiler/backend/proofs (13s) [23] OK
Starting work on word_unreachProofTheory
word_unreachProofTheory compiler/backend/proofs (7s) [22] OK
Starting work on stack_allocProofTheory
word_instProofTheory compiler/backend/proofs (50s) [21] OK
Starting work on word_to_stackProofTheory
word_allocProofTheory compiler/backend/proofs(497s) [20] OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory compiler/backend/proofs (73s) [19] OK
Starting work on data_liveProofTheory
Finished compiler/backend/semantics [#theories: 20] (1529.030s)
data_liveProofTheory compiler/backend/proofs (73s) [18] OK
Starting work on data_simpProofTheory
data_simpProofTheory compiler/backend/proofs (10s) [17] OK
Starting work on data_spaceProofTheory
TextIOProofTheory basis(380s) [16] OK
Starting work on SexpProgTheory
data_spaceProofTheory compiler/backend/proofs (20s) [15] OK
Starting work on basis_ffiTheory
basis_ffiTheory basis (77s) [14] OK
Starting work on bvi_to_dataProofTheory
stack_allocProofTheory compiler/backend/proofs(426s) [13] OK
Starting work on data_to_word_memoryProofTheory
SexpProgTheory basis(119s) [12] OK
Starting work on basisProgTheory
basisProgTheory basis (61s) [11] OK
Starting work on basis-heap
bvi_to_dataProofTheory compiler/backend/proofs (96s) [10] OK
basis-heap basis(111s) OK
Finished basis [#theories: 35] (2068.550s)
Starting work on compilerTheory
compilerTheory compiler (53s) [9] OK
Finished compiler [#theories: 1] (53.240s)
word_to_stackProofTheory compiler/backend/proofs(776s) [8] OK
data_to_word_memoryProofTheory compiler/backend/proofs(614s) [7] OK
Starting work on data_to_word_gcProofTheory
data_to_word_gcProofTheory compiler/backend/proofs(195s) [6] OK
Starting work on data_to_word_bignumProofTheory
Starting work on stack_to_labProofTheory
data_to_word_bignumProofTheory compiler/backend/proofs(135s) [5] OK
Starting work on data_to_word_assignProofTheory
stack_to_labProofTheory compiler/backend/proofs(333s) [4] OK
data_to_word_assignProofTheory compiler/backend/proofs(445s) FAIL<1>
*** Holmake aborted - 1 target failed:
*** data_to_word_assignProofTheory in $(CAKEMLDIR)/compiler/backend/proofs (status 1)
Saved theorem _______ "assign_WordOpW8"
Saved theorem _______ "mw2n_2_IMP"
Saved theorem _______ "IMP_mw2n_2"
Saved theorem _______ "evaluate_WordOp64_on_32"
Saved theorem _______ "IMP_encode_header_NOT_NONE"
Saved theorem _______ "assign_WordOpW64"
Saved theorem _______ "assign_WordShiftW8"
Saved theorem _______ "evaluate_WordShift64_on_32"
Saved theorem _______ "assign_WordShiftW64"
Saved theorem _______ "Smallnum_w2n_word8"
Saved theorem _______ "word8_shift_MIN"
Saved theorem _______ "word64_shift_sat"
Saved theorem _______ "word64_halves_w2n"
Saved theorem _______ "word_exp_ShiftW8"
Saved theorem _______ "shift64_on_32"
Saved theorem _______ "w2w_shift_lookup"
Proved triviality ___ "insert_Word_eq"
Saved theorem _______ "evaluate_WordShiftVar64"
Proved triviality ___ "lo_and_63"
Proved triviality ___ "evaluate_WordShiftVar64_on_32_count"
Proved triviality ___ "evaluate_WordShiftVar64_on_32_step"
Saved theorem _______ "evaluate_WordShiftVar64_on_32"
Saved theorem _______ "evaluate_clamp_W8"
Saved theorem _______ "assign_WordShiftVarW8"
Proved triviality ___ "inter_adjust_set_EVEN"
Saved theorem _______ "assign_WordShiftVarW64"
Saved theorem _______ "w2w_select_id"
Saved theorem _______ "extract_append_id"
Saved theorem _______ "word1_cases"
Saved theorem _______ "w2w_w2w_64"
Proved triviality ___ "fp_greater"
Saved theorem _______ "assign_FP_cmp"
Saved theorem _______ "assign_FP_top"
Saved theorem _______ "assign_FP_bop"
Saved theorem _______ "assign_FP_uop"
Saved theorem _______ "assign_Label"
Saved theorem _______ "do_app_Ref"
Saved theorem _______ "assign_Ref"
Saved theorem _______ "assign_Update"
Saved theorem _______ "assign_El"
Saved theorem _______ "assign_ElemAt"
Saved theorem _______ "assign_UpdateByte"
Saved theorem _______ "assign_DerefByte"
Saved theorem _______ "get_real_bit_offset_lemma"
Proved triviality ___ "b2w_index"
/scratch/cakeml/regression2/cakeml-3543/compiler/backend/proofs/data_to_word_assignProofScript.sml:15642: error: Value or constructor (MULT_DIV_MULT_LEMMA) has not been declared in structure miscTheory
Found near [miscTheory.MULT_DIV_MULT_LEMMA]
error in quse /scratch/cakeml/regression2/cakeml-3543/compiler/backend/proofs/data_to_word_assignProofScript.sml : Fail "Static Errors"
error in load /scratch/cakeml/regression2/cakeml-3543/compiler/backend/proofs/data_to_word_assignProofScript : Fail "Static Errors"
Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
Full log: /scratch/cakeml/regression2/cakeml-3543/compiler/backend/proofs/.hol/logs/data_to_word_assignProofTheory