Job 1380

CakeML:05bb6c4ce145c198ba5bfe7ff8e609d2d64d530a
  Minor tweaks [Oct 21 12:39:26]
#802 (data-cost)
Merging into:bc1d24030a96270694c72cff1c37f656c1e85a9f
  Disambiguate some terms [Oct 16 13:02:29]
HOL:e29e41f2928e541b5157935a1f289cb29f9a32d4
  Improve build's behaviour when user's c/line options are bad [Oct 23 00:01:00]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Oct 26 10:20:21 Claimed job
Oct 26 10:20:30 Building HOL
Oct 26 10:35:53 Starting developers
Oct 26 10:35:58 Finished developers                                               4s 113MB
Oct 26 10:35:58 Starting developers/bin
Oct 26 10:36:05 Finished developers/bin                                           6s   1GB
Oct 26 10:36:05 Starting semantics/ffi
Oct 26 10:36:16 Finished semantics/ffi                                           11s 229MB
Oct 26 10:36:16 Starting semantics
Oct 26 10:37:51 Finished semantics                                             1m34s   1GB
Oct 26 10:37:52 Starting semantics/proofs
Oct 26 10:41:25 Finished semantics/proofs                                      3m33s   1GB
Oct 26 10:41:26 Starting semantics/alt_semantics
Oct 26 10:41:35 Finished semantics/alt_semantics                                  9s 247MB
Oct 26 10:41:35 Starting semantics/alt_semantics/proofs
Oct 26 10:43:49 Finished semantics/alt_semantics/proofs                        2m13s 816MB
Oct 26 10:43:50 Starting basis/pure
Oct 26 10:46:54 Finished basis/pure                                            3m04s 832MB
Oct 26 10:46:54 Starting translator
Oct 26 10:48:16 FAILED: translator
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Starting work on README.md
Starting work on ml_progTheory
README.md                                       real:    0s  user:    0s     OK
ml_progTheory                                   real:   16s  user:   15s     OK
Starting work on ml_translatorTheory
ml_translatorTheory                             real:   36s  user:   35s     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_pmatchTheory                                 real:   15s  user:   14s     OK
ml_optimiseTheory                               real:   17s  user:   16s     OK
Starting work on ml_module_demoTheory
Starting work on ml_pmatch_demoTheory
Starting work on ml_translator_demoTheory
Starting work on ml_translator_testTheory
ml_module_demoTheory                            real:   10s  user:    9sFAIL<1>
    Reason:
       Can't unify term (*Created from opaque signature*) with
          'a option (*In Basis*) (Different type constructors)
 Found near
   cert |> DISCH lookup_var_hyp |> GEN env_tm |>
   MATCH_MP Eval_Var_LOOKUP_VAR_elim
 error in quse /home/cake/oven/regression/cakeml-1380/translator/ml_translatorLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/translator/ml_translatorLib : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1380/translator/ml_module_demoScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
ml_pmatch_demoTheory                                                    M-KILLED
ml_translator_demoTheory                                                M-KILLED
ml_translator_testTheory                                                M-KILLED