Overview

Job 1492

CakeML:3d4a96b446a3347e5cb94f1b123332937de84554
  Fix reference to HOL examples theory that has moved
HOL:2940fb376d13d7cba972ad9c7ab6d10ccb02c638
  Fix a reference to a theorem I deleted in 7ddaf003f4
Machine:oven3 4.19.67.1.amd64-smp
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               7s 141MB
 Starting developers/bin
 Finished developers/bin                                          12s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           24s 267MB
 Starting semantics
 Finished semantics                                             3m02s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      7m22s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 20s 320MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        4m38s   1GB
 Starting basis/pure
 Finished basis/pure                                            6m14s 870MB
 Starting translator
 Finished translator                                            5m42s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m30s   2GB
 Starting characteristic
 Finished characteristic                                       12m49s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    3m29s   1GB
 Starting basis
 Finished basis                                              1h32m53s  18GB
 Starting compiler/inference
 Finished compiler/inference                                    2m30s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            2m05s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   6m47s   2GB
 Starting compiler/backend
 Finished compiler/backend                                      9m17s   4GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   47s 743MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 2m18s 817MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                4m28s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                1m21s 780MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                3m09s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               3m43s   1GB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  40s 882MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    37s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   41s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   43s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   40s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  42s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 2m26s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                              12m07s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             5m23s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                         1h02m54s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     7m38s 982MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                            1h41m02s  23GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         21m20s   4GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        29m40s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                        15m16s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        22m51s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       20m24s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         5m43s 881MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             46s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            47s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            45s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            47s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           47s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                         28m14s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       3m58s   4GB
 Starting candle/set-theory
 Finished candle/set-theory                                       56s 769MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       23s 648MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                3m54s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             3m55s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               3m43s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            11m38s   5GB
 Starting candle/overloading/syntax
 Finished candle/overloading/syntax                             6m39s   1GB
 Starting candle/overloading/semantics
 Finished candle/overloading/semantics                         27m04s   2GB
 Starting characteristic/examples
 Finished characteristic/examples                               2m44s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   33m47s  14GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           5m51s   2GB
 Starting examples
 Finished examples                                             15m05s   3GB
 Starting examples/compilation/x64
 Finished examples/compilation/x64                           5h10m55s  13GB
 Starting examples/compilation/x64/proofs
 Finished examples/compilation/x64/proofs                       3m10s   2GB
 Starting examples/compilation/ag32
 Finished examples/compilation/ag32                          1h14m31s   7GB
 Starting examples/compilation/ag32/proofs
 Finished examples/compilation/ag32/proofs                      1m35s   3GB
 Starting examples/cost
 Finished examples/cost                                      1h51m14s   7GB
 Starting examples/lpr_checker
 Finished examples/lpr_checker                                  8m13s   2GB
 Starting examples/lpr_checker/compilation
 Finished examples/lpr_checker/compilation                     36m08s  10GB
 Starting examples/lpr_checker/compilation/proofs
 Finished examples/lpr_checker/compilation/proofs               1m23s   3GB
 Starting examples/lpr_checker/array
 Finished examples/lpr_checker/array                           31m43s   4GB
 Starting examples/lpr_checker/array/compilation
 Finished examples/lpr_checker/array/compilation               42m27s  12GB
 Starting examples/lpr_checker/array/compilation/proofs
 Finished examples/lpr_checker/array/compilation/proofs         1m41s   3GB
 Starting examples/opentheory
 Finished examples/opentheory                                  19m55s   4GB
 Starting examples/opentheory
 Finished examples/opentheory                                      2s  33MB
 Starting examples/opentheory/compilation
 Finished examples/opentheory/compilation                    1h08m47s  20GB
 Starting examples/opentheory/compilation/proofs
 Finished examples/opentheory/compilation/proofs                1m25s   4GB
 Starting examples/opentheory/compilation/ag32
 Finished examples/opentheory/compilation/ag32               1h14m52s  18GB
 Starting examples/opentheory/compilation/ag32/proofs
 Finished examples/opentheory/compilation/ag32/proofs           3m17s   5GB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                           8m42s   1GB
 Starting translator/other-examples
 Finished translator/other-examples                             3m51s   1GB
 Starting compiler/parsing/tests
 Finished compiler/parsing/tests                                  57s 585MB
 Starting compiler/inference/tests
 Finished compiler/inference/tests                             14m59s   3GB
 Starting compiler/bootstrap/translation
 Finished compiler/bootstrap/translation                     5h08m00s  55GB
 Starting unverified/sexpr-bootstrap/x64/64
 Finished unverified/sexpr-bootstrap/x64/64                    24m15s   8GB
 Starting unverified/sexpr-bootstrap/x64/32
 Finished unverified/sexpr-bootstrap/x64/32                    20m52s   8GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      3s  32MB
 Starting compiler/bootstrap/compilation/x64/64
 Finished compiler/bootstrap/compilation/x64/64             26h38m54s 109GB
 Starting compiler/bootstrap/compilation/x64/64/proofs
 Finished compiler/bootstrap/compilation/x64/64/proofs          4m26s  18GB
 Starting compiler/bootstrap/compilation/x64/32
 Finished compiler/bootstrap/compilation/x64/32             21h25m02s  68GB
 Starting compiler/bootstrap/compilation/x64/32/proofs
 Finished compiler/bootstrap/compilation/x64/32/proofs          4m19s  14GB
 Starting compiler/bootstrap/compilation/ag32/32
 Finished compiler/bootstrap/compilation/ag32/32            24h35m21s  86GB
 Starting compiler/bootstrap/compilation/ag32/32/proofs
 Finished compiler/bootstrap/compilation/ag32/32/proofs        19m23s  38GB
 SUCCESS