CakeML:4921efc30eff74884245445c7a1656f94aaa4bb6
update parse
#990 (rup)
Merging into:62d6b6509f4f15779b7bcb31490eb4ac9333d41a
Merge pull request #986 from ShunyaoLiang/scope
HOL:e546764f153c268543103c60ed61bd9941768e05
Speedup examples/probability building process
Machine:lammmington
Claimed job
Reusing HOL
Starting developers
Finished developers 2s 213MB
Starting developers/bin
Finished developers/bin 10s 1GB
Starting compiler/proofs
Finished compiler/proofs 1h48m53s 33GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 8h03m32s 89GB
Starting semantics/ffi
Finished semantics/ffi 7s 721MB
Starting semantics
Finished semantics 0s 62MB
Starting semantics/proofs
Finished semantics/proofs 33s 2GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 37s 1GB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 10m54s 5GB
Starting basis/pure
Finished basis/pure 0s 68MB
Starting translator
Finished translator 1m45s 3GB
Starting compiler/parsing
Finished compiler/parsing 0s 71MB
Starting characteristic
Finished characteristic 0s 88MB
Starting translator/monadic
Finished translator/monadic 0s 90MB
Starting basis
Finished basis 3m35s 5GB
Starting compiler/inference
Finished compiler/inference 0s 83MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 0s 65MB
Starting compiler/backend/gc
Finished compiler/backend/gc 0s 134MB
Starting compiler/backend
Finished compiler/backend 16s 1GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 92MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 0s 98MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 0s 93MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 0s 93MB
Starting compiler/encoders/arm8_asl
FAILED: compiler/encoders/arm8_asl
HOLORIG=/scratch/cakeml/regression2/cakeml-2356/compiler/encoders/arm8_asl [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Cloning into 'armv8.6-asl-snapshot'...
Note: switching to '7b8e94ba2e2d91fe8cdfdb21b18f36c70f772cb1'.
You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.
If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:
git switch -c <new-branch-name>
Or undo this operation with:
git switch -
Turn off this advice by setting config variable advice.detachedHead to false
HEAD is now at 7b8e94b Completely remove address translation.
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanned 36 directories
Starting work on lemTheory
Starting work on lem_boolTheory
lem_boolTheory ...-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (0s) OK
Starting work on lem_basic_classesTheory
lem_basic_classesTheory ...mv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (5s) OK
Starting work on lem_functionTheory
Starting work on lem_numTheory
Starting work on lem_tupleTheory
lem_tupleTheory ...equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (0s) OK
lem_functionTheory ...iv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (0s) OK
Starting work on lem_maybeTheory
lem_maybeTheory ...equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (0s) OK
lemTheory ...8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (6s) OK
Starting work on lem_assert_extraTheory
lem_assert_extraTheory ...rmv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (5s) OK
Starting work on lem_maybe_extraTheory
lem_maybe_extraTheory ...armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (4s) OK
lem_numTheory ...l-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (49s) OK
Starting work on lem_function_extraTheory
Starting work on lem_listTheory
Starting work on lem_set_helpersTheory
lem_set_helpersTheory ...armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (17s) OK
lem_function_extraTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/lem (19s) OK
lem_listTheory ...-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (26s) OK
Starting work on lem_list_extra_sailTheory
Starting work on lem_string_sailTheory
Starting work on lem_setTheory
Starting work on lem_eitherTheory
lem_string_sailTheory ...armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (19s) OK
Starting work on lem_showTheory
lem_list_extra_sailTheory ...8.6-asl-snapshot/A64_ISA_v86A/lib/lem (20s) OK
Starting work on lem_num_extraTheory
lem_setTheory ...l-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (21s) OK
Starting work on lem_mapTheory
lem_eitherTheory ...quiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (21s) OK
Starting work on lem_relationTheory
lem_num_extraTheory ...v/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (20s) OK
Starting work on lem_sortingTheory
lem_mapTheory ...l-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (20s) OK
Starting work on lem_map_extraTheory
lem_showTheory ...-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (23s) OK
Starting work on lem_machine_wordTheory
lem_relationTheory ...iv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (28s) OK
Starting work on lem_wordTheory
lem_map_extraTheory ...v/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (19s) OK
Starting work on lem_string_extra_sailTheory
lem_sortingTheory ...uiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (20s) OK
Starting work on lem_set_extra_sailTheory
lem_machine_wordTheory ...rmv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (21s) OK
lem_set_extra_sailTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/lem (21s) OK
lem_string_extra_sailTheory ...6-asl-snapshot/A64_ISA_v86A/lib/lem (21s) OK
Starting work on lem_show_extraTheory
lem_wordTheory ...-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (56s) OK
Starting work on lem_pervasives_sailTheory
lem_show_extraTheory .../armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (22s) OK
lem_pervasives_sailTheory ...8.6-asl-snapshot/A64_ISA_v86A/lib/lem (19s) OK
Starting work on lem_pervasives_extra_sailTheory
lem_pervasives_extra_sailTheory ...l-snapshot/A64_ISA_v86A/lib/lem (19s) OK
Starting work on lemheap
Starting work on sail2_instr_kindsTheory
Starting work on sail2_valuesTheory
lemheap ...rm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (0s) OK
Starting work on lemheap
lemheap ...rm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (57s) OK
Finished $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem [#theories: 29] (591.580s)
sail2_instr_kindsTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/sail (27s) OK
sail2_valuesTheory ...v/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail (65s) OK
Starting work on sail2_operatorsTheory
Starting work on sail2_state_monadTheory
Starting work on sail2_valuesAuxiliaryTheory
sail2_valuesAuxiliaryTheory ...-asl-snapshot/A64_ISA_v86A/lib/sail (23s)FAIL<1>
Saved theorem _______ "pad_list_rw"
Saved theorem _______ "pad_list_ind_rw"
Saved theorem _______ "reverse_endianness_list_rw"
Saved theorem _______ "reverse_endianness_list_ind_rw"
Exception raised at IntDP_Munge.COOPER_CONV:
Tried to prove generalised goal (generalising to...) but it was false
error in quse /scratch/cakeml/regression2/HOL-e546764f153c268543103c60ed61bd9941768e05/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail/sail2_valuesAuxiliaryScript.sml : HOL_ERR {message = "at IntDP_Munge.COOPER_CONV:\nTried to prove generalised goal (generalising to...) but it was false", origin_function = "tprove", origin_structure = "Defn"}
error in load /scratch/cakeml/regression2/HOL-e546764f153c268543103c60ed61bd9941768e05/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail/sail2_valuesAuxiliaryScript : HOL_ERR {message = "at IntDP_Munge.COOPER_CONV:\nTried to prove generalised goal (generalising to...) but it was false", origin_function = "tprove", origin_structure = "Defn"}
Uncaught exception: HOL_ERR {message = "at IntDP_Munge.COOPER_CONV:\nTried to prove generalised goal (generalising to...) but it was false", origin_function = "tprove", origin_structure = "Defn"}
sail2_operatorsTheory ...rmv8.6-asl-snapshot/A64_ISA_v86A/lib/sail (23s)MKILLED
sail2_state_monadTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/sail (24s)MKILLED