Job 1151

CakeML:9100408c52f4fddf83cb6ecdd3babc7e76aee79e
  Restore EL_CONS_IF in misc [Jan 16 15:06:08]
#719 (master-suc)
Merging into:3a8cdd942237e58c14d85d24f8d9997cac1784b4
  Merge pull request #718 from CakeML/lpr [Jan 16 12:30:11]
HOL:76a40cfe6a3828bd446bfff504267c4197ffaaf3
  documentation for nameCases stuff [Jan 18 02:32:00]
Machine:oven3 4.19.67.1.amd64-smp

Jan 19 21:39:31 Claimed job
Jan 19 21:39:43 Building HOL
Jan 19 22:02:52 Starting developers
Jan 19 22:02:59 Finished developers                                               6s 138MB
Jan 19 22:02:59 Starting developers/bin
Jan 19 22:03:14 Finished developers/bin                                          14s   1GB
Jan 19 22:03:14 Starting semantics/ffi
Jan 19 22:03:37 Finished semantics/ffi                                           22s 248MB
Jan 19 22:03:38 Starting semantics
Jan 19 22:06:40 Finished semantics                                             3m01s   1GB
Jan 19 22:06:40 Starting semantics/proofs
Jan 19 22:13:54 Finished semantics/proofs                                      7m14s 937MB
Jan 19 22:13:54 Starting semantics/alt_semantics
Jan 19 22:14:13 Finished semantics/alt_semantics                                 18s 299MB
Jan 19 22:14:13 Starting semantics/alt_semantics/proofs
Jan 19 22:18:43 Finished semantics/alt_semantics/proofs                        4m29s 969MB
Jan 19 22:18:43 Starting basis/pure
Jan 19 22:24:36 Finished basis/pure                                            5m52s 841MB
Jan 19 22:24:36 Starting translator
Jan 19 22:29:51 Finished translator                                            5m15s   1GB
Jan 19 22:29:52 Starting compiler/parsing
Jan 19 22:32:10 Finished compiler/parsing                                      2m18s   3GB
Jan 19 22:32:10 Starting characteristic
Jan 19 22:44:28 Finished characteristic                                       12m17s   2GB
Jan 19 22:44:29 Starting translator/monadic
Jan 19 22:47:52 Finished translator/monadic                                    3m22s   1GB
Jan 19 22:47:52 Starting basis
Jan 19 23:56:32 Finished basis                                              1h08m39s  11GB
Jan 19 23:56:32 Starting compiler/inference
Jan 20 00:01:14 Finished compiler/inference                                    4m41s   1GB
Jan 20 00:01:14 Starting compiler/backend/reg_alloc
Jan 20 00:03:10 Finished compiler/backend/reg_alloc                            1m55s   1GB
Jan 20 00:03:10 Starting compiler/backend/gc
Jan 20 00:09:32 Finished compiler/backend/gc                                   6m22s   2GB
Jan 20 00:09:33 Starting compiler/backend
Jan 20 00:17:57 Finished compiler/backend                                      8m24s   2GB
Jan 20 00:17:57 Starting compiler/encoders/asm
Jan 20 00:18:44 Finished compiler/encoders/asm                                   46s 789MB
Jan 20 00:18:44 Starting compiler/encoders/x64
Jan 20 00:20:50 Finished compiler/encoders/x64                                 2m05s 630MB
Jan 20 00:20:50 Starting compiler/encoders/arm7
Jan 20 00:24:38 Finished compiler/encoders/arm7                                3m48s   1GB
Jan 20 00:24:39 Starting compiler/encoders/arm8
Jan 20 00:25:50 Finished compiler/encoders/arm8                                1m11s 574MB
Jan 20 00:25:50 Starting compiler/encoders/mips
Jan 20 00:28:20 Finished compiler/encoders/mips                                2m29s   1GB
Jan 20 00:28:20 Starting compiler/encoders/riscv
Jan 20 00:31:19 Finished compiler/encoders/riscv                               2m58s   1GB
Jan 20 00:31:19 Starting compiler/encoders/ag32
Jan 20 00:31:56 Finished compiler/encoders/ag32                                  37s 792MB
Jan 20 00:31:57 Starting compiler/backend/x64
Jan 20 00:32:33 Finished compiler/backend/x64                                    36s 907MB
Jan 20 00:32:34 Starting compiler/backend/arm7
Jan 20 00:33:16 Finished compiler/backend/arm7                                   42s   1GB
Jan 20 00:33:16 Starting compiler/backend/arm8
Jan 20 00:33:54 Finished compiler/backend/arm8                                   37s 947MB
Jan 20 00:33:54 Starting compiler/backend/mips
Jan 20 00:34:34 Finished compiler/backend/mips                                   40s   1GB
Jan 20 00:34:35 Starting compiler/backend/riscv
Jan 20 00:35:12 Finished compiler/backend/riscv                                  37s   1GB
Jan 20 00:35:13 Starting compiler/backend/ag32
Jan 20 00:37:32 Finished compiler/backend/ag32                                 2m18s   1GB
Jan 20 00:37:32 Starting compiler/parsing/proofs
Jan 20 00:49:51 Finished compiler/parsing/proofs                              12m18s   1GB
Jan 20 00:49:51 Starting compiler/inference/proofs
Jan 20 00:56:18 Finished compiler/inference/proofs                             6m26s   1GB
Jan 20 00:56:18 Starting compiler/backend/semantics
Jan 20 01:53:20 Finished compiler/backend/semantics                           57m01s   1GB
Jan 20 01:53:20 Starting compiler/backend/reg_alloc/proofs
Jan 20 02:00:38 Finished compiler/backend/reg_alloc/proofs                     7m17s 918MB
Jan 20 02:00:38 Starting compiler/backend/proofs
Jan 20 04:00:33 Finished compiler/backend/proofs                            1h59m54s  16GB
Jan 20 04:00:33 Starting compiler/encoders/x64/proofs
Jan 20 04:21:07 Finished compiler/encoders/x64/proofs                         20m34s   7GB
Jan 20 04:21:08 Starting compiler/encoders/arm7/proofs
Jan 20 04:49:03 Finished compiler/encoders/arm7/proofs                        27m54s   3GB
Jan 20 04:49:03 Starting compiler/encoders/arm8/proofs
Jan 20 05:02:59 Finished compiler/encoders/arm8/proofs                        13m55s   1GB
Jan 20 05:02:59 Starting compiler/encoders/mips/proofs
Jan 20 05:24:06 Finished compiler/encoders/mips/proofs                        21m06s   3GB
Jan 20 05:24:06 Starting compiler/encoders/riscv/proofs
Jan 20 05:43:21 Finished compiler/encoders/riscv/proofs                       19m14s   1GB
Jan 20 05:43:21 Starting compiler/encoders/ag32/proofs
Jan 20 05:48:51 Finished compiler/encoders/ag32/proofs                         5m29s 808MB
Jan 20 05:48:51 Starting compiler/backend/x64/proofs
Jan 20 05:49:33 Finished compiler/backend/x64/proofs                             41s   1GB
Jan 20 05:49:33 Starting compiler/backend/arm7/proofs
Jan 20 05:50:17 Finished compiler/backend/arm7/proofs                            44s   1GB
Jan 20 05:50:18 Starting compiler/backend/arm8/proofs
Jan 20 05:50:59 Finished compiler/backend/arm8/proofs                            41s   1GB
Jan 20 05:50:59 Starting compiler/backend/mips/proofs
Jan 20 05:51:42 Finished compiler/backend/mips/proofs                            42s   1GB
Jan 20 05:51:42 Starting compiler/backend/riscv/proofs
Jan 20 05:52:23 Finished compiler/backend/riscv/proofs                           40s   1GB
Jan 20 05:52:23 Starting compiler/backend/ag32/proofs
Jan 20 06:11:25 Finished compiler/backend/ag32/proofs                         19m01s   2GB
Jan 20 06:11:25 Starting compiler/proofs
Jan 20 06:15:02 Finished compiler/proofs                                       3m37s   3GB
Jan 20 06:15:03 Starting candle/set-theory
Jan 20 06:15:57 Finished candle/set-theory                                       54s 816MB
Jan 20 06:15:58 Starting candle/syntax-lib
Jan 20 06:16:21 Finished candle/syntax-lib                                       22s 667MB
Jan 20 06:16:21 Starting candle/standard/syntax
Jan 20 06:20:04 Finished candle/standard/syntax                                3m42s   1GB
Jan 20 06:20:04 Starting candle/standard/semantics
Jan 20 06:23:42 Finished candle/standard/semantics                             3m37s   1GB
Jan 20 06:23:42 Starting candle/standard/monadic
Jan 20 06:27:10 Finished candle/standard/monadic                               3m27s   1GB
Jan 20 06:27:10 Starting candle/standard/ml_kernel
Jan 20 06:37:58 Finished candle/standard/ml_kernel                            10m48s   3GB
Jan 20 06:37:59 Starting candle/standard/opentheory
Jan 20 06:57:48 Finished candle/standard/opentheory                           19m48s   4GB
Jan 20 06:57:48 Starting candle/standard/opentheory/compilation
Jan 20 08:05:13 Finished candle/standard/opentheory/compilation             1h07m24s  19GB
Jan 20 08:05:13 Starting candle/standard/opentheory/compilation/proofs
Jan 20 08:06:32 Finished candle/standard/opentheory/compilation/proofs         1m18s   3GB
Jan 20 08:06:32 Starting characteristic/examples
Jan 20 08:09:40 Finished characteristic/examples                               3m07s   2GB
Jan 20 08:09:40 Starting tutorial/solutions
Jan 20 08:40:48 Finished tutorial/solutions                                   31m08s   7GB
Jan 20 08:40:49 Starting translator/monadic/examples
Jan 20 08:45:54 Finished translator/monadic/examples                           5m05s   2GB
Jan 20 08:45:55 Starting examples
Jan 20 08:48:12 FAILED: examples
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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
README.md                                                                                                                                                    real:    0s  user:    0s     OK
Starting work on lcsTheory
lcsTheory                                                                                                                                                    real:   27s  user:   25s     OK
Starting work on diffTheory
regexp_parserTheory                                                                                                                                          real:   29s  user:   27s     OK
Starting work on divTheory
diffTheory                                                                                                                                                   real:   86s  user:   83s     OK
Starting work on diffProgTheory
divTheory                                                                                                                                                    real:  106s  user:  102sFAIL<1>
 Saved theorem _____ "nsLookup_div_env_1_pfun_eqs"
 Adding nsLookup representation thms for [div_env_1]
 Using translator specification minus_v_thm from theory mlbasicsProg
 Saved theorem _____ "oddLoop_spec"
 Saved theorem _____ "nsLookup_div_env_2_pfun_eqs"
 error in quse /root/regression/cakeml-1151/examples/divScript.sml : Fail "Static Errors"
 error in load /root/regression/cakeml-1151/examples/divScript : Fail "Static Errors"
 /root/regression/cakeml-1151/examples/divScript.sml:156: error: Value or constructor (ADD_1_SUC) has not been declared
 Found near [ADD_CLAUSES, ADD_1_SUC]
 Uncaught exception: Fail "Static Errors"
quicksortProgTheory                                                                                                                                                                  M-KILLED
catProgTheory                                                                                                                                                                        M-KILLED
diffProgTheory                                                                                                                                                                       M-KILLED