Job 732

CakeML:a81eb139c2c7cda42446483ad2e78190ff31a46d
  Stop assuming term eqtype in pegComplete [Feb 18 19:38:50]
#618 (monadic-trans-cleanup)
Merging into:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
  Stop assuming term eqtype in ml_monad_translatorBase [Feb 16 11:48:28]
HOL:45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1
  Testing for src/Boolify [Feb 15 06:20:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 18 20:03:39 Claimed job
Feb 18 20:03:44 Reusing HOL
Feb 18 20:03:48 Starting developers
Feb 18 20:03:50 Finished developers                                               0s  33MB
Feb 18 20:03:50 Starting developers/bin
Feb 18 20:04:25 Finished developers/bin                                          34s 204MB
Feb 18 20:04:26 Starting semantics/ffi
Feb 18 20:04:34 Finished semantics/ffi                                            7s 224MB
Feb 18 20:04:35 Starting semantics
Feb 18 20:05:53 Finished semantics                                             1m16s   1GB
Feb 18 20:05:53 Starting semantics/proofs
Feb 18 20:08:45 Finished semantics/proofs                                      2m51s   1GB
Feb 18 20:08:46 Starting basis/pure
Feb 18 20:09:30 Finished basis/pure                                              43s 633MB
Feb 18 20:09:31 Starting translator
Feb 18 20:11:06 Finished translator                                            1m34s   1GB
Feb 18 20:11:06 Starting compiler/parsing
Feb 18 20:12:04 Finished compiler/parsing                                        56s   2GB
Feb 18 20:12:05 Starting characteristic
Feb 18 20:16:15 Finished characteristic                                        4m09s   1GB
Feb 18 20:16:16 Starting translator/monadic
Feb 18 20:17:39 Finished translator/monadic                                    1m22s   1GB
Feb 18 20:17:40 Starting basis
Feb 18 20:34:04 Finished basis                                                16m23s   3GB
Feb 18 20:34:05 Starting compiler/inference
Feb 18 20:35:35 Finished compiler/inference                                    1m29s   1GB
Feb 18 20:35:36 Starting compiler/backend/reg_alloc
Feb 18 20:36:27 Finished compiler/backend/reg_alloc                              49s   1GB
Feb 18 20:36:27 Starting compiler/backend/gc
Feb 18 20:44:08 Finished compiler/backend/gc                                   7m39s   2GB
Feb 18 20:44:08 Starting compiler/backend
Feb 18 20:44:10 Finished compiler/backend                                         0s  41MB
Feb 18 20:44:11 Starting compiler/encoders/asm
Feb 18 20:44:12 Finished compiler/encoders/asm                                    0s  32MB
Feb 18 20:44:12 Starting compiler/encoders/x64
Feb 18 20:44:35 Finished compiler/encoders/x64                                   21s 953MB
Feb 18 20:44:36 Starting compiler/encoders/arm6
Feb 18 20:45:19 Finished compiler/encoders/arm6                                  42s 734MB
Feb 18 20:45:19 Starting compiler/encoders/arm8
Feb 18 20:45:31 Finished compiler/encoders/arm8                                  11s 858MB
Feb 18 20:45:32 Starting compiler/encoders/mips
Feb 18 20:45:48 Finished compiler/encoders/mips                                  14s   1GB
Feb 18 20:45:48 Starting compiler/encoders/riscv
Feb 18 20:46:01 Finished compiler/encoders/riscv                                 12s 760MB
Feb 18 20:46:02 Starting compiler/encoders/ag32
Feb 18 20:46:17 Finished compiler/encoders/ag32                                  14s 762MB
Feb 18 20:46:18 Starting compiler/backend/x64
Feb 18 20:46:33 Finished compiler/backend/x64                                    14s   1GB
Feb 18 20:46:34 Starting compiler/backend/arm6
Feb 18 20:46:51 Finished compiler/backend/arm6                                   16s   1GB
Feb 18 20:46:52 Starting compiler/backend/arm8
Feb 18 20:47:07 Finished compiler/backend/arm8                                   14s 833MB
Feb 18 20:47:07 Starting compiler/backend/mips
Feb 18 20:47:24 Finished compiler/backend/mips                                   16s   1GB
Feb 18 20:47:25 Starting compiler/backend/riscv
Feb 18 20:47:41 Finished compiler/backend/riscv                                  14s   1GB
Feb 18 20:47:41 Starting compiler/backend/ag32
Feb 18 20:48:47 Finished compiler/backend/ag32                                 1m04s   1GB
Feb 18 20:48:48 Starting compiler/parsing/proofs
Feb 18 20:54:18 Finished compiler/parsing/proofs                               5m29s 855MB
Feb 18 20:54:19 Starting compiler/inference/proofs
Feb 18 20:56:56 Finished compiler/inference/proofs                             2m36s   1GB
Feb 18 20:56:57 Starting compiler/backend/semantics
Feb 18 21:03:47 Finished compiler/backend/semantics                            6m49s   2GB
Feb 18 21:03:48 Starting compiler/backend/reg_alloc/proofs
Feb 18 21:06:23 Finished compiler/backend/reg_alloc/proofs                     2m34s 797MB
Feb 18 21:06:24 Starting compiler/backend/proofs
Feb 18 21:41:15 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/regression/cakeml-732/basis/pure]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/balanced_bst]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-732/basis/pure]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-732/basis/pure]0;Holmake: ~/regression/cakeml-732/misc]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-732/misc]0;Holmake: ~/regression/cakeml-732/developers]0;Holmake: ~/regression/cakeml-732/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-732/misc]0;Holmake: ~/regression/cakeml-732/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-732/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-732/misc]0;Holmake: ~/regression/cakeml-732/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-732/basis/pure]0;Holmake: ~/regression/cakeml-732/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-732/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-732/semantics]0;Holmake: ~/regression/cakeml-732/semantics/ffi]0;Holmake: ~/regression/cakeml-732/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-732/semantics]0;Holmake: ~/regression/cakeml-732/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-732/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-732/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-732/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-732/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-732/semantics/proofs]0;Holmake: ~/regression/cakeml-732/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ~/regression/cakeml-732/translator/monadic]0;Holmake: ~/regression/cakeml-732/characteristic]0;Holmake: ~/regression/cakeml-732/compiler/parsing]0;Holmake: ~/regression/cakeml-732/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-732/characteristic]0;Holmake: ~/regression/cakeml-732/translator]0;Holmake: ~/regression/cakeml-732/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-732/characteristic]0;Holmake: ~/regression/cakeml-732/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-732/translator/monadic]0;Holmake: ~/regression/cakeml-732/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
data_simpProofTheory                                OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                               OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                                 OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                  OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                                OK
Starting work on bvl_handleProofTheory
clos_annotateProofTheory                            OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                               OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                               OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                                 OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                               OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                              OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory                               OK
Starting work on clos_labelsProofTheory
clos_ticksProofTheory                               OK
Starting work on clos_knownProofTheory
bvi_tailrecProofTheory                              OK
Starting work on bvl_to_bviProofTheory
clos_labelsProofTheory                              OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                                 OK
Starting work on clos_numberProofTheory
clos_numberProofTheory                              OK
Starting work on word_simpProofTheory
clos_knownProofTheory                               OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                OK
Starting work on word_gcFunctionsTheory
clos_callProofTheory                                OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                              OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                               OK
Starting work on word_allocProofTheory
word_bignumProofTheory                              OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory                              OK
Starting work on word_removeProofTheory
word_instProofTheory                                OK
Starting work on flat_elimProofTheory
word_removeProofTheory                              OK
Starting work on flat_exh_matchProofTheory
flat_exh_matchProofTheory                           OK
Starting work on flat_reorder_matchProofTheory
flat_elimProofTheory                                OK
Starting work on flat_to_patProofTheory
flat_reorder_matchProofTheory                       OK
Starting work on flat_uncheck_ctorsProofTheory
flat_uncheck_ctorsProofTheory                       OK
Starting work on lab_filterProofTheory
flat_to_patProofTheory                              OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                               OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                              OK
Starting work on source_to_flatProofTheory
data_to_word_memoryProofTheory                      OK
Starting work on stack_allocProofTheory
source_to_flatProofTheory                           OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                              OK
Starting work on word_to_stackProofTheory
word_allocProofTheory                               OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                             OK
Starting work on data_to_word_gcProofTheory
stack_removeProofTheory                             OK
Starting work on lab_to_targetProofTheory
data_to_word_gcProofTheory                          OK
Starting work on data_to_word_bignumProofTheory
lab_to_targetProofTheory                            OK
Starting work on word_elimProofTheory
stack_allocProofTheory                              OK
Starting work on README.md
README.md                                           OK
word_elimProofTheory                                OK
data_to_word_bignumProofTheory                      OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory                            OK
Starting work on stack_to_labProofTheory
stack_to_labProofTheory                             OK
data_to_word_assignProofTheory                      OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                             OK
Starting work on backendProofTheory
backendProofTheory                         FAILED! <1>
    Reason: Can't unify ''a to term (Requires equality type)
 Found near pairSyntax.dest_pair (assoc k d1)
 /home/myreen/regression/cakeml-732/compiler/backend/proofs/backendProofScript.sml:362: error: Type error in function application.
    Function: map get_pair : (''a * term) list -> term list
    Argument: d2 : (term * term) list
    Reason: Can't unify ''a to term (Requires equality type)
 Found near map get_pair d2
 error in quse /home/myreen/regression/cakeml-732/compiler/backend/proofs/backendProofScript.sml : Fail "Static Errors"
 error in load backendProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"