Job 881

CakeML:494ff482b4d0a1cf9bc89b8d5708c38f1e51994c
  Extirpate intermediate theorem syntax [May 13 01:26:57]
#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 17 12:39:33 Claimed job
May 17 12:39:35 Reusing HOL
May 17 12:39:40 Starting developers
May 17 12:39:40 Finished developers                                               0s  23MB
May 17 12:39:41 Starting developers/bin
May 17 12:39:44 Finished developers/bin                                           2s 207MB
May 17 12:39:44 Starting semantics/ffi
May 17 12:39:52 Finished semantics/ffi                                            7s 214MB
May 17 12:39:52 Starting semantics
May 17 12:41:08 Finished semantics                                             1m15s   1GB
May 17 12:41:08 Starting semantics/proofs
May 17 12:44:04 Finished semantics/proofs                                      2m55s   1GB
May 17 12:44:04 Starting basis/pure
May 17 12:47:35 Finished basis/pure                                            3m29s 613MB
May 17 12:47:35 Starting translator
May 17 12:49:11 Finished translator                                            1m35s   1GB
May 17 12:49:11 Starting compiler/parsing
May 17 12:50:08 Finished compiler/parsing                                        56s   1GB
May 17 12:50:08 Starting characteristic
May 17 12:55:13 Finished characteristic                                        5m04s   1GB
May 17 12:55:13 Starting translator/monadic
May 17 12:56:39 Finished translator/monadic                                    1m25s   1GB
May 17 12:56:40 Starting basis
May 17 12:57:14 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-881/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-881/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-881/misc]0;Holmake: ~/regression/cakeml-881/developers]0;Holmake: ~/regression/cakeml-881/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-881/misc]0;Holmake: ~/regression/cakeml-881/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-881/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-881/misc]0;Holmake: ~/regression/cakeml-881/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: pure]0;Holmake: pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-881/characteristic]0;Holmake: ~/regression/cakeml-881/compiler/parsing]0;Holmake: ~/regression/cakeml-881/semantics]0;Holmake: ~/regression/cakeml-881/semantics/ffi]0;Holmake: ~/regression/cakeml-881/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-881/semantics]0;Holmake: ~/regression/cakeml-881/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-881/compiler/parsing]0;Holmake: ~/regression/cakeml-881/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-881/characteristic]0;Holmake: ~/regression/cakeml-881/semantics/proofs]0;Holmake: ~/regression/cakeml-881/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-881/characteristic]0;Holmake: ~/regression/cakeml-881/translator]0;Holmake: ~/regression/cakeml-881/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-881/characteristic]0;Holmake: ~/regression/cakeml-881/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-881/translator/monadic]0;Holmake: ~/regression/cakeml-881/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-881/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-881/translator/monadic]0;Holmake: ~/regression/cakeml-881/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
MarshallingTheory                                                                                                                 OK
Starting work on fsFFITheory
runtimeFFITheory                                                                                                                  OK
Starting work on README.md
README.md                                                                                                                         OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                                       OK
clFFITheory                                                                                                                       OK
RuntimeProgTheory                                                                                                                 OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                                       OK
Starting work on fsFFIPropsTheory
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-881/basis/fsFFIPropsScript.sml:87: error: ; expected but val was found
 error in quse /home/myreen/regression/cakeml-881/basis/fsFFIPropsScript.sml : Fail "Static Errors"
 error in load fsFFIPropsScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
OptionProgTheory                                                                                                            M-KILLED
RuntimeProofTheory                                                                                                          M-KILLED