CakeML:1329912153a1f42e278015eb59108568f07918f0 Fix rebindHOL:5f1d5f38720df80ec8640b257180a08f7d2683bf Removed "funpow" for lambda terms, using FUNPOW (APP f) insteadMachine:pavlovaArtefacts:cake-unverified-x64-64.tar.gz cake-unverified-x64-32.tar.gz Claimed job Reusing HOL Starting developers Finished developers 2s 189MB Starting developers/bin Finished developers/bin 10s 1GB Starting compiler/proofs Finished compiler/proofs 1h41m32s 43GB Starting compiler/bootstrap/translation Finished compiler/bootstrap/translation 8h12m12s 74GB Starting semantics/ffi Finished semantics/ffi 7s 531MB Starting semantics Finished semantics 0s 67MB Starting semantics/proofs Finished semantics/proofs 33s 2GB Starting semantics/alt_semantics Finished semantics/alt_semantics 38s 1GB Starting semantics/alt_semantics/proofs Finished semantics/alt_semantics/proofs 10m51s 5GB Starting basis/pure Finished basis/pure 0s 71MB Starting translator Finished translator 1m43s 3GB Starting compiler/parsing Finished compiler/parsing 0s 73MB Starting characteristic Finished characteristic 0s 92MB Starting translator/monadic Finished translator/monadic 0s 98MB Starting basis Finished basis 3m56s 10GB Starting compiler/inference Finished compiler/inference 0s 86MB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 0s 65MB Starting compiler/backend/gc Finished compiler/backend/gc 0s 130MB Starting compiler/backend Finished compiler/backend 17s 1GB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 89MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 0s 94MB Starting compiler/encoders/arm7 Finished compiler/encoders/arm7 0s 94MB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 0s 89MB Starting compiler/encoders/arm8_asl Finished compiler/encoders/arm8_asl 2m10s 1GB Starting compiler/encoders/mips Finished compiler/encoders/mips 0s 90MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 0s 90MB Starting compiler/encoders/ag32 Finished compiler/encoders/ag32 0s 85MB Starting compiler/backend/x64 Finished compiler/backend/x64 0s 127MB Starting compiler/backend/arm7 Finished compiler/backend/arm7 0s 127MB Starting compiler/backend/arm8 Finished compiler/backend/arm8 0s 127MB Starting compiler/backend/mips Finished compiler/backend/mips 0s 127MB Starting compiler/backend/riscv Finished compiler/backend/riscv 0s 127MB Starting compiler/backend/ag32 Finished compiler/backend/ag32 1m17s 3GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 0s 71MB Starting compiler/inference/proofs Finished compiler/inference/proofs 0s 88MB Starting compiler/backend/semantics Finished compiler/backend/semantics 1m23s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 0s 94MB Starting compiler/backend/proofs Finished compiler/backend/proofs 1m04s 5GB Starting compiler/backend/serialiser Finished compiler/backend/serialiser 1s 201MB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 9m31s 5GB Starting compiler/encoders/arm7/proofs Finished compiler/encoders/arm7/proofs 13m04s 8GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 6m28s 5GB Starting compiler/encoders/arm8_asl/proofs Finished compiler/encoders/arm8_asl/proofs 13m53s 4GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 9m58s 6GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 8m16s 6GB Starting compiler/encoders/ag32/proofs Finished compiler/encoders/ag32/proofs 2m25s 2GB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 39s 3GB Starting compiler/backend/arm7/proofs Finished compiler/backend/arm7/proofs 44s 3GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 38s 2GB 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 47s 4GB Starting compiler/backend/ag32/proofs Finished compiler/backend/ag32/proofs 12m57s 6GB Starting candle/set-theory Finished candle/set-theory 43s 1GB Starting candle/syntax-lib Finished candle/syntax-lib 0s 73MB Starting candle/standard/syntax Finished candle/standard/syntax 15s 1GB Starting candle/standard/semantics Finished candle/standard/semantics 2m22s 2GB Starting candle/standard/monadic Finished candle/standard/monadic 0s 100MB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 1m46s 6GB Starting candle/overloading/syntax Finished candle/overloading/syntax 3m26s 3GB Starting candle/overloading/semantics Finished candle/overloading/semantics 11m15s 4GB Starting candle/overloading/monadic Finished candle/overloading/monadic 2m34s 3GB Starting candle/overloading/ml_kernel Finished candle/overloading/ml_kernel 7m31s 7GB Starting candle/overloading/ml_checker Finished candle/overloading/ml_checker 2m31s 7GB Starting candle/prover Finished candle/prover 9m48s 5GB Starting pancake Finished pancake 57s 1GB Starting pancake/ffi Finished pancake/ffi 0s 20MB Starting pancake/semantics Finished pancake/semantics 2m20s 2GB Starting pancake/parser Finished pancake/parser 26s 2GB Starting pancake/proofs Finished pancake/proofs 29m26s 8GB Starting characteristic/examples Finished characteristic/examples 1m33s 6GB Starting tutorial/solutions Finished tutorial/solutions 15m36s 12GB Starting translator/monadic/examples Finished translator/monadic/examples 3m39s 5GB Starting examples Finished examples 14m20s 7GB Starting examples/compilation/x64 Finished examples/compilation/x64 1h56m00s 34GB Starting examples/compilation/x64/proofs Finished examples/compilation/x64/proofs 3m43s 6GB Starting examples/compilation/ag32 Finished examples/compilation/ag32 29m36s 9GB Starting examples/compilation/ag32/proofs Finished examples/compilation/ag32/proofs 1m37s 6GB Starting examples/compilation/to_word Finished examples/compilation/to_word 3m55s 12GB Starting examples/lpr_checker Finished examples/lpr_checker 1m11s 2GB Starting examples/lpr_checker/array Finished examples/lpr_checker/array 34m14s 12GB Starting examples/lpr_checker/array/compilation Finished examples/lpr_checker/array/compilation 36m28s 80GB Starting examples/lpr_checker/array/compilation/proofs Finished examples/lpr_checker/array/compilation/proofs 2m01s 9GB Starting examples/lpr_checker/array/compilation/proofsARM8 Finished examples/lpr_checker/array/compilation/proofsARM8 12m26s 49GB Starting examples/opentheory Finished examples/opentheory 10m47s 11GB Starting examples/opentheory Finished examples/opentheory 0s 123MB Starting examples/opentheory/compilation Finished examples/opentheory/compilation 35m43s 58GB Starting examples/opentheory/compilation/proofs Finished examples/opentheory/compilation/proofs 1m26s 6GB Starting examples/opentheory/compilation/ag32 Finished examples/opentheory/compilation/ag32 31m44s 51GB Starting examples/opentheory/compilation/ag32/proofs Finished examples/opentheory/compilation/ag32/proofs 2m21s 9GB Starting examples/sat_encodings Finished examples/sat_encodings 2m38s 1GB Starting examples/sat_encodings/case_studies Finished examples/sat_encodings/case_studies 1m56s 2GB Starting examples/sat_encodings/translation Finished examples/sat_encodings/translation 5m54s 7GB Starting examples/sat_encodings/translation/compilation Finished examples/sat_encodings/translation/compilation 35m16s 32GB Starting examples/deflate Finished examples/deflate 1m12s 1GB Starting examples/deflate/translation Finished examples/deflate/translation 1m37s 7GB Starting examples/deflate/translation/compilation Finished examples/deflate/translation/compilation 16m20s 27GB Starting examples/vipr Finished examples/vipr 4m06s 7GB Starting examples/vipr/compilation Finished examples/vipr/compilation 20m03s 37GB Starting translator/okasaki-examples Finished translator/okasaki-examples 4m56s 4GB Starting translator/other-examples Finished translator/other-examples 1m08s 3GB Starting compiler/parsing/tests Finished compiler/parsing/tests 32s 1GB Starting compiler/inference/tests Finished compiler/inference/tests 7m23s 6GB Starting compiler/printing/test Finished compiler/printing/test 3m30s 5GB Starting icing/flover Finished icing/flover 35m07s 4GB Starting icing/ Finished icing/ 55m07s 32GB Starting icing/examples Finished icing/examples 1m40s 8GB Starting compiler/repl Finished compiler/repl 8m43s 8GB Starting unverified/sexpr-bootstrap/x64/64 Finished unverified/sexpr-bootstrap/x64/64 10m55s 16GB Starting unverified/sexpr-bootstrap/x64/32 Finished unverified/sexpr-bootstrap/x64/32 9m12s 14GB Starting compiler/benchmarks Finished compiler/benchmarks 43s 713MB Starting compiler/bootstrap/compilation/x64/64 Resuming compiler/bootstrap/compilation/x64/64 Resuming compiler/bootstrap/compilation/x64/64 Resuming compiler/bootstrap/compilation/x64/64