Job 366

CakeML:bacdfd84c86ee6dd48ef9740a9cc3e5246e3ac48
  Use symbolic names for word shift funs [Jul 12 04:31:41]
#498 (basis-word-ops)
Merging into:ec623912b1a55939bceccd7ad699b2bc29780c08
  Fix stack_to_labProof: shadowed binding [Jul 12 23:31:29]
HOL:01930d56ce7a31c10ff7f422a0cf535a8c502a59
  Add hypotheses count check to TAC_PROOF. [Jul 17 11:44:44]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Jul 17 14:46:22 Claimed job
Jul 17 14:46:34 Building HOL
Jul 17 14:58:59 Starting developers/bin
Jul 17 14:59:09 Finished developers/bin                                           8s 224MB
Jul 17 14:59:11 Starting semantics/ffi
Jul 17 15:00:14 Finished semantics/ffi                                         1m00s 535MB
Jul 17 15:00:16 Starting semantics
Jul 17 15:02:38 Finished semantics                                             2m20s 917MB
Jul 17 15:02:40 Starting semantics/proofs
Jul 17 15:05:57 Finished semantics/proofs                                      3m15s   1GB
Jul 17 15:05:59 Starting basis/pure
Jul 17 15:11:50 Finished basis/pure                                            5m48s 763MB
Jul 17 15:11:52 Starting translator
Jul 17 15:18:29 Finished translator                                            6m35s 971MB
Jul 17 15:18:31 Starting compiler/parsing
Jul 17 15:20:42 Finished compiler/parsing                                      2m08s   2GB
Jul 17 15:20:44 Starting characteristic
Jul 17 15:25:01 Finished characteristic                                        4m14s   1GB
Jul 17 15:25:03 Starting basis
Jul 17 15:53:50 Finished basis                                                28m44s   2GB
Jul 17 15:53:52 Starting translator/monadic
Jul 17 15:53:56 Finished translator/monadic                                       1s  30MB
Jul 17 15:53:58 Starting compiler/inference
Jul 17 15:56:37 Finished compiler/inference                                    2m37s   1GB
Jul 17 15:56:39 Starting compiler/backend/reg_alloc
Jul 17 15:57:36 Finished compiler/backend/reg_alloc                              54s   1GB
Jul 17 15:57:38 Starting compiler/backend/gc
Jul 17 15:58:01 FAILED: compiler/backend/gc
]0;Holmake: /scratch/cakeml/regression/HOL-01930d56ce7a31c10ff7f422a0cf535a8c502a59/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-01930d56ce7a31c10ff7f422a0cf535a8c502a59/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
Starting work on multiwordTheory
multiwordTheory                                                                                                                                  FAILED! <1>
 !u1 u2 us v1 vs.
     (LENGTH us = LENGTH vs) /\
     mw2n (REVERSE (u1::u2::us)) DIV mw2n (REVERSE (v1::vs)) < dimword (:'a) /\
     dimword (:'a) DIV 2 <= w2n v1 ==>
     MIN ((w2n u1 * dimword (:'a) + w2n u2) DIV w2n v1) (dimword (:'a) - 1) <=
     mw2n (REVERSE (u1::u2::us)) DIV mw2n (REVERSE (v1::vs)) + 2
 
 failed.
 Failed to prove theorem mw_div_range2.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 1946 (THEN1 on line 1925) (THEN1 on line 1921) (THEN1 on line 1920) (THEN1 on line 1916)", origin_function = "by", origin_structure = "BasicProvers"}
]0;Holmake: ..]0;Holmake: .