OverviewCakeML:26f4bae8dd00abd7a5ed6212dd12cda0d3d99af5
Fix name changes due to previous commit
#688 (issue683)
Merging into:67adb612363d45c5e20127cef6b64a9d3ad43081
Make some disruptive overloads local
HOL:4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6
upgraded regexp compiler to use binary-map set to represent worklist;
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 0s 19MB
Starting developers/bin
Finished developers/bin 1m31s 164MB
Starting semantics/ffi
Finished semantics/ffi 8s 216MB
Starting semantics
Finished semantics 1m16s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m54s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 5s 293MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 1m45s 854MB
Starting basis/pure
Finished basis/pure 44s 774MB
Starting translator
Finished translator 1m43s 1GB
Starting compiler/parsing
Finished compiler/parsing 55s 1GB
Starting characteristic
Finished characteristic 5m08s 1GB
Starting translator/monadic
Finished translator/monadic 1m22s 1GB
Starting basis
Finished basis 19m34s 3GB
Starting compiler/inference
Finished compiler/inference 1m35s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 58s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 7m56s 1GB
Starting compiler/backend
Finished compiler/backend 0s 45MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 35MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 22s 703MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 44s 708MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 11s 556MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 14s 801MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 13s 804MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 14s 757MB
Starting compiler/backend/x64
Finished compiler/backend/x64 15s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 16s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 15s 932MB
Starting compiler/backend/mips
Finished compiler/backend/mips 16s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 15s 862MB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m05s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m33s 822MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m38s 966MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 5m51s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m09s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 39m44s 3GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 8m58s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m02s 2GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m25s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m14s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m17s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m27s 801MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 16s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 16s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 15s 754MB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 17s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 16s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 8m45s 2GB
Starting compiler/proofs
Finished compiler/proofs 1m28s 2GB
Starting candle/set-theory
Finished candle/set-theory 25s 747MB
Starting candle/syntax-lib
Finished candle/syntax-lib 8s 580MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m38s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m31s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m31s 1GB
Starting candle/standard/ml_kernel
FAILED: candle/standard/ml_kernel
]0;Holmake: ~/regression/cakeml-1029/basis/pure]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-1029/basis/pure]0;Holmake: ~/regression/cakeml-1029/misc]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-1029/misc]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-1029/misc]0;Holmake: ~/regression/cakeml-1029/developers]0;Holmake: ~/regression/cakeml-1029/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-1029/misc]0;Holmake: ~/regression/cakeml-1029/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1029/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1029/misc]0;Holmake: ~/regression/cakeml-1029/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-1029/basis/pure]0;Holmake: ~/regression/cakeml-1029/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-1029/basis]0;Holmake: ~/regression/cakeml-1029/characteristic]0;Holmake: ~/regression/cakeml-1029/compiler/parsing]0;Holmake: ~/regression/cakeml-1029/semantics]0;Holmake: ~/regression/cakeml-1029/semantics/ffi]0;Holmake: ~/regression/cakeml-1029/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-1029/semantics]0;Holmake: ~/regression/cakeml-1029/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-1029/compiler/parsing]0;Holmake: ~/regression/cakeml-1029/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-1029/characteristic]0;Holmake: ~/regression/cakeml-1029/semantics/proofs]0;Holmake: ~/regression/cakeml-1029/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-1029/characteristic]0;Holmake: ~/regression/cakeml-1029/translator]0;Holmake: ~/regression/cakeml-1029/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-1029/characteristic]0;Holmake: ~/regression/cakeml-1029/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-1029/basis]0;Holmake: ~/regression/cakeml-1029/translator/monadic]0;Holmake: ~/regression/cakeml-1029/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-1029/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-1029/translator/monadic]0;Holmake: ~/regression/cakeml-1029/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-1029/basis]0;Holmake: ~/regression/cakeml-1029/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../monadic]0;Holmake: ../syntax]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-lib[1mWorking in $(CAKEMLDIR)/candle/syntax-lib[0m
]0;Holmake: ../syntax]0;Holmake: ../syntax[1mWorking in $(CAKEMLDIR)/candle/standard/syntax[0m
]0;Holmake: ../monadic]0;Holmake: ../monadic[1mWorking in $(CAKEMLDIR)/candle/standard/monadic[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/candle/standard/ml_kernel[0m
Starting work on ml_hol_kernelProgTheory
Starting work on README.md
README.md OK
ml_hol_kernelProgTheory FAILED! <1>
Instantiated polymorphic monadic exceptions
Translating context
Adding nsLookup representation thms for [ml_hol_kernelProg_env_107]
Saved theorem _____ "nsLookup_ml_hol_kernelProg_env_108_pfun_eqs"
Saved theorem _____ "context_v_thm"
Saved theorem _____ "nsLookup_ml_hol_kernelProg_env_109_pfun_eqs"
Saved theorem _____ "candle_prog_thm"
error in quse /home/myreen/regression/cakeml-1029/candle/standard/ml_kernel/ml_hol_kernelProgScript.sml : UnsupportedType ?
error in load ml_hol_kernelProgScript : UnsupportedType ?
Uncaught exception: UnsupportedType ?