Job 1154

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:b219f4bb4132ea21f42769a8edf7e3abde4cc48d
  emacs-mode: some indentation tweaks [Jan 22 06:44:58]
Machine:oven3 4.19.67.1.amd64-smp

Jan 23 09:15:02 Claimed job
Jan 23 09:15:10 Building HOL
Jan 23 09:38:09 Starting developers
Jan 23 09:38:16 Finished developers                                               6s  74MB
Jan 23 09:38:16 Starting developers/bin
Jan 23 09:38:31 Finished developers/bin                                          14s   1GB
Jan 23 09:38:31 Starting semantics/ffi
Jan 23 09:38:54 Finished semantics/ffi                                           23s 239MB
Jan 23 09:38:55 Starting semantics
Jan 23 09:41:55 Finished semantics                                             3m00s   1GB
Jan 23 09:41:55 Starting semantics/proofs
Jan 23 09:48:56 Finished semantics/proofs                                      7m00s   1GB
Jan 23 09:48:56 Starting semantics/alt_semantics
Jan 23 09:49:15 Finished semantics/alt_semantics                                 19s 307MB
Jan 23 09:49:16 Starting semantics/alt_semantics/proofs
Jan 23 09:53:38 Finished semantics/alt_semantics/proofs                        4m22s 873MB
Jan 23 09:53:38 Starting basis/pure
Jan 23 09:59:31 Finished basis/pure                                            5m52s 908MB
Jan 23 09:59:31 Starting translator
Jan 23 10:04:46 Finished translator                                            5m15s   1GB
Jan 23 10:04:46 Starting compiler/parsing
Jan 23 10:07:06 Finished compiler/parsing                                      2m19s   2GB
Jan 23 10:07:06 Starting characteristic
Jan 23 10:19:17 Finished characteristic                                       12m10s   1GB
Jan 23 10:19:17 Starting translator/monadic
Jan 23 10:22:30 Finished translator/monadic                                    3m12s   1GB
Jan 23 10:22:30 Starting basis
Jan 23 11:31:27 Finished basis                                              1h08m54s  23GB
Jan 23 11:31:27 Starting compiler/inference
Jan 23 11:36:09 Finished compiler/inference                                    4m41s   2GB
Jan 23 11:36:09 Starting compiler/backend/reg_alloc
Jan 23 11:38:02 Finished compiler/backend/reg_alloc                            1m53s   1GB
Jan 23 11:38:02 Starting compiler/backend/gc
Jan 23 11:44:14 Finished compiler/backend/gc                                   6m11s   2GB
Jan 23 11:44:14 Starting compiler/backend
Jan 23 11:52:41 Finished compiler/backend                                      8m26s   3GB
Jan 23 11:52:41 Starting compiler/encoders/asm
Jan 23 11:53:30 Finished compiler/encoders/asm                                   48s 692MB
Jan 23 11:53:30 Starting compiler/encoders/x64
Jan 23 11:55:32 Finished compiler/encoders/x64                                 2m02s 922MB
Jan 23 11:55:33 Starting compiler/encoders/arm7
Jan 23 11:59:24 Finished compiler/encoders/arm7                                3m51s   1GB
Jan 23 11:59:24 Starting compiler/encoders/arm8
Jan 23 12:00:37 Finished compiler/encoders/arm8                                1m12s 800MB
Jan 23 12:00:38 Starting compiler/encoders/mips
Jan 23 12:03:13 Finished compiler/encoders/mips                                2m34s   1GB
Jan 23 12:03:13 Starting compiler/encoders/riscv
Jan 23 12:06:12 Finished compiler/encoders/riscv                               2m58s   1GB
Jan 23 12:06:12 Starting compiler/encoders/ag32
Jan 23 12:06:48 Finished compiler/encoders/ag32                                  35s 803MB
Jan 23 12:06:48 Starting compiler/backend/x64
Jan 23 12:07:26 Finished compiler/backend/x64                                    37s   1GB
Jan 23 12:07:26 Starting compiler/backend/arm7
Jan 23 12:08:09 Finished compiler/backend/arm7                                   42s   1GB
Jan 23 12:08:09 Starting compiler/backend/arm8
Jan 23 12:08:45 Finished compiler/backend/arm8                                   35s 997MB
Jan 23 12:08:45 Starting compiler/backend/mips
Jan 23 12:09:22 Finished compiler/backend/mips                                   36s 942MB
Jan 23 12:09:22 Starting compiler/backend/riscv
Jan 23 12:10:01 Finished compiler/backend/riscv                                  39s   1GB
Jan 23 12:10:01 Starting compiler/backend/ag32
Jan 23 12:12:20 Finished compiler/backend/ag32                                 2m18s   1GB
Jan 23 12:12:20 Starting compiler/parsing/proofs
Jan 23 12:24:34 Finished compiler/parsing/proofs                              12m13s   1GB
Jan 23 12:24:35 Starting compiler/inference/proofs
Jan 23 12:30:56 Finished compiler/inference/proofs                             6m21s   1GB
Jan 23 12:30:57 Starting compiler/backend/semantics
Jan 23 13:27:45 Finished compiler/backend/semantics                           56m46s   2GB
Jan 23 13:27:45 Starting compiler/backend/reg_alloc/proofs
Jan 23 13:35:15 Finished compiler/backend/reg_alloc/proofs                     7m29s 888MB
Jan 23 13:35:15 Starting compiler/backend/proofs
Jan 23 15:34:57 Finished compiler/backend/proofs                            1h59m41s  16GB
Jan 23 15:34:57 Starting compiler/encoders/x64/proofs
Jan 23 15:55:08 Finished compiler/encoders/x64/proofs                         20m10s   5GB
Jan 23 15:55:08 Starting compiler/encoders/arm7/proofs
Jan 23 16:23:06 Finished compiler/encoders/arm7/proofs                        27m57s   3GB
Jan 23 16:23:06 Starting compiler/encoders/arm8/proofs
Jan 23 16:37:18 Finished compiler/encoders/arm8/proofs                        14m11s   1GB
Jan 23 16:37:19 Starting compiler/encoders/mips/proofs
Jan 23 16:58:47 Finished compiler/encoders/mips/proofs                        21m28s   2GB
Jan 23 16:58:47 Starting compiler/encoders/riscv/proofs
Jan 23 17:17:41 Finished compiler/encoders/riscv/proofs                       18m53s   1GB
Jan 23 17:17:41 Starting compiler/encoders/ag32/proofs
Jan 23 17:23:07 Finished compiler/encoders/ag32/proofs                         5m26s 813MB
Jan 23 17:23:08 Starting compiler/backend/x64/proofs
Jan 23 17:23:48 Finished compiler/backend/x64/proofs                             40s   1GB
Jan 23 17:23:48 Starting compiler/backend/arm7/proofs
Jan 23 17:24:32 Finished compiler/backend/arm7/proofs                            43s 864MB
Jan 23 17:24:32 Starting compiler/backend/arm8/proofs
Jan 23 17:25:12 Finished compiler/backend/arm8/proofs                            39s   1GB
Jan 23 17:25:12 Starting compiler/backend/mips/proofs
Jan 23 17:25:55 Finished compiler/backend/mips/proofs                            42s   1GB
Jan 23 17:25:55 Starting compiler/backend/riscv/proofs
Jan 23 17:26:37 Finished compiler/backend/riscv/proofs                           41s   1GB
Jan 23 17:26:37 Starting compiler/backend/ag32/proofs
Jan 23 17:45:49 Finished compiler/backend/ag32/proofs                         19m11s   2GB
Jan 23 17:45:50 Starting compiler/proofs
Jan 23 17:49:18 Finished compiler/proofs                                       3m28s   3GB
Jan 23 17:49:18 Starting candle/set-theory
Jan 23 17:50:15 Finished candle/set-theory                                       56s 727MB
Jan 23 17:50:15 Starting candle/syntax-lib
Jan 23 17:50:38 Finished candle/syntax-lib                                       22s 618MB
Jan 23 17:50:38 Starting candle/standard/syntax
Jan 23 17:54:21 Finished candle/standard/syntax                                3m42s   1GB
Jan 23 17:54:21 Starting candle/standard/semantics
Jan 23 17:57:58 Finished candle/standard/semantics                             3m36s   1GB
Jan 23 17:57:58 Starting candle/standard/monadic
Jan 23 18:01:18 Finished candle/standard/monadic                               3m20s   1GB
Jan 23 18:01:19 Starting candle/standard/ml_kernel
Jan 23 18:12:07 Finished candle/standard/ml_kernel                            10m48s   4GB
Jan 23 18:12:07 Starting candle/standard/opentheory
Jan 23 18:31:48 Finished candle/standard/opentheory                           19m40s   4GB
Jan 23 18:31:48 Starting candle/standard/opentheory/compilation
Jan 23 19:39:39 Finished candle/standard/opentheory/compilation             1h07m50s  17GB
Jan 23 19:39:39 Starting candle/standard/opentheory/compilation/proofs
Jan 23 19:41:03 Finished candle/standard/opentheory/compilation/proofs         1m23s   4GB
Jan 23 19:41:03 Starting characteristic/examples
Jan 23 19:44:23 Finished characteristic/examples                               3m20s   2GB
Jan 23 19:44:24 Starting tutorial/solutions
Jan 23 20:15:43 Finished tutorial/solutions                                   31m18s   7GB
Jan 23 20:15:43 Starting translator/monadic/examples
Jan 23 20:20:44 Finished translator/monadic/examples                           5m01s   2GB
Jan 23 20:20:44 Starting examples
Jan 23 20:22:57 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
regexp_parserTheory                                                                                                                                          real:   25s  user:   24s     OK
Starting work on divTheory
lcsTheory                                                                                                                                                    real:   26s  user:   24s     OK
Starting work on diffTheory
diffTheory                                                                                                                                                   real:   84s  user:   81s     OK
Starting work on diffProgTheory
divTheory                                                                                                                                                    real:  104s  user:   99sFAIL<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-1154/examples/divScript.sml : Fail "Static Errors"
 error in load /root/regression/cakeml-1154/examples/divScript : Fail "Static Errors"
 /root/regression/cakeml-1154/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