Job 1528

CakeML:e80ca9e987f82878ddf439c72890f5a6a31d56ba
  Fix more proofs [May 18 08:01:56]
HOL:1354090035c466ccae632435bb016c0bebf281d7
  Move large_numberTheory to examples/probability [May 13 23:47:06]
Machine:oven3 4.19.67.1.amd64-smp

May 18 08:02:57 Claimed job
May 18 08:03:03 Reusing HOL
May 18 08:04:01 Starting developers
May 18 08:04:09 Finished developers                                               8s 109MB
May 18 08:04:10 Starting developers/bin
May 18 08:04:22 Finished developers/bin                                          12s   1GB
May 18 08:04:22 Starting semantics/ffi
May 18 08:04:48 Finished semantics/ffi                                           25s 263MB
May 18 08:04:48 Starting semantics
May 18 08:07:40 Finished semantics                                             2m51s   1GB
May 18 08:07:41 Starting semantics/proofs
May 18 08:15:26 Finished semantics/proofs                                      7m44s   1GB
May 18 08:15:26 Starting semantics/alt_semantics
May 18 08:15:48 Finished semantics/alt_semantics                                 21s 358MB
May 18 08:15:48 Starting semantics/alt_semantics/proofs
May 18 08:20:36 Finished semantics/alt_semantics/proofs                        4m48s   1GB
May 18 08:20:36 Starting basis/pure
May 18 08:22:21 Finished basis/pure                                            1m44s 766MB
May 18 08:22:22 Starting translator
May 18 08:29:14 Finished translator                                            6m52s   1GB
May 18 08:29:15 Starting compiler/parsing
May 18 08:31:52 Finished compiler/parsing                                      2m37s   2GB
May 18 08:31:53 Starting characteristic
May 18 08:43:48 Finished characteristic                                       11m55s   1GB
May 18 08:43:49 Starting translator/monadic
May 18 08:47:18 Finished translator/monadic                                    3m28s   1GB
May 18 08:47:18 Starting basis
May 18 10:24:02 Finished basis                                              1h36m42s  16GB
May 18 10:24:03 Starting compiler/inference
May 18 10:26:27 Finished compiler/inference                                    2m23s   1GB
May 18 10:26:27 Starting compiler/backend/reg_alloc
May 18 10:28:37 Finished compiler/backend/reg_alloc                            2m09s   1GB
May 18 10:28:37 Starting compiler/backend/gc
May 18 10:35:19 Finished compiler/backend/gc                                   6m41s   2GB
May 18 10:35:19 Starting compiler/backend
May 18 10:44:57 Finished compiler/backend                                      9m37s   3GB
May 18 10:44:57 Starting compiler/encoders/asm
May 18 10:45:45 Finished compiler/encoders/asm                                   47s 919MB
May 18 10:45:46 Starting compiler/encoders/x64
May 18 10:48:04 Finished compiler/encoders/x64                                 2m18s 830MB
May 18 10:48:05 Starting compiler/encoders/arm7
May 18 10:52:37 Finished compiler/encoders/arm7                                4m32s   1GB
May 18 10:52:37 Starting compiler/encoders/arm8
May 18 10:54:01 Finished compiler/encoders/arm8                                1m23s 683MB
May 18 10:54:01 Starting compiler/encoders/mips
May 18 10:57:15 Finished compiler/encoders/mips                                3m13s   1GB
May 18 10:57:15 Starting compiler/encoders/riscv
May 18 11:01:11 Finished compiler/encoders/riscv                               3m55s   1GB
May 18 11:01:12 Starting compiler/encoders/ag32
May 18 11:01:50 Finished compiler/encoders/ag32                                  38s 809MB
May 18 11:01:50 Starting compiler/backend/x64
May 18 11:02:31 Finished compiler/backend/x64                                    40s   1GB
May 18 11:02:31 Starting compiler/backend/arm7
May 18 11:03:12 Finished compiler/backend/arm7                                   41s   1GB
May 18 11:03:13 Starting compiler/backend/arm8
May 18 11:03:57 Finished compiler/backend/arm8                                   44s   1GB
May 18 11:03:57 Starting compiler/backend/mips
May 18 11:04:40 Finished compiler/backend/mips                                   42s   1GB
May 18 11:04:40 Starting compiler/backend/riscv
May 18 11:05:22 Finished compiler/backend/riscv                                  41s   1GB
May 18 11:05:22 Starting compiler/backend/ag32
May 18 11:07:49 Finished compiler/backend/ag32                                 2m26s   1GB
May 18 11:07:49 Starting compiler/parsing/proofs
May 18 11:20:40 Finished compiler/parsing/proofs                              12m51s   1GB
May 18 11:20:41 Starting compiler/inference/proofs
May 18 11:21:06 FAILED: compiler/inference/proofs
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Starting work on README.md
Starting work on inferPropsTheory
README.md                                                                                                                                                    real:    0s  user:    0s     OK
inferPropsTheory                                                                                                                                             real:   23s  user:   21sFAIL<1>
 Saved theorem _____ "generalise_list_length"
 Saved theorem _____ "generalise_subst"
 Saved theorem _____ "generalise_subst_empty"
 Saved theorem _____ "infer_st_rewrs"
 Saved theorem _____ "add_constraint_success"
 /root/regression/cakeml-1528/compiler/inference/proofs/inferPropsScript.sml:441: error: Value or constructor (infer_st_subst) has not been declared
 Found near [infer_st_subst]
 error in quse /root/regression/cakeml-1528/compiler/inference/proofs/inferPropsScript.sml : Fail "Static Errors"
 error in load /root/regression/cakeml-1528/compiler/inference/proofs/inferPropsScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"