CakeML:557a4854b3a3753d216bd00a20b323ee3ca4d3ae Tweak markdown to look better as html #590 (howto)Merging into:2e9c8e4f622247379354a7408d480f5a67333abc Tweak gitignoresHOL:89daca206b2ad7a8e43f3a59c20a178cc04d7748 Fix bug: TypeBase.simpls_of not being filled in on loadMachine:oven2 4.13.0-37-generic x86_64 GNU/Linux Claimed job Reusing HOL Starting developers Finished developers 0s 30MB Starting developers/bin Finished developers/bin 31s 140MB Starting semantics/ffi Finished semantics/ffi 9s 215MB Starting semantics Finished semantics 1m23s 1GB Starting semantics/proofs Finished semantics/proofs 3m22s 1GB Starting basis/pure Finished basis/pure 51s 685MB Starting translator Finished translator 1m40s 1GB Starting compiler/parsing Finished compiler/parsing 1m06s 2GB Starting characteristic Finished characteristic 3m14s 1GB Starting translator/monadic Finished translator/monadic 1m27s 1GB Starting basis Finished basis 16m14s 3GB Starting compiler/inference Finished compiler/inference 1m39s 1GB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 51s 1GB Starting compiler/backend/gc Finished compiler/backend/gc 8m01s 1GB Starting compiler/backend Finished compiler/backend 1s 17MB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 16MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 24s 922MB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 51s 963MB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 12s 860MB Starting compiler/encoders/mips Finished compiler/encoders/mips 16s 1GB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 13s 772MB Starting compiler/encoders/ag32 Finished compiler/encoders/ag32 15s 718MB Starting compiler/backend/x64 Finished compiler/backend/x64 16s 852MB Starting compiler/backend/arm6 Finished compiler/backend/arm6 19s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 17s 901MB Starting compiler/backend/mips Finished compiler/backend/mips 16s 957MB Starting compiler/backend/riscv Finished compiler/backend/riscv 17s 1GB Starting compiler/backend/ag32 Finished compiler/backend/ag32 1m14s 1GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 6m17s 922MB Starting compiler/inference/proofs Finished compiler/inference/proofs 2m55s 1GB Starting compiler/backend/semantics Finished compiler/backend/semantics 7m44s 1GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 2m46s 846MB Starting compiler/backend/proofs Finished compiler/backend/proofs 39m57s 5GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 9m58s 5GB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 14m27s 3GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 6m08s 1GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 10m58s 2GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 8m03s 1GB Starting compiler/encoders/ag32/proofs Finished compiler/encoders/ag32/proofs 2m47s 631MB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 18s 1GB Starting compiler/backend/arm6/proofs Finished compiler/backend/arm6/proofs 20s 969MB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 18s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 18s 920MB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 18s 1GB Starting compiler/backend/ag32/proofs Finished compiler/backend/ag32/proofs 9m34s 2GB Starting compiler/proofs Finished compiler/proofs 1m21s 3GB Starting candle/set-theory Finished candle/set-theory 24s 707MB Starting candle/syntax-lib Finished candle/syntax-lib 9s 552MB Starting candle/standard/syntax Finished candle/standard/syntax 1m47s 1GB Starting candle/standard/semantics Finished candle/standard/semantics 1m38s 1GB Starting candle/standard/monadic Finished candle/standard/monadic 1m44s 1GB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 15m32s 3GB Starting candle/standard/opentheory Finished candle/standard/opentheory 9m00s 4GB Starting candle/standard/opentheory/compilation Finished candle/standard/opentheory/compilation 30m11s 14GB Starting candle/standard/opentheory/compilation/proofs Finished candle/standard/opentheory/compilation/proofs 49s 6GB Starting characteristic/examples Finished characteristic/examples 1m30s 2GB Starting tutorial/solutions Finished tutorial/solutions 12m56s 8GB Starting translator/monadic/examples Finished translator/monadic/examples 2m10s 2GB Starting examples Finished examples 8m00s 3GB Starting examples/compilation/x64 Finished examples/compilation/x64 2h03m06s 12GB Starting examples/compilation/x64/proofs Finished examples/compilation/x64/proofs 1m52s 4GB Starting examples/compilation/ag32 Finished examples/compilation/ag32 28m09s 5GB Starting examples/compilation/ag32/proofs Finished examples/compilation/ag32/proofs 47s 4GB Starting translator/okasaki-examples Finished translator/okasaki-examples 4m08s 1GB Starting translator/other-examples Finished translator/other-examples 41s 1GB Starting compiler/parsing/tests Finished compiler/parsing/tests 26s 577MB Starting compiler/inference/tests Finished compiler/inference/tests 4m10s 5GB Starting compiler/bootstrap/translation Finished compiler/bootstrap/translation 3h33m34s 53GB Starting unverified/sexpr-bootstrap/x64/64 Finished unverified/sexpr-bootstrap/x64/64 8m26s 17GB Starting unverified/sexpr-bootstrap/x64/32 Finished unverified/sexpr-bootstrap/x64/32 4m51s 21GB Starting compiler/bootstrap/compilation/x64/64 Finished compiler/bootstrap/compilation/x64/64 10h02m15s 63GB Starting compiler/bootstrap/compilation/x64/64/proofs Finished compiler/bootstrap/compilation/x64/64/proofs 6m00s 30GB Starting compiler/bootstrap/compilation/x64/32 Finished compiler/bootstrap/compilation/x64/32 8h58m19s 64GB Starting compiler/bootstrap/compilation/x64/32/proofs Finished compiler/bootstrap/compilation/x64/32/proofs 6m00s 32GB SUCCESS