OverviewCakeML:c28756be21bfff1937e0e3428b040dbd0471ad99
Fix part of backendProof
HOL:1354090035c466ccae632435bb016c0bebf281d7
Move large_numberTheory to examples/probability
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 104MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 233MB
Starting semantics
Finished semantics 1m28s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m49s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 9s 388MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m22s 712MB
Starting basis/pure
Finished basis/pure 52s 808MB
Starting translator
Finished translator 3m41s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m17s 1GB
Starting characteristic
Finished characteristic 5m51s 2GB
Starting translator/monadic
Finished translator/monadic 1m40s 1GB
Starting basis
Finished basis 47m18s 12GB
Starting compiler/inference
Finished compiler/inference 1m09s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m09s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m38s 2GB
Starting compiler/backend
Finished compiler/backend 5m10s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 23s 665MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 26s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 53s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 13s 938MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 18s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 15s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 18s 896MB
Starting compiler/backend/x64
Finished compiler/backend/x64 20s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 20s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 18s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 19s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 20s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m14s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 6m05s 1GB
Starting compiler/inference/proofs
FAILED: compiler/inference/proofs
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/inference
Starting work on README.md
Starting work on inferPropsTheory
README.md real: 0s user: 0s OK
inferPropsTheory real: 10s user: 9sFAIL<1>
Saved theorem _____ "generalise_list_length"
Saved theorem _____ "generalise_subst"
Saved theorem _____ "generalise_subst_empty"
Saved theorem _____ "infer_st_rewrs"
error in quse /home/cake/oven/regression/cakeml-1529/compiler/inference/proofs/inferPropsScript.sml : Fail "Static Errors"
error in load /home/cake/oven/regression/cakeml-1529/compiler/inference/proofs/inferPropsScript : Fail "Static Errors"
Saved theorem _____ "add_constraint_success"
/home/cake/oven/regression/cakeml-1529/compiler/inference/proofs/inferPropsScript.sml:441: error: Value or constructor (infer_st_subst) has not been declared
Found near [infer_st_subst]
Uncaught exception: Fail "Static Errors"