CakeML:0707cf969893c98e748c2a3f3b16bf3308b59193
Fix a proof that refers to translator-generated name
#1300 (vname)
Merging into:1516f558501b58a9bff7891a1d62f24e3fbaf45a
Convert process_topdecs patterns to Quote syntax (#1294)
HOL:f02a261b181e0408a16745877f3feb8f1b8c1cb6
Modernise syntax in milawa_proofp
Machine:pavlova
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 202MB
Starting developers/bin
Finished developers/bin 4s 91MB
Starting misc
Finished misc 38s 1GB
Starting compiler/proofs
Finished compiler/proofs 1h01m29s 12GB
Starting compiler/bootstrap/compilation/x64/64/proofs
FAILED: compiler/bootstrap/compilation/x64/64/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)/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)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
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 $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/prover
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/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 $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
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/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/serialiser
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanned 111 directories
Starting work on basis_cvTheory
Starting work on ml_monadStoreTheory
Starting work on holSyntaxLibTheory
Starting work on ast_extrasTheory
basis_cvTheory basis/pure (10s) OK
Finished $(CAKEMLDIR)/basis/pure [#theories: 1] (10.630s)
Finished $(CAKEMLDIR)/unverified/reg_alloc (0.000s)
Finished $(CAKEMLDIR)/compiler/backend/reg_alloc (0.000s)
Starting work on x64_targetProofTheory
ast_extrasTheory candle/prover (12s) OK
Starting work on permsTheory
holSyntaxLibTheory candle/syntax-lib (12s) OK
Finished $(CAKEMLDIR)/candle/syntax-lib [#theories: 1] (12.460s)
Starting work on holSyntaxTheory
ml_monadStoreTheory translator/monadic (19s) OK
Finished $(CAKEMLDIR)/translator/monadic [#theories: 1] (19.820s)
Starting work on unify_cvTheory
holSyntaxTheory candle/standard/syntax (20s) OK
Starting work on holSyntaxExtraTheory
unify_cvTheory compiler/inference (16s) OK
Starting work on infer_cvTheory
permsTheory candle/prover (49s) OK
Starting work on num_list_enc_decTheory
holSyntaxExtraTheory candle/standard/syntax (36s) OK
Starting work on holBoolSyntaxTheory
num_list_enc_decTheory compiler/backend/serialiser (21s) OK
Starting work on holKernelTheory
infer_cvTheory compiler/inference (58s) OK
Finished $(CAKEMLDIR)/compiler/inference [#theories: 2] (75.110s)
Starting work on num_tree_enc_decTheory
holBoolSyntaxTheory candle/standard/syntax (28s) OK
Starting work on holAxiomsSyntaxTheory
num_tree_enc_decTheory compiler/backend/serialiser (16s) OK
Starting work on backend_enc_decTheory
holKernelTheory candle/standard/monadic (31s) OK
Starting work on holKernelPmatchTheory
holAxiomsSyntaxTheory candle/standard/syntax (17s) OK
Finished $(CAKEMLDIR)/candle/standard/syntax [#theories: 4] (101.810s)
Starting work on holKernelProofTheory
holKernelPmatchTheory candle/standard/monadic (20s) OK
Starting work on runtime_checkTheory
runtime_checkTheory candle/standard/ml_kernel (17s) OK
Starting work on ml_hol_kernel_funsProgTheory
holKernelProofTheory candle/standard/monadic (53s) OK
Finished $(CAKEMLDIR)/candle/standard/monadic [#theories: 3] (105.400s)
Starting work on print_thmTheory
backend_enc_decTheory compiler/backend/serialiser (58s) OK
Starting work on compute_syntaxTheory
print_thmTheory candle/standard/ml_kernel (14s) OK
Finished $(CAKEMLDIR)/compiler/backend/serialiser [#theories: 3] (96.650s)
Starting work on monadic_encTheory
compute_syntaxTheory candle/prover/compute (23s) OK
Starting work on compute_evalTheory
monadic_encTheory compiler/encoders/monadic_enc (12s) OK
Starting work on compute_syntaxProofTheory
compute_evalTheory candle/prover/compute (19s) OK
Starting work on compute_execTheory
compute_execTheory candle/prover/compute (17s) OK
Starting work on computeTheory
computeTheory candle/prover/compute (16s) OK
Starting work on compute_pmatchTheory
compute_pmatchTheory candle/prover/compute (18s) OK
Starting work on monadic_enc64Theory
compute_syntaxProofTheory candle/prover/compute (87s) OK
Starting work on compute_evalProofTheory
monadic_enc64Theory compiler/encoders/monadic_enc (15s) OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 2] (27.970s)
Starting work on caml_lexTheory
compute_evalProofTheory candle/prover/compute (71s) OK
Starting work on compute_execProofTheory
ml_hol_kernel_funsProgTheory candle/standard/ml_kernel(209s) OK
Finished $(CAKEMLDIR)/candle/standard/ml_kernel [#theories: 3] (240.970s)
Starting work on candle_kernelProgTheory
compute_execProofTheory candle/prover/compute (14s) OK
Starting work on computeProofTheory
computeProofTheory candle/prover/compute (42s) OK
Finished $(CAKEMLDIR)/candle/prover/compute [#theories: 9] (310.960s)
Starting work on addPrintValsTheory
addPrintValsTheory compiler/printing (12s) OK
Starting work on addTypePPTheory
addTypePPTheory compiler/printing (7s) OK
Starting work on printTweaksTheory
caml_lexTheory compiler/parsing/ocaml(141s) OK
Starting work on camlPEGTheory
printTweaksTheory compiler/printing (10s) OK
Finished $(CAKEMLDIR)/compiler/printing [#theories: 3] (29.530s)
Starting work on evaluate_skipTheory
candle_kernelProgTheory candle/prover(131s) OK
Starting work on candle_kernel_valsTheory
evaluate_skipTheory compiler/repl (97s) OK
Starting work on evaluate_initTheory
camlPEGTheory compiler/parsing/ocaml(107s) OK
Starting work on camlPtreeConversionTheory
x64_targetProofTheory compiler/encoders/x64/proofs(557s) OK
Finished $(CAKEMLDIR)/compiler/encoders/x64/proofs [#theories: 1] (557.160s)
Starting work on x64_configProofTheory
candle_kernel_valsTheory candle/prover (91s) OK
Starting work on candle_prover_invTheory
x64_configProofTheory compiler/backend/x64/proofs (29s) OK
Finished $(CAKEMLDIR)/compiler/backend/x64/proofs [#theories: 1] (29.980s)
Starting work on repl_moduleProgTheory
camlPtreeConversionTheory compiler/parsing/ocaml (53s) OK
Starting work on caml_parserTheory
candle_prover_invTheory candle/prover (30s) OK
Starting work on candle_kernel_permsTheory
caml_parserTheory compiler/parsing/ocaml (14s) OK
Finished $(CAKEMLDIR)/compiler/parsing/ocaml [#theories: 4] (317.790s)
Starting work on repl_decs_allowedTheory
evaluate_initTheory compiler/repl (96s) OK
Starting work on backend_asmTheory
repl_decs_allowedTheory compiler/repl (26s) OK
Starting work on repl_check_and_tweakTheory
backend_asmTheory compiler/backend/cv_compute (24s) OK
Starting work on backend_arm8Theory
backend_arm8Theory compiler/backend/cv_compute (18s) OK
Starting work on backend_x64Theory
repl_moduleProgTheory compiler/repl (94s) OK
Starting work on repl_init_envProgTheory
backend_x64Theory compiler/backend/cv_compute (19s) OK
Finished $(CAKEMLDIR)/compiler/backend/cv_compute [#theories: 3] (63.090s)
Starting work on to_data_cvTheory
repl_check_and_tweakTheory compiler/repl (44s) OK
Starting work on repl_init_typesTheory
repl_init_envProgTheory compiler/repl (48s) OK
Starting work on repl_typesTheory
candle_kernel_permsTheory candle/prover(147s) OK
Starting work on candle_kernel_funsTheory
repl_init_typesTheory compiler/repl (67s) OK
Starting work on decProgTheory
repl_typesTheory compiler/repl (71s) OK
Starting work on repl_initTheory
candle_kernel_funsTheory candle/prover (68s) OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory candle/prover (69s) OK
Starting work on candle_basis_evaluateTheory
repl_initTheory compiler/repl (95s) OK
Finished $(CAKEMLDIR)/compiler/repl [#theories: 9] (642.280s)
Starting work on README.md
README.md compiler/bootstrap/compilation/x64/64/proofs (0s) OK
decProgTheory compiler/bootstrap/translation(157s) OK
Starting work on to_flatProgTheory
candle_basis_evaluateTheory candle/prover (40s) OK
Starting work on candle_prover_semanticsTheory
candle_prover_semanticsTheory candle/prover(100s) OK
Finished $(CAKEMLDIR)/candle/prover [#theories: 10] (741.370s)
to_data_cvTheory cv_translator(406s) OK
Starting work on backend_cvTheory
to_flatProgTheory compiler/bootstrap/translation(304s) OK
Starting work on to_closProgTheory
backend_cvTheory cv_translator(213s) OK
Starting work on backend_64_cvTheory
backend_64_cvTheory cv_translator(179s) OK
Starting work on backend_arm8_cvTheory
Starting work on backend_x64_cvTheory
backend_x64_cvTheory cv_translator(138s) OK
to_closProgTheory compiler/bootstrap/translation(417s) OK
Starting work on to_bvlProgTheory
backend_arm8_cvTheory cv_translator(154s) OK
Starting work on cake_compile_heap
cake_compile_heap cv_translator (71s) OK
Finished $(CAKEMLDIR)/cv_translator [#theories: 5] (1163.140s)
to_bvlProgTheory compiler/bootstrap/translation(100s)FAIL<1>
Saved theorem _______ "bvl_jump_jumplist_side_def"
Saved definition ____ "bvl_jump_jumplist_ind_def"
ERROR: Unable to prove induction for bvl_jumpTheory.JumpList_def.
This induction goal has been left as an assumption on
the theorem returned by the translator. You can prove
it with something like the following before JumpList
is used in subsequent translations.
val res = translate_no_ind bvl_jumpTheory.JumpList_def;
Theorem bvl_jump_jumplist_ind[local]:
bvl_jump_jumplist_ind
Proof
once_rewrite_tac [fetch "-" "bvl_jump_jumplist_ind_def"]
\\ rpt gen_tac
\\ rpt (disch_then strip_assume_tac)
\\ match_mp_tac (latest_ind ())
\\ rpt strip_tac
\\ last_x_assum match_mp_tac
\\ rpt strip_tac
\\ gvs [FORALL_PROD]
QED
val _ = bvl_jump_jumplist_ind |> update_precondition;
Here `translate_no_ind` does the same as `translate`
except it does not attempt the induction proof.
Saved theorem _______ "nsLookup_to_bvlProg_env_7_pfun_eqs"
Adding nsLookup representation thms for [to_bvlProg_env_6]
Adding nsLookup representation thms for [to_bvlProg_env_7]
WARNING: bvl_jump_jumplist has a precondition.
Saved theorem _______ "bvl_jump_jumplist_v_thm"
Proved triviality ___ "bvl_jump_jumplist_ind"
Updating bvl_jump_jumplist_v_thm
Saved theorem _______ "bvl_jump_jumplist_v_thm"
Proof of
a b. bvl_jump_jumplist_side a b T
failed.
Exception raised at Q.prove:
at BasicProvers.Cases_on:
at BasicProvers.find_subterm:
No var with name "x1" free in goal, or in outer universal quantifiers
Full log: /scratch/cakeml/regression/cakeml-3117/compiler/bootstrap/translation/.hol/logs/to_bvlProgTheory