Job 1104

CakeML:ad7809ba45169fdd32a8986db35d6597d181bab2
  Adjust proof to avoid infinite loop [Nov 28 01:48:27]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Nov 28 01:54:19 Claimed job
Nov 28 01:54:25 Building HOL
Nov 28 02:04:41 Starting developers
Nov 28 02:04:45 Finished developers                                               3s 107MB
Nov 28 02:04:45 Starting developers/bin
Nov 28 02:04:51 Finished developers/bin                                           5s 964MB
Nov 28 02:04:51 Starting semantics/ffi
Nov 28 02:05:00 Finished semantics/ffi                                            9s 251MB
Nov 28 02:05:00 Starting semantics
Nov 28 02:06:22 Finished semantics                                             1m21s   1GB
Nov 28 02:06:22 Starting semantics/proofs
Nov 28 02:09:16 Finished semantics/proofs                                      2m53s   1GB
Nov 28 02:09:16 Starting semantics/alt_semantics
Nov 28 02:09:23 Finished semantics/alt_semantics                                  6s 294MB
Nov 28 02:09:23 Starting semantics/alt_semantics/proofs
Nov 28 02:11:04 Finished semantics/alt_semantics/proofs                        1m40s   1GB
Nov 28 02:11:04 Starting basis/pure
Nov 28 02:13:44 Finished basis/pure                                            2m40s 845MB
Nov 28 02:13:44 Starting translator
Nov 28 02:15:25 Finished translator                                            1m40s   1GB
Nov 28 02:15:25 Starting compiler/parsing
Nov 28 02:16:27 Finished compiler/parsing                                      1m02s   1GB
Nov 28 02:16:27 Starting characteristic
Nov 28 02:21:35 FAILED: characteristic
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Starting work on temporalTheory
Starting work on README.md
Starting work on cfFFITypeTheory
README.md                                       real:    0s  user:    0s     OK
temporalTheory                                  real:    2s  user:    2s     OK
cfFFITypeTheory                                 real:    9s  user:    8s     OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory                               real:   18s  user:   17s     OK
Starting work on cfHeapsTheory
cfHeapsTheory                                   real:   13s  user:   12s     OK
Starting work on cfStoreTheory
cfStoreTheory                                   real:   16s  user:   15s     OK
Starting work on cfNormaliseTheory
cfNormaliseTheory                               real:   14s  user:   13s     OK
Starting work on cfAppTheory
cfAppTheory                                     real:   17s  user:   16s     OK
Starting work on cfTheory
cfTheory                                        real:   78s  user:   76s     OK
Starting work on cfTacticsTheory
cfTacticsTheory                                 real:   13s  user:   13s     OK
Starting work on cfDivTheory
Starting work on cfLetAutoTheory
Starting work on cfMainTheory
cfMainTheory                                    real:   19s  user:   18s     OK
cfLetAutoTheory                                 real:   22s  user:   21s     OK
cfDivTheory                                     real:  123s  user:  121sFAIL<1>
               vs i xv 
               app p fv [xv] (Hs i * one (... ... []))
                 (POSTv v'.
                      &... ... * Hs (... ... ) * one (... ... (... ... )))) 
          Q (LFLATTEN (LGENLIST (fromList  events) NONE))) 
     app p (some_repeat_clos env) [fv; xv] H ($POSTd Q)
 
 failed.
 Failed to prove theorem repeat_POSTd_one_FFI_part_FLATTEN.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 4833) (THEN1 on line 4787) (THEN1 on line 4776)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}