CakeML:726e2d5b2688f471f56c465bbd919a1113255f51 Merge branch 'origin/master' into local #577 (local)Merging into:fc7210e6e390f10177982607373a07ef1e4b5808 Update for new s-expression syntax (usingHOL:5e4369a4a208507b43df4343e08b5fca51872a25 Slightly extend documentation of fn-update syntax with more exampleMachine:oven2 4.13.0-37-generic x86_64 GNU/Linux Claimed job Building HOL Starting developers Finished developers 0s 20MB Starting developers/bin Finished developers/bin 32s 140MB Starting semantics/ffi Finished semantics/ffi 34s 472MB Starting semantics Finished semantics 1m32s 870MB Starting semantics/proofs Finished semantics/proofs 3m03s 1GB Starting basis/pure Finished basis/pure 3m38s 769MB Starting translator Finished translator 1m15s 1GB Starting compiler/parsing Finished compiler/parsing 1m17s 2GB Starting characteristic Finished characteristic 2m32s 1GB Starting translator/monadic Finished translator/monadic 1m27s 1GB Starting basis Finished basis 16m09s 3GB Starting compiler/inference Finished compiler/inference 1m58s 1GB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 48s 909MB Starting compiler/backend/gc Finished compiler/backend/gc 7m33s 2GB Starting compiler/backend Finished compiler/backend 1s 17MB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 17MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 47s 531MB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 1m40s 1GB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 23s 455MB Starting compiler/encoders/mips Finished compiler/encoders/mips 55s 863MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 1m00s 863MB Starting compiler/encoders/ag32 Finished compiler/encoders/ag32 15s 770MB Starting compiler/backend/x64 Finished compiler/backend/x64 17s 1GB Starting compiler/backend/arm6 Finished compiler/backend/arm6 17s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 17s 1GB Starting compiler/backend/mips Finished compiler/backend/mips 17s 1GB Starting compiler/backend/riscv Finished compiler/backend/riscv 17s 1GB Starting compiler/backend/ag32 Finished compiler/backend/ag32 1m13s 1GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 6m12s 908MB Starting compiler/inference/proofs Finished compiler/inference/proofs 2m54s 932MB Starting compiler/backend/semantics Finished compiler/backend/semantics 9m12s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 2m49s 508MB Starting compiler/backend/proofs Finished compiler/backend/proofs 43m26s 3GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 10m27s 5GB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 14m55s 3GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 6m09s 1GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 10m27s 2GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 8m02s 863MB Starting compiler/encoders/ag32/proofs Finished compiler/encoders/ag32/proofs 2m45s 955MB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 19s 1GB Starting compiler/backend/arm6/proofs Finished compiler/backend/arm6/proofs 21s 872MB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 18s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 20s 1GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 19s 1GB Starting compiler/backend/ag32/proofs Finished compiler/backend/ag32/proofs 9m36s 2GB Starting compiler/proofs Finished compiler/proofs 1m18s 2GB Starting candle/set-theory Finished candle/set-theory 30s 628MB Starting candle/syntax-lib Finished candle/syntax-lib 9s 563MB Starting candle/standard/syntax Finished candle/standard/syntax 1m33s 683MB Starting candle/standard/semantics Finished candle/standard/semantics 1m19s 832MB Starting candle/standard/monadic Finished candle/standard/monadic 1m34s 1GB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 15m16s 2GB Starting candle/standard/opentheory Finished candle/standard/opentheory 7m50s 2GB Starting candle/standard/opentheory/compilation Finished candle/standard/opentheory/compilation 29m27s 23GB Starting candle/standard/opentheory/compilation/proofs Finished candle/standard/opentheory/compilation/proofs 36s 4GB Starting characteristic/examples Finished characteristic/examples 1m28s 1GB Starting tutorial/solutions Finished tutorial/solutions 13m13s 6GB Starting translator/monadic/examples Finished translator/monadic/examples 1m51s 2GB Starting examples Finished examples 6m26s 3GB Starting examples/compilation/x64 Finished examples/compilation/x64 1h56m03s 10GB Starting examples/compilation/x64/proofs Finished examples/compilation/x64/proofs 1m47s 3GB Starting examples/compilation/ag32 Finished examples/compilation/ag32 26m19s 3GB Starting examples/compilation/ag32/proofs Finished examples/compilation/ag32/proofs 28s 2GB Starting compiler/benchmarks Finished compiler/benchmarks 0s 4MB Starting translator/okasaki-examples Finished translator/okasaki-examples 3m31s 1GB Starting translator/other-examples Finished translator/other-examples 3m13s 1GB Starting compiler/parsing/tests Finished compiler/parsing/tests 25s 337MB Starting compiler/inference/tests Finished compiler/inference/tests 4m06s 2GB Starting compiler/bootstrap/translation Finished compiler/bootstrap/translation 3h13m38s 51GB Starting unverified/sexpr-bootstrap/x64/64 Finished unverified/sexpr-bootstrap/x64/64 8m06s 13GB Starting unverified/sexpr-bootstrap/x64/32 Finished unverified/sexpr-bootstrap/x64/32 5m25s 17GB Starting compiler/bootstrap/compilation/x64/64