Job 1415

CakeML:b641d8a56ecb8c610d16eaf37f7d8131b6c4f2be
  Merge pull request #807 from CakeML/issue797 [Dec 10 13:31:32]
HOL:a4312426afc04b5e4d7aa33a72ef1fb535e4cf6a
  Tidy up Kolmogorov uncomputable script file (deleting much) [Dec 14 06:39:51]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Dec 15 13:52:51 Claimed job
Dec 15 13:53:04 Building HOL
Dec 15 14:06:52 Starting developers
Dec 15 14:06:54 Finished developers                                               2s 114MB
Dec 15 14:06:54 Starting developers/bin
Dec 15 14:07:00 Finished developers/bin                                           5s   1GB
Dec 15 14:07:01 Starting semantics/ffi
Dec 15 14:07:11 Finished semantics/ffi                                            9s 290MB
Dec 15 14:07:11 Starting semantics
Dec 15 14:07:33 FAILED: semantics
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[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
Starting work on grammarTheory
Starting work on lprefix_lubTheory
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory                                                                 real:    0s  user:    0s     OK
Starting work on lem_list_extraTheory
lprefix_lubTheory                                                             real:    2s  user:    2s     OK
Starting work on lem_set_extraTheory
grammarTheory                                                                 real:    3s  user:    2s     OK
Starting work on lem_stringTheory
lem_set_extraTheory                                                           real:    0s  user:    0s     OK
Starting work on lem_string_extraTheory
lem_stringTheory                                                              real:    0s  user:    0s     OK
Starting work on byteTheory
set_sepTheory                                                                 real:    3s  user:    3s     OK
Starting work on progTheory
lem_list_extraTheory                                                          real:    3s  user:    2s     OK
Starting work on README.md
README.md                                                                     real:    0s  user:    0s     OK
Starting work on addancs
addancs                                                                       real:    0s  user:    0s     OK
Starting work on astScript
astScript                                                                     real:    0s  user:    0s     OK
Starting work on fpSemTheory
lem_string_extraTheory                                                        real:    3s  user:    3s     OK
Starting work on namespaceScript
namespaceScript                                                               real:    0s  user:    0s     OK
Starting work on namespaceTheory
byteTheory                                                                    real:    3s  user:    3s     OK
Starting work on tokensScript
tokensScript                                                                  real:    0s  user:    0s     OK
Starting work on tokensTheory
progTheory                                                                    real:    3s  user:    3s     OK
Starting work on addressTheory
fpSemTheory                                                                   real:    3s  user:    3s     OK
namespaceTheory                                                               real:    2s  user:    2s     OK
Starting work on astTheory
tokensTheory                                                                  real:    4s  user:    3s     OK
Starting work on gramTheory
addressTheory                                                                 real:    6s  user:    5s     OK
Starting work on miscTheory
astTheory                                                                     real:    7s  user:    7s     OK
Starting work on semanticPrimitivesTheory
gramTheory                                                                    real:   10s  user:    9s     OK
miscTheory                                                                    real:    8s  user:    7sFAIL<1>
 l n. n  LENGTH l  REVERSE (DROP n (REVERSE l)) = TAKE (LENGTH l  n) l
 
 failed.
 Failed to prove theorem revdroprev.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 65)
 error in quse /home/myreen/regression/cakeml-1415/misc/miscScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 65)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1415/misc/miscScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 65)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 65)", origin_function = "THEN1", origin_structure = "Tactical"}
semanticPrimitivesTheory                                                                              M-KILLED