Job 779

CakeML:a478fddb6f76220d45e0ec482d4cb75e4913fdf8
  Fix for removal of script-file new_attribute fn [Apr 08 07:26:54]
#625 (thm-attribute-fix)
Merging into:ab7ea440afff89d5f90e2b85415c2e27f7894561
  Use Theory.current_definitions instead of fetch [Apr 10 09:36:45]
HOL:729baf5e526741114f4346767d17d0da3a1b6c20
  Remove (generated file) Thm-sig.sml when cleaning src/thm [Apr 07 04:31:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 10 09:45:47 Claimed job
Apr 10 09:45:51 Reusing HOL
Apr 10 09:46:38 Starting developers
Apr 10 09:46:40 Finished developers                                               2s  21MB
Apr 10 09:46:41 Starting developers/bin
Apr 10 09:47:54 Finished developers/bin                                        1m13s 918MB
Apr 10 09:47:55 Starting semantics/ffi
Apr 10 09:48:05 Finished semantics/ffi                                            9s 224MB
Apr 10 09:48:05 Starting semantics
Apr 10 09:49:26 Finished semantics                                             1m20s   1GB
Apr 10 09:49:26 Starting semantics/proofs
Apr 10 09:52:20 Finished semantics/proofs                                      2m53s   1GB
Apr 10 09:52:20 Starting basis/pure
Apr 10 09:53:08 Finished basis/pure                                              47s 814MB
Apr 10 09:53:08 Starting translator
Apr 10 09:54:47 Finished translator                                            1m38s   1GB
Apr 10 09:54:47 Starting compiler/parsing
Apr 10 09:55:44 Finished compiler/parsing                                        56s   3GB
Apr 10 09:55:45 Starting characteristic
Apr 10 10:00:58 Finished characteristic                                        5m13s   1GB
Apr 10 10:00:59 Starting translator/monadic
Apr 10 10:02:25 Finished translator/monadic                                    1m26s   1GB
Apr 10 10:02:25 Starting basis
Apr 10 10:02:45 FAILED: basis
]0;Holmake: pure]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: pure]0;Holmake: ~/oven/regression/cakeml-779/misc]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-779/misc]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-779/misc]0;Holmake: ~/oven/regression/cakeml-779/developers]0;Holmake: ~/oven/regression/cakeml-779/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-779/misc]0;Holmake: ~/oven/regression/cakeml-779/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-779/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-779/misc]0;Holmake: ~/oven/regression/cakeml-779/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: pure]0;Holmake: pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-779/characteristic]0;Holmake: ~/oven/regression/cakeml-779/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-779/semantics]0;Holmake: ~/oven/regression/cakeml-779/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-779/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-779/semantics]0;Holmake: ~/oven/regression/cakeml-779/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-779/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-779/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-779/characteristic]0;Holmake: ~/oven/regression/cakeml-779/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-779/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-779/characteristic]0;Holmake: ~/oven/regression/cakeml-779/translator]0;Holmake: ~/oven/regression/cakeml-779/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-779/characteristic]0;Holmake: ~/oven/regression/cakeml-779/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-779/translator/monadic]0;Holmake: ~/oven/regression/cakeml-779/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-779/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-779/translator/monadic]0;Holmake: ~/oven/regression/cakeml-779/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                                                   FAILED! <1>
    Argument: (mk_export_f add_match_thms) :
       string -> (string * thm) list -> unit
    Reason: Value being applied does not have a function type
 Found near
   ThmSetData.new_exporter "xlet_auto_match" (mk_export_f add_match_thms)
 error in quse /home/cake/oven/regression/cakeml-779/characteristic/cfLetAutoLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/characteristic/cfLetAutoLib : Fail "Static Errors"
 error in load $(CAKEMLDIR)/characteristic/cfLib : Fail "Static Errors"
 error in load RuntimeProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
fsFFITheory                                                            M-KILLED