Job 726

CakeML:479eb999b0103028858ceaea4488ee1ba981a551
  Fix generated readme [Feb 11 17:43:36]
HOL:f535214bfea72da93f045caf3e8a2e2a485bed6f
  Add theory presenting abstract view of computation states [Feb 14 10:59:58]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 15 13:45:09 Claimed job
Feb 15 13:45:21 Building HOL
Feb 15 13:52:59 Starting developers
Feb 15 13:53:00 Finished developers                                               0s  22MB
Feb 15 13:53:00 Starting developers/bin
Feb 15 13:53:32 Finished developers/bin                                          30s 205MB
Feb 15 13:53:33 Starting semantics/ffi
Feb 15 13:54:06 Finished semantics/ffi                                           32s 420MB
Feb 15 13:54:07 Starting semantics
Feb 15 13:55:37 Finished semantics                                             1m28s   1GB
Feb 15 13:55:38 Starting semantics/proofs
Feb 15 13:58:35 Finished semantics/proofs                                      2m57s   1GB
Feb 15 13:58:36 Starting basis/pure
Feb 15 14:02:09 Finished basis/pure                                            3m31s 823MB
Feb 15 14:02:10 Starting translator
Feb 15 14:03:15 FAILED: translator
]0;Holmake: ~/regression/cakeml-726/basis/pure]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-726/basis/pure]0;Holmake: ~/regression/cakeml-726/misc]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-726/misc]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-726/misc]0;Holmake: ~/regression/cakeml-726/developers]0;Holmake: ~/regression/cakeml-726/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-726/misc]0;Holmake: ~/regression/cakeml-726/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-726/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-726/misc]0;Holmake: ~/regression/cakeml-726/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-726/basis/pure]0;Holmake: ~/regression/cakeml-726/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-726/semantics]0;Holmake: ~/regression/cakeml-726/semantics/ffi]0;Holmake: ~/regression/cakeml-726/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-726/semantics]0;Holmake: ~/regression/cakeml-726/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-726/semantics/proofs]0;Holmake: ~/regression/cakeml-726/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator[0m
Starting work on ml_progTheory
Starting work on README.md
README.md                                           OK
ml_progTheory                                       OK
Starting work on ml_translatorTheory
ml_translatorTheory                                 OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_pmatchTheory                                     OK
ml_optimiseTheory                                   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                       FAILED! <1>
 /home/myreen/regression/cakeml-726/translator/ml_translatorLib.sml:3893: error: Type error in function application.
    Function: List.map (rand o rator o fst o dest_eq) : term list -> term list
    Argument: lcs : ''a list
    Reason: Can't unify term to ''a (Requires equality type)
 Found near
   List.filter (can dest_var) (List.map (... o ... o fst o dest_eq) lcs)
 error in quse /home/myreen/regression/cakeml-726/translator/ml_translatorLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/translator/ml_translatorLib : Fail "Static Errors"
 error in load 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