OverviewCakeML:a8b9659ecd65278efdf70d9d258350039548a605
Use modules in bootstrap translation.
#537 (translator-mods)
Merging into:cc95061c249ee1e7010fa61ef0171faa133fc739
Merge pull request #533 from CakeML/remove-cheats
HOL:2b21ba94b82750c0305d602c746adbc223f4e3ca
Merge pull request #595 from talsewell/perms
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 32s 196MB
Starting semantics/ffi
Finished semantics/ffi 34s 405MB
Starting semantics
Finished semantics 1m19s 924MB
Starting semantics/proofs
Finished semantics/proofs 2m41s 951MB
Starting basis/pure
Finished basis/pure 3m26s 879MB
Starting translator
Finished translator 2m58s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m12s 1GB
Starting characteristic
Finished characteristic 2m22s 1GB
Starting translator/monadic
Finished translator/monadic 1m22s 1GB
Starting basis
Finished basis 16m44s 3GB
Starting compiler/inference
Finished compiler/inference 1m40s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 46s 791MB
Starting compiler/backend/gc
Finished compiler/backend/gc 9m53s 3GB
Starting compiler/backend
Finished compiler/backend 2s 18MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 15MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 54s 598MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 1m47s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 25s 450MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 56s 807MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 59s 918MB
Starting compiler/backend/x64
Finished compiler/backend/x64 17s 903MB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 18s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 16s 888MB
Starting compiler/backend/mips
Finished compiler/backend/mips 18s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 18s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 6m04s 819MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m52s 928MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 8m55s 1GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 7m04s 473MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 41m06s 4GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 7m14s 3GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 7m31s 4GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 5m22s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 7m27s 1GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m00s 804MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 19s 1GB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 22s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 18s 819MB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 19s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 19s 1GB
Starting compiler/proofs
Finished compiler/proofs 1m17s 2GB
Starting candle/set-theory
Finished candle/set-theory 28s 602MB
Starting candle/syntax-lib
Finished candle/syntax-lib 9s 445MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m30s 836MB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m18s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m32s 739MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 16m02s 8GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 8m42s 7GB
Starting candle/standard/opentheory/compilation
Finished candle/standard/opentheory/compilation 34m55s 26GB
Starting characteristic/examples
Finished characteristic/examples 1m33s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 13m44s 7GB
Starting translator/monadic/examples
Finished translator/monadic/examples 1m43s 2GB
Starting examples
Finished examples 5m40s 5GB
Starting examples/compilation
Finished examples/compilation 1h55m06s 13GB
Starting examples/compilation/proofs
Finished examples/compilation/proofs 1m57s 3GB
Starting compiler/benchmarks
Finished compiler/benchmarks 0s 4MB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 3m44s 1GB
Starting translator/other-examples
Finished translator/other-examples 3m24s 968MB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 25s 305MB
Starting compiler/inference/tests
Finished compiler/inference/tests 4m14s 5GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 7h23m12s 51GB
Starting unverified/sexpr-bootstrap/x64/64
Finished unverified/sexpr-bootstrap/x64/64 8m04s 15GB
Starting unverified/sexpr-bootstrap/x64/32
Finished unverified/sexpr-bootstrap/x64/32 5m10s 16GB
Starting compiler/bootstrap/compilation/x64/64
Finished compiler/bootstrap/compilation/x64/64 15h16m07s 64GB
Starting compiler/bootstrap/compilation/x64/64/proofs
Finished compiler/bootstrap/compilation/x64/64/proofs 4m10s 24GB
Starting compiler/bootstrap/compilation/x64/32
Finished compiler/bootstrap/compilation/x64/32 10h17m09s 58GB
Starting compiler/bootstrap/compilation/x64/32/proofs
Finished compiler/bootstrap/compilation/x64/32/proofs 3m28s 20GB
SUCCESS