OverviewCakeML:1966a12a9c6027c9f1a08795c8f6ab1a8ef82e8a
Pancake 16bit ShMem: compiler/backend updates for hw_offset & ag32
#1212 (16bit)
Merging into:73ba86109b0d5d28a6f514d796811288728f4cc5
Merge pull request #1214 from CakeML/theory-syntax
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
Change bossLib.oneline to preserve input hypotheses as hypotheses
Machine:lammmington
Claimed job
Reusing HOL
Starting developers
Finished developers 3s 175MB
Starting developers/bin
Finished developers/bin 3s 592MB
Starting misc
Finished misc 39s 1GB
Starting compiler/proofs
Finished compiler/proofs 1h25m52s 43GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 5h52m07s 95GB
Starting semantics/ffi
Finished semantics/ffi 8s 544MB
Starting semantics
Finished semantics 0s 62MB
Starting semantics/proofs
Finished semantics/proofs 23s 815MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 20s 716MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 10m33s 2GB
Starting basis/pure
Finished basis/pure 0s 105MB
Starting translator
Finished translator 1m37s 3GB
Starting compiler/parsing
Finished compiler/parsing 0s 68MB
Starting characteristic
Finished characteristic 1s 128MB
Starting translator/monadic
Finished translator/monadic 1s 125MB
Starting translator/monadic/monad_base
Finished translator/monadic/monad_base 0s 61MB
Starting basis
Finished basis 2m22s 4GB
Starting compiler
Finished compiler 2s 223MB
Starting compiler/inference
Finished compiler/inference 1s 115MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 0s 101MB
Starting compiler/backend/gc
Finished compiler/backend/gc 1s 147MB
Starting compiler/backend
Finished compiler/backend 4s 273MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 94MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 0s 91MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 0s 90MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 0s 92MB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 12s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 0s 91MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 0s 96MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 0s 88MB
Starting compiler/encoders/tests
Finished compiler/encoders/tests 1s 107MB
Starting compiler/encoders/monadic_enc
Finished compiler/encoders/monadic_enc 1s 152MB
Starting compiler/backend/x64
Finished compiler/backend/x64 1s 149MB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 1s 148MB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 1s 148MB
Starting compiler/backend/mips
Finished compiler/backend/mips 1s 149MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 1s 149MB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m05s 3GB
Starting compiler/backend/pattern_matching
Finished compiler/backend/pattern_matching 0s 61MB
Starting compiler/parsing/ocaml
Finished compiler/parsing/ocaml 1m42s 1GB
Starting compiler/printing
Finished compiler/printing 1s 119MB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 0s 70MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 1s 122MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 3m10s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1s 119MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 50s 3GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1s 152MB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 10m33s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m26s 9GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 7m04s 4GB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 16m43s 3GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 10m06s 7GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m10s 4GB
Starting compiler/encoders/ag32/proofs
FAILED: compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
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)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanned 31 directories
Starting work on README.md
Starting work on ag32_targetProofTheory
README.md (0s) OK
ag32_targetProofTheory (262s)FAIL<1>
<<HOL message: Created theory "ag32_targetProof">>
Proved triviality ___ "bytes_in_memory_thm"
Proved triviality ___ "bytes_in_memory_thm2"
Proved triviality ___ "add_carry_lem"
Proved triviality ___ "add_carry_lem2"
Proved triviality ___ "shift_lem"
Proved triviality ___ "long_mul_lem"
Proved triviality ___ "load_lem2"
Proved triviality ___ "length_ag32_encode"
Proved triviality ___ "ag32_target_ok"
Proved triviality ___ "aligned_pc"
Saved theorem _______ "concat_bytes"
Proved triviality ___ "funcT_thm"
Proved triviality ___ "shiftT_thm"
Saved theorem _______ "Decode_Encode"
Proved triviality ___ "ag32_run"
Proved triviality ___ "bytes_in_memory_IMP_all_pcs_MEM"
Skip (correct)
Const (correct)
Binop (correct)
Shift (correct)
Div (correct)
LongMul (correct)
LongMul (correct)
AddCarry (correct)
AddOverflow (correct)
SubOverflow (correct)
Mem (correct)
Proof of
encoder_correct ag32_target
failed.
Failed to prove theorem ag32_encoder_correct.
Exception raised at Tactical.THEN1:
first subgoal not solved by second tactic
error in quse /scratch/cakeml/regression3/cakeml-2920/compiler/encoders/ag32/proofs/ag32_targetProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic", origin_function = "THEN1", origin_structure = "Tactical", source_location = Loc_Unknown}
error in load /scratch/cakeml/regression3/cakeml-2920/compiler/encoders/ag32/proofs/ag32_targetProofScript : HOL_ERR {message = "first subgoal not solved by second tactic", origin_function = "THEN1", origin_structure = "Tactical", source_location = Loc_Unknown}
Uncaught exception at /scratch/cakeml/regression3/HOL-466a40abe43a384327cf9fd1ada840fa176b961d/src/prekernel/Feedback.sml:124: HOL_ERR {message = "first subgoal not solved by second tactic", origin_function = "THEN1", origin_structure = "Tactical", source_location = Loc_Unknown}
Full log: /scratch/cakeml/regression3/cakeml-2920/compiler/encoders/ag32/proofs/.hol/logs/ag32_targetProofTheory