CakeML:33e99acd8473d0f3b26811cff129818bb6b04743 Merge pull request #545 from CakeML/explorerHOL:06df083877b529892a4a72756c28eadd543bb754 Add fold to sptree and a few lemmas about sizeMachine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/LinuxArtefacts:cake-unverified-x64-64.tar.gz cake-unverified-x64-32.tar.gz cake-x64-64.tar.gz cake-x64-32.tar.gz Claimed job Reusing HOL Starting developers/bin Finished developers/bin 1m11s 914MB Starting semantics/ffi Finished semantics/ffi 11s 248MB Starting semantics Finished semantics 1m12s 767MB Starting semantics/proofs Finished semantics/proofs 2m41s 1GB Starting basis/pure Finished basis/pure 49s 666MB Starting translator Finished translator 3m00s 1GB Starting compiler/parsing Finished compiler/parsing 1m14s 1GB Starting characteristic Finished characteristic 2m28s 1GB Starting translator/monadic Finished translator/monadic 1m23s 1GB Starting basis Finished basis 16m30s 3GB Starting compiler/inference Finished compiler/inference 1m41s 1GB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 47s 1GB Starting compiler/backend/gc Finished compiler/backend/gc 7m13s 1GB Starting compiler/backend Finished compiler/backend 3s 16MB Starting compiler/encoders/asm Finished compiler/encoders/asm 1s 14MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 51s 609MB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 1m42s 1GB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 25s 492MB Starting compiler/encoders/mips Finished compiler/encoders/mips 58s 766MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 1m00s 889MB Starting compiler/backend/x64 Finished compiler/backend/x64 17s 867MB Starting compiler/backend/arm6 Finished compiler/backend/arm6 20s 972MB 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 18s 1GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 6m05s 779MB Starting compiler/inference/proofs Finished compiler/inference/proofs 2m49s 1GB Starting compiler/backend/semantics Finished compiler/backend/semantics 8m49s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 7m12s 547MB Starting compiler/backend/proofs Finished compiler/backend/proofs 40m33s 3GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 7m20s 4GB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 7m32s 3GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 5m24s 951MB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 7m22s 1GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 7m52s 784MB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 20s 1GB Starting compiler/backend/arm6/proofs Finished compiler/backend/arm6/proofs 23s 1GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 20s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 20s 925MB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 20s 1GB Starting compiler/proofs Finished compiler/proofs 1m20s 2GB Starting candle/set-theory Finished candle/set-theory 25s 603MB Starting candle/syntax-lib Finished candle/syntax-lib 10s 662MB Starting candle/standard/syntax Finished candle/standard/syntax 1m32s 664MB Starting candle/standard/semantics Finished candle/standard/semantics 1m21s 1GB Starting candle/standard/monadic Finished candle/standard/monadic 1m33s 855MB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 16m03s 4GB Starting candle/standard/opentheory Finished candle/standard/opentheory 8m42s 5GB Starting candle/standard/opentheory/compilation Finished candle/standard/opentheory/compilation 33m49s 17GB Starting candle/standard/opentheory/compilation/proofs Finished candle/standard/opentheory/compilation/proofs 37s 4GB Starting characteristic/examples Finished characteristic/examples 1m35s 2GB Starting tutorial/solutions Finished tutorial/solutions 13m12s 6GB Starting translator/monadic/examples Finished translator/monadic/examples 1m47s 2GB Starting examples Finished examples 5m41s 3GB Starting examples/compilation Finished examples/compilation 1h55m06s 10GB Starting examples/compilation/proofs Finished examples/compilation/proofs 2m04s 3GB Starting compiler/benchmarks Finished compiler/benchmarks 0s 4MB Starting translator/okasaki-examples Finished translator/okasaki-examples 3m28s 1GB Starting translator/other-examples Finished translator/other-examples 3m29s 750MB Starting compiler/parsing/tests Finished compiler/parsing/tests 24s 341MB Starting compiler/inference/tests Finished compiler/inference/tests 3m53s 4GB Starting compiler/bootstrap/translation Finished compiler/bootstrap/translation 6h55m19s 53GB Starting unverified/sexpr-bootstrap/x64/64 Finished unverified/sexpr-bootstrap/x64/64 8m09s 15GB Starting unverified/sexpr-bootstrap/x64/32 Finished unverified/sexpr-bootstrap/x64/32 5m24s 18GB Starting compiler/bootstrap/compilation/x64/64 Finished compiler/bootstrap/compilation/x64/64 18h30m25s 64GB Starting compiler/bootstrap/compilation/x64/64/proofs Finished compiler/bootstrap/compilation/x64/64/proofs 3m18s 25GB Starting compiler/bootstrap/compilation/x64/32 Finished compiler/bootstrap/compilation/x64/32 10h15m48s 64GB Starting compiler/bootstrap/compilation/x64/32/proofs Finished compiler/bootstrap/compilation/x64/32/proofs 4m06s 21GB SUCCESS