Overview

Job 22

CakeML:17a3f934e17ae9231719fe54e90a889ffb28eb9d
  Make new ffi type an actual type (was abbreviation)
HOL:35c71676c41ba3f906572b8a9afe0b1052f1ec35
  Merge pull request #493 from abxy/bugfix/hol-mode-clean-leading-tacti
Machine:cakeml1852 4.4.0-22-generic x86_64 GNU/Linux
Artefacts:cake-x64.tar.gz
cake-riscv.tar.gz

 Claimed job
 Building HOL
 Starting semantics/ffi
 Finished semantics/ffi                                         1m07s 359MB
 Starting semantics
 Finished semantics                                             2m37s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m24s   1GB
 Starting basis/pure
 Finished basis/pure                                            5m58s 729MB
 Starting translator
 Finished translator                                            7m01s 958MB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m24s   1GB
 Starting characteristic
 Finished characteristic                                        4m36s   1GB
 Starting basis
 Finished basis                                                28m54s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    3m48s   1GB
 Starting compiler/inference
 Finished compiler/inference                                    2m43s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              48s 696MB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  15m44s   2GB
 Starting compiler/backend
 Finished compiler/backend                                         1s  14MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  13MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m11s 453MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                3m00s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  46s 445MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m19s 726MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m33s 457MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    39s 895MB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   44s 989MB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   43s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   41s 960MB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  43s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m40s 869MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             4m19s 930MB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           19m05s   4GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     1m11s 428MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                            1h11m35s   4GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         11m38s 978MB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        14m06s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         9m42s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        13m46s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       13m55s   1GB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             51s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            56s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            51s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            51s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           51s   1GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m41s   1GB
 Starting candle/set-theory
 Finished candle/set-theory                                     1m40s 653MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       21s 546MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                2m59s 713MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             2m26s 907MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               2m50s 863MB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            11m45s   2GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                              29s 633MB
 Starting characteristic/examples
 Finished characteristic/examples                               2m03s   1GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   31m29s  10GB
 Starting examples
 Finished examples                                              8m45s   2GB
 Starting examples/compilation
 Finished examples/compilation                               4h04m53s  11GB
 Starting examples/compilation/proofs
 Finished examples/compilation/proofs                           5m14s   3GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                1h39m53s  14GB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                           7m25s   1GB
 Starting translator/other-examples
 Finished translator/other-examples                             6m42s   1GB
 Starting compiler/parsing/tests
 Finished compiler/parsing/tests                                  37s 388MB
 Starting compiler/bootstrap/translation
 Finished compiler/bootstrap/translation                     7h23m53s  30GB
 Starting compiler/bootstrap/translation/x64
 Finished compiler/bootstrap/translation/x64                   17m58s  38GB
 Starting compiler/bootstrap/compilation/x64
 Resuming compiler/bootstrap/compilation/x64
 Finished compiler/bootstrap/compilation/x64                       3s  16MB
 Starting compiler/bootstrap/compilation/x64/proofs
 Finished compiler/bootstrap/compilation/x64/proofs             2m46s  21GB
 Starting compiler/bootstrap/translation/riscv
 Finished compiler/bootstrap/translation/riscv                 19m27s  21GB
 Starting compiler/bootstrap/compilation/riscv
 Finished compiler/bootstrap/compilation/riscv              18h32m21s  89GB
 SUCCESS