CakeML:8ac36a22c960a9f4aaae14aa89dabaf177cd63fa Merge pull request #974 from CakeML/dominanceHOL:e7f2e175666a4f2e69629143d260e17e1817b475 Minor additions to cv<->term transfer theoremsMachine:pavlovaArtefacts:cake-unverified-x64-64.tar.gz cake-unverified-x64-32.tar.gz cake-x64-64.tar.gz cake-x64-32.tar.gz Claimed job Building HOL Starting developers Finished developers 2s 190MB Starting developers/bin Finished developers/bin 9s 1GB Starting compiler/proofs Finished compiler/proofs 1h45m09s 47GB Starting compiler/bootstrap/translation Finished compiler/bootstrap/translation 8h11m14s 76GB Starting semantics/ffi Finished semantics/ffi 7s 655MB Starting semantics Finished semantics 0s 66MB Starting semantics/proofs Finished semantics/proofs 36s 1GB Starting semantics/alt_semantics Finished semantics/alt_semantics 38s 1GB Starting semantics/alt_semantics/proofs Finished semantics/alt_semantics/proofs 10m56s 3GB Starting basis/pure Finished basis/pure 0s 67MB Starting translator Finished translator 1m43s 3GB Starting compiler/parsing Finished compiler/parsing 0s 70MB Starting characteristic Finished characteristic 0s 90MB Starting translator/monadic Finished translator/monadic 0s 95MB Starting basis Finished basis 3m38s 5GB Starting compiler/inference Finished compiler/inference 0s 80MB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 0s 66MB Starting compiler/backend/gc Finished compiler/backend/gc 0s 131MB Starting compiler/backend Finished compiler/backend 16s 1GB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 90MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 0s 89MB Starting compiler/encoders/arm7 Finished compiler/encoders/arm7 0s 92MB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 0s 87MB Starting compiler/encoders/arm8_asl Finished compiler/encoders/arm8_asl 2h09m21s 41GB Starting compiler/encoders/mips Finished compiler/encoders/mips 0s 87MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 0s 90MB Starting compiler/encoders/ag32 Finished compiler/encoders/ag32 0s 90MB Starting compiler/backend/x64 Finished compiler/backend/x64 0s 129MB Starting compiler/backend/arm7 Finished compiler/backend/arm7 0s 129MB Starting compiler/backend/arm8 Finished compiler/backend/arm8 0s 129MB Starting compiler/backend/mips Finished compiler/backend/mips 0s 129MB Starting compiler/backend/riscv Finished compiler/backend/riscv 0s 129MB Starting compiler/backend/ag32 Finished compiler/backend/ag32 1m18s 2GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 0s 73MB Starting compiler/inference/proofs Finished compiler/inference/proofs 0s 87MB Starting compiler/backend/semantics Finished compiler/backend/semantics 1m28s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 0s 96MB Starting compiler/backend/proofs Finished compiler/backend/proofs 1m02s 4GB Starting compiler/backend/serialiser Finished compiler/backend/serialiser 1s 188MB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 9m22s 5GB Starting compiler/encoders/arm7/proofs Finished compiler/encoders/arm7/proofs 12m58s 7GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 6m28s 4GB Starting compiler/encoders/arm8_asl/proofs Finished compiler/encoders/arm8_asl/proofs 48m10s 8GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 10m09s 7GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 8m29s 3GB Starting compiler/encoders/ag32/proofs Finished compiler/encoders/ag32/proofs 2m20s 2GB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 39s 3GB Starting compiler/backend/arm7/proofs Finished compiler/backend/arm7/proofs 42s 2GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 38s 3GB Starting compiler/backend/arm8_asl Finished compiler/backend/arm8_asl 27s 2GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 42s 3GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 48s 3GB Starting compiler/backend/ag32/proofs Finished compiler/backend/ag32/proofs 13m04s 6GB Starting candle/set-theory Finished candle/set-theory 42s 1GB Starting candle/syntax-lib Finished candle/syntax-lib 0s 67MB Starting candle/standard/syntax Finished candle/standard/syntax 15s 1GB Starting candle/standard/semantics Finished candle/standard/semantics 2m20s 2GB Starting candle/standard/monadic Finished candle/standard/monadic 0s 102MB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 1m48s 5GB Starting candle/overloading/syntax Finished candle/overloading/syntax 3m28s 2GB Starting candle/overloading/semantics Finished candle/overloading/semantics 11m23s 5GB Starting candle/overloading/monadic Finished candle/overloading/monadic 2m32s 3GB Starting candle/overloading/ml_kernel Finished candle/overloading/ml_kernel 7m27s 6GB Starting candle/overloading/ml_checker Finished candle/overloading/ml_checker 2m32s 7GB Starting candle/prover Finished candle/prover 9m48s 5GB Starting pancake Finished pancake 59s 1GB Starting pancake/ffi Finished pancake/ffi 0s 21MB Starting pancake/semantics Finished pancake/semantics 2m17s 2GB Starting pancake/parser Finished pancake/parser 26s 2GB Starting pancake/proofs Finished pancake/proofs 29m43s 8GB Starting characteristic/examples Finished characteristic/examples 1m35s 6GB Starting tutorial/solutions Finished tutorial/solutions 15m27s 12GB Starting translator/monadic/examples Finished translator/monadic/examples 3m42s 5GB Starting examples Finished examples 14m31s 7GB Starting examples/compilation/x64 Finished examples/compilation/x64 1h56m40s 24GB Starting examples/compilation/x64/proofs Finished examples/compilation/x64/proofs 3m42s 6GB Starting examples/compilation/ag32 Finished examples/compilation/ag32 29m56s 12GB Starting examples/compilation/ag32/proofs Finished examples/compilation/ag32/proofs 1m25s 7GB Starting examples/compilation/to_word Finished examples/compilation/to_word 3m50s 12GB Starting examples/lpr_checker Finished examples/lpr_checker 1m13s 2GB Starting examples/lpr_checker/array Finished examples/lpr_checker/array 28m42s 10GB Starting examples/lpr_checker/array/compilation Finished examples/lpr_checker/array/compilation 34m37s 42GB Starting examples/lpr_checker/array/compilation/proofs Finished examples/lpr_checker/array/compilation/proofs 2m02s 9GB Starting examples/lpr_checker/array/compilation/proofsARM8 Finished examples/lpr_checker/array/compilation/proofsARM8 8m55s 48GB Starting examples/pseudo_bool Finished examples/pseudo_bool 1m58s 2GB Starting examples/pseudo_bool/cnf_encoding Finished examples/pseudo_bool/cnf_encoding 35s 1GB Starting examples/pseudo_bool/graph_encoding Finished examples/pseudo_bool/graph_encoding 48s 1GB Starting examples/pseudo_bool/array Finished examples/pseudo_bool/array 50m19s 12GB Starting examples/pseudo_bool/array/compilation Finished examples/pseudo_bool/array/compilation 1h48m31s 122GB Starting examples/pseudo_bool/array/compilation/proofs Finished examples/pseudo_bool/array/compilation/proofs 3m00s 7GB Starting examples/opentheory Finished examples/opentheory 10m47s 7GB Starting examples/opentheory Finished examples/opentheory 0s 123MB Starting examples/opentheory/compilation Finished examples/opentheory/compilation 36m11s 46GB Starting examples/opentheory/compilation/proofs Finished examples/opentheory/compilation/proofs 1m29s 6GB Starting examples/opentheory/compilation/ag32 Finished examples/opentheory/compilation/ag32 32m02s 49GB Starting examples/opentheory/compilation/ag32/proofs Finished examples/opentheory/compilation/ag32/proofs 2m17s 11GB Starting examples/sat_encodings Finished examples/sat_encodings 2m33s 1GB Starting examples/sat_encodings/case_studies Finished examples/sat_encodings/case_studies 1m58s 2GB Starting examples/sat_encodings/translation Finished examples/sat_encodings/translation 6m06s 7GB Starting examples/sat_encodings/translation/compilation Finished examples/sat_encodings/translation/compilation 35m36s 36GB Starting examples/deflate Finished examples/deflate 1m13s 2GB Starting examples/deflate/translation Finished examples/deflate/translation 1m35s 7GB Starting examples/deflate/translation/compilation Finished examples/deflate/translation/compilation 16m35s 22GB Starting examples/vipr Finished examples/vipr 3m59s 7GB Starting examples/vipr/compilation Finished examples/vipr/compilation 20m04s 28GB Starting translator/okasaki-examples Finished translator/okasaki-examples 4m56s 4GB Starting translator/other-examples Finished translator/other-examples 3m41s 3GB Starting compiler/parsing/tests Finished compiler/parsing/tests 32s 1GB Starting compiler/inference/tests Finished compiler/inference/tests 7m33s 5GB Starting compiler/printing/test Finished compiler/printing/test 3m27s 6GB Starting icing/flover Finished icing/flover 35m56s 3GB Starting icing/ Finished icing/ 55m39s 31GB Starting icing/examples Finished icing/examples 1m41s 8GB Starting compiler/repl Finished compiler/repl 8m44s 10GB Starting unverified/sexpr-bootstrap/x64/64 Finished unverified/sexpr-bootstrap/x64/64 11m01s 17GB Starting unverified/sexpr-bootstrap/x64/32 Finished unverified/sexpr-bootstrap/x64/32 9m02s 14GB Starting compiler/benchmarks Finished compiler/benchmarks 43s 713MB Starting compiler/bootstrap/compilation/x64/64 Finished compiler/bootstrap/compilation/x64/64 14h45m56s 146GB Starting compiler/bootstrap/compilation/x64/64/proofs Finished compiler/bootstrap/compilation/x64/64/proofs 21m04s 39GB Starting compiler/bootstrap/compilation/x64/32 Finished compiler/bootstrap/compilation/x64/32 7h15m38s 103GB Starting compiler/bootstrap/compilation/x64/32/proofs Finished compiler/bootstrap/compilation/x64/32/proofs 3m42s 17GB Starting compiler/bootstrap/compilation/ag32/32 Finished compiler/bootstrap/compilation/ag32/32 7h40m07s 142GB Starting compiler/bootstrap/compilation/ag32/32/proofs Finished compiler/bootstrap/compilation/ag32/32/proofs 7m37s 49GB SUCCESS