Job 2797

CakeML:b0d59513984d51b81a6556e8af366c0a2bd33377
  Make lexer understand long names (e.g. Foo.Bar.Baz.f) [Mar 31 20:51:20]
#1152 (lexer-fix)
Merging into:e7e9834e1b1dfda72d0c264ed85dc7a674f82796
  Merge pull request #1151 from CakeML/pb_opt [Apr 06 20:39:02]
HOL:aa266667af464b9d3a22e8be1415d8f3af014c82
  Implement EQ_MP_TAC, which reverses primitive rule EQ_MP [Apr 01 04:57:21]
Machine:pavlova

Apr 06 20:41:17 Claimed job
Apr 06 20:41:23 Reusing HOL
Apr 06 20:41:34 Starting developers
Apr 06 20:41:38 Finished developers                                               3s 206MB
Apr 06 20:41:39 Starting developers/bin
Apr 06 20:41:45 Finished developers/bin                                           5s 746MB
Apr 06 20:41:46 Starting misc
Apr 06 20:42:28 Finished misc                                                    41s   1GB
Apr 06 20:42:29 Starting compiler/proofs
Apr 06 22:28:38 Finished compiler/proofs                                    1h46m07s  35GB
Apr 06 22:28:38 Starting compiler/bootstrap/translation
Apr 07 04:14:57 Finished compiler/bootstrap/translation                     5h46m15s  61GB
Apr 07 04:14:58 Starting semantics/ffi
Apr 07 04:15:08 Finished semantics/ffi                                            9s 584MB
Apr 07 04:15:08 Starting semantics
Apr 07 04:15:10 Finished semantics                                                0s  52MB
Apr 07 04:15:11 Starting semantics/proofs
Apr 07 04:15:16 FAILED: semantics/proofs
Scanning $(HOLDIR)/src/bag
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/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
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanned 18 directories
Starting work on README.md
Starting work on cmlPtreeConversionPropsTheory
README.md                                                           (0s)     OK
cmlPtreeConversionPropsTheory                                       (2s)FAIL<1>
 <<HOL message: Created theory "cmlPtreeConversionProps">>
 Saved definition ____ "user_expressible_tyname_def"
 Saved induction _____ "user_expressible_tyname_ind"
 Saved definition ____ "tyname_to_AST_def"
 Saved induction _____ "tyname_to_AST_ind"
 error in quse /scratch/cakeml/regression/cakeml-2797/semantics/proofs/cmlPtreeConversionPropsScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression/cakeml-2797/semantics/proofs/cmlPtreeConversionPropsScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression/HOL-aa266667af464b9d3a22e8be1415d8f3af014c82/src/parse/Parse.sml:492: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse", source_location = Loc_Unknown}