CakeML:02b4196c6f4e9a47347568a05dddd023d5487c7d update types.txt #974 (dominance)Merging into:7101a3f2e0c3885412c05e63735ec6da155253ee Fix for adjusted Inductive syntaxHOL:be29184419aaa27f96bbbf8fb1b90d0e40385c33 [emacs-mode] Handle new Inductive label syntaxesMachine:pavlova Claimed job Reusing HOL Starting developers Finished developers 2s 229MB Starting developers/bin Finished developers/bin 12s 1GB Starting compiler/proofs Finished compiler/proofs 1h41m56s 33GB Starting compiler/bootstrap/translation Finished compiler/bootstrap/translation 8h14m25s 77GB Starting semantics/ffi Finished semantics/ffi 7s 610MB Starting semantics Finished semantics 0s 66MB Starting semantics/proofs Finished semantics/proofs 34s 2GB Starting semantics/alt_semantics Finished semantics/alt_semantics 39s 1GB Starting semantics/alt_semantics/proofs Finished semantics/alt_semantics/proofs 11m03s 6GB Starting basis/pure Finished basis/pure 0s 66MB Starting translator Finished translator 1m49s 3GB Starting compiler/parsing Finished compiler/parsing 0s 70MB Starting characteristic Finished characteristic 0s 86MB Starting translator/monadic Finished translator/monadic 0s 91MB Starting basis Finished basis 3m35s 5GB Starting compiler/inference Finished compiler/inference 0s 81MB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 0s 66MB Starting compiler/backend/gc Finished compiler/backend/gc 0s 137MB Starting compiler/backend Finished compiler/backend 16s 1GB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 91MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 0s 90MB Starting compiler/encoders/arm7 Finished compiler/encoders/arm7 0s 94MB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 0s 90MB Starting compiler/encoders/arm8_asl Finished compiler/encoders/arm8_asl 2m17s 1GB 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 132MB Starting compiler/backend/arm7 Finished compiler/backend/arm7 0s 130MB Starting compiler/backend/arm8 Finished compiler/backend/arm8 0s 122MB Starting compiler/backend/mips Finished compiler/backend/mips 0s 121MB Starting compiler/backend/riscv Finished compiler/backend/riscv 0s 121MB Starting compiler/backend/ag32 Finished compiler/backend/ag32 1m19s 4GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 0s 72MB Starting compiler/inference/proofs Finished compiler/inference/proofs 0s 86MB Starting compiler/backend/semantics Finished compiler/backend/semantics 1m23s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 0s 90MB Starting compiler/backend/proofs Finished compiler/backend/proofs 1m01s 2GB Starting compiler/backend/serialiser Finished compiler/backend/serialiser 1s 202MB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 9m22s 5GB Starting compiler/encoders/arm7/proofs Finished compiler/encoders/arm7/proofs 12m57s 8GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 6m19s 6GB Starting compiler/encoders/arm8_asl/proofs Finished compiler/encoders/arm8_asl/proofs 13m58s 4GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 9m56s 7GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 8m15s 6GB Starting compiler/encoders/ag32/proofs Finished compiler/encoders/ag32/proofs 2m20s 2GB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 37s 3GB Starting compiler/backend/arm7/proofs Finished compiler/backend/arm7/proofs 47s 3GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 38s 3GB Starting compiler/backend/arm8_asl Finished compiler/backend/arm8_asl 28s 2GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 42s 3GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 49s 3GB Starting compiler/backend/ag32/proofs Finished compiler/backend/ag32/proofs 12m51s 5GB Starting candle/set-theory Finished candle/set-theory 44s 1GB Starting candle/syntax-lib Finished candle/syntax-lib 0s 68MB 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 104MB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 1m51s 6GB Starting candle/overloading/syntax Finished candle/overloading/syntax 3m24s 2GB Starting candle/overloading/semantics Finished candle/overloading/semantics 11m12s 4GB Starting candle/overloading/monadic Finished candle/overloading/monadic 2m32s 3GB Starting candle/overloading/ml_kernel Finished candle/overloading/ml_kernel 7m31s 6GB Starting candle/overloading/ml_checker Finished candle/overloading/ml_checker 2m32s 7GB Starting candle/prover Finished candle/prover 9m45s 5GB Starting pancake Finished pancake 1m00s 1GB Starting pancake/ffi Finished pancake/ffi 0s 21MB Starting pancake/semantics Finished pancake/semantics 2m21s 3GB Starting pancake/parser Finished pancake/parser 25s 1GB Starting pancake/proofs Finished pancake/proofs 29m20s 8GB Starting characteristic/examples Finished characteristic/examples 1m36s 5GB Starting tutorial/solutions Finished tutorial/solutions 15m32s 13GB Starting translator/monadic/examples Finished translator/monadic/examples 3m43s 5GB Starting examples Finished examples 14m40s 7GB Starting examples/compilation/x64 Finished examples/compilation/x64 1h56m20s 37GB Starting examples/compilation/x64/proofs Finished examples/compilation/x64/proofs 3m45s 6GB Starting examples/compilation/ag32 Finished examples/compilation/ag32 29m22s 10GB Starting examples/compilation/ag32/proofs Finished examples/compilation/ag32/proofs 1m29s 7GB Starting examples/compilation/to_word Finished examples/compilation/to_word 3m54s 12GB Starting examples/lpr_checker Finished examples/lpr_checker 1m13s 2GB Starting examples/lpr_checker/array Finished examples/lpr_checker/array 29m08s 19GB Starting examples/lpr_checker/array/compilation Finished examples/lpr_checker/array/compilation 37m00s 85GB Starting examples/lpr_checker/array/compilation/proofs Finished examples/lpr_checker/array/compilation/proofs 1m52s 10GB Starting examples/lpr_checker/array/compilation/proofsARM8 Finished examples/lpr_checker/array/compilation/proofsARM8 23m12s 37GB Starting examples/pseudo_bool Finished examples/pseudo_bool 1m57s 2GB Starting examples/pseudo_bool/cnf_encoding Finished examples/pseudo_bool/cnf_encoding 34s 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 49m53s 16GB Starting examples/pseudo_bool/array/compilation Finished examples/pseudo_bool/array/compilation 1h49m25s 115GB Starting examples/pseudo_bool/array/compilation/proofs Finished examples/pseudo_bool/array/compilation/proofs 3m04s 7GB Starting examples/opentheory Finished examples/opentheory 10m30s 7GB Starting examples/opentheory Finished examples/opentheory 0s 133MB Starting examples/opentheory/compilation Finished examples/opentheory/compilation 35m37s 46GB Starting examples/opentheory/compilation/proofs Finished examples/opentheory/compilation/proofs 1m27s 6GB Starting examples/opentheory/compilation/ag32 Finished examples/opentheory/compilation/ag32 31m25s 44GB Starting examples/opentheory/compilation/ag32/proofs Finished examples/opentheory/compilation/ag32/proofs 2m19s 11GB Starting examples/sat_encodings Finished examples/sat_encodings 2m38s 1GB Starting examples/sat_encodings/case_studies Finished examples/sat_encodings/case_studies 1m57s 2GB Starting examples/sat_encodings/translation Finished examples/sat_encodings/translation 5m59s 7GB Starting examples/sat_encodings/translation/compilation Finished examples/sat_encodings/translation/compilation 34m50s 41GB Starting examples/deflate Finished examples/deflate 1m12s 1GB Starting examples/deflate/translation Finished examples/deflate/translation 1m35s 7GB Starting examples/deflate/translation/compilation Finished examples/deflate/translation/compilation 16m26s 20GB Starting examples/vipr Finished examples/vipr 3m58s 5GB Starting examples/vipr/compilation Finished examples/vipr/compilation 19m21s 32GB Starting translator/okasaki-examples Finished translator/okasaki-examples 4m53s 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 7m27s 7GB Starting compiler/printing/test Finished compiler/printing/test 3m29s 6GB Starting icing/flover Finished icing/flover 36m02s 4GB Starting icing/ Finished icing/ 55m36s 31GB Starting icing/examples Finished icing/examples 1m40s 8GB Starting compiler/repl Finished compiler/repl 8m38s 10GB Starting unverified/sexpr-bootstrap/x64/64 Finished unverified/sexpr-bootstrap/x64/64 10m50s 15GB Starting unverified/sexpr-bootstrap/x64/32 Finished unverified/sexpr-bootstrap/x64/32 9m00s 13GB Starting compiler/benchmarks Finished compiler/benchmarks 43s 713MB Starting compiler/bootstrap/compilation/x64/64 Finished compiler/bootstrap/compilation/x64/64 14h06m21s 151GB Starting compiler/bootstrap/compilation/x64/64/proofs Finished compiler/bootstrap/compilation/x64/64/proofs 20m59s 46GB Starting compiler/bootstrap/compilation/x64/32 Finished compiler/bootstrap/compilation/x64/32 7h13m45s 120GB Starting compiler/bootstrap/compilation/x64/32/proofs Finished compiler/bootstrap/compilation/x64/32/proofs 3m27s 18GB Starting compiler/bootstrap/compilation/ag32/32 Finished compiler/bootstrap/compilation/ag32/32 7h31m50s 129GB Starting compiler/bootstrap/compilation/ag32/32/proofs Finished compiler/bootstrap/compilation/ag32/32/proofs 7m21s 40GB SUCCESS