CakeML:1b5f8be3242a8a1d13d1289f21c06650fb5eb463
Update translator for new length check
HOL:2abaf720bc88c75a793eac0e280e392479d1745e
Let ANSI colouring happen on screen terminals
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers/bin
Finished developers/bin 3s 150MB
Starting semantics/ffi
Finished semantics/ffi 9s 268MB
Starting semantics
Finished semantics 1m11s 962MB
Starting semantics/proofs
Finished semantics/proofs 2m46s 1GB
Starting basis/pure
Finished basis/pure 50s 815MB
Starting translator
FAILED: translator
]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/formal-languages]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developers[1mWorking in ../developers[0m
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../misc]0;Holmake: ../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator[0m
Starting work on heap
heap OK
Starting work on ml_progTheory
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_translator_demoTheory FAILED! <1>
Cannot find file /home/myreen/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/sigobj/holmake_not_interactive.ui
error in load /home/myreen/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/sigobj/holmake_not_interactive : Fail "Cannot find file /home/myreen/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/sigobj/holmake_not_interactive.ui"
Uncaught exception: Fail "Cannot find file /home/myreen/regression/HOL-2abaf720bc88c75a793eac0e280e392479d1745e/sigobj/holmake_not_interactive.ui"
ml_module_demoTheory M-KILLED
ml_pmatch_demoTheory M-KILLED
ml_translator_testTheory M-KILLED