Job 936

CakeML:c4c57f1c16dbe3848caced5fae8651461786c070
  Avoid a parsing issue by avoiding Unicode || [Jul 09 11:41:21]
HOL:8a1dd56be791249751d00e89a4f65bc95edcb755
  Announce add_strliteral_form in release notes [Jul 08 07:09:56]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jul 09 11:43:24 Claimed job
Jul 09 11:43:27 Reusing HOL
Jul 09 11:43:32 Starting developers
Jul 09 11:43:32 Finished developers                                               0s  26MB
Jul 09 11:43:32 Starting developers/bin
Jul 09 11:43:36 Finished developers/bin                                           2s 144MB
Jul 09 11:43:36 Starting semantics/ffi
Jul 09 11:43:44 Finished semantics/ffi                                            8s 217MB
Jul 09 11:43:44 Starting semantics
Jul 09 11:45:26 Finished semantics                                             1m41s   1GB
Jul 09 11:45:26 Starting semantics/proofs
Jul 09 11:48:34 Finished semantics/proofs                                      3m07s   1GB
Jul 09 11:48:35 Starting semantics/alt_semantics
Jul 09 11:48:41 Finished semantics/alt_semantics                                  6s 309MB
Jul 09 11:48:41 Starting semantics/alt_semantics/proofs
Jul 09 11:50:32 Finished semantics/alt_semantics/proofs                        1m50s 791MB
Jul 09 11:50:33 Starting basis/pure
Jul 09 11:51:23 Finished basis/pure                                              50s 649MB
Jul 09 11:51:23 Starting translator
Jul 09 11:53:12 Finished translator                                            1m48s   1GB
Jul 09 11:53:12 Starting compiler/parsing
Jul 09 11:54:19 Finished compiler/parsing                                      1m06s   2GB
Jul 09 11:54:19 Starting characteristic
Jul 09 12:00:21 Finished characteristic                                        6m01s   2GB
Jul 09 12:00:21 Starting translator/monadic
Jul 09 12:02:31 Finished translator/monadic                                    2m08s   1GB
Jul 09 12:02:31 Starting basis
Jul 09 12:25:53 Finished basis                                                23m21s   2GB
Jul 09 12:25:53 Starting compiler/inference
Jul 09 12:27:30 Finished compiler/inference                                    1m36s   1GB
Jul 09 12:27:30 Starting compiler/backend/reg_alloc
Jul 09 12:28:32 Finished compiler/backend/reg_alloc                            1m01s   1GB
Jul 09 12:28:32 Starting compiler/backend/gc
Jul 09 12:37:10 Finished compiler/backend/gc                                   8m37s   1GB
Jul 09 12:37:10 Starting compiler/backend
Jul 09 12:37:11 Finished compiler/backend                                         0s  42MB
Jul 09 12:37:11 Starting compiler/encoders/asm
Jul 09 12:37:11 Finished compiler/encoders/asm                                    0s  37MB
Jul 09 12:37:12 Starting compiler/encoders/x64
Jul 09 12:38:07 Finished compiler/encoders/x64                                   55s 950MB
Jul 09 12:38:08 Starting compiler/encoders/arm7
Jul 09 12:39:44 Finished compiler/encoders/arm7                                1m36s   1GB
Jul 09 12:39:44 Starting compiler/encoders/arm8
Jul 09 12:40:13 Finished compiler/encoders/arm8                                  28s 576MB
Jul 09 12:40:14 Starting compiler/encoders/mips
Jul 09 12:41:16 Finished compiler/encoders/mips                                1m02s   1GB
Jul 09 12:41:17 Starting compiler/encoders/riscv
Jul 09 12:42:33 Finished compiler/encoders/riscv                               1m16s 862MB
Jul 09 12:42:34 Starting compiler/encoders/ag32
Jul 09 12:42:48 Finished compiler/encoders/ag32                                  14s 769MB
Jul 09 12:42:49 Starting compiler/backend/x64
Jul 09 12:43:05 Finished compiler/backend/x64                                    15s 983MB
Jul 09 12:43:05 Starting compiler/backend/arm7
Jul 09 12:43:23 Finished compiler/backend/arm7                                   17s   1GB
Jul 09 12:43:23 Starting compiler/backend/arm8
Jul 09 12:43:40 Finished compiler/backend/arm8                                   16s   1GB
Jul 09 12:43:40 Starting compiler/backend/mips
Jul 09 12:43:58 Finished compiler/backend/mips                                   17s   1GB
Jul 09 12:43:58 Starting compiler/backend/riscv
Jul 09 12:44:15 Finished compiler/backend/riscv                                  16s   1GB
Jul 09 12:44:16 Starting compiler/backend/ag32
Jul 09 12:45:21 Finished compiler/backend/ag32                                 1m04s   1GB
Jul 09 12:45:21 Starting compiler/parsing/proofs
Jul 09 12:50:55 Finished compiler/parsing/proofs                               5m33s 805MB
Jul 09 12:50:55 Starting compiler/inference/proofs
Jul 09 12:53:59 Finished compiler/inference/proofs                             3m03s   1GB
Jul 09 12:53:59 Starting compiler/backend/semantics
Jul 09 13:03:29 Finished compiler/backend/semantics                            9m30s   2GB
Jul 09 13:03:29 Starting compiler/backend/reg_alloc/proofs
Jul 09 13:06:53 Finished compiler/backend/reg_alloc/proofs                     3m23s 758MB
Jul 09 13:06:53 Starting compiler/backend/proofs
Jul 09 13:18:24 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/regression/cakeml-936/basis/pure]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/balanced_bst]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-936/basis/pure]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-936/basis/pure]0;Holmake: ~/regression/cakeml-936/misc]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-936/misc]0;Holmake: ~/regression/cakeml-936/developers]0;Holmake: ~/regression/cakeml-936/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-936/misc]0;Holmake: ~/regression/cakeml-936/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-936/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-936/misc]0;Holmake: ~/regression/cakeml-936/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-936/basis/pure]0;Holmake: ~/regression/cakeml-936/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-936/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-936/semantics]0;Holmake: ~/regression/cakeml-936/semantics/ffi]0;Holmake: ~/regression/cakeml-936/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-936/semantics]0;Holmake: ~/regression/cakeml-936/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-936/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-936/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-936/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-936/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-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/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-936/semantics/proofs]0;Holmake: ~/regression/cakeml-936/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-936/translator/monadic]0;Holmake: ~/regression/cakeml-936/characteristic]0;Holmake: ~/regression/cakeml-936/compiler/parsing]0;Holmake: ~/regression/cakeml-936/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-936/characteristic]0;Holmake: ~/regression/cakeml-936/translator]0;Holmake: ~/regression/cakeml-936/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-936/characteristic]0;Holmake: ~/regression/cakeml-936/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-936/translator/monadic]0;Holmake: ~/regression/cakeml-936/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
data_liveProofTheory                                                                                       OK
Starting work on bvi_to_dataProofTheory
bvi_letProofTheory                                                                                         OK
Starting work on clos_annotateProofTheory
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_elimProofTheory                                                                                       OK
Starting work on flat_reorder_matchProofTheory
data_to_word_memoryProofTheory                                                                    FAILED! <1>
   Grammar-deltas:
     overload_on("copy_list_tupled")
   invalidated by DelConstant(data_to_word_memoryProof$copy_list_tupled)>>
 Saved definition __ "copy_list_def"
 Saved induction ___ "copy_list_ind"
 Saved theorem _____ "copy_list_thm"
 Saved theorem _____ "memory_rel_FromList"
 error in quse /home/myreen/regression/cakeml-936/compiler/backend/proofs/data_to_word_memoryProofScript.sml : HOL_ERR {message = "at line 5776, character 22:\nLexical error - Character \"\226\" is a lexical error", origin_function = "Absyn", origin_structure = "Parse"}
 error in load data_to_word_memoryProofScript : HOL_ERR {message = "at line 5776, character 22:\nLexical error - Character \"\226\" is a lexical error", origin_function = "Absyn", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "at line 5776, character 22:\nLexical error - Character \"\226\" is a lexical error", origin_function = "Absyn", origin_structure = "Parse"}
word_allocProofTheory                                                                                M-KILLED
flat_exh_matchProofTheory                                                                            M-KILLED
flat_reorder_matchProofTheory                                                                        M-KILLED