CakeML:9fa5ba7564cbadc002cc5a417efbaef6bd7ecc6b
Fix 32-bit pancake translation
#989 (pan_errors)
Merging into:77aba466f2652250e9b3dd44c55db74bdab6d392
Add parameters to the scope-checker
HOL:e546764f153c268543103c60ed61bd9941768e05
Speedup examples/probability building process
Machine:pavlova
Claimed job
Building HOL
Starting developers
Finished developers 2s 176MB
Starting developers/bin
Finished developers/bin 15s 1GB
Starting compiler/proofs
Finished compiler/proofs 1h51m14s 48GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 8h18m40s 84GB
Starting semantics/ffi
Finished semantics/ffi 7s 642MB
Starting semantics
Finished semantics 0s 66MB
Starting semantics/proofs
Finished semantics/proofs 33s 2GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 36s 1GB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 11m02s 3GB
Starting basis/pure
Finished basis/pure 0s 69MB
Starting translator
Finished translator 1m41s 5GB
Starting compiler/parsing
Finished compiler/parsing 0s 67MB
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 84MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 0s 67MB
Starting compiler/backend/gc
Finished compiler/backend/gc 0s 130MB
Starting compiler/backend
Finished compiler/backend 17s 1GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 93MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 0s 94MB
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/regression/cakeml-2359/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 (4s) 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 (51s) 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 (18s) 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 (18s) 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 (20s) OK
Starting work on lem_mapTheory
lem_eitherTheory ...quiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (20s) OK
Starting work on lem_relationTheory
lem_num_extraTheory ...v/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (19s) 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 (27s) OK
Starting work on lem_wordTheory
lem_sortingTheory ...uiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (21s) OK
Starting work on lem_set_extra_sailTheory
lem_map_extraTheory ...v/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (19s) OK
Starting work on lem_string_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 (55s) OK
Starting work on lem_pervasives_sailTheory
lem_show_extraTheory .../armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (21s) 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 (54s) OK
Finished $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem [#theories: 29] (584.290s)
sail2_instr_kindsTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/sail (26s) OK
sail2_valuesTheory ...v/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail (61s) 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/regression/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/regression/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 (24s)MKILLED
sail2_state_monadTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/sail (24s)MKILLED