OverviewCakeML:747a323c230d3c8f26d9ff8769b6fba15056be00
Update HOL_STORE precondition theorem
#511 (argparse)
Merging into:1bb8663a0aeb377eb22aeb600de4bc536e647744
Merge pull request #519 from CakeML/basis_ffi-fix
HOL:76194473b2249ceab539f6265399c7749c579965
Delete unnecessary code in Conv.testconv
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 37s 913MB
Starting semantics/ffi
Finished semantics/ffi 39s 390MB
Starting semantics
Finished semantics 1m28s 980MB
Starting semantics/proofs
Finished semantics/proofs 2m45s 1GB
Starting basis/pure
Finished basis/pure 3m43s 687MB
Starting translator
Finished translator 1m15s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m40s 1GB
Starting characteristic
Finished characteristic 2m40s 1GB
Starting translator/monadic
Finished translator/monadic 1m26s 1GB
Starting basis
Finished basis 22m45s 4GB
Starting compiler/inference
Finished compiler/inference 2m19s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m06s 915MB
Starting compiler/backend/gc
Finished compiler/backend/gc 12m15s 3GB
Starting compiler/backend
Finished compiler/backend 2s 18MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 1s 14MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 59s 642MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 1m59s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 28s 458MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m02s 862MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m03s 665MB
Starting compiler/backend/x64
Finished compiler/backend/x64 18s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 20s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 18s 1GB
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 6m14s 830MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m56s 963MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 9m40s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 7m31s 606MB
Starting compiler/backend/proofs
Resuming compiler/backend/proofs
Finished compiler/backend/proofs 56s 425MB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 7m40s 4GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 7m56s 2GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 5m35s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 7m36s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m16s 883MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 21s 1GB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 23s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 20s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 20s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 20s 822MB
Starting compiler/proofs
Finished compiler/proofs 1m27s 2GB
Starting candle/set-theory
Finished candle/set-theory 34s 617MB
Starting candle/syntax-lib
Finished candle/syntax-lib 10s 626MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m39s 608MB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m28s 902MB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m41s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 21m39s 7GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 10m00s 8GB
Starting characteristic/examples
Finished characteristic/examples 1m59s 2GB
Starting tutorial/solutions
Finished tutorial/solutions 16m20s 6GB
Starting translator/monadic/examples
Finished translator/monadic/examples 2m09s 3GB
Starting examples
Finished examples 7m21s 5GB
Starting examples/compilation
Finished examples/compilation 2h30m54s 11GB
Starting examples/compilation/proofs
Finished examples/compilation/proofs 2m09s 3GB
Starting compiler/benchmarks
Finished compiler/benchmarks 0s 4MB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 3m47s 1GB
Starting translator/other-examples
Finished translator/other-examples 3m47s 1GB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 27s 269MB
Starting compiler/inference/tests
Resuming compiler/inference/tests