OverviewCakeML:bc1d24030a96270694c72cff1c37f656c1e85a9f
Disambiguate some terms
HOL:e29e41f2928e541b5157935a1f289cb29f9a32d4
Improve build's behaviour when user's c/line options are bad
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 104MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 239MB
Starting semantics
Finished semantics 1m24s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m38s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 9s 282MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m15s 798MB
Starting basis/pure
Finished basis/pure 51s 862MB
Starting translator
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: 17s user: 16s 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_pmatch_demoTheory real: 10s user: 8sFAIL<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-1381/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-1381/translator/ml_pmatch_demoScript : Fail "Static Errors"
Uncaught exception: Fail "Static Errors"
ml_module_demoTheory M-KILLED
ml_translator_demoTheory M-KILLED
ml_translator_testTheory M-KILLED