CakeML Regression Test

Job 1921

CakeML:5591164cf6fe6c771ccd622e191f6ff9e4a628f5
  use repeated rewriting in Closure_tac [Jun 11 17:29:23]
#890 (pseudo_bool)
Merging into:f7195c3d29d6bd5f389a7ff307f998a45d56552f
  Merge pull request #888 from CakeML/deflate [Jun 09 07:20:45]
HOL:48bc6e3fcf4f5c1a81a122354d8838d83bbce3ef
  Re-organise Holmake code to isolate some "file-system" code [Jun 07 01:51:29]
Machine:oven3

Jun 13 06:26:14 Claimed job
Jun 13 06:26:17 Reusing HOL
Jun 13 06:27:09 Starting developers
Jun 13 06:27:17 Finished developers                                               8s 134MB
Jun 13 06:27:18 Starting developers/bin
Jun 13 06:27:31 Finished developers/bin                                          13s   1GB
Jun 13 06:27:31 Starting semantics/ffi
Jun 13 06:27:55 Finished semantics/ffi                                           23s 224MB
Jun 13 06:27:55 Starting semantics
Jun 13 06:32:51 Finished semantics                                             4m55s   1GB
Jun 13 06:32:51 Starting semantics/proofs
Jun 13 06:48:30 Finished semantics/proofs                                     15m38s   1GB
Jun 13 06:48:30 Starting semantics/alt_semantics
Jun 13 06:49:32 Finished semantics/alt_semantics                               1m01s 530MB
Jun 13 06:49:32 Starting semantics/alt_semantics/proofs
Jun 13 07:14:54 Finished semantics/alt_semantics/proofs                       25m21s   1GB
Jun 13 07:14:54 Starting basis/pure
Jun 13 07:17:14 Finished basis/pure                                            2m19s 928MB
Jun 13 07:17:14 Starting translator
Jun 13 07:25:07 Finished translator                                            7m52s   1GB
Jun 13 07:25:08 Starting compiler/parsing
Jun 13 07:27:57 Finished compiler/parsing                                      2m49s   4GB
Jun 13 07:27:57 Starting characteristic
Jun 13 07:42:47 Finished characteristic                                       14m49s   2GB
Jun 13 07:42:47 Starting translator/monadic
Jun 13 07:46:55 Finished translator/monadic                                    4m07s   1GB
Jun 13 07:46:55 Starting basis
Jun 13 09:36:26 Finished basis                                              1h49m29s  24GB
Jun 13 09:36:27 Starting compiler/inference
Jun 13 09:39:41 Finished compiler/inference                                    3m13s   1GB
Jun 13 09:39:41 Starting compiler/backend/reg_alloc
Jun 13 09:42:55 Finished compiler/backend/reg_alloc                            3m13s   1GB
Jun 13 09:42:55 Starting compiler/backend/gc
Jun 13 09:51:39 Finished compiler/backend/gc                                   8m43s   2GB
Jun 13 09:51:39 Starting compiler/backend
Jun 13 10:03:19 Finished compiler/backend                                     11m40s   2GB
Jun 13 10:03:20 Starting compiler/encoders/asm
Jun 13 10:04:25 Finished compiler/encoders/asm                                 1m04s 762MB
Jun 13 10:04:25 Starting compiler/encoders/x64
Jun 13 10:05:29 Finished compiler/encoders/x64                                 1m03s   1GB
Jun 13 10:05:29 Starting compiler/encoders/arm7
Jun 13 10:07:36 Finished compiler/encoders/arm7                                2m06s 820MB
Jun 13 10:07:36 Starting compiler/encoders/arm8
Jun 13 10:08:14 Finished compiler/encoders/arm8                                  37s 755MB
Jun 13 10:08:15 Starting compiler/encoders/arm8_asl
Jun 13 10:15:20 Finished compiler/encoders/arm8_asl                            7m05s   1GB
Jun 13 10:15:21 Starting compiler/encoders/mips
Jun 13 10:16:04 Finished compiler/encoders/mips                                  43s   1GB
Jun 13 10:16:04 Starting compiler/encoders/riscv
Jun 13 10:16:42 Finished compiler/encoders/riscv                                 37s 836MB
Jun 13 10:16:42 Starting compiler/encoders/ag32
Jun 13 10:17:32 Finished compiler/encoders/ag32                                  49s 906MB
Jun 13 10:17:32 Starting compiler/backend/x64
Jun 13 10:18:21 Finished compiler/backend/x64                                    48s   1GB
Jun 13 10:18:21 Starting compiler/backend/arm7
Jun 13 10:19:13 Finished compiler/backend/arm7                                   51s   1GB
Jun 13 10:19:13 Starting compiler/backend/arm8
Jun 13 10:20:04 Finished compiler/backend/arm8                                   50s   1GB
Jun 13 10:20:04 Starting compiler/backend/mips
Jun 13 10:20:55 Finished compiler/backend/mips                                   50s   1GB
Jun 13 10:20:55 Starting compiler/backend/riscv
Jun 13 10:21:48 Finished compiler/backend/riscv                                  51s   1GB
Jun 13 10:21:48 Starting compiler/backend/ag32
Jun 13 10:24:47 Finished compiler/backend/ag32                                 2m59s   1GB
Jun 13 10:24:47 Starting compiler/parsing/proofs
Jun 13 10:33:29 Finished compiler/parsing/proofs                               8m41s   1GB
Jun 13 10:33:29 Starting compiler/inference/proofs
Jun 13 10:39:43 Finished compiler/inference/proofs                             6m13s   1GB
Jun 13 10:39:43 Starting compiler/backend/semantics
Jun 13 11:50:49 Finished compiler/backend/semantics                         1h11m05s   2GB
Jun 13 11:50:49 Starting compiler/backend/reg_alloc/proofs
Jun 13 11:58:39 Finished compiler/backend/reg_alloc/proofs                     7m49s   1GB
Jun 13 11:58:39 Starting compiler/backend/proofs
Jun 13 13:47:29 Finished compiler/backend/proofs                            1h48m50s  16GB
Jun 13 13:47:30 Starting compiler/backend/serialiser
Jun 13 13:50:53 Finished compiler/backend/serialiser                           3m23s   1GB
Jun 13 13:50:53 Starting compiler/encoders/x64/proofs
Jun 13 14:12:19 Finished compiler/encoders/x64/proofs                         21m25s   5GB
Jun 13 14:12:19 Starting compiler/encoders/arm7/proofs
Jun 13 14:42:12 Finished compiler/encoders/arm7/proofs                        29m53s   8GB
Jun 13 14:42:12 Starting compiler/encoders/arm8/proofs
Jun 13 14:57:47 Finished compiler/encoders/arm8/proofs                        15m34s   1GB
Jun 13 14:57:47 Starting compiler/encoders/arm8_asl/proofs
Jun 13 15:32:42 Finished compiler/encoders/arm8_asl/proofs                    34m54s   2GB
Jun 13 15:32:42 Starting compiler/encoders/mips/proofs
Jun 13 15:55:04 Finished compiler/encoders/mips/proofs                        22m21s   2GB
Jun 13 15:55:04 Starting compiler/encoders/riscv/proofs
Jun 13 16:15:18 Finished compiler/encoders/riscv/proofs                       20m13s   1GB
Jun 13 16:15:18 Starting compiler/encoders/ag32/proofs
Jun 13 16:21:03 Finished compiler/encoders/ag32/proofs                         5m45s 868MB
Jun 13 16:21:04 Starting compiler/backend/x64/proofs
Jun 13 16:22:06 Finished compiler/backend/x64/proofs                           1m02s   1GB
Jun 13 16:22:06 Starting compiler/backend/arm7/proofs
Jun 13 16:23:09 Finished compiler/backend/arm7/proofs                          1m02s   1GB
Jun 13 16:23:10 Starting compiler/backend/arm8/proofs
Jun 13 16:24:12 Finished compiler/backend/arm8/proofs                          1m02s   1GB
Jun 13 16:24:12 Starting compiler/backend/arm8_asl
Jun 13 16:25:05 Finished compiler/backend/arm8_asl                               52s   1GB
Jun 13 16:25:05 Starting compiler/backend/mips/proofs
Jun 13 16:26:08 Finished compiler/backend/mips/proofs                          1m02s   1GB
Jun 13 16:26:08 Starting compiler/backend/riscv/proofs
Jun 13 16:27:11 Finished compiler/backend/riscv/proofs                         1m02s   1GB
Jun 13 16:27:11 Starting compiler/backend/ag32/proofs
Jun 13 16:57:24 Finished compiler/backend/ag32/proofs                         30m12s   2GB
Jun 13 16:57:25 Starting compiler/proofs
Jun 13 17:01:58 Finished compiler/proofs                                       4m33s   3GB
Jun 13 17:01:58 Starting candle/set-theory
Jun 13 17:03:09 Finished candle/set-theory                                     1m10s   1GB
Jun 13 17:03:09 Starting candle/syntax-lib
Jun 13 17:03:37 Finished candle/syntax-lib                                       28s 633MB
Jun 13 17:03:37 Starting candle/standard/syntax
Jun 13 17:08:08 Finished candle/standard/syntax                                4m30s   1GB
Jun 13 17:08:08 Starting candle/standard/semantics
Jun 13 17:12:11 Finished candle/standard/semantics                             4m02s   1GB
Jun 13 17:12:11 Starting candle/standard/monadic
Jun 13 17:16:13 Finished candle/standard/monadic                               4m00s   2GB
Jun 13 17:16:13 Starting candle/standard/ml_kernel
Jun 13 17:30:05 Finished candle/standard/ml_kernel                            13m52s   3GB
Jun 13 17:30:05 Starting candle/overloading/syntax
Jun 13 17:36:59 Finished candle/overloading/syntax                             6m53s   1GB
Jun 13 17:36:59 Starting candle/overloading/semantics
Jun 13 18:03:19 Finished candle/overloading/semantics                         26m19s   2GB
Jun 13 18:03:19 Starting candle/overloading/monadic
Jun 13 18:08:56 Finished candle/overloading/monadic                            5m36s   1GB
Jun 13 18:08:57 Starting candle/overloading/ml_kernel
Jun 13 18:24:34 Finished candle/overloading/ml_kernel                         15m36s   3GB
Jun 13 18:24:34 Starting candle/overloading/ml_checker
Jun 13 18:30:05 Finished candle/overloading/ml_checker                         5m30s   2GB
Jun 13 18:30:05 Starting candle/prover
Jun 13 18:54:13 Finished candle/prover                                        24m07s   3GB
Jun 13 18:54:13 Starting pancake
Jun 13 19:02:31 Finished pancake                                               8m18s   4GB
Jun 13 19:02:31 Starting pancake/ffi
Jun 13 19:02:32 Finished pancake/ffi                                              0s  30MB
Jun 13 19:02:32 Starting pancake/semantics
Jun 13 19:07:59 Finished pancake/semantics                                     5m26s   1GB
Jun 13 19:07:59 Starting pancake/proofs
Jun 13 19:34:01 Finished pancake/proofs                                       26m01s   4GB
Jun 13 19:34:01 Starting characteristic/examples
Jun 13 19:37:10 Finished characteristic/examples                               3m08s   2GB
Jun 13 19:37:10 Starting tutorial/solutions
Jun 13 20:13:45 Finished tutorial/solutions                                   36m34s   9GB
Jun 13 20:13:45 Starting translator/monadic/examples
Jun 13 20:20:45 Finished translator/monadic/examples                           6m59s   2GB
Jun 13 20:20:45 Starting examples
Jun 13 20:31:25 FAILED: examples
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[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)/src/coalgebras[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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[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
Scanned 29 directories
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
README.md                                                                                                                                                                                             (0s)     OK
Starting work on divTheory
lcsTheory                                                                                                                                                                                            (34s)     OK
Starting work on diffTheory
diffTheory                                                                                                                                                                                           (87s)     OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                                                                       (178s)     OK
Starting work on doubleProgTheory
quicksortProgTheory                                                                                                                                                                                 (199s)     OK
Starting work on array_searchProgTheory
divTheory                                                                                                                                                                                           (234s)     OK
Starting work on echoProgTheory
diffProgTheory                                                                                                                                                                                      (189s)     OK
Starting work on filterProgTheory
doubleProgTheory                                                                                                                                                                                    (158s)     OK
Starting work on grepProgTheory
echoProgTheory                                                                                                                                                                                      (136s)     OK
Starting work on helloErrProgTheory
array_searchProgTheory                                                                                                                                                                              (198s)     OK
Starting work on helloProgTheory
helloErrProgTheory                                                                                                                                                                                  (136s)     OK
Starting work on insertSortProgTheory
helloProgTheory                                                                                                                                                                                     (130s)     OK
Starting work on iocatProgTheory
filterProgTheory                                                                                                                                                                                    (229s)     OK
Starting work on lispProgTheory
lispProgTheory                                                                                                                                                                                       (70s)FAIL<1>
 error in quse /root/regression/cakeml-1921/examples/lispProgScript.sml : Fail "Static Errors"
 error in load /root/regression/cakeml-1921/examples/lispProgScript : Fail "Static Errors"
 /root/regression/cakeml-1921/examples/lispProgScript.sml:5: error: Structure (parsingTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 /root/regression/cakeml-1921/examples/lispProgScript.sml:5: error: Structure (source_valuesTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 /root/regression/cakeml-1921/examples/lispProgScript.sml:5: error: Structure (printingTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 Uncaught exception: Fail "Static Errors"
grepProgTheory                                                                                                                                                                                      (282s)MKILLED
insertSortProgTheory                                                                                                                                                                                (106s)MKILLED
iocatProgTheory                                                                                                                                                                                      (85s)MKILLED