Job 1643

CakeML:9a03dca8726c37de968502e45299f80be91d9e59
  Complete pegComplete [Nov 18 15:47:20]
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:6ad5e919416a5bf9dbe3bf35248a3cee706d8be5
  Disable unicode_version of `Borel` (Manual building broken), also nee [Nov 15 07:48:55]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 19 07:00:01 Claimed job
Nov 19 07:00:10 Reusing HOL
Nov 19 07:00:50 Starting developers
Nov 19 07:00:55 Finished developers                                               4s 116MB
Nov 19 07:00:55 Starting developers/bin
Nov 19 07:01:02 Finished developers/bin                                           6s   1GB
Nov 19 07:01:02 Starting semantics/ffi
Nov 19 07:01:14 Finished semantics/ffi                                           11s 211MB
Nov 19 07:01:14 Starting semantics
Nov 19 07:02:44 Finished semantics                                             1m29s   1GB
Nov 19 07:02:44 Starting semantics/proofs
Nov 19 07:03:25 FAILED: semantics/proofs
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(CAKEMLDIR)/developers
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Finished $(CAKEMLDIR)/misc                                             (0.000s) 
Starting work on README.md
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on namespacePropsTheory
README.md                                         semantics/proofs  (0s)     OK
astPropsTheory                                    semantics/proofs  (7s)     OK
namespacePropsTheory                              semantics/proofs (12s)     OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                         semantics/proofs  (7s)     OK
gramPropsTheory                                   semantics/proofs (23s)     OK
Starting work on cmlPtreeConversionPropsTheory
cmlPtreeConversionPropsTheory                     semantics/proofs (12s)FAIL<1>
 
 valid_ptree cmlG pt  MAP TK toks = ptree_fringe pt 
 (N  {nPattern; nPtuple; nPapp; nPbase; nPcons; nPConApp} 
  ptree_head pt = NN N 
  p. ptree_Pattern N pt = SOME p) 
 (ptree_head pt = NN nPatternList  pl. ptree_Plist pt = SOME pl  pl  [])
 
 failed.
 Failed to prove theorem Pattern_OK0.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 437) (THEN1 on line 438) (THEN1 on line 441) (THEN1 on line 449) (THEN1 on line 455) (THEN1 on line 456) (THEN1 on line 457) (THEN1 on line 458) (THEN1 on line 459) (THEN1 on line 461)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
semanticPrimitivesPropsTheory                     semantics/proofs (25s)MKILLED