Job 877

CakeML:494ff482b4d0a1cf9bc89b8d5708c38f1e51994c
  Extirpate intermediate theorem syntax [May 13 01:26:57]
#635 (thm)
Merging into:8f8560b3414274dcffa62719ba224df92d8cb039
  Merge pull request #651 from talsewell/translator_messages [May 15 03:55:41]
HOL:f6c660ddb3151f18cd07b606f2439087858abe20
  Further polish Definition documentation (incl. schematic attribute) [May 16 14:38:46]
Machine:brain12 4.14.89.1.amd64-smp x86_64 GNU/Linux

May 17 08:50:08 Claimed job
May 17 08:50:15 Building HOL
May 17 09:06:23 Starting developers
May 17 09:06:26 Finished developers                                               2s  32MB
May 17 09:06:26 Starting developers/bin
May 17 09:06:36 Finished developers/bin                                           9s 923MB
May 17 09:06:36 Starting semantics/ffi
May 17 09:07:45 Finished semantics/ffi                                         1m08s 497MB
May 17 09:07:45 Starting semantics
May 17 09:10:44 Finished semantics                                             2m58s   1GB
May 17 09:10:44 Starting semantics/proofs
May 17 09:16:50 Finished semantics/proofs                                      6m05s   1GB
May 17 09:16:50 Starting basis/pure
May 17 09:23:52 Finished basis/pure                                            7m01s   1GB
May 17 09:23:52 Starting translator
May 17 09:27:09 Finished translator                                            3m15s   1GB
May 17 09:27:09 Starting compiler/parsing
May 17 09:29:06 Finished compiler/parsing                                      1m57s   2GB
May 17 09:29:06 Starting characteristic
May 17 09:39:53 Finished characteristic                                       10m46s   1GB
May 17 09:39:54 Starting translator/monadic
May 17 09:42:45 Finished translator/monadic                                    2m51s   1GB
May 17 09:42:45 Starting basis
May 17 09:43:58 FAILED: basis
]0;Holmake: pure]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/context-free]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
Starting work on regexp2dfa
regexp2dfa                                                                                                                       OK
]0;Holmake: pure]0;Holmake: /local/hbecker/regression/cakeml-877/misc]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: /local/hbecker/regression/cakeml-877/misc]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: /local/hbecker/regression/cakeml-877/misc]0;Holmake: /local/hbecker/regression/cakeml-877/developers]0;Holmake: /local/hbecker/regression/cakeml-877/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: /local/hbecker/regression/cakeml-877/misc]0;Holmake: /local/hbecker/regression/cakeml-877/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/cakeml-877/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: /local/hbecker/regression/cakeml-877/misc]0;Holmake: /local/hbecker/regression/cakeml-877/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: pure]0;Holmake: pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: /local/hbecker/regression/cakeml-877/characteristic]0;Holmake: /local/hbecker/regression/cakeml-877/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-877/semantics]0;Holmake: /local/hbecker/regression/cakeml-877/semantics/ffi]0;Holmake: /local/hbecker/regression/cakeml-877/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: /local/hbecker/regression/cakeml-877/semantics]0;Holmake: /local/hbecker/regression/cakeml-877/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: /local/hbecker/regression/cakeml-877/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-877/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: /local/hbecker/regression/cakeml-877/characteristic]0;Holmake: /local/hbecker/regression/cakeml-877/semantics/proofs]0;Holmake: /local/hbecker/regression/cakeml-877/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: /local/hbecker/regression/cakeml-877/characteristic]0;Holmake: /local/hbecker/regression/cakeml-877/translator]0;Holmake: /local/hbecker/regression/cakeml-877/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: /local/hbecker/regression/cakeml-877/characteristic]0;Holmake: /local/hbecker/regression/cakeml-877/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: .]0;Holmake: /local/hbecker/regression/cakeml-877/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-877/translator/monadic/monad_base]0;Holmake: /local/hbecker/regression/cakeml-877/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: /local/hbecker/regression/cakeml-877/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-877/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/basis
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"
 error in quse /local/hbecker/regression/cakeml-877/basis/fsFFIPropsScript.sml : Fail "Static Errors"
 error in load fsFFIPropsScript : Fail "Static Errors"
 Saved theorem _____ "bumpFD_numchars"
 /local/hbecker/regression/cakeml-877/basis/fsFFIPropsScript.sml:87: error: ; expected but val was found
 Uncaught exception: Fail "Static Errors"
OptionProgTheory                                                                                                           M-KILLED
RuntimeProofTheory                                                                                                         M-KILLED