OverviewCakeML:de1a9c9091a35102041035a513fdb4a67afc0a06
Make x64 .S template more robust against PIC
HOL:55ec86f14c6689ab158f12ef0d7818adfea3a160
More useful theorems about the rationals
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux
Artefacts:cake-riscv.tar.gz
cake-x64.tar.gz
Claimed job
Building HOL
Starting semantics/ffi
Finished semantics/ffi 1m07s 349MB
Starting semantics
Finished semantics 2m39s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m33s 988MB
Starting basis/pure
Finished basis/pure 6m05s 726MB
Starting translator
Finished translator 7m08s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m24s 1GB
Starting characteristic
Finished characteristic 4m42s 1GB
Starting basis
Finished basis 27m50s 2GB
Starting translator/monadic
Finished translator/monadic 3m40s 1GB
Starting compiler/inference
Finished compiler/inference 2m48s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 49s 788MB
Starting compiler/backend/gc
Finished compiler/backend/gc 16m10s 2GB
Starting compiler/backend
Finished compiler/backend 1s 23MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 11MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m14s 432MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 3m00s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 47s 382MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m19s 755MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m29s 444MB
Starting compiler/backend/x64
Finished compiler/backend/x64 39s 856MB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 45s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 43s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 43s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 42s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 4m50s 708MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 4m23s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 19m31s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1m11s 379MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 1h12m00s 6GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 11m53s 1GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 13m56s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 9m27s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 13m26s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 14m22s 859MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 53s 1GB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 1m01s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 52s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 57s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 55s 1GB
Starting compiler/proofs
Finished compiler/proofs 1m56s 1GB
Starting candle/set-theory
Finished candle/set-theory 1m46s 545MB
Starting candle/syntax-lib
Finished candle/syntax-lib 21s 554MB
Starting candle/standard/syntax
Finished candle/standard/syntax 3m07s 822MB
Starting candle/standard/semantics
Finished candle/standard/semantics 2m30s 719MB
Starting candle/standard/monadic
Finished candle/standard/monadic 2m53s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 12m03s 3GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 31s 578MB
Starting characteristic/examples
Finished characteristic/examples 2m10s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 33m33s 8GB
Starting examples
Finished examples 7m44s 2GB
Starting examples/compilation
Finished examples/compilation 4h12m14s 14GB
Starting examples/compilation/proofs
Finished examples/compilation/proofs 5m24s 3GB
Starting compiler/benchmarks
Finished compiler/benchmarks 1h45m50s 24GB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 7m33s 1GB
Starting translator/other-examples
Finished translator/other-examples 7m08s 902MB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 38s 352MB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 7h40m57s 22GB
Starting compiler/bootstrap/translation/x64
Finished compiler/bootstrap/translation/x64 18m11s 36GB
Starting compiler/bootstrap/compilation/x64
Finished compiler/bootstrap/compilation/x64 16h00m59s 83GB
Starting compiler/bootstrap/compilation/x64/proofs
Finished compiler/bootstrap/compilation/x64/proofs 3m03s 22GB
Starting compiler/bootstrap/translation/riscv
Finished compiler/bootstrap/translation/riscv 19m45s 40GB
Starting compiler/bootstrap/compilation/riscv
Finished compiler/bootstrap/compilation/riscv 21h48m23s 90GB
SUCCESS