Job 1645

CakeML:f3c5b4918d6bfd10d4e8ed819c241a11ec7ff531
  Update ptreeConversionProps [Nov 19 08:26:42]
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:bbc4316ab6255e29628563000a9b6b171290f1be
  Fix congruence code (from acd5d8650) to also work with non-equalities [Nov 18 00:28:52]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 19 13:14:43 Claimed job
Nov 19 13:14:46 Building HOL
Nov 19 13:23:47 Starting developers
Nov 19 13:23:50 Finished developers                                               2s 102MB
Nov 19 13:23:50 Starting developers/bin
Nov 19 13:23:56 Finished developers/bin                                           6s   1GB
Nov 19 13:23:56 Starting semantics/ffi
Nov 19 13:24:07 Finished semantics/ffi                                           10s 265MB
Nov 19 13:24:07 Starting semantics
Nov 19 13:25:45 Finished semantics                                             1m37s   1GB
Nov 19 13:25:45 Starting semantics/proofs
Nov 19 13:29:20 Finished semantics/proofs                                      3m34s   1GB
Nov 19 13:29:20 Starting semantics/alt_semantics
Nov 19 13:29:31 Finished semantics/alt_semantics                                 11s 391MB
Nov 19 13:29:32 Starting semantics/alt_semantics/proofs
Nov 19 13:31:51 Finished semantics/alt_semantics/proofs                        2m18s   1GB
Nov 19 13:31:51 Starting basis/pure
Nov 19 13:34:35 Finished basis/pure                                            2m43s   1GB
Nov 19 13:34:35 Starting translator
Nov 19 13:35:48 FAILED: translator
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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$(HOLDIR)/examples/formal-languages/regular[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)/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)/semantics/proofs[0m
Finished $(CAKEMLDIR)/misc                                                                                                                                         (0.000s) 
Starting work on ml_progTheory
ml_progTheory                                                                                                                                       translator (17s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                                                                                                                 translator (37s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_pmatchTheory                                                                                                                                     translator (13s)FAIL<1>
   | Match env' =>
     ext.
       env' = ext ++ env 
       Pmatch aenv s ps vs =
       SOME (aenv with v := nsAppend (alist_to_ns ext) aenv.v)
 
 failed.
 error in quse /home/myreen/regression/cakeml-1645/translator/ml_pmatchScript.sml : HOL_ERR {message = " (THEN1 on line 117)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1645/translator/ml_pmatchScript : HOL_ERR {message = " (THEN1 on line 117)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 117)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
ml_optimiseTheory                                                                                                                                   translator (13s)MKILLED