Job 366

  Use symbolic names for word shift funs
#498 (basis-word-ops)
Merging into:ec623912b1a55939bceccd7ad699b2bc29780c08
  Fix stack_to_labProof: shadowed binding
  Add hypotheses count check to TAC_PROOF.
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers/bin
 Finished developers/bin                                           8s 224MB
 Starting semantics/ffi
 Finished semantics/ffi                                         1m00s 535MB
 Starting semantics
 Finished semantics                                             2m20s 917MB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m15s   1GB
 Starting basis/pure
 Finished basis/pure                                            5m48s 763MB
 Starting translator
 Finished translator                                            6m35s 971MB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m08s   2GB
 Starting characteristic
 Finished characteristic                                        4m14s   1GB
 Starting basis
 Finished basis                                                28m44s   2GB
 Starting translator/monadic
 Finished translator/monadic                                       1s  30MB
 Starting compiler/inference
 Finished compiler/inference                                    2m37s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              54s   1GB
 Starting compiler/backend/gc
 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 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: .