OverviewCakeML:d594f73a33abc00808d85fecff9ed7b3797d4aa5
Fix stack_to_labProof: shadowed binding
#497 (labs_exist)
Merging into:645d4af010862abf8d2245a879b09d51e48d9afc
Update lem files (Tested with Lem 7405e91)
HOL:7ed3f12092db2062b6fccb60e9735143ecd5c7e5
Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOL
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers/bin
Finished developers/bin 8s 224MB
Starting semantics/ffi
Finished semantics/ffi 16s 238MB
Starting semantics
Finished semantics 1m59s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m17s 1GB
Starting basis/pure
Finished basis/pure 1m27s 725MB
Starting translator
Finished translator 6m40s 985MB
Starting compiler/parsing
Finished compiler/parsing 2m14s 2GB
Starting characteristic
Finished characteristic 4m26s 1GB
Starting basis
Finished basis 28m57s 2GB
Starting translator/monadic
Finished translator/monadic 2s 11MB
Starting compiler/inference
Finished compiler/inference 2m07s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 55s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 13m11s 3GB
Starting compiler/backend
Finished compiler/backend 3s 14MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 11MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 26s 404MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 1m11s 414MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 12s 368MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 15s 494MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 12s 409MB
Starting compiler/backend/x64
Finished compiler/backend/x64 31s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 34s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 33s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 32s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 29s 929MB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 3m58s 884MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 3m57s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 13m59s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1m23s 445MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 55m53s 3GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m41s 1GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 9m42s 1GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 7m55s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 10m40s 1GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 12m24s 1GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 34s 1GB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 37s 897MB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 33s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 34s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 35s 1GB
Starting compiler/proofs
Finished compiler/proofs 2m26s 2GB
Starting candle/set-theory
Finished candle/set-theory 45s 587MB
Starting candle/syntax-lib
Finished candle/syntax-lib 17s 538MB
Starting candle/standard/syntax
Finished candle/standard/syntax 2m45s 752MB
Starting candle/standard/semantics
Finished candle/standard/semantics 2m15s 903MB
Starting candle/standard/monadic
Finished candle/standard/monadic 2m22s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 10m18s 2GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 24s 666MB
Starting characteristic/examples
Finished characteristic/examples 2m24s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 35m08s 11GB
Starting translator/monadic/examples
Finished translator/monadic/examples 2m58s 2GB
Starting examples
Finished examples 8m05s 2GB
Starting examples/compilation
Finished examples/compilation 5h45m57s 23GB
Starting examples/compilation/proofs
Finished examples/compilation/proofs 5m25s 5GB
Starting compiler/benchmarks
Finished compiler/benchmarks 0s 4MB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 6m34s 1GB
Starting translator/other-examples
Finished translator/other-examples 53s 697MB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 40s 360MB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 8h09m56s 42GB
Starting unverified/sexpr-bootstrap/x64/64
Finished unverified/sexpr-bootstrap/x64/64 11m15s 14GB
Starting unverified/sexpr-bootstrap/x64/32
Finished unverified/sexpr-bootstrap/x64/32 9m00s 13GB
Starting compiler/bootstrap/compilation/x64/64
Finished compiler/bootstrap/compilation/x64/64 26h33m11s 95GB
Starting compiler/bootstrap/compilation/x64/64/proofs
Finished compiler/bootstrap/compilation/x64/64/proofs 5m21s 26GB
Starting compiler/bootstrap/compilation/x64/32
Resuming compiler/bootstrap/compilation/x64/32
Finished compiler/bootstrap/compilation/x64/32 24h14m59s 89GB
Starting compiler/bootstrap/compilation/x64/32/proofs
Finished compiler/bootstrap/compilation/x64/32/proofs 6m20s 24GB
SUCCESS