CakeML:010837902da82bc67d57f2a5c9b910cf3d136a87 Merge branch 'master' into argparse #511 (argparse)Merging into:59886cd0205c1d5d943ef10a26890f79b515b68f Merge pull request #561 from CakeML/print-typesHOL:7f7650b1f7d9fbc79f55646dabcf225b5cf0fff4 Magic keyword for store_thm hack has to be "Theorem"Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64 Claimed job Building HOL Starting developers/bin Finished developers/bin 1m08s 916MB Starting semantics/ffi Finished semantics/ffi 38s 505MB Starting semantics Finished semantics 1m30s 894MB Starting semantics/proofs Finished semantics/proofs 2m51s 1GB Starting basis/pure Finished basis/pure 3m36s 641MB Starting translator Finished translator 3m00s 1GB Starting compiler/parsing Finished compiler/parsing 1m13s 1GB Starting characteristic Finished characteristic 2m30s 1GB Starting translator/monadic Finished translator/monadic 1m27s 1GB Starting basis Finished basis 17m56s 2GB Starting compiler/inference Finished compiler/inference 1m43s 1GB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 46s 1GB Starting compiler/backend/gc Finished compiler/backend/gc 7m20s 1GB Starting compiler/backend Finished compiler/backend 2s 17MB Starting compiler/encoders/asm Finished compiler/encoders/asm 1s 12MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 51s 643MB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 1m44s 1GB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 26s 474MB Starting compiler/encoders/mips Finished compiler/encoders/mips 58s 831MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 1m00s 1GB Starting compiler/encoders/ag32 Finished compiler/encoders/ag32 17s 806MB Starting compiler/backend/x64 Finished compiler/backend/x64 17s 1GB Starting compiler/backend/arm6 Finished compiler/backend/arm6 18s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 17s 892MB Starting compiler/backend/mips Finished compiler/backend/mips 18s 1GB Starting compiler/backend/riscv Finished compiler/backend/riscv 18s 1GB Starting compiler/backend/ag32 Finished compiler/backend/ag32 1m11s 984MB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 5m55s 834MB Starting compiler/inference/proofs Finished compiler/inference/proofs 2m51s 847MB Starting compiler/backend/semantics Finished compiler/backend/semantics 8m46s 1GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 2m40s 564MB Starting compiler/backend/proofs Finished compiler/backend/proofs 42m40s 4GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 9m48s 4GB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 14m55s 2GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 6m02s 1GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 10m32s 1GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 7m55s 877MB Starting compiler/encoders/ag32/proofs Finished compiler/encoders/ag32/proofs 2m43s 577MB 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 21s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 21s 1GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 21s 1GB Starting compiler/backend/ag32/proofs Finished compiler/backend/ag32/proofs 9m17s 2GB Starting compiler/proofs Finished compiler/proofs 1m24s 2GB Starting candle/set-theory Finished candle/set-theory 31s 599MB Starting candle/syntax-lib Finished candle/syntax-lib 10s 662MB Starting candle/standard/syntax Finished candle/standard/syntax 1m34s 674MB Starting candle/standard/semantics Finished candle/standard/semantics 1m20s 812MB Starting candle/standard/monadic Finished candle/standard/monadic 1m34s 1GB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 18m32s 4GB Starting candle/standard/opentheory Finished candle/standard/opentheory 8m09s 3GB Starting candle/standard/opentheory/compilation Finished candle/standard/opentheory/compilation 30m59s 23GB Starting candle/standard/opentheory/compilation/proofs Finished candle/standard/opentheory/compilation/proofs 38s 5GB Starting characteristic/examples Finished characteristic/examples 1m37s 1GB Starting tutorial/solutions Finished tutorial/solutions 14m55s 7GB Starting translator/monadic/examples Finished translator/monadic/examples 1m46s 2GB Starting examples Finished examples 6m34s 3GB Starting examples/compilation/x64 Finished examples/compilation/x64 2h05m08s 13GB Starting examples/compilation/x64/proofs Finished examples/compilation/x64/proofs 2m11s 3GB Starting examples/compilation/ag32 Finished examples/compilation/ag32 29m47s 5GB Starting examples/compilation/ag32/proofs Finished examples/compilation/ag32/proofs 28s 2GB Starting compiler/benchmarks Finished compiler/benchmarks 0s 5MB Starting translator/okasaki-examples Finished translator/okasaki-examples 3m23s 1GB Starting translator/other-examples Finished translator/other-examples 3m30s 763MB Starting compiler/parsing/tests Finished compiler/parsing/tests 24s 357MB Starting compiler/inference/tests