CakeML:804fcaa356c30094a81e8319eefbb4cfbec0dc94 Fix for deletion of terminationTheory #849 (delete_terminationTheory)Merging into:2e67690f5f745a2fa7b80c5dae218e9861ff1ea6 Merge pull request #847 from CakeML/clos-smart-opHOL:6dcb52a09341deda5c5068c06f92c6eaa2af36b6 emacs-mode: display *Holmake* buffer better when it does its thingMachine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64 Claimed job Reusing HOL Starting developers Finished developers 4s 87MB Starting developers/bin Finished developers/bin 6s 1GB Starting semantics/ffi Finished semantics/ffi 8s 205MB Starting semantics Finished semantics 1m26s 1GB Starting semantics/proofs Finished semantics/proofs 3m49s 1GB Starting semantics/alt_semantics Finished semantics/alt_semantics 12s 340MB Starting semantics/alt_semantics/proofs Finished semantics/alt_semantics/proofs 2m36s 800MB Starting basis/pure Finished basis/pure 52s 855MB Starting translator Finished translator 3m01s 1GB Starting compiler/parsing Finished compiler/parsing 1m18s 2GB Starting characteristic Finished characteristic 5m57s 1GB Starting translator/monadic Finished translator/monadic 1m43s 1GB Starting basis Finished basis 48m41s 11GB Starting compiler/inference Finished compiler/inference 1m09s 1GB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 1m10s 1GB Starting compiler/backend/gc Finished compiler/backend/gc 3m34s 1GB Starting compiler/backend Finished compiler/backend 4m49s 2GB Starting compiler/encoders/asm Finished compiler/encoders/asm 24s 751MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 27s 1GB Starting compiler/encoders/arm7 Finished compiler/encoders/arm7 52s 732MB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 14s 601MB Starting compiler/encoders/mips Finished compiler/encoders/mips 18s 1GB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 17s 797MB Starting compiler/encoders/ag32 Finished compiler/encoders/ag32 19s 611MB Starting compiler/backend/x64 Finished compiler/backend/x64 19s 1GB Starting compiler/backend/arm7 Finished compiler/backend/arm7 21s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 19s 1GB Starting compiler/backend/mips Finished compiler/backend/mips 20s 1GB Starting compiler/backend/riscv Finished compiler/backend/riscv 20s 1GB Starting compiler/backend/ag32 Finished compiler/backend/ag32 1m12s 1GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 3m59s 1GB Starting compiler/inference/proofs Finished compiler/inference/proofs 2m33s 1GB Starting compiler/backend/semantics Finished compiler/backend/semantics 33m09s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 3m47s 814MB Starting compiler/backend/proofs Finished compiler/backend/proofs 57m33s 18GB Starting compiler/backend/serialiser Finished compiler/backend/serialiser 1m14s 1GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 10m21s 4GB Starting compiler/encoders/arm7/proofs Finished compiler/encoders/arm7/proofs 14m00s 3GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 7m06s 1GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 10m35s 2GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 9m31s 1GB Starting compiler/encoders/ag32/proofs Finished compiler/encoders/ag32/proofs 2m46s 645MB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 23s 1GB Starting compiler/backend/arm7/proofs Finished compiler/backend/arm7/proofs 24s 1GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 23s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 23s 1GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 24s 1GB Starting compiler/backend/ag32/proofs Finished compiler/backend/ag32/proofs 13m30s 2GB Starting compiler/proofs Finished compiler/proofs 1m48s 4GB Starting candle/set-theory Finished candle/set-theory 29s 947MB Starting candle/syntax-lib Finished candle/syntax-lib 11s 701MB Starting candle/standard/syntax Finished candle/standard/syntax 1m53s 1GB Starting candle/standard/semantics Finished candle/standard/semantics 1m47s 1GB Starting candle/standard/monadic Finished candle/standard/monadic 1m49s 1GB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 6m00s 3GB Starting candle/overloading/syntax Finished candle/overloading/syntax 3m15s 1GB Starting candle/overloading/semantics Finished candle/overloading/semantics 12m13s 2GB Starting pancake Finished pancake 2m00s 2GB Starting pancake/ffi Finished pancake/ffi 0s 4MB Starting pancake/semantics Finished pancake/semantics 2m26s 1GB Starting pancake/proofs Finished pancake/proofs 12m46s 6GB Starting characteristic/examples Finished characteristic/examples 1m25s 3GB Starting tutorial/solutions Finished tutorial/solutions 17m04s 9GB Starting translator/monadic/examples Finished translator/monadic/examples 3m32s 2GB Starting examples Finished examples 9m55s 4GB Starting examples/compilation/x64 Finished examples/compilation/x64 2h34m26s 19GB Starting examples/compilation/x64/proofs Finished examples/compilation/x64/proofs 2m09s 3GB Starting examples/compilation/ag32 Finished examples/compilation/ag32 35m52s 9GB Starting examples/compilation/ag32/proofs Finished examples/compilation/ag32/proofs 50s 3GB Starting examples/cost Finished examples/cost 1h00m32s 7GB Starting examples/lpr_checker Finished examples/lpr_checker 49s 838MB Starting examples/lpr_checker/array Finished examples/lpr_checker/array 30m36s 5GB Starting examples/lpr_checker/array/compilation Finished examples/lpr_checker/array/compilation 1h28m24s 35GB Starting examples/lpr_checker/array/compilation/proofs Finished examples/lpr_checker/array/compilation/proofs 1m54s 4GB Starting examples/opentheory Finished examples/opentheory 10m02s 3GB Starting examples/opentheory Finished examples/opentheory 1s 26MB Starting examples/opentheory/compilation Finished examples/opentheory/compilation 36m20s 28GB Starting examples/opentheory/compilation/proofs Finished examples/opentheory/compilation/proofs 42s 3GB Starting examples/opentheory/compilation/ag32 Finished examples/opentheory/compilation/ag32 40m25s 35GB Starting examples/opentheory/compilation/ag32/proofs Finished examples/opentheory/compilation/ag32/proofs 2m07s 6GB Starting examples/sat_encodings Finished examples/sat_encodings 1m51s 800MB Starting examples/sat_encodings/case_studies Finished examples/sat_encodings/case_studies 1m42s 713MB Starting examples/sat_encodings/translation Finished examples/sat_encodings/translation 5m54s 3GB Starting examples/sat_encodings/translation/compilation Finished examples/sat_encodings/translation/compilation 54m09s 19GB Starting translator/okasaki-examples Finished translator/okasaki-examples 4m50s 1GB Starting translator/other-examples Finished translator/other-examples 46s 1GB Starting compiler/parsing/tests Finished compiler/parsing/tests 30s 531MB Starting compiler/inference/tests Finished compiler/inference/tests 8m18s 5GB Starting compiler/bootstrap/translation