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