Job 884

CakeML:c0c414227216aeb093403783caa3a56449bfb337
  Extirpate intermediate theorem syntax [May 20 00:14:44]
#635 (thm)
Merging into:c3cbbfd27bd9e1f2836f8f307279178dc76ac571
  Merge pull request #650 from CakeML/tweak-how-to [May 17 12:31:32]
HOL:f6c660ddb3151f18cd07b606f2439087858abe20
  Further polish Definition documentation (incl. schematic attribute) [May 16 14:38:46]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 20 04:26:00 Claimed job
May 20 04:26:05 Reusing HOL
May 20 04:26:10 Starting developers
May 20 04:26:10 Finished developers                                               0s  22MB
May 20 04:26:11 Starting developers/bin
May 20 04:26:14 Finished developers/bin                                           3s 207MB
May 20 04:26:14 Starting semantics/ffi
May 20 04:26:22 Finished semantics/ffi                                            7s 227MB
May 20 04:26:22 Starting semantics
May 20 04:27:39 Finished semantics                                             1m16s   1GB
May 20 04:27:39 Starting semantics/proofs
May 20 04:30:36 Finished semantics/proofs                                      2m56s   1GB
May 20 04:30:37 Starting basis/pure
May 20 04:31:21 Finished basis/pure                                              43s 619MB
May 20 04:31:21 Starting translator
May 20 04:32:57 Finished translator                                            1m35s   1GB
May 20 04:32:57 Starting compiler/parsing
May 20 04:33:54 Finished compiler/parsing                                        56s   2GB
May 20 04:33:54 Starting characteristic
May 20 04:39:02 Finished characteristic                                        5m07s   2GB
May 20 04:39:03 Starting translator/monadic
May 20 04:40:27 Finished translator/monadic                                    1m23s   1GB
May 20 04:40:27 Starting basis
May 20 04:41:02 FAILED: basis
]0;Holmake: pure]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: pure]0;Holmake: ~/regression/cakeml-884/misc]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-884/misc]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-884/misc]0;Holmake: ~/regression/cakeml-884/developers]0;Holmake: ~/regression/cakeml-884/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-884/misc]0;Holmake: ~/regression/cakeml-884/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-884/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-884/misc]0;Holmake: ~/regression/cakeml-884/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: pure]0;Holmake: pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-884/characteristic]0;Holmake: ~/regression/cakeml-884/compiler/parsing]0;Holmake: ~/regression/cakeml-884/semantics]0;Holmake: ~/regression/cakeml-884/semantics/ffi]0;Holmake: ~/regression/cakeml-884/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-884/semantics]0;Holmake: ~/regression/cakeml-884/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-884/compiler/parsing]0;Holmake: ~/regression/cakeml-884/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-884/characteristic]0;Holmake: ~/regression/cakeml-884/semantics/proofs]0;Holmake: ~/regression/cakeml-884/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-884/characteristic]0;Holmake: ~/regression/cakeml-884/translator]0;Holmake: ~/regression/cakeml-884/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-884/characteristic]0;Holmake: ~/regression/cakeml-884/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-884/translator/monadic]0;Holmake: ~/regression/cakeml-884/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-884/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-884/translator/monadic]0;Holmake: ~/regression/cakeml-884/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/basis[0m
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on runtimeFFITheory
runtimeFFITheory                                                                                           OK
Starting work on README.md
README.md                                                                                                  OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                OK
MarshallingTheory                                                                                          OK
Starting work on fsFFITheory
clFFITheory                                                                                                OK
RuntimeProgTheory                                                                                          OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                           OK
Starting work on ListProgTheory
fsFFIPropsTheory                                                                                  FAILED! <1>
 Saved theorem _____ "numchars_self"
 Saved theorem _____ "nextFD_ltX"
 Saved theorem _____ "nextFD_leX"
 Saved theorem _____ "nextFD_NOT_MEM"
 Saved theorem _____ "nextFD_numchars"
 Saved theorem _____ "bumpFD_numchars"
 /home/myreen/regression/cakeml-884/basis/fsFFIPropsScript.sml:87: error: ; expected but val was found
 error in quse /home/myreen/regression/cakeml-884/basis/fsFFIPropsScript.sml : Fail "Static Errors"
 error in load fsFFIPropsScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
RuntimeProofTheory                                                                                   M-KILLED
ListProgTheory                                                                                       M-KILLED