CakeML Regression Test

Job 1153

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:3442e83152ffba29232458cc95a9cfcc86e1dece
  Get Moscow ML quote filter to build given bb2fff9e [Jan 20 06:05:00]
Machine:oven3 4.19.67.1.amd64-smp

Jan 20 23:48:26 Claimed job
Jan 20 23:48:33 Building HOL
Jan 21 00:11:41 Starting developers
Jan 21 00:11:48 Finished developers                                               7s 153MB
Jan 21 00:11:49 Starting developers/bin
Jan 21 00:12:04 Finished developers/bin                                          14s   1GB
Jan 21 00:12:04 Starting semantics/ffi
Jan 21 00:12:27 Finished semantics/ffi                                           23s 241MB
Jan 21 00:12:28 Starting semantics
Jan 21 00:15:28 Finished semantics                                             3m00s 905MB
Jan 21 00:15:29 Starting semantics/proofs
Jan 21 00:22:35 Finished semantics/proofs                                      7m06s 902MB
Jan 21 00:22:35 Starting semantics/alt_semantics
Jan 21 00:22:54 Finished semantics/alt_semantics                                 18s 307MB
Jan 21 00:22:55 Starting semantics/alt_semantics/proofs
Jan 21 00:27:16 Finished semantics/alt_semantics/proofs                        4m21s 897MB
Jan 21 00:27:16 Starting basis/pure
Jan 21 00:33:07 Finished basis/pure                                            5m50s 841MB
Jan 21 00:33:07 Starting translator
Jan 21 00:38:27 Finished translator                                            5m19s   1GB
Jan 21 00:38:28 Starting compiler/parsing
Jan 21 00:40:48 Finished compiler/parsing                                      2m19s   3GB
Jan 21 00:40:48 Starting characteristic
Jan 21 00:53:05 Finished characteristic                                       12m17s   1GB
Jan 21 00:53:06 Starting translator/monadic
Jan 21 00:56:25 Finished translator/monadic                                    3m18s   1GB
Jan 21 00:56:25 Starting basis
Jan 21 02:04:12 Finished basis                                              1h07m47s  17GB
Jan 21 02:04:13 Starting compiler/inference
Jan 21 02:08:55 Finished compiler/inference                                    4m42s   2GB
Jan 21 02:08:56 Starting compiler/backend/reg_alloc
Jan 21 02:10:51 Finished compiler/backend/reg_alloc                            1m54s   1GB
Jan 21 02:10:51 Starting compiler/backend/gc
Jan 21 02:17:19 Finished compiler/backend/gc                                   6m27s   2GB
Jan 21 02:17:19 Starting compiler/backend
Jan 21 02:25:47 Finished compiler/backend                                      8m27s   3GB
Jan 21 02:25:47 Starting compiler/encoders/asm
Jan 21 02:26:34 Finished compiler/encoders/asm                                   46s 672MB
Jan 21 02:26:34 Starting compiler/encoders/x64
Jan 21 02:28:42 Finished compiler/encoders/x64                                 2m07s 879MB
Jan 21 02:28:42 Starting compiler/encoders/arm7
Jan 21 02:32:31 Finished compiler/encoders/arm7                                3m48s   1GB
Jan 21 02:32:32 Starting compiler/encoders/arm8
Jan 21 02:33:43 Finished compiler/encoders/arm8                                1m10s 832MB
Jan 21 02:33:43 Starting compiler/encoders/mips
Jan 21 02:36:21 Finished compiler/encoders/mips                                2m37s   1GB
Jan 21 02:36:21 Starting compiler/encoders/riscv
Jan 21 02:39:29 Finished compiler/encoders/riscv                               3m07s   1GB
Jan 21 02:39:29 Starting compiler/encoders/ag32
Jan 21 02:40:09 Finished compiler/encoders/ag32                                  39s 545MB
Jan 21 02:40:09 Starting compiler/backend/x64
Jan 21 02:40:48 Finished compiler/backend/x64                                    39s   1GB
Jan 21 02:40:48 Starting compiler/backend/arm7
Jan 21 02:41:30 Finished compiler/backend/arm7                                   41s   1GB
Jan 21 02:41:30 Starting compiler/backend/arm8
Jan 21 02:42:12 Finished compiler/backend/arm8                                   41s   1GB
Jan 21 02:42:12 Starting compiler/backend/mips
Jan 21 02:42:48 Finished compiler/backend/mips                                   35s 923MB
Jan 21 02:42:48 Starting compiler/backend/riscv
Jan 21 02:43:31 Finished compiler/backend/riscv                                  43s   1GB
Jan 21 02:43:31 Starting compiler/backend/ag32
Jan 21 02:45:51 Finished compiler/backend/ag32                                 2m19s   1GB
Jan 21 02:45:51 Starting compiler/parsing/proofs
Jan 21 02:58:04 Finished compiler/parsing/proofs                              12m12s   1GB
Jan 21 02:58:04 Starting compiler/inference/proofs
Jan 21 03:04:30 Finished compiler/inference/proofs                             6m25s   1GB
Jan 21 03:04:30 Starting compiler/backend/semantics
Jan 21 04:00:27 Finished compiler/backend/semantics                           55m57s   2GB
Jan 21 04:00:28 Starting compiler/backend/reg_alloc/proofs
Jan 21 04:07:50 Finished compiler/backend/reg_alloc/proofs                     7m22s 961MB
Jan 21 04:07:51 Starting compiler/backend/proofs
Jan 21 06:07:04 Finished compiler/backend/proofs                            1h59m12s  13GB
Jan 21 06:07:04 Starting compiler/encoders/x64/proofs
Jan 21 06:27:15 Finished compiler/encoders/x64/proofs                         20m11s   4GB
Jan 21 06:27:15 Starting compiler/encoders/arm7/proofs
Jan 21 06:54:33 Finished compiler/encoders/arm7/proofs                        27m17s   3GB
Jan 21 06:54:33 Starting compiler/encoders/arm8/proofs
Jan 21 07:08:46 Finished compiler/encoders/arm8/proofs                        14m12s   1GB
Jan 21 07:08:46 Starting compiler/encoders/mips/proofs
Jan 21 07:29:54 Finished compiler/encoders/mips/proofs                        21m07s   3GB
Jan 21 07:29:54 Starting compiler/encoders/riscv/proofs
Jan 21 07:48:41 Finished compiler/encoders/riscv/proofs                       18m46s   1GB
Jan 21 07:48:42 Starting compiler/encoders/ag32/proofs
Jan 21 07:54:01 Finished compiler/encoders/ag32/proofs                         5m19s 937MB
Jan 21 07:54:01 Starting compiler/backend/x64/proofs
Jan 21 07:54:43 Finished compiler/backend/x64/proofs                             42s   1GB
Jan 21 07:54:43 Starting compiler/backend/arm7/proofs
Jan 21 07:55:27 Finished compiler/backend/arm7/proofs                            43s 887MB
Jan 21 07:55:27 Starting compiler/backend/arm8/proofs
Jan 21 07:56:08 Finished compiler/backend/arm8/proofs                            40s   1GB
Jan 21 07:56:08 Starting compiler/backend/mips/proofs
Jan 21 07:56:50 Finished compiler/backend/mips/proofs                            41s   1GB
Jan 21 07:56:50 Starting compiler/backend/riscv/proofs
Jan 21 07:57:33 Finished compiler/backend/riscv/proofs                           42s   1GB
Jan 21 07:57:33 Starting compiler/backend/ag32/proofs
Jan 21 08:17:16 Finished compiler/backend/ag32/proofs                         19m42s   1GB
Jan 21 08:17:16 Starting compiler/proofs
Jan 21 08:20:42 Finished compiler/proofs                                       3m25s   3GB
Jan 21 08:20:42 Starting candle/set-theory
Jan 21 08:21:38 Finished candle/set-theory                                       55s 782MB
Jan 21 08:21:38 Starting candle/syntax-lib
Jan 21 08:22:01 Finished candle/syntax-lib                                       22s 706MB
Jan 21 08:22:01 Starting candle/standard/syntax
Jan 21 08:25:41 Finished candle/standard/syntax                                3m40s 992MB
Jan 21 08:25:41 Starting candle/standard/semantics
Jan 21 08:29:19 Finished candle/standard/semantics                             3m37s   1GB
Jan 21 08:29:19 Starting candle/standard/monadic
Jan 21 08:32:47 Finished candle/standard/monadic                               3m27s   1GB
Jan 21 08:32:47 Starting candle/standard/ml_kernel
Jan 21 08:43:42 Finished candle/standard/ml_kernel                            10m54s   3GB
Jan 21 08:43:42 Starting candle/standard/opentheory
Jan 21 09:03:48 Finished candle/standard/opentheory                           20m05s   4GB
Jan 21 09:03:48 Starting candle/standard/opentheory/compilation
Jan 21 10:11:05 Finished candle/standard/opentheory/compilation             1h07m16s  13GB
Jan 21 10:11:05 Starting candle/standard/opentheory/compilation/proofs
Jan 21 10:12:31 Finished candle/standard/opentheory/compilation/proofs         1m25s   4GB
Jan 21 10:12:31 Starting characteristic/examples
Jan 21 10:15:35 Finished characteristic/examples                               3m04s   2GB
Jan 21 10:15:36 Starting tutorial/solutions
Jan 21 10:46:56 Finished tutorial/solutions                                   31m20s   6GB
Jan 21 10:46:57 Starting translator/monadic/examples
Jan 21 10:52:10 Finished translator/monadic/examples                           5m12s   2GB
Jan 21 10:52:10 Starting examples
Jan 21 10:54:29 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:   26s  user:   24s     OK
Starting work on diffTheory
regexp_parserTheory                                                                                                                                          real:   26s  user:   25s     OK
Starting work on divTheory
diffTheory                                                                                                                                                   real:   87s  user:   84s     OK
Starting work on diffProgTheory
divTheory                                                                                                                                                    real:  109s  user:  105sFAIL<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-1153/examples/divScript.sml : Fail "Static Errors"
 error in load /root/regression/cakeml-1153/examples/divScript : Fail "Static Errors"
 /root/regression/cakeml-1153/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