Job 1642

CakeML:9a03dca8726c37de968502e45299f80be91d9e59
  Complete pegComplete [Nov 18 15:47:20]
#846 (pattern-aliases)
Merging into:6b1184f731754a44e6368258d6c1b1cc729aa0f5
  Merge pull request #843 from CakeML/newline-fix [Nov 13 19:24:32]
HOL:6ad5e919416a5bf9dbe3bf35248a3cee706d8be5
  Disable unicode_version of `Borel` (Manual building broken), also nee [Nov 15 07:48:55]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 18 19:17:09 Claimed job
Nov 18 19:17:14 Building HOL
Nov 18 19:26:14 Starting developers
Nov 18 19:26:17 Finished developers                                               2s 107MB
Nov 18 19:26:17 Starting developers/bin
Nov 18 19:26:24 Finished developers/bin                                           6s   1GB
Nov 18 19:26:24 Starting semantics/ffi
Nov 18 19:26:35 Finished semantics/ffi                                           10s 273MB
Nov 18 19:26:35 Starting semantics
Nov 18 19:28:12 Finished semantics                                             1m36s   1GB
Nov 18 19:28:12 Starting semantics/proofs
Nov 18 19:28:56 FAILED: semantics/proofs
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Starting work on NTpropertiesTheory
Starting work on pegTheory
Starting work on README.md
Starting work on astPropsTheory
README.md                                                                                                                                              semantics/proofs  (0s)     OK
Starting work on namespacePropsTheory
NTpropertiesTheory                                                                                                               examples/formal-languages/context-free  (4s)     OK
Starting work on gramPropsTheory
pegTheory                                                                                                                        examples/formal-languages/context-free  (6s)     OK
Starting work on pegexecTheory
astPropsTheory                                                                                                                                         semantics/proofs  (8s)     OK
pegexecTheory                                                                                                                    examples/formal-languages/context-free  (3s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 3]                                                                                                   (14.150s) 
Finished $(CAKEMLDIR)/misc                                                                                                                                                  (0.000s) 
namespacePropsTheory                                                                                                                                   semantics/proofs (13s)     OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                                                                                                                              semantics/proofs  (7s)     OK
gramPropsTheory                                                                                                                                        semantics/proofs (21s)     OK
Starting work on cmlPtreeConversionPropsTheory
cmlPtreeConversionPropsTheory                                                                                                                          semantics/proofs (13s)FAIL<1>
 (ptree_head pt = NN nPatternList  pl. ptree_Plist pt = SOME pl  pl  [])
 
 failed.
 Failed to prove theorem Pattern_OK0.
 
 Exception raised at Tactical.FIRST_ASSUM:
  (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)
 error in quse /home/myreen/regression/cakeml-1642/semantics/proofs/cmlPtreeConversionPropsScript.sml : 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"}
 error in load /home/myreen/regression/cakeml-1642/semantics/proofs/cmlPtreeConversionPropsScript : 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"}
 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 (26s)MKILLED