OverviewCakeML:1afd9c2ae712011d1edddfc51a00c38d36bbb43a
Merge pull request #906 from CakeML/candle-features
HOL:2639637652b5be738521f6efa56cbf8a10e52599
Start to revise simplifier documentation to capture recent changes
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
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
Reusing HOL
Starting developers
Finished developers 5s 100MB
Starting developers/bin
Finished developers/bin 1m44s 1GB
Starting semantics/ffi
Finished semantics/ffi 9s 198MB
Starting semantics
Finished semantics 2m33s 1GB
Starting semantics/proofs
Finished semantics/proofs 8m55s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 28s 563MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 16m03s 3GB
Starting basis/pure
Finished basis/pure 1m06s 875MB
Starting translator
Finished translator 7m49s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m32s 5GB
Starting characteristic
Finished characteristic 7m18s 2GB
Starting translator/monadic
Finished translator/monadic 2m00s 1GB
Starting basis
Finished basis 55m33s 18GB
Starting compiler/inference
Finished compiler/inference 1m34s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m45s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 4m32s 2GB
Starting compiler/backend
Finished compiler/backend 5m57s 2GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 30s 709MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 29s 789MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 1m01s 844MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 17s 621MB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 2m59s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 21s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 19s 940MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 21s 1GB
Starting compiler/backend/x64
Finished compiler/backend/x64 21s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 23s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 21s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 21s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 21s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m30s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 4m19s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 3m00s 932MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 30m57s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 4m01s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 1h42m36s 18GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1m44s 2GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 10m25s 5GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 14m48s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 7m20s 1GB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 16m34s 3GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 11m21s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 9m34s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m51s 819MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 25s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 26s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 26s 1GB
Starting compiler/backend/arm8_asl
Finished compiler/backend/arm8_asl 20s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 25s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 27s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 14m17s 2GB
Starting compiler/proofs
Finished compiler/proofs 2m11s 5GB
Starting candle/set-theory
Finished candle/set-theory 34s 889MB
Starting candle/syntax-lib
Finished candle/syntax-lib 13s 543MB
Starting candle/standard/syntax
Finished candle/standard/syntax 2m07s 926MB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m47s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 2m01s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 7m10s 3GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m46s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 12m42s 2GB
Starting candle/overloading/monadic
Finished candle/overloading/monadic 2m48s 1GB
Starting candle/overloading/ml_kernel
Finished candle/overloading/ml_kernel 7m55s 2GB
Starting candle/overloading/ml_checker
Finished candle/overloading/ml_checker 2m30s 2GB
Starting candle/prover
Finished candle/prover 26m12s 3GB
Starting pancake
Finished pancake 3m18s 4GB
Starting pancake/ffi
Finished pancake/ffi 0s 9MB
Starting pancake/semantics
Finished pancake/semantics 2m39s 1GB
Starting pancake/proofs
Finished pancake/proofs 13m18s 5GB
Starting characteristic/examples
Finished characteristic/examples 1m28s 2GB
Starting tutorial/solutions
Finished tutorial/solutions 16m35s 8GB
Starting translator/monadic/examples
Finished translator/monadic/examples 4m01s 2GB
Starting examples
Finished examples 10m51s 4GB
Starting examples/compilation/x64
Finished examples/compilation/x64 2h08m41s 12GB
Starting examples/compilation/x64/proofs
Finished examples/compilation/x64/proofs 2m02s 3GB
Starting examples/compilation/ag32
Finished examples/compilation/ag32 34m12s 8GB
Starting examples/compilation/ag32/proofs
Finished examples/compilation/ag32/proofs 50s 4GB
Starting examples/lpr_checker
Finished examples/lpr_checker 59s 996MB
Starting examples/lpr_checker/array
Finished examples/lpr_checker/array 36m51s 5GB
Starting examples/lpr_checker/array/compilation
Finished examples/lpr_checker/array/compilation 41m33s 24GB
Starting examples/lpr_checker/array/compilation/proofs
Finished examples/lpr_checker/array/compilation/proofs 1m24s 6GB
Starting examples/opentheory
Finished examples/opentheory 11m08s 3GB
Starting examples/opentheory
Finished examples/opentheory 1s 18MB
Starting examples/opentheory/compilation
Finished examples/opentheory/compilation 39m40s 19GB
Starting examples/opentheory/compilation/proofs
Finished examples/opentheory/compilation/proofs 50s 4GB
Starting examples/opentheory/compilation/ag32
Finished examples/opentheory/compilation/ag32 35m55s 22GB
Starting examples/opentheory/compilation/ag32/proofs
Finished examples/opentheory/compilation/ag32/proofs 1m44s 5GB
Starting examples/sat_encodings
Finished examples/sat_encodings 1m51s 713MB
Starting examples/sat_encodings/case_studies
Finished examples/sat_encodings/case_studies 1m43s 821MB
Starting examples/sat_encodings/translation
Finished examples/sat_encodings/translation 5m58s 5GB
Starting examples/sat_encodings/translation/compilation
Finished examples/sat_encodings/translation/compilation 51m56s 23GB
Starting examples/deflate
Finished examples/deflate 52s 812MB
Starting examples/deflate/translation
Finished examples/deflate/translation 1m38s 3GB
Starting examples/deflate/translation/compilation
Finished examples/deflate/translation/compilation 23m24s 17GB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 5m13s 1GB
Starting translator/other-examples
Finished translator/other-examples 49s 1GB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 30s 692MB
Starting compiler/inference/tests
Finished compiler/inference/tests 8m45s 4GB
Starting compiler/printing/test
Finished compiler/printing/test 3m43s 3GB
Starting icing/flover
Finished icing/flover 51m21s 1GB
Starting icing/
Finished icing/ 1h16m43s 6GB
Starting icing/examples
Finished icing/examples 1m31s 3GB
Starting compiler/repl
Finished compiler/repl 2h35m18s 24GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 4h54m15s 42GB
Starting unverified/sexpr-bootstrap/x64/64
Finished unverified/sexpr-bootstrap/x64/64 10m58s 13GB
Starting unverified/sexpr-bootstrap/x64/32
Finished unverified/sexpr-bootstrap/x64/32 8m42s 11GB
Starting compiler/benchmarks
Finished compiler/benchmarks 3s 29MB
Starting compiler/bootstrap/compilation/x64/64
Finished compiler/bootstrap/compilation/x64/64 11h48m39s 64GB
Starting compiler/bootstrap/compilation/x64/64/proofs
Finished compiler/bootstrap/compilation/x64/64/proofs 20m58s 30GB
Starting compiler/bootstrap/compilation/x64/32
Finished compiler/bootstrap/compilation/x64/32 6h40m27s 63GB
Starting compiler/bootstrap/compilation/x64/32/proofs
Finished compiler/bootstrap/compilation/x64/32/proofs 3m21s 11GB
Starting compiler/bootstrap/compilation/ag32/32
Finished compiler/bootstrap/compilation/ag32/32 6h54m05s 64GB
Starting compiler/bootstrap/compilation/ag32/32/proofs
Finished compiler/bootstrap/compilation/ag32/32/proofs 8m17s 16GB
SUCCESS