Overview

Job 430

CakeML:42c919452dd418e7f3f60eec74e38fb6a9cc9d41
  Rename `flag` configuration type to `flagConf`
#511 (argparse)
Merging into:348a74050804214128ce62f0274f4443cc6730dd
  Remove exhProps
HOL:b4b8e85c8559502f116df8acd4f6cbb3c390263b
  Don't export ERR from HolKernel
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers/bin
 Finished developers/bin                                           8s 142MB
 Starting semantics/ffi
 Finished semantics/ffi                                         1m01s 379MB
 Starting semantics
 Finished semantics                                             2m30s 795MB
 Starting semantics/proofs
 Finished semantics/proofs                                      5m14s   1GB
 Starting basis/pure
 Finished basis/pure                                            5m46s 610MB
 Starting translator
 FAILED: translator
]0;Holmake: ../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-b4b8e85c8559502f116df8acd4f6cbb3c390263b/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_pmatch_demoTheory                                                                                                                             FAILED! <1>
 /scratch/cakeml/regression/cakeml-430/basis/pure/mlvectorSyntax.sml:11: error: Value or constructor (ERR) has not been declared
 Found near raise ERR "dest_vector_type" ""
 error in quse /scratch/cakeml/regression/cakeml-430/basis/pure/mlvectorSyntax.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/basis/pure/mlvectorSyntax : 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