CakeML Regression Test

Job 1546

CakeML:1a644f8a7269bb1b4de9636240741fcdfe989d6e
  Fix a translation [Jun 13 21:10:45]
#829 (help)
Merging into:36d5c13ef89908d2c2bf082c13186087bd1502f6
  Merge pull request #828 from CakeML/sat_encodings [Jun 04 08:57:36]
HOL:b7716bd92d1115f6a85cbf82d4dd47e1bb88828a
  Remove unnecessary dependencies in examples/polynomial/polynomial [Jun 09 01:52:42]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 13 21:11:21 Claimed job
Jun 13 21:11:23 Reusing HOL
Jun 13 21:11:28 Starting developers
Jun 13 21:11:31 Finished developers                                               2s 103MB
Jun 13 21:11:31 Starting developers/bin
Jun 13 21:11:37 Finished developers/bin                                           5s   1GB
Jun 13 21:11:37 Starting semantics/ffi
Jun 13 21:11:47 Finished semantics/ffi                                            9s 289MB
Jun 13 21:11:48 Starting semantics
Jun 13 21:13:14 Finished semantics                                             1m26s   1GB
Jun 13 21:13:14 Starting semantics/proofs
Jun 13 21:16:45 Finished semantics/proofs                                      3m31s   1GB
Jun 13 21:16:46 Starting semantics/alt_semantics
Jun 13 21:16:54 Finished semantics/alt_semantics                                  8s 417MB
Jun 13 21:16:55 Starting semantics/alt_semantics/proofs
Jun 13 21:19:08 Finished semantics/alt_semantics/proofs                        2m12s   1GB
Jun 13 21:19:08 Starting basis/pure
Jun 13 21:20:01 Finished basis/pure                                              53s   1GB
Jun 13 21:20:02 Starting translator
Jun 13 21:23:22 Finished translator                                            3m19s   2GB
Jun 13 21:23:22 Starting compiler/parsing
Jun 13 21:24:32 Finished compiler/parsing                                      1m09s   4GB
Jun 13 21:24:32 Starting characteristic
Jun 13 21:30:19 Finished characteristic                                        5m47s   4GB
Jun 13 21:30:19 Starting translator/monadic
Jun 13 21:32:06 Finished translator/monadic                                    1m45s   3GB
Jun 13 21:32:06 Starting basis
Jun 13 22:16:14 Finished basis                                                44m07s  41GB
Jun 13 22:16:14 Starting compiler/inference
Jun 13 22:17:22 Finished compiler/inference                                    1m07s   1GB
Jun 13 22:17:23 Starting compiler/backend/reg_alloc
Jun 13 22:18:30 Finished compiler/backend/reg_alloc                            1m06s   1GB
Jun 13 22:18:30 Starting compiler/backend/gc
Jun 13 22:21:57 Finished compiler/backend/gc                                   3m27s   4GB
Jun 13 22:21:57 Starting compiler/backend
Jun 13 22:27:05 Finished compiler/backend                                      5m07s   5GB
Jun 13 22:27:05 Starting compiler/encoders/asm
Jun 13 22:27:28 Finished compiler/encoders/asm                                   22s   1GB
Jun 13 22:27:28 Starting compiler/encoders/x64
Jun 13 22:27:55 Finished compiler/encoders/x64                                   26s   1GB
Jun 13 22:27:55 Starting compiler/encoders/arm7
Jun 13 22:28:46 Finished compiler/encoders/arm7                                  50s   1GB
Jun 13 22:28:46 Starting compiler/encoders/arm8
Jun 13 22:29:00 Finished compiler/encoders/arm8                                  13s   1GB
Jun 13 22:29:00 Starting compiler/encoders/mips
Jun 13 22:29:18 Finished compiler/encoders/mips                                  18s   1GB
Jun 13 22:29:19 Starting compiler/encoders/riscv
Jun 13 22:29:34 Finished compiler/encoders/riscv                                 15s   1GB
Jun 13 22:29:34 Starting compiler/encoders/ag32
Jun 13 22:29:53 Finished compiler/encoders/ag32                                  18s 966MB
Jun 13 22:29:53 Starting compiler/backend/x64
Jun 13 22:30:13 Finished compiler/backend/x64                                    19s   1GB
Jun 13 22:30:13 Starting compiler/backend/arm7
Jun 13 22:30:35 Finished compiler/backend/arm7                                   21s   1GB
Jun 13 22:30:35 Starting compiler/backend/arm8
Jun 13 22:30:55 Finished compiler/backend/arm8                                   20s   1GB
Jun 13 22:30:55 Starting compiler/backend/mips
Jun 13 22:31:16 Finished compiler/backend/mips                                   20s   1GB
Jun 13 22:31:17 Starting compiler/backend/riscv
Jun 13 22:31:38 Finished compiler/backend/riscv                                  21s   1GB
Jun 13 22:31:39 Starting compiler/backend/ag32
Jun 13 22:32:50 Finished compiler/backend/ag32                                 1m11s   2GB
Jun 13 22:32:50 Starting compiler/parsing/proofs
Jun 13 22:38:43 Finished compiler/parsing/proofs                               5m52s   2GB
Jun 13 22:38:43 Starting compiler/inference/proofs
Jun 13 22:41:15 Finished compiler/inference/proofs                             2m32s   2GB
Jun 13 22:41:15 Starting compiler/backend/semantics
Jun 13 23:07:59 Finished compiler/backend/semantics                           26m43s   5GB
Jun 13 23:07:59 Starting compiler/backend/reg_alloc/proofs
Jun 13 23:11:15 Finished compiler/backend/reg_alloc/proofs                     3m16s   1GB
Jun 13 23:11:16 Starting compiler/backend/proofs
Jun 14 00:05:27 Finished compiler/backend/proofs                              54m11s  20GB
Jun 14 00:05:27 Starting compiler/encoders/x64/proofs
Jun 14 00:14:46 Finished compiler/encoders/x64/proofs                          9m18s   4GB
Jun 14 00:14:46 Starting compiler/encoders/arm7/proofs
Jun 14 00:27:32 Finished compiler/encoders/arm7/proofs                        12m45s   7GB
Jun 14 00:27:32 Starting compiler/encoders/arm8/proofs
Jun 14 00:34:16 Finished compiler/encoders/arm8/proofs                         6m42s   3GB
Jun 14 00:34:16 Starting compiler/encoders/mips/proofs
Jun 14 00:44:05 Finished compiler/encoders/mips/proofs                         9m48s   6GB
Jun 14 00:44:05 Starting compiler/encoders/riscv/proofs
Jun 14 00:52:34 Finished compiler/encoders/riscv/proofs                        8m29s   3GB
Jun 14 00:52:35 Starting compiler/encoders/ag32/proofs
Jun 14 00:54:56 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Jun 14 00:54:56 Starting compiler/backend/x64/proofs
Jun 14 00:55:17 Finished compiler/backend/x64/proofs                             21s   1GB
Jun 14 00:55:17 Starting compiler/backend/arm7/proofs
Jun 14 00:55:40 Finished compiler/backend/arm7/proofs                            22s   1GB
Jun 14 00:55:41 Starting compiler/backend/arm8/proofs
Jun 14 00:56:02 Finished compiler/backend/arm8/proofs                            21s   1GB
Jun 14 00:56:02 Starting compiler/backend/mips/proofs
Jun 14 00:56:24 Finished compiler/backend/mips/proofs                            21s   1GB
Jun 14 00:56:25 Starting compiler/backend/riscv/proofs
Jun 14 00:56:48 Finished compiler/backend/riscv/proofs                           23s   2GB
Jun 14 00:56:48 Starting compiler/backend/ag32/proofs
Jun 14 01:08:58 Finished compiler/backend/ag32/proofs                         12m08s   4GB
Jun 14 01:08:59 Starting compiler/proofs
Jun 14 01:10:44 Finished compiler/proofs                                       1m44s   6GB
Jun 14 01:10:44 Starting candle/set-theory
Jun 14 01:11:15 Finished candle/set-theory                                       30s   1GB
Jun 14 01:11:15 Starting candle/syntax-lib
Jun 14 01:11:26 Finished candle/syntax-lib                                       11s 792MB
Jun 14 01:11:26 Starting candle/standard/syntax
Jun 14 01:13:19 Finished candle/standard/syntax                                1m52s   1GB
Jun 14 01:13:19 Starting candle/standard/semantics
Jun 14 01:15:05 Finished candle/standard/semantics                             1m46s   2GB
Jun 14 01:15:05 Starting candle/standard/monadic
Jun 14 01:16:50 Finished candle/standard/monadic                               1m44s   1GB
Jun 14 01:16:50 Starting candle/standard/ml_kernel
Jun 14 01:22:18 Finished candle/standard/ml_kernel                             5m27s   6GB
Jun 14 01:22:18 Starting candle/overloading/syntax
Jun 14 01:25:32 Finished candle/overloading/syntax                             3m14s   1GB
Jun 14 01:25:32 Starting candle/overloading/semantics
Jun 14 01:37:36 Finished candle/overloading/semantics                         12m03s   7GB
Jun 14 01:37:36 Starting characteristic/examples
Jun 14 01:38:56 Finished characteristic/examples                               1m19s   5GB
Jun 14 01:38:56 Starting tutorial/solutions
Jun 14 01:54:22 Finished tutorial/solutions                                   15m25s  12GB
Jun 14 01:54:22 Starting translator/monadic/examples
Jun 14 01:57:49 Finished translator/monadic/examples                           3m27s   3GB
Jun 14 01:57:50 Starting examples
Jun 14 02:07:01 Finished examples                                              9m11s   6GB
Jun 14 02:07:01 Starting examples/compilation/x64
Jun 14 04:29:25 Finished examples/compilation/x64                           2h22m22s  23GB
Jun 14 04:29:25 Starting examples/compilation/x64/proofs
Jun 14 04:31:24 Finished examples/compilation/x64/proofs                       1m58s   3GB
Jun 14 04:31:24 Starting examples/compilation/ag32
Jun 14 05:05:23 Finished examples/compilation/ag32                            33m59s  15GB
Jun 14 05:05:23 Starting examples/compilation/ag32/proofs
Jun 14 05:06:18 Finished examples/compilation/ag32/proofs                        54s   5GB
Jun 14 05:06:19 Starting examples/cost
Jun 14 06:01:42 Finished examples/cost                                        55m22s  13GB
Jun 14 06:01:42 Starting examples/lpr_checker
Jun 14 06:05:37 Finished examples/lpr_checker                                  3m54s   6GB
Jun 14 06:05:37 Starting examples/lpr_checker/compilation
Jun 14 06:24:18 Finished examples/lpr_checker/compilation                     18m40s  14GB
Jun 14 06:24:18 Starting examples/lpr_checker/compilation/proofs
Jun 14 06:25:02 Finished examples/lpr_checker/compilation/proofs                 44s   4GB
Jun 14 06:25:02 Starting examples/lpr_checker/array
Jun 14 06:38:46 Finished examples/lpr_checker/array                           13m43s   5GB
Jun 14 06:38:46 Starting examples/lpr_checker/array/compilation
Jun 14 06:58:47 Finished examples/lpr_checker/array/compilation               20m00s  20GB
Jun 14 06:58:47 Starting examples/lpr_checker/array/compilation/proofs
Jun 14 06:59:35 Finished examples/lpr_checker/array/compilation/proofs           48s   5GB
Jun 14 06:59:36 Starting examples/opentheory
Jun 14 07:08:55 Finished examples/opentheory                                   9m17s   6GB
Jun 14 07:08:55 Starting examples/opentheory
Jun 14 07:08:56 Finished examples/opentheory                                      0s  98MB
Jun 14 07:08:56 Starting examples/opentheory/compilation
Jun 14 07:39:30 Finished examples/opentheory/compilation                      30m33s  21GB
Jun 14 07:39:30 Starting examples/opentheory/compilation/proofs
Jun 14 07:40:16 Finished examples/opentheory/compilation/proofs                  45s   4GB
Jun 14 07:40:16 Starting examples/opentheory/compilation/ag32
Jun 14 08:12:15 Finished examples/opentheory/compilation/ag32                 31m58s  19GB
Jun 14 08:12:15 Starting examples/opentheory/compilation/ag32/proofs
Jun 14 08:13:53 Finished examples/opentheory/compilation/ag32/proofs           1m37s   9GB
Jun 14 08:13:54 Starting examples/sat_encodings
Jun 14 08:15:44 Finished examples/sat_encodings                                1m50s   1GB
Jun 14 08:15:44 Starting examples/sat_encodings/case_studies
Jun 14 08:17:18 Finished examples/sat_encodings/case_studies                   1m33s   1GB
Jun 14 08:17:18 Starting examples/sat_encodings/translation
Jun 14 08:22:54 Finished examples/sat_encodings/translation                    5m35s   6GB
Jun 14 08:22:54 Starting examples/sat_encodings/translation/compilation
Jun 14 09:07:46 Finished examples/sat_encodings/translation/compilation       44m51s  21GB
Jun 14 09:07:46 Starting translator/okasaki-examples
Jun 14 09:12:10 Finished translator/okasaki-examples                           4m23s   2GB
Jun 14 09:12:10 Starting translator/other-examples
Jun 14 09:14:17 Finished translator/other-examples                             2m05s   2GB
Jun 14 09:14:17 Starting compiler/parsing/tests
Jun 14 09:14:42 Finished compiler/parsing/tests                                  24s 674MB
Jun 14 09:14:42 Starting compiler/inference/tests
Jun 14 09:21:59 Finished compiler/inference/tests                              7m17s   7GB
Jun 14 09:21:59 Starting compiler/bootstrap/translation
Jun 14 11:49:53 Finished compiler/bootstrap/translation                     2h27m53s  39GB
Jun 14 11:49:53 Starting unverified/sexpr-bootstrap/x64/64
Jun 14 12:01:58 FAILED: unverified/sexpr-bootstrap/x64/64
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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/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
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/developers/bin[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Starting work on cake.S
Starting work on README.md
Starting work on cake-sexpr-x64-64
README.md                                                                                                                                            real:    0s  user:    0s     OK
cake.S                                                                                                                                               real:    0s  user:    0s     OK
cake-sexpr-x64-64                                                                                                                                    real:   79s  user:   73s     OK
Starting work on cake.S
cake.S                                                                                                                                               real:  634s  user:  605s     OK
Starting work on cake
cake                                                                                                                                                 real:    6s  user:    5s     OK
Starting work on extract_code.cake
extract_code.cake                                                                                                                                    real:    2s  user:    1s     OK
Starting work on how-to.cake
how-to.cake                                                                                                                                          real:    0s  user:    0s     OK
Starting work on how-to.cake
how-to.cake                                                                                                                                          real:    0s  user:    0sFAIL<2>
 ./cake  <how-to.cml >how-to.cake.S
 ### ERROR: parse error
 CakeML heap space exhausted.
 Makefile:70: recipe for target 'how-to.cake.S' failed
 make: *** [how-to.cake.S] Error 1
 rm how-to.cake.S