OverviewCakeML:42c919452dd418e7f3f60eec74e38fb6a9cc9d41
Rename `flag` configuration type to `flagConf`
#511 (argparse)
Merging into:348a74050804214128ce62f0274f4443cc6730dd
Remove exhProps
HOL:44b4d95a0dee002148eab60371346d0360517c5d
Define longest_prefix and common_prefixes (over sets of lists)
Machine:oven1 (2) 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers/bin
Finished developers/bin 35s 911MB
Starting semantics/ffi
Finished semantics/ffi 11s 254MB
Starting semantics
Finished semantics 1m10s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m40s 1GB
Starting basis/pure
Finished basis/pure 50s 633MB
Starting translator
Finished translator 1m34s 890MB
Starting compiler/parsing
Finished compiler/parsing 1m32s 1GB
Starting characteristic
Finished characteristic 2m21s 1GB
Starting translator/monadic
Finished translator/monadic 1m26s 1GB
Starting basis
Finished basis 18m00s 5GB
Starting compiler/inference
Finished compiler/inference 1m24s 923MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 32s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 7m44s 3GB
Starting compiler/backend
Finished compiler/backend 2s 13MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 1s 11MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 16s 424MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 43s 436MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 7s 382MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 9s 471MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 8s 441MB
Starting compiler/backend/x64
Finished compiler/backend/x64 18s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 19s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 18s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 18s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 19s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 6m08s 776MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m47s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 8m55s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 47s 614MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 35m08s 4GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 6m08s 1GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 6m19s 1GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 5m08s 968MB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 6m51s 1GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 7m53s 827MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 19s 745MB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 22s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 18s 819MB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 20s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 19s 1GB
Starting compiler/proofs
Finished compiler/proofs 1m21s 2GB
Starting candle/set-theory
Finished candle/set-theory 25s 590MB
Starting candle/syntax-lib
Finished candle/syntax-lib 10s 521MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m32s 643MB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m19s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m24s 846MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 3m27s 2GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 14s 677MB
Starting characteristic/examples
Finished characteristic/examples 1m41s 2GB
Starting tutorial/solutions
Finished tutorial/solutions 14m43s 6GB
Starting translator/monadic/examples
Finished translator/monadic/examples 1m49s 3GB
Starting examples
FAILED: examples
]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/formal-languages]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/formal-languages/context-free]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ../basis]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../misc]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/examples/machine-code/hoare-triple]0;Holmake: ~/regression_2/HOL-44b4d95a0dee002148eab60371346d0360517c5d/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: ../basis]0;Holmake: ../characteristic]0;Holmake: ../compiler/parsing]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: ../compiler/parsing]0;Holmake: ../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../characteristic]0;Holmake: ../translator]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../translator]0;Holmake: ../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../characteristic]0;Holmake: ../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../basis]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../basis]0;Holmake: ../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on heap
Starting work on README.md
README.md OK
heap OK
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on echoProgTheory
Starting work on grepProgTheory
lcsTheory OK
Starting work on diffTheory
echoProgTheory OK
Starting work on helloErrProgTheory
diffTheory OK
Starting work on diffProgTheory
catProgTheory OK
Starting work on helloProgTheory
helloErrProgTheory OK
Starting work on insertSortProgTheory
helloProgTheory OK
Starting work on iocatProgTheory
grepProgTheory FAILED! <1>
Saved theorem _____ "regexp_matcher_with_limit_v_thm"
Saved theorem _____ "tolist_fromlist_map_cancel"
Updating regexp_matcher_with_limit_v_thm
Saved theorem _____ "regexp_matcher_with_limit_v_thm"
Saved theorem _____ "regexp_matcher_correct"
Saved theorem _____ "INTRO_FLOOKUP"
Translating coreloop_1
error in quse /home/cake/regression_2/cakeml-428/examples/grepProgScript.sml : HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
error in load grepProgScript : HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
Uncaught exception: HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
diffProgTheory M-KILLED
insertSortProgTheory M-KILLED
iocatProgTheory M-KILLED