OverviewCakeML:7df18a4aaeea9380277b0a3f92bbc3871a73a8b2
Merge remote-tracking branch 'refs/remotes/origin/thunks' into thunks
#1246 (thunks)
Merging into:6ddaf6f8d86d8d5f57f0bcfc8fdd78f855e3daae
Make it clearer that HOL master should be used
HOL:927277205acf69a2b54b46ff3c7bd4c3294187a7
Update hash for change fixing while problems in armv8.6-asl-snapshot
Machine:pavlova
Claimed job
Building HOL
Starting developers
Finished developers 3s 182MB
Starting developers/bin
Finished developers/bin 2s 89MB
Starting misc
Finished misc 51s 1GB
Starting compiler/proofs
Finished compiler/proofs 1h11m12s 24GB
Starting compiler/bootstrap/compilation/x64/64/proofs
Finished compiler/bootstrap/compilation/x64/64/proofs 5h55m19s 62GB
Starting semantics/ffi
Finished semantics/ffi 7s 539MB
Starting semantics
Finished semantics 0s 59MB
Starting semantics/proofs
Finished semantics/proofs 20s 855MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 16s 758MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 4m06s 3GB
Starting basis/pure
Finished basis/pure 0s 97MB
Starting translator
Finished translator 1m21s 2GB
Starting compiler/parsing
Finished compiler/parsing 0s 67MB
Starting characteristic
Finished characteristic 1s 125MB
Starting translator/monadic
Finished translator/monadic 1s 122MB
Starting translator/monadic/monad_base
Finished translator/monadic/monad_base 0s 60MB
Starting basis
Finished basis 1m49s 3GB
Starting compiler
Finished compiler 2s 226MB
Starting compiler/inference
Finished compiler/inference 1s 126MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 0s 96MB
Starting compiler/backend/gc
Finished compiler/backend/gc 1s 147MB
Starting compiler/backend
Finished compiler/backend 4s 262MB
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 96MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 0s 93MB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 1h56m50s 32GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 0s 91MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 0s 92MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 0s 91MB
Starting compiler/encoders/tests
Finished compiler/encoders/tests 1s 120MB
Starting compiler/encoders/monadic_enc
Finished compiler/encoders/monadic_enc 17s 1GB
Starting compiler/backend/x64
Finished compiler/backend/x64 1s 150MB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 1s 152MB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 1s 151MB
Starting compiler/backend/mips
Finished compiler/backend/mips 1s 150MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 1s 152MB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 56s 2GB
Starting compiler/backend/pattern_matching
Finished compiler/backend/pattern_matching 0s 63MB
Starting compiler/parsing/ocaml
Finished compiler/parsing/ocaml 1m40s 1GB
Starting compiler/printing
Finished compiler/printing 1s 124MB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 0s 70MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 1s 118MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 2m42s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1s 131MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 45s 3GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1s 155MB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 0s 91MB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 11m00s 5GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m45s 4GB
Starting compiler/encoders/arm8_asl/proofs
FAILED: compiler/encoders/arm8_asl/proofs
HOLORIG=/scratch/cakeml/regression/cakeml-2995/compiler/encoders/arm8_asl/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
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)/src/sort
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/l3-machine-code/lib
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 $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(HOLDIR)/examples/formal-languages/context-free
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)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanned 43 directories
Starting work on l3_equivalenceTheory
Starting work on l3_equivalence_miscTheory
l3_equivalence_miscTheory examples/l3-machine-code/arm8/asl-equiv (12s) OK
Starting work on l3_equivalence_lemmasTheory
l3_equivalenceTheory examples/l3-machine-code/arm8/asl-equiv (20s) OK
l3_equivalence_lemmasTheory ...ples/l3-machine-code/arm8/asl-equiv (19s)FAIL<1>
<<HOL message: Created theory "l3_equivalence_lemmas">>
Saved theorem _______ "shiftr"
Saved theorem _______ "shiftl"
Saved theorem _______ "nat_of_int"
Saved theorem _______ "nat_of_int_Num"
Saved theorem _______ "bools_of_nat_aux_def"
Saved theorem _______ "bools_of_nat"
Saved theorem _______ "add_one_bool_ignore_overflow_def"
Saved theorem _______ "add_one_bool_ignore_overflow"
Saved theorem _______ "nat_of_bools_aux"
Saved theorem _______ "nat_of_bools"
Saved theorem _______ "bools_of_int_def"
Saved theorem _______ "LENGTH_bools_of_int"
Saved theorem _______ "v2n_fixwidth"
Saved theorem _______ "bool_of_bitU_bitU_of_bool"
Saved theorem _______ "ROR"
Saved theorem _______ "repeat"
Saved theorem _______ "integer_subrange_pos"
Saved theorem _______ "integer_subrange_neg"
Saved theorem _______ "OPTION_MAP_just_list"
Saved theorem _______ "shl_int_pos"
Saved theorem _______ "vec_of_bits_access_vec_dec_single"
Saved theorem _______ "replicate_bits_pos"
Proof of
n = dimindex (:) zext_ones (&n) (&m) = v2w (Ones m)
failed.
Failed to prove theorem zext_ones_pos.
Exception raised at Tactical.THEN1:
first subgoal not solved by second tactic
error in quse /scratch/cakeml/regression/HOL-927277205acf69a2b54b46ff3c7bd4c3294187a7/examples/l3-machine-code/arm8/asl-equiv/l3_equivalence_lemmasScript.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/regression/HOL-927277205acf69a2b54b46ff3c7bd4c3294187a7/examples/l3-machine-code/arm8/asl-equiv/l3_equivalence_lemmasScript : 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/regression/HOL-927277205acf69a2b54b46ff3c7bd4c3294187a7/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/regression/HOL-927277205acf69a2b54b46ff3c7bd4c3294187a7/examples/l3-machine-code/arm8/asl-equiv/.hol/logs/l3_equivalence_lemmasTheory