OverviewCakeML:37176c66e6292c8902944ddcb5608c5b58462b61
Merge pull request #416 from CakeML/mlton_benchmarks
HOL:17dce4e3a0065d55ecb638375ec7790674a33b73
Prove more theorems about real_of_int connection
Machine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-x64-64.tar.gz
Claimed job
Building HOL
Starting semantics/ffi
Finished semantics/ffi 1m06s 424MB
Starting semantics
Finished semantics 2m38s 842MB
Starting semantics/proofs
Finished semantics/proofs 3m29s 1GB
Starting basis/pure
Finished basis/pure 6m01s 691MB
Starting translator
Finished translator 7m15s 962MB
Starting compiler/parsing
Finished compiler/parsing 2m24s 1GB
Starting characteristic
Finished characteristic 4m44s 1GB
Starting basis
Finished basis 27m43s 2GB
Starting translator/monadic
Finished translator/monadic 3m29s 949MB
Starting compiler/inference
Finished compiler/inference 2m50s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 50s 665MB
Starting compiler/backend/gc
Finished compiler/backend/gc 15m56s 2GB
Starting compiler/backend
Finished compiler/backend 1s 20MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 11MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m15s 421MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 3m09s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 47s 415MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m27s 785MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m31s 477MB
Starting compiler/backend/x64
Finished compiler/backend/x64 42s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 47s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 44s 944MB
Starting compiler/backend/mips
Finished compiler/backend/mips 45s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 44s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 4m45s 643MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 4m15s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 18m59s 4GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1m14s 373MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 1h10m24s 4GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 11m27s 1GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 13m54s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 9m28s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 13m04s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 14m03s 877MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 50s 1GB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 57s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 52s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 54s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 54s 1GB
Starting compiler/proofs
Finished compiler/proofs 2m37s 1GB
Starting candle/set-theory
Finished candle/set-theory 1m41s 661MB
Starting candle/syntax-lib
Finished candle/syntax-lib 20s 545MB
Starting candle/standard/syntax
Finished candle/standard/syntax 3m00s 679MB
Starting candle/standard/semantics
Finished candle/standard/semantics 2m24s 993MB
Starting candle/standard/monadic
Finished candle/standard/monadic 2m46s 887MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 11m14s 2GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 31s 592MB
Starting characteristic/examples
Finished characteristic/examples 2m18s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 32m19s 12GB
Starting examples
Finished examples 7m36s 1GB
Starting examples/compilation
Finished examples/compilation 4h38m12s 12GB
Starting examples/compilation/proofs
Finished examples/compilation/proofs 5m35s 4GB
Starting compiler/benchmarks
Finished compiler/benchmarks 0s 4MB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 7m21s 1GB
Starting translator/other-examples
Finished translator/other-examples 7m11s 1GB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 38s 389MB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 8h16m45s 51GB
Starting compiler/bootstrap/compilation/x64/64
Finished compiler/bootstrap/compilation/x64/64 23h25m31s 96GB
Starting compiler/bootstrap/compilation/x64/64/proofs
Finished compiler/bootstrap/compilation/x64/64/proofs 4m24s 18GB
Starting compiler/bootstrap/compilation/x64/32
Finished compiler/bootstrap/compilation/x64/32 23h23m55s 94GB
Starting compiler/bootstrap/compilation/x64/32/proofs
Finished compiler/bootstrap/compilation/x64/32/proofs 2m44s 19GB
SUCCESS