CakeML:609a5b400ab059bf8de77c3081c6f987f0f4ae09 Add monadic translator examples backHOL:c3abae06e308d6ad1836808d5c3ea1a9637c0376 Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOLMachine:cakeml1795 4.4.0-98-generic x86_64 GNU/LinuxArtefacts:cake-x64-64.tar.gz cake-x64-32.tar.gz Claimed job Reusing HOL Starting semantics/ffi Finished semantics/ffi 20s 263MB Starting semantics Finished semantics 2m06s 1GB Starting semantics/proofs Finished semantics/proofs 3m27s 1GB Starting basis/pure Finished basis/pure 1m19s 617MB Starting translator Finished translator 6m58s 1GB Starting compiler/parsing Finished compiler/parsing 2m18s 2GB Starting characteristic Finished characteristic 4m31s 1GB Starting basis Finished basis 33m44s 2GB Starting translator/monadic Finished translator/monadic 1s 18MB Starting compiler/inference Finished compiler/inference 2m10s 1GB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 48s 784MB Starting compiler/backend/gc Finished compiler/backend/gc 14m07s 4GB Starting compiler/backend Finished compiler/backend 2s 14MB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 21MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 32s 489MB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 1m26s 552MB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 14s 401MB Starting compiler/encoders/mips Finished compiler/encoders/mips 19s 461MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 16s 430MB Starting compiler/backend/x64 Finished compiler/backend/x64 39s 1GB Starting compiler/backend/arm6 Finished compiler/backend/arm6 46s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 40s 1GB Starting compiler/backend/mips Finished compiler/backend/mips 43s 1GB Starting compiler/backend/riscv Finished compiler/backend/riscv 43s 1GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 4m25s 892MB Starting compiler/inference/proofs Finished compiler/inference/proofs 4m12s 1GB Starting compiler/backend/semantics Finished compiler/backend/semantics 18m26s 3GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 1m17s 505MB Starting compiler/backend/proofs Finished compiler/backend/proofs 1h07m53s 4GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 10m53s 1GB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 10m35s 948MB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 8m34s 1GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 11m19s 2GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 13m33s 989MB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 52s 1GB Starting compiler/backend/arm6/proofs Finished compiler/backend/arm6/proofs 54s 1GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 49s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 51s 1GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 52s 1GB Starting compiler/proofs Finished compiler/proofs 2m44s 2GB Starting candle/set-theory Finished candle/set-theory 45s 554MB Starting candle/syntax-lib Finished candle/syntax-lib 19s 590MB Starting candle/standard/syntax Finished candle/standard/syntax 2m53s 630MB Starting candle/standard/semantics Finished candle/standard/semantics 2m19s 861MB Starting candle/standard/monadic Finished candle/standard/monadic 2m36s 989MB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 10m43s 2GB Starting candle/standard/opentheory Finished candle/standard/opentheory 28s 705MB Starting characteristic/examples Finished characteristic/examples 2m31s 1GB Starting tutorial/solutions Finished tutorial/solutions 37m10s 10GB Starting translator/monadic/examples Finished translator/monadic/examples 3m28s 3GB Starting examples Finished examples 8m29s 2GB Starting examples/compilation Finished examples/compilation 5h58m17s 17GB Starting examples/compilation/proofs Finished examples/compilation/proofs 6m17s 5GB Starting compiler/benchmarks Finished compiler/benchmarks 0s 4MB Starting translator/okasaki-examples Finished translator/okasaki-examples 7m04s 1GB Starting translator/other-examples Finished translator/other-examples 57s 1GB Starting compiler/parsing/tests Finished compiler/parsing/tests 37s 392MB Starting compiler/bootstrap/translation Finished compiler/bootstrap/translation 8h40m32s 35GB Starting compiler/bootstrap/compilation/x64/64 Finished compiler/bootstrap/compilation/x64/64 26h36m30s 97GB Starting compiler/bootstrap/compilation/x64/64/proofs Finished compiler/bootstrap/compilation/x64/64/proofs 7m01s 25GB Starting compiler/bootstrap/compilation/x64/32 Finished compiler/bootstrap/compilation/x64/32 23h00m58s 89GB Starting compiler/bootstrap/compilation/x64/32/proofs Finished compiler/bootstrap/compilation/x64/32/proofs 3m23s 25GB SUCCESS