Job 1103

CakeML:e0ecc2d2e1fde1d89e128eb508f2f715aa560da7
  Make a proof more robust [Nov 27 15:03:26]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 27 15:07:50 Claimed job
Nov 27 15:07:58 Building HOL
Nov 27 15:18:43 Starting developers
Nov 27 15:18:47 Finished developers                                               3s  80MB
Nov 27 15:18:48 Starting developers/bin
Nov 27 15:18:55 Finished developers/bin                                           6s 960MB
Nov 27 15:18:55 Starting semantics/ffi
Nov 27 15:19:04 Finished semantics/ffi                                            9s 219MB
Nov 27 15:19:05 Starting semantics
Nov 27 15:20:30 Finished semantics                                             1m25s   1GB
Nov 27 15:20:31 Starting semantics/proofs
Nov 27 15:23:30 Finished semantics/proofs                                      2m59s   1GB
Nov 27 15:23:30 Starting semantics/alt_semantics
Nov 27 15:23:38 Finished semantics/alt_semantics                                  7s 266MB
Nov 27 15:23:38 Starting semantics/alt_semantics/proofs
Nov 27 15:25:27 Finished semantics/alt_semantics/proofs                        1m48s 701MB
Nov 27 15:25:27 Starting basis/pure
Nov 27 15:28:17 Finished basis/pure                                            2m49s 710MB
Nov 27 15:28:17 Starting translator
Nov 27 15:30:06 Finished translator                                            1m48s   1GB
Nov 27 15:30:06 Starting compiler/parsing
Nov 27 15:31:12 Finished compiler/parsing                                      1m05s   2GB
Nov 27 15:31:12 Starting characteristic
Nov 27 15:36:26 FAILED: characteristic
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Starting work on temporalTheory
Starting work on README.md
Starting work on cfFFITypeTheory
README.md                                       real:    0s  user:    0s     OK
temporalTheory                                  real:    2s  user:    1s     OK
cfFFITypeTheory                                 real:    9s  user:    8s     OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory                               real:   19s  user:   18s     OK
Starting work on cfHeapsTheory
cfHeapsTheory                                   real:   13s  user:   12s     OK
Starting work on cfStoreTheory
cfStoreTheory                                   real:   17s  user:   16s     OK
Starting work on cfNormaliseTheory
cfNormaliseTheory                               real:   15s  user:   14s     OK
Starting work on cfAppTheory
cfAppTheory                                     real:   18s  user:   17s     OK
Starting work on cfTheory
cfTheory                                        real:   79s  user:   77s     OK
Starting work on cfTacticsTheory
cfTacticsTheory                                 real:   13s  user:   12s     OK
Starting work on cfDivTheory
Starting work on cfLetAutoTheory
Starting work on cfMainTheory
cfMainTheory                                    real:   20s  user:   19s     OK
cfLetAutoTheory                                 real:   23s  user:   21s     OK
cfDivTheory                                     real:  126s  user:  123sFAIL<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"}