Job 317

CakeML:662d8e97d01498aaefd517f555945913cfb545bd
  Fix alt_semantics/proofs/interpTheory for latest HOL [May 11 00:22:54]
HOL:244be4f0bb5e9410122a35a88571fcb951974f1d
  Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOL [May 10 10:31:00]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

May 11 00:27:37 Claimed job
May 11 00:27:46 Building HOL
May 11 00:39:18 Starting developers/bin
May 11 00:39:29 Finished developers/bin                                           8s 155MB
May 11 00:39:30 Starting semantics/ffi
May 11 00:40:34 Finished semantics/ffi                                         1m01s 356MB
May 11 00:40:36 Starting semantics
May 11 00:42:59 Finished semantics                                             2m21s 874MB
May 11 00:43:01 Starting semantics/proofs
May 11 00:46:13 Finished semantics/proofs                                      3m10s   1GB
May 11 00:46:15 Starting basis/pure
May 11 00:52:02 Finished basis/pure                                            5m44s 675MB
May 11 00:52:04 Starting translator
May 11 00:58:47 Finished translator                                            6m40s   1GB
May 11 00:58:49 Starting compiler/parsing
May 11 01:01:00 Finished compiler/parsing                                      2m09s   2GB
May 11 01:01:02 Starting characteristic
May 11 01:03:48 FAILED: characteristic
]0;Holmake: .]0;Holmake: ../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-244be4f0bb5e9410122a35a88571fcb951974f1d/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developersWorking in ../developers
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../misc]0;Holmake: ../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ../compiler/parsing]0;Holmake: ../semantics]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../compiler/parsing]0;Holmake: ../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: .]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: .]0;Holmake: ../translator]0;Holmake: ../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/characteristic
Starting work on heap
heap                                                                         OK
Starting work on cfFFITypeTheory
cfFFITypeTheory                                                              OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory                                                            OK
Starting work on cfHeapsTheory
cfHeapsTheory                                                                OK
Starting work on cfStoreTheory
cfStoreTheory                                                                OK
Starting work on cfNormaliseTheory
cfNormaliseTheory                                                            OK
Starting work on cfAppTheory
cfAppTheory                                                                  OK
Starting work on cfTheory
cfTheory                                                            FAILED! <1>
 Saved definition __ "app_aw8update_def"
 
 Exception raised at Absyn.Absyn:
 on line 1307, characters 16-23:
 No rule for [+, TM]
 error in quse /scratch/cakeml/regression/cakeml-317/characteristic/cfScript.sml : HOL_ERR {message = "on line 1307, characters 16-23:\nNo rule for [+, TM]", origin_function = "Absyn", origin_structure = "Absyn"}
 error in load cfScript : HOL_ERR {message = "on line 1307, characters 16-23:\nNo rule for [+, TM]", origin_function = "Absyn", origin_structure = "Absyn"}
 Uncaught exception: HOL_ERR {message = "on line 1307, characters 16-23:\nNo rule for [+, TM]", origin_function = "Absyn", origin_structure = "Absyn"}
 on line 1307, characters 16-23:
 No rule for [+, TM]