OverviewCakeML:018eec673b8b703adeecb85ccab09ec91be05cb3
Merge pull request #791 from CakeML/lpr_opt
HOL:841cced433cd0e9e4913c6e9c05c9b7542e38a6b
Handle change to Slavonic asterisk (25dec53e17) in Manual production
Machine:oven5s3 5.7.19 x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 3s 84MB
Starting developers/bin
Finished developers/bin 8s 1GB
Starting semantics/ffi
Finished semantics/ffi 9s 1GB
Starting semantics
Finished semantics 1m12s 2GB
Starting semantics/proofs
Finished semantics/proofs 3m05s 2GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 7s 1GB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m01s 2GB
Starting basis/pure
Finished basis/pure 43s 1GB
Starting translator
Finished translator 2m27s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m02s 2GB
Starting characteristic
Finished characteristic 5m31s 2GB
Starting translator/monadic
Finished translator/monadic 1m25s 2GB
Starting basis
Finished basis 31m32s 11GB
Starting compiler/inference
Finished compiler/inference 56s 2GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 51s 2GB
Starting compiler/backend/gc
Finished compiler/backend/gc 2m51s 2GB
Starting compiler/backend
Finished compiler/backend 3m59s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 21s 1GB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 24s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 47s 2GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 11s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 15s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 13s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 16s 1GB
Starting compiler/backend/x64
Finished compiler/backend/x64 16s 2GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 17s 2GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 16s 2GB
Starting compiler/backend/mips
Finished compiler/backend/mips 16s 2GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 16s 2GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m03s 2GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 4m26s 2GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m15s 2GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 25m22s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m07s 2GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 47m03s 17GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m38s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m57s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m30s 2GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 10m21s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m25s 2GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m25s 2GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 18s 2GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 20s 2GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 18s 2GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 19s 2GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 19s 2GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 12m19s 3GB
Starting compiler/proofs
Finished compiler/proofs 1m26s 3GB
Starting candle/set-theory
Finished candle/set-theory 24s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 9s 1GB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m40s 2GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m38s 3GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m33s 2GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m10s 5GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 2m49s 2GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 12m03s 3GB
Starting characteristic/examples
Finished characteristic/examples 1m09s 4GB
Starting tutorial/solutions
Finished tutorial/solutions 14m08s 7GB
Starting translator/monadic/examples
Finished translator/monadic/examples 2m28s 3GB
Starting examples
Finished examples 6m48s 5GB
Starting examples/compilation/x64
Finished examples/compilation/x64 2h15m17s 15GB
Starting examples/compilation/x64/proofs
Finished examples/compilation/x64/proofs 1m20s 3GB
Starting examples/compilation/ag32
Finished examples/compilation/ag32 31m41s 6GB
Starting examples/compilation/ag32/proofs
Finished examples/compilation/ag32/proofs 41s 4GB
Starting examples/cost
Finished examples/cost 44m55s 6GB
Starting examples/lpr_checker
Finished examples/lpr_checker 3m34s 2GB
Starting examples/lpr_checker/compilation
Finished examples/lpr_checker/compilation 16m20s 9GB
Starting examples/lpr_checker/compilation/proofs
Finished examples/lpr_checker/compilation/proofs 37s 3GB
Starting examples/lpr_checker/array
Finished examples/lpr_checker/array 14m05s 4GB
Starting examples/lpr_checker/array/compilation
Finished examples/lpr_checker/array/compilation 19m02s 10GB
Starting examples/lpr_checker/array/compilation/proofs
Finished examples/lpr_checker/array/compilation/proofs 44s 4GB
Starting examples/opentheory
Finished examples/opentheory 9m06s 6GB
Starting examples/opentheory
Finished examples/opentheory 1s 21MB
Starting examples/opentheory/compilation
Finished examples/opentheory/compilation 30m56s 19GB
Starting examples/opentheory/compilation/proofs
Finished examples/opentheory/compilation/proofs 36s 3GB
Starting examples/opentheory/compilation/ag32
Finished examples/opentheory/compilation/ag32 32m30s 17GB
Starting examples/opentheory/compilation/ag32/proofs
Finished examples/opentheory/compilation/ag32/proofs 1m28s 5GB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 3m57s 2GB
Starting translator/other-examples
Finished translator/other-examples 34s 2GB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 22s 2GB
Resuming compiler/inference/tests
Finished compiler/inference/tests 4m20s 5GB
Starting compiler/bootstrap/translation
FAILED: compiler/bootstrap/translation
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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$(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/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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[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
Starting work on monadic_encTheory
Starting work on README.md
Starting work on to_flatProgTheory
README.md real: 0s user: 0s OK
monadic_encTheory real: 9s user: 8s OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory real: 12s user: 11s OK
monadic_enc32Theory real: 12s user: 11s OK
to_flatProgTheory real: 396s user: 390s OK
Starting work on to_closProgTheory
to_closProgTheory real: 396s user: 390s OK
Starting work on to_bvlProgTheory
to_bvlProgTheory real: 376s user: 368s OK
Starting work on to_bviProgTheory
to_bviProgTheory real: 315s user: 308s OK
Starting work on to_dataProgTheory
to_dataProgTheory real: 165s user: 161s OK
Starting work on lexerProgTheory
lexerProgTheory real: 233s user: 230s OK
Starting work on parserProgTheory
parserProgTheory real: 479s user: 469s OK
Starting work on reg_allocProgTheory
reg_allocProgTheory real: 919s user: 903s OK
Starting work on inferProgTheory
inferProgTheory real: 988s user: 978s OK
Starting work on explorerProgTheory
explorerProgTheory real: 668s user: 660s OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory real: 260s user: 248s OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word32ProgTheory real: 1070s user: 1049s OK
Starting work on to_target32ProgTheory
to_word64ProgTheory real: 1109s user: 1079s OK
Starting work on to_target64ProgTheory
to_target32ProgTheory real: 626s user: 608s OK
Starting work on arm7ProgTheory
to_target64ProgTheory real: 642s user: 619s OK
Starting work on x64ProgTheory
arm7ProgTheory real: 258s user: 251s OK
Starting work on ag32ProgTheory
x64ProgTheory real: 214s user: 206s OK
Starting work on arm8ProgTheory
ag32ProgTheory real: 187s user: 179s OK
Starting work on compiler32ProgTheory
arm8ProgTheory real: 231s user: 223s OK
Starting work on riscvProgTheory
riscvProgTheory real: 21s user: 18sFAIL<1>
Heap: Resizing from 4.27G to 4.27G. Estimated ratio 6.65
GC: Completed with insufficient space
Heap: Full GC (after) Major heap used 754.60M of 806.36M (94%). Alloc space used 31.81M of 777.00M (4%). Total space 4.27G 18% full.
Heap: Local spaces 1548, permanent spaces 35, code spaces 97, stack spaces 2
Heap: Code area: total 916.00K occupied: 636.30K
Heap: Stack area: total 2.00M
Uncaught exception: Interrupt
GC (Total): Non-GC time: CPU user: 11.464 system: 1.148 real: 13.363
GC (Total): GC time: CPU user: 7.523 system: 0.428 real: 7.951
Heap: Total CPU GC time 7.951secs, Non-GC 12.612secs, ratio 0.630
compiler32ProgTheory M-KILLED