Overview

Job 1366

CakeML:9a0180ee6a0bbcf4cc2d2aee6efc20caa0f62e95
  Add sexpr files to cake-x64-64.tar.gz artefact
#788 (symbols)
Merging into:411c80da717a8e99b5a8e7f6519e95637ecb7225
  Merge pull request #752 from sorear/rv_fixes
HOL:841cced433cd0e9e4913c6e9c05c9b7542e38a6b
  Handle change to Slavonic asterisk (25dec53e17) in Manual production
Machine:oven5s2 5.7.19 x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               1s 120MB
 Starting developers/bin
 Finished developers/bin                                           8s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           11s   4GB
 Starting semantics
 Finished semantics                                             2m02s   8GB
 Starting semantics/proofs
 Finished semantics/proofs                                      5m49s   8GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 13s   4GB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        3m10s   8GB
 Starting basis/pure
 Finished basis/pure                                            4m09s   8GB
 Starting translator
 Finished translator                                            3m35s   8GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m24s   9GB
 Starting characteristic
 Finished characteristic                                        5m28s   8GB
 Starting translator/monadic
 Finished translator/monadic                                    1m29s   8GB
 Starting basis
 Finished basis                                                31m53s  29GB
 Starting compiler/inference
 Finished compiler/inference                                    1m05s   8GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              50s   8GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   3m01s   8GB
 Starting compiler/backend
 Finished compiler/backend                                      3m59s   8GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   21s   8GB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m00s   8GB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                1m58s   8GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  38s   8GB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m23s   8GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m29s   8GB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  17s   8GB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    16s   8GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   17s   8GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   16s   8GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   17s   8GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  17s   8GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                   58s   8GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m41s   8GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m12s   8GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           24m04s  11GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m23s   8GB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              49m00s  17GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          8m51s  16GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        12m40s  13GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m37s  12GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        10m35s  13GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m22s   8GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m28s   8GB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             21s   8GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            22s   8GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            21s   8GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            21s   8GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           21s   8GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                         11m30s  16GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m48s  10GB
 Starting candle/set-theory
 Finished candle/set-theory                                       24s   8GB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s   8GB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m36s   8GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m38s   8GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m33s   8GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             4m54s  16GB
 Starting candle/overloading/syntax
 Finished candle/overloading/syntax                             2m41s   8GB
 Starting candle/overloading/semantics
 Finished candle/overloading/semantics                         11m28s   8GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m14s  13GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   13m22s  20GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           2m45s  12GB
 Starting examples
 Finished examples                                              6m56s  16GB
 Starting examples/compilation/x64
 Finished examples/compilation/x64                           2h00m01s  37GB
 Starting examples/compilation/x64/proofs
 Finished examples/compilation/x64/proofs                       1m29s   9GB
 Starting examples/compilation/ag32
 Finished examples/compilation/ag32                            27m33s  19GB
 Starting examples/compilation/ag32/proofs
 Finished examples/compilation/ag32/proofs                        41s   9GB
 Starting examples/cost
 Finished examples/cost                                        40m23s  23GB
 Starting examples/lpr_checker
 Finished examples/lpr_checker                                  3m33s  16GB
 Starting examples/lpr_checker/compilation
 Finished examples/lpr_checker/compilation                     14m35s  21GB
 Starting examples/lpr_checker/compilation/proofs
 Finished examples/lpr_checker/compilation/proofs                 37s   8GB
 Resuming examples/lpr_checker/array
 Finished examples/lpr_checker/array                           12m51s  16GB
 Starting examples/lpr_checker/array/compilation
 Finished examples/lpr_checker/array/compilation               17m28s  24GB
 Starting examples/lpr_checker/array/compilation/proofs
 Finished examples/lpr_checker/array/compilation/proofs           45s   9GB
 Starting examples/opentheory
 Finished examples/opentheory                                   8m31s  16GB
 Starting examples/opentheory
 Finished examples/opentheory                                      0s  57MB
 Starting examples/opentheory/compilation
 Finished examples/opentheory/compilation                      30m32s  52GB
 Starting examples/opentheory/compilation/proofs
 Finished examples/opentheory/compilation/proofs                  37s   9GB
 Starting examples/opentheory/compilation/ag32
 Finished examples/opentheory/compilation/ag32                 30m55s  33GB
 Starting examples/opentheory/compilation/ag32/proofs
 Finished examples/opentheory/compilation/ag32/proofs           1m27s  15GB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                           3m41s   8GB
 Starting translator/other-examples
 Finished translator/other-examples                             1m45s   8GB
 Starting compiler/parsing/tests
 Finished compiler/parsing/tests                                  22s   8GB
 Starting compiler/inference/tests
 Finished compiler/inference/tests                              3m55s   8GB
 Starting compiler/bootstrap/translation
 Finished compiler/bootstrap/translation                     2h27m45s  82GB
 Starting unverified/sexpr-bootstrap/x64/64
 Finished unverified/sexpr-bootstrap/x64/64                     8m54s  12GB
 Starting unverified/sexpr-bootstrap/x64/32
 Finished unverified/sexpr-bootstrap/x64/32                     7m24s  11GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      1s  58MB
 Starting compiler/bootstrap/compilation/x64/64
 FAILED: compiler/bootstrap/compilation/x64/64
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                                                                                                                                                                                                                      real:    0s  user:    0s     OK
cake-sexpr-32                                                                                                                                                                                                                                  real:   67s  user:   60s     OK
cake-sexpr-64                                                                                                                                                                                                                                  real:   71s  user:   63s     OK
to_dataBootstrapTheory                                                                                                                                                                                                                         real: 3413s  user: 3353s     OK
Starting work on to_lab_x64BootstrapTheory
to_lab_x64BootstrapTheory                                                                                                                                                                                                                      real:   75s  user:   69sFAIL<1>
 Heap: Resizing from 20.92G to 20.92G.  Estimated ratio 7.68
 GC: Completed with insufficient space
 Heap: Full GC (after) Major heap used 2.74G of 2.75G (100%). Alloc space used 379.71M of 6.36G (6%). Total space 20.92G 15% full.
 Heap: Local spaces 8990, permanent spaces 31, code spaces 740, stack spaces 2
 Heap: Code area: total 4.74M occupied: 3.34M
 Heap: Stack area: total 4.00M
 Uncaught exception: Interrupt
 GC (Total): Non-GC time: CPU user: 41.304 system: 5.122 real: 46.532
 GC (Total): GC time: CPU user: 27.708 system: 1.295 real: 29.006
 Heap: Total CPU GC time 29.003secs,  Non-GC 46.427secs, ratio 0.625