Job 1059

CakeML:7a02513c65a386bede9403ea7b0038a034c68fff
  Fix cmlPtreeConversionProps proof broken by infix change [Oct 31 01:12:31]
#695 (ocaml-infixes)
Merging into:dc73bd8f21601e06bdc92eb303865a3992673970
  Merge pull request #694 from CakeML/remove-oom [Oct 13 07:36:28]
HOL:f11debc0b86c4c7bb97d340bf5ace2f75d4c69fd
  Holmake: key monitor function on combination of PID and tag-string [Oct 30 11:27:47]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Oct 31 01:50:51 Claimed job
Oct 31 01:50:53 Reusing HOL
Oct 31 01:51:44 Starting developers
Oct 31 01:51:47 Finished developers                                               3s 116MB
Oct 31 01:51:48 Starting developers/bin
Oct 31 01:51:53 Finished developers/bin                                           5s 964MB
Oct 31 01:51:53 Starting semantics/ffi
Oct 31 01:52:02 Finished semantics/ffi                                            9s 230MB
Oct 31 01:52:03 Starting semantics
Oct 31 01:53:17 Finished semantics                                             1m13s   1GB
Oct 31 01:53:17 Starting semantics/proofs
Oct 31 01:56:06 Finished semantics/proofs                                      2m48s 930MB
Oct 31 01:56:06 Starting semantics/alt_semantics
Oct 31 01:56:13 Finished semantics/alt_semantics                                  7s 324MB
Oct 31 01:56:13 Starting semantics/alt_semantics/proofs
Oct 31 01:57:56 Finished semantics/alt_semantics/proofs                        1m42s   1GB
Oct 31 01:57:56 Starting basis/pure
Oct 31 02:00:31 Finished basis/pure                                            2m34s 824MB
Oct 31 02:00:31 Starting translator
Oct 31 02:02:14 Finished translator                                            1m42s   1GB
Oct 31 02:02:14 Starting compiler/parsing
Oct 31 02:03:14 Finished compiler/parsing                                        59s   2GB
Oct 31 02:03:14 Starting characteristic
Oct 31 02:08:21 Finished characteristic                                        5m07s   1GB
Oct 31 02:08:21 Starting translator/monadic
Oct 31 02:09:45 Finished translator/monadic                                    1m24s   1GB
Oct 31 02:09:46 Starting basis
Oct 31 02:17:55 FAILED: basis
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md                                       real:    0s  user:    0s     OK
Starting work on runtimeFFITheory
MarshallingTheory                               real:    9s  user:    9s     OK
Starting work on fsFFITheory
runtimeFFITheory                                real:    9s  user:    8s     OK
Starting work on basis_ffi.o
basis_ffi.o                                     real:    0s  user:    0s     OK
clFFITheory                                     real:   10s  user:    9s     OK
RuntimeProgTheory                               real:   21s  user:   20s     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                     real:   14s  user:   13s     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                real:   13s  user:   13s     OK
Starting work on ListProgTheory
RuntimeProofTheory                              real:   22s  user:   21s     OK
fsFFIPropsTheory                                real:   48s  user:   47s     OK
ListProgTheory                                  real:   38s  user:   37s     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                 real:   23s  user:   22s     OK
VectorProgTheory                                real:   27s  user:   26s     OK
Starting work on StringProgTheory
StringProgTheory                                real:   31s  user:   29s     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                              real:   34s  user:   33s     OK
Starting work on IntProgTheory
IntProgTheory                                   real:   31s  user:   30s     OK
Starting work on RatProgTheory
RatProgTheory                                   real:   38s  user:   36s     OK
Starting work on CharProgTheory
CharProgTheory                                  real:   23s  user:   22s     OK
Starting work on Word64ProgTheory
Word64ProgTheory                                real:   27s  user:   26s     OK
Starting work on Word8ProgTheory
Word8ProgTheory                                 real:   23s  user:   22s     OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory                            real:   26s  user:   25s     OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory                           real:   38s  user:   37s     OK
ArrayProgTheory                                 real:   74s  user:   72s     OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory                                   real:   48s  user:   46s     OK
Starting work on HashtableProgTheory
ArrayProofTheory                                real:   67s  user:   66s     OK
HashtableProgTheory                             real:   26s  user:   25sFAIL<1>
 <<HOL message: Created theory "HashtableProg">>
 Loading translation: MapProg ... done.
 Saved theorem _____ "nsLookup_HashtableProg_env_pfun_eqs"
 error in quse /home/cur/sao/cakeml/regression/cakeml-1059/basis/HashtableProgScript.sml : HOL_ERR {message = "not terminated with nil", origin_function = "dest_list", origin_structure = "listSyntax"}
 error in load /home/cur/sao/cakeml/regression/cakeml-1059/basis/HashtableProgScript : HOL_ERR {message = "not terminated with nil", origin_function = "dest_list", origin_structure = "listSyntax"}
 Uncaught exception: HOL_ERR {message = "not terminated with nil", origin_function = "dest_list", origin_structure = "listSyntax"}