OverviewCakeML:07bca965721baed53cea03de48b0e523ff1af007
Merge pull request #711 from CakeML/refs-unchanged
HOL:1953e213323da8b8944f33aa70644f7077326dda
Emacs mode: start of implementation of holscript-mode
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
Claimed job
Building HOL
Starting developers
Finished developers 0s 21MB
Starting developers/bin
Finished developers/bin 3s 237MB
Starting semantics/ffi
Finished semantics/ffi 7s 227MB
Starting semantics
Finished semantics 1m24s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m02s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 6s 315MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 1m58s 793MB
Starting basis/pure
Finished basis/pure 2m51s 878MB
Starting translator
Finished translator 2m27s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m07s 2GB
Starting characteristic
Finished characteristic 5m20s 2GB
Starting translator/monadic
Finished translator/monadic 1m26s 1GB
Starting basis
Finished basis 32m19s 22GB
Starting compiler/inference
Finished compiler/inference 1m43s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m00s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m08s 2GB
Starting compiler/backend
Finished compiler/backend 3m44s 2GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 19s 546MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 52s 813MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 1m38s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 29s 827MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m04s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m19s 802MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 16s 532MB
Starting compiler/backend/x64
Finished compiler/backend/x64 16s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 17s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 17s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 17s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 17s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m05s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m28s 941MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m43s 921MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 26m40s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m14s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 59m49s 16GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m07s 5GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m41s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m09s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m19s 3GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m33s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m23s 857MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 17s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 17s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 16s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 17s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 17s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 9m04s 2GB
Starting compiler/proofs
Finished compiler/proofs 2m02s 3GB
Starting candle/set-theory
Finished candle/set-theory 25s 868MB
Starting candle/syntax-lib
Finished candle/syntax-lib 9s 606MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m42s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m34s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m34s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m00s 4GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 9m15s 3GB
Starting candle/standard/opentheory/compilation
Finished candle/standard/opentheory/compilation 30m11s 9GB
Starting candle/standard/opentheory/compilation/proofs
Finished candle/standard/opentheory/compilation/proofs 45s 2GB
Starting characteristic/examples
Finished characteristic/examples 1m31s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 13m32s 6GB
Starting translator/monadic/examples
Finished translator/monadic/examples 2m52s 2GB
Starting examples
Finished examples 9m17s 3GB
Starting examples/compilation/x64
Finished examples/compilation/x64 2h05m04s 12GB
Starting examples/compilation/x64/proofs
Finished examples/compilation/x64/proofs 1m49s 2GB
Starting examples/compilation/ag32
Finished examples/compilation/ag32 29m06s 6GB
Starting examples/compilation/ag32/proofs
Finished examples/compilation/ag32/proofs 53s 2GB
Starting examples/cost
Finished examples/cost 26m53s 5GB
Starting examples/lrat_checker
Finished examples/lrat_checker 3m22s 2GB
Starting examples/lrat_checker/compilation
Finished examples/lrat_checker/compilation 15m39s 7GB
Starting examples/lrat_checker/compilation/proofs
Finished examples/lrat_checker/compilation/proofs 39s 2GB
Starting examples/lrat_checker/array
Finished examples/lrat_checker/array 6m12s 5GB
Starting examples/lrat_checker/array/compilation
Finished examples/lrat_checker/array/compilation 13m37s 9GB
Starting examples/lrat_checker/array/compilation/proofs
Finished examples/lrat_checker/array/compilation/proofs 47s 2GB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 4m09s 2GB
Starting translator/other-examples
Finished translator/other-examples 1m51s 1GB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 23s 490MB
Starting compiler/inference/tests
Finished compiler/inference/tests 4m24s 3GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 3h22m35s 45GB
Starting unverified/sexpr-bootstrap/x64/64
Finished unverified/sexpr-bootstrap/x64/64 15m08s 3GB
Starting unverified/sexpr-bootstrap/x64/32
Finished unverified/sexpr-bootstrap/x64/32 10m50s 7GB
Starting compiler/benchmarks
Finished compiler/benchmarks 37m05s 2GB
Starting compiler/bootstrap/compilation/x64/64
Finished compiler/bootstrap/compilation/x64/64 13h49m52s 64GB
Starting compiler/bootstrap/compilation/x64/64/proofs
Finished compiler/bootstrap/compilation/x64/64/proofs 2m52s 11GB
Starting compiler/bootstrap/compilation/x64/32
Finished compiler/bootstrap/compilation/x64/32 12h38m37s 64GB
Starting compiler/bootstrap/compilation/x64/32/proofs
Finished compiler/bootstrap/compilation/x64/32/proofs 4m14s 5GB
Starting compiler/bootstrap/compilation/ag32/32
Finished compiler/bootstrap/compilation/ag32/32 12h59m12s 64GB
Starting compiler/bootstrap/compilation/ag32/32/proofs
Finished compiler/bootstrap/compilation/ag32/32/proofs 33m54s 16GB
SUCCESS