Job 140

CakeML:a696379561e163af05c38d6212e3f280081df7e4
  Fixed isSubString so that it finds suffixes. [Jan 05 05:05:01]
#422 (master)
Merging into:00605b2ed98e568aeec57b47a504daab27e5ce8b
  Add missing comma [Jan 06 12:42:45]
HOL:95995a06a5b32c848273aeab7a2cb7c184c66b44
  Merge branch 'pr/506' into master [Jan 08 04:24:55]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Jan 08 19:46:25 Claimed job
Jan 08 19:46:34 Building HOL
Jan 08 19:59:02 Starting semantics/ffi
Jan 08 20:00:11 Finished semantics/ffi                                         1m06s 334MB
Jan 08 20:00:13 Starting semantics
Jan 08 20:02:51 Finished semantics                                             2m35s 901MB
Jan 08 20:02:53 Starting semantics/proofs
Jan 08 20:06:25 Finished semantics/proofs                                      3m29s   1GB
Jan 08 20:06:27 Starting basis/pure
Jan 08 20:12:24 Finished basis/pure                                            5m55s 630MB
Jan 08 20:12:26 Starting translator
Jan 08 20:19:36 Finished translator                                            7m07s 972MB
Jan 08 20:19:38 Starting compiler/parsing
Jan 08 20:22:01 Finished compiler/parsing                                      2m20s   1GB
Jan 08 20:22:03 Starting characteristic
Jan 08 20:26:41 Finished characteristic                                        4m36s   1GB
Jan 08 20:26:43 Starting basis
Jan 08 20:30:45 FAILED: basis
]0;Holmake: pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/formal-languages/regular
]0;Holmake: pureRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-95995a06a5b32c848273aeab7a2cb7c184c66b44/examples/machine-code/hoare-triple
]0;Holmake: ../miscRecursively calling Holmake in ../developers
]0;Holmake: ../developers]0;Holmake: ../developersFinished recursive invocation in ../developers
]0;Holmake: ../miscRecursively calling Holmake in ../misc/lem_lib_stub
]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stubFinished recursive invocation in ../misc/lem_lib_stub
]0;Holmake: ../misc]0;Holmake: ../miscFinished recursive invocation in ../misc
]0;Holmake: pure]0;Holmake: pureFinished recursive invocation in pure
]0;Holmake: .Recursively calling Holmake in ../characteristic
]0;Holmake: ../characteristicRecursively calling Holmake in ../compiler/parsing
]0;Holmake: ../compiler/parsingRecursively calling Holmake in ../semantics
]0;Holmake: ../semanticsRecursively calling Holmake in ../semantics/ffi
]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffiFinished recursive invocation in ../semantics/ffi
]0;Holmake: ../semantics]0;Holmake: ../semanticsFinished recursive invocation in ../semantics
]0;Holmake: ../compiler/parsing]0;Holmake: ../compiler/parsingFinished recursive invocation in ../compiler/parsing
]0;Holmake: ../characteristicRecursively calling Holmake in ../semantics/alt_semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsFinished recursive invocation in ../semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/proofs
]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsFinished recursive invocation in ../semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsFinished recursive invocation in ../semantics/alt_semantics/proofs
]0;Holmake: ../characteristicRecursively calling Holmake in ../translator
]0;Holmake: ../translator]0;Holmake: ../translatorFinished recursive invocation in ../translator
]0;Holmake: ../characteristic]0;Holmake: ../characteristicFinished recursive invocation in ../characteristic
]0;Holmake: .]0;Holmake: .Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on fsFFITheory
Starting work on basis_ffi.o
basis_ffi.o                                                                  OK
clFFITheory                                                                  OK
RuntimeProgTheory                                                            OK
Starting work on OptionProgTheory
fsFFITheory                                                                  OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                             OK
Starting work on ListProgTheory
fsFFIPropsTheory                                                             OK
ListProgTheory                                                               OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                              OK
VectorProgTheory                                                             OK
Starting work on StringProgTheory
StringProgTheory                                                    FAILED! <1>
 s1 s2. issubstring_side s1 s2
 
 failed.
 error in quse /scratch/cakeml/regression/cakeml-140/basis/StringProgScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load StringProgScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 First unsolved sub-goal is
 
 issubstring_aux_side s1 s2 (strlen s1) 0 (strlen s2 + 1  strlen s1)