Job 894

CakeML:832ba913bb8d71bbd0514342d905cd372210464b
  Merge with latest master [May 22 09:20:05]
#633 (FMA_support)
Merging into:21975585998034b43aee723e21c7043f250a58fd
  Merge pull request #635 from CakeML/thm [May 22 08:49:19]
HOL:15a1e85b5308eeb3ca329cafe2c409f1fd21edfd
  Fix Holmake regressions arising from b03aecf7b [May 20 00:34:31]
Machine:brain08 4.14.89.1.amd64-smp x86_64 GNU/Linux

May 22 09:38:57 Claimed job
May 22 09:39:04 Building HOL
May 22 09:54:15 Starting developers
May 22 09:54:17 Finished developers                                               1s  42MB
May 22 09:54:17 Starting developers/bin
May 22 09:54:26 Finished developers/bin                                           8s 929MB
May 22 09:54:26 Starting semantics/ffi
May 22 09:55:36 Finished semantics/ffi                                         1m10s 596MB
May 22 09:55:37 Starting semantics
May 22 09:58:32 Finished semantics                                             2m54s   1GB
May 22 09:58:32 Starting semantics/proofs
May 22 10:04:29 Finished semantics/proofs                                      5m56s   1GB
May 22 10:04:29 Starting basis/pure
May 22 10:11:20 Finished basis/pure                                            6m50s 560MB
May 22 10:11:20 Starting translator
May 22 10:14:34 Finished translator                                            3m13s   1GB
May 22 10:14:34 Starting compiler/parsing
May 22 10:16:26 Finished compiler/parsing                                      1m52s   2GB
May 22 10:16:27 Starting characteristic
May 22 10:26:43 Finished characteristic                                       10m16s   2GB
May 22 10:26:43 Starting translator/monadic
May 22 10:29:24 Finished translator/monadic                                    2m40s   1GB
May 22 10:29:24 Starting basis
May 22 11:02:22 Finished basis                                                32m57s   2GB
May 22 11:02:23 Starting compiler/inference
May 22 11:06:12 Finished compiler/inference                                    3m49s   1GB
May 22 11:06:13 Starting compiler/backend/reg_alloc
May 22 11:07:48 Finished compiler/backend/reg_alloc                            1m35s   1GB
May 22 11:07:49 Starting compiler/backend/gc
May 22 11:24:26 Finished compiler/backend/gc                                  16m36s   2GB
May 22 11:24:26 Starting compiler/backend
May 22 11:24:34 Finished compiler/backend                                         8s 290MB
May 22 11:24:35 Starting compiler/encoders/asm
May 22 11:24:36 Finished compiler/encoders/asm                                    0s  26MB
May 22 11:24:36 Starting compiler/encoders/x64
May 22 11:26:34 Finished compiler/encoders/x64                                 1m57s 739MB
May 22 11:26:34 Starting compiler/encoders/arm7
May 22 11:30:19 Finished compiler/encoders/arm7                                3m44s   2GB
May 22 11:30:19 Starting compiler/encoders/arm8
May 22 11:31:24 Finished compiler/encoders/arm8                                1m05s   1GB
May 22 11:31:25 Starting compiler/encoders/mips
May 22 11:33:41 Finished compiler/encoders/mips                                2m15s   1GB
May 22 11:33:41 Starting compiler/encoders/riscv
May 22 11:36:13 Finished compiler/encoders/riscv                               2m32s   1GB
May 22 11:36:14 Starting compiler/encoders/ag32
May 22 11:36:43 Finished compiler/encoders/ag32                                  29s 799MB
May 22 11:36:43 Starting compiler/backend/x64
May 22 11:37:22 Finished compiler/backend/x64                                    38s 838MB
May 22 11:37:22 Starting compiler/backend/arm7
May 22 11:38:05 Finished compiler/backend/arm7                                   42s   1GB
May 22 11:38:05 Starting compiler/backend/arm8
May 22 11:38:42 Finished compiler/backend/arm8                                   36s   1GB
May 22 11:38:42 Starting compiler/backend/mips
May 22 11:39:20 Finished compiler/backend/mips                                   37s   1GB
May 22 11:39:20 Starting compiler/backend/riscv
May 22 11:39:57 Finished compiler/backend/riscv                                  37s   1GB
May 22 11:39:57 Starting compiler/backend/ag32
May 22 11:42:14 Finished compiler/backend/ag32                                 2m16s   1GB
May 22 11:42:14 Starting compiler/parsing/proofs
May 22 11:53:12 Finished compiler/parsing/proofs                              10m57s 873MB
May 22 11:53:12 Starting compiler/inference/proofs
May 22 11:58:51 Finished compiler/inference/proofs                             5m38s   1GB
May 22 11:58:51 Starting compiler/backend/semantics
May 22 12:12:28 Finished compiler/backend/semantics                           13m36s   2GB
May 22 12:12:28 Starting compiler/backend/reg_alloc/proofs
May 22 12:19:08 Finished compiler/backend/reg_alloc/proofs                     6m39s   1GB
May 22 12:19:08 Starting compiler/backend/proofs
May 22 12:27:57 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/machine-code/multiword]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: /local/hbecker/regression/cakeml-894/basis/pure]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/balanced_bst]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: /local/hbecker/regression/cakeml-894/basis/pure]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/formal-languages]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/formal-languages/context-free]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
Starting work on regexp2dfa
regexp2dfa                                                                                                                       OK
]0;Holmake: /local/hbecker/regression/cakeml-894/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-894/misc]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/fun-op-sem/lprefix_lub]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: /local/hbecker/regression/cakeml-894/misc]0;Holmake: /local/hbecker/regression/cakeml-894/developers]0;Holmake: /local/hbecker/regression/cakeml-894/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: /local/hbecker/regression/cakeml-894/misc]0;Holmake: /local/hbecker/regression/cakeml-894/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/cakeml-894/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: /local/hbecker/regression/cakeml-894/misc]0;Holmake: /local/hbecker/regression/cakeml-894/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: /local/hbecker/regression/cakeml-894/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-894/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: /local/hbecker/regression/cakeml-894/translator/monadic/monad_base]0;Holmake: /local/hbecker/regression/cakeml-894/semantics]0;Holmake: /local/hbecker/regression/cakeml-894/semantics/ffi]0;Holmake: /local/hbecker/regression/cakeml-894/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: /local/hbecker/regression/cakeml-894/semantics]0;Holmake: /local/hbecker/regression/cakeml-894/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: /local/hbecker/regression/cakeml-894/translator/monadic/monad_base]0;Holmake: /local/hbecker/regression/cakeml-894/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../reg_alloc]0;Holmake: /local/hbecker/regression/cakeml-894/unverified/reg_alloc]0;Holmake: /local/hbecker/regression/cakeml-894/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/l3-machine-code/common]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: /local/hbecker/regression/cakeml-894/semantics/proofs]0;Holmake: /local/hbecker/regression/cakeml-894/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: /local/hbecker/regression/cakeml-894/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-894/characteristic]0;Holmake: /local/hbecker/regression/cakeml-894/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-894/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: /local/hbecker/regression/cakeml-894/characteristic]0;Holmake: /local/hbecker/regression/cakeml-894/translator]0;Holmake: /local/hbecker/regression/cakeml-894/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: /local/hbecker/regression/cakeml-894/characteristic]0;Holmake: /local/hbecker/regression/cakeml-894/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: /local/hbecker/regression/cakeml-894/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-894/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/proofs
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                                                                                                  FAILED! <1>
 Saved theorem _____ "word_gc_move_roots_IMP_EVERY2"
 Saved theorem _____ "word_gen_gc_move_roots_IMP_EVERY2"
 Saved theorem _____ "word_gen_gc_partial_move_roots_IMP_EVERY2"
 Saved theorem _____ "word_gc_IMP_EVERY2"
 Saved theorem _____ "word_gc_fun_LENGTH"
 error in quse /local/hbecker/regression/cakeml-894/compiler/backend/proofs/word_gcFunctionsScript.sml : HOL_ERR {message = "at line 559, character 51:\nDon't expect to find a ) in this position after a ;\nat line 559, character 73 and at line 559, character 51.\n", origin_function = "Absyn", origin_structure = "Absyn"}
 error in load word_gcFunctionsScript : HOL_ERR {message = "at line 559, character 51:\nDon't expect to find a ) in this position after a ;\nat line 559, character 73 and at line 559, character 51.\n", origin_function = "Absyn", origin_structure = "Absyn"}
 Don't expect to find a ) in this position after a ;
 at line 559, character 73 and at line 559, character 51.
 Uncaught exception: HOL_ERR {message = "at line 559, character 51:\nDon't expect to find a ) in this position after a ;\nat line 559, character 73 and at line 559, character 51.\n", origin_function = "Absyn", origin_structure = "Absyn"}
bvl_to_bviProofTheory                                                                                                      M-KILLED
word_bignumProofTheory                                                                                                     M-KILLED
clos_to_bvlProofTheory                                                                                                     M-KILLED