CakeML Regression Test

Job 2060

CakeML:29121bf320e463ee435b112eac99656eb6ef0d37
  Merge branch 'master' into libm_gen [Dec 06 15:36:07]
#911 (libm_gen)
Merging into:68d5c7577d631f58bb40f40e1ebfe49873f26a38
  Merge pull request #915 from CakeML/translator-fix [Dec 03 06:09:07]
HOL:cf37a2b2a4f27c3748bb4bb8738c08373abde4c3
  Update PropLogic example to use modern syntax [Nov 30 09:32:01]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Dec 06 23:02:54 Claimed job
Dec 06 23:02:59 Reusing HOL
Dec 06 23:03:38 Starting developers
Dec 06 23:03:44 Finished developers                                               5s 116MB
Dec 06 23:03:44 Starting developers/bin
Dec 06 23:03:50 Finished developers/bin                                           5s   1GB
Dec 06 23:03:50 Starting compiler/proofs
Dec 07 00:49:03 Finished compiler/proofs                                    1h45m11s  18GB
Dec 07 00:49:03 Starting compiler/bootstrap/translation
Dec 07 05:41:45 Finished compiler/bootstrap/translation                     4h52m39s  34GB
Dec 07 05:41:45 Starting semantics/ffi
Dec 07 05:41:50 Finished semantics/ffi                                            4s 140MB
Dec 07 05:41:50 Starting semantics
Dec 07 05:41:52 Finished semantics                                                1s  18MB
Dec 07 05:41:52 Starting semantics/proofs
Dec 07 05:42:23 Finished semantics/proofs                                        31s 882MB
Dec 07 05:42:23 Starting semantics/alt_semantics
Dec 07 05:42:50 Finished semantics/alt_semantics                                 26s 686MB
Dec 07 05:42:50 Starting semantics/alt_semantics/proofs
Dec 07 05:54:43 Finished semantics/alt_semantics/proofs                       11m52s   1GB
Dec 07 05:54:43 Starting basis/pure
Dec 07 05:54:45 Finished basis/pure                                               1s  23MB
Dec 07 05:54:45 Starting translator
Dec 07 05:56:34 Finished translator                                            1m48s   1GB
Dec 07 05:56:34 Starting compiler/parsing
Dec 07 05:56:35 Finished compiler/parsing                                         1s  20MB
Dec 07 05:56:35 Starting characteristic
Dec 07 05:56:37 Finished characteristic                                           1s  22MB
Dec 07 05:56:37 Starting translator/monadic
Dec 07 05:56:39 Finished translator/monadic                                       1s  22MB
Dec 07 05:56:40 Starting basis
Dec 07 06:00:03 Finished basis                                                 3m23s   2GB
Dec 07 06:00:04 Starting compiler/inference
Dec 07 06:00:05 Finished compiler/inference                                       1s  19MB
Dec 07 06:00:05 Starting compiler/backend/reg_alloc
Dec 07 06:00:07 Finished compiler/backend/reg_alloc                               1s  19MB
Dec 07 06:00:07 Starting compiler/backend/gc
Dec 07 06:00:09 Finished compiler/backend/gc                                      2s  25MB
Dec 07 06:00:10 Starting compiler/backend
Dec 07 06:00:21 Finished compiler/backend                                        10s 618MB
Dec 07 06:00:21 Starting compiler/encoders/asm
Dec 07 06:00:23 Finished compiler/encoders/asm                                    1s  23MB
Dec 07 06:00:23 Starting compiler/encoders/x64
Dec 07 06:00:24 Finished compiler/encoders/x64                                    1s  25MB
Dec 07 06:00:25 Starting compiler/encoders/arm7
Dec 07 06:00:26 Finished compiler/encoders/arm7                                   1s  22MB
Dec 07 06:00:26 Starting compiler/encoders/arm8
Dec 07 06:00:28 Finished compiler/encoders/arm8                                   1s  25MB
Dec 07 06:00:28 Starting compiler/encoders/arm8_asl
Dec 07 06:03:43 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Dec 07 06:03:43 Starting compiler/encoders/mips
Dec 07 06:03:45 Finished compiler/encoders/mips                                   1s  22MB
Dec 07 06:03:45 Starting compiler/encoders/riscv
Dec 07 06:03:47 Finished compiler/encoders/riscv                                  1s  24MB
Dec 07 06:03:47 Starting compiler/encoders/ag32
Dec 07 06:03:49 Finished compiler/encoders/ag32                                   1s  21MB
Dec 07 06:03:49 Starting compiler/backend/x64
Dec 07 06:03:51 Finished compiler/backend/x64                                     2s  27MB
Dec 07 06:03:51 Starting compiler/backend/arm7
Dec 07 06:03:54 Finished compiler/backend/arm7                                    2s  21MB
Dec 07 06:03:54 Starting compiler/backend/arm8
Dec 07 06:03:56 Finished compiler/backend/arm8                                    2s  23MB
Dec 07 06:03:56 Starting compiler/backend/mips
Dec 07 06:03:59 Finished compiler/backend/mips                                    2s  22MB
Dec 07 06:03:59 Starting compiler/backend/riscv
Dec 07 06:04:01 Finished compiler/backend/riscv                                   2s  22MB
Dec 07 06:04:01 Starting compiler/backend/ag32
Dec 07 06:05:28 Finished compiler/backend/ag32                                 1m26s   1GB
Dec 07 06:05:28 Starting compiler/parsing/proofs
Dec 07 06:05:29 Finished compiler/parsing/proofs                                  1s  21MB
Dec 07 06:05:29 Starting compiler/inference/proofs
Dec 07 06:05:31 Finished compiler/inference/proofs                                1s  22MB
Dec 07 06:05:31 Starting compiler/backend/semantics
Dec 07 06:06:39 Finished compiler/backend/semantics                            1m07s   1GB
Dec 07 06:06:39 Starting compiler/backend/reg_alloc/proofs
Dec 07 06:06:41 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Dec 07 06:06:41 Starting compiler/backend/proofs
Dec 07 06:07:34 Finished compiler/backend/proofs                                 53s   2GB
Dec 07 06:07:35 Starting compiler/backend/serialiser
Dec 07 06:07:38 Finished compiler/backend/serialiser                              2s  29MB
Dec 07 06:07:38 Starting compiler/encoders/x64/proofs
Dec 07 06:17:30 Finished compiler/encoders/x64/proofs                          9m52s   4GB
Dec 07 06:17:31 Starting compiler/encoders/arm7/proofs
Dec 07 06:31:25 Finished compiler/encoders/arm7/proofs                        13m53s   4GB
Dec 07 06:31:25 Starting compiler/encoders/arm8/proofs
Dec 07 06:38:26 Finished compiler/encoders/arm8/proofs                         7m01s   1GB
Dec 07 06:38:26 Starting compiler/encoders/arm8_asl/proofs
Dec 07 06:54:26 Finished compiler/encoders/arm8_asl/proofs                    15m58s   2GB
Dec 07 06:54:26 Starting compiler/encoders/mips/proofs
Dec 07 07:05:06 Finished compiler/encoders/mips/proofs                        10m39s   2GB
Dec 07 07:05:07 Starting compiler/encoders/riscv/proofs
Dec 07 07:14:12 Finished compiler/encoders/riscv/proofs                        9m05s   1GB
Dec 07 07:14:13 Starting compiler/encoders/ag32/proofs
Dec 07 07:16:55 Finished compiler/encoders/ag32/proofs                         2m42s 802MB
Dec 07 07:16:55 Starting compiler/backend/x64/proofs
Dec 07 07:17:20 Finished compiler/backend/x64/proofs                             24s   1GB
Dec 07 07:17:20 Starting compiler/backend/arm7/proofs
Dec 07 07:17:47 Finished compiler/backend/arm7/proofs                            26s   1GB
Dec 07 07:17:47 Starting compiler/backend/arm8/proofs
Dec 07 07:18:14 Finished compiler/backend/arm8/proofs                            27s   1GB
Dec 07 07:18:14 Starting compiler/backend/arm8_asl
Dec 07 07:18:36 Finished compiler/backend/arm8_asl                               21s   1GB
Dec 07 07:18:36 Starting compiler/backend/mips/proofs
Dec 07 07:19:03 Finished compiler/backend/mips/proofs                            26s   1GB
Dec 07 07:19:03 Starting compiler/backend/riscv/proofs
Dec 07 07:19:30 Finished compiler/backend/riscv/proofs                           26s   1GB
Dec 07 07:19:30 Starting compiler/backend/ag32/proofs
Dec 07 07:32:59 Finished compiler/backend/ag32/proofs                         13m28s   3GB
Dec 07 07:32:59 Starting candle/set-theory
Dec 07 07:33:34 Finished candle/set-theory                                       34s 941MB
Dec 07 07:33:34 Starting candle/syntax-lib
Dec 07 07:33:36 Finished candle/syntax-lib                                        1s  21MB
Dec 07 07:33:36 Starting candle/standard/syntax
Dec 07 07:33:45 Finished candle/standard/syntax                                   9s 525MB
Dec 07 07:33:45 Starting candle/standard/semantics
Dec 07 07:35:30 Finished candle/standard/semantics                             1m44s   1GB
Dec 07 07:35:31 Starting candle/standard/monadic
Dec 07 07:35:33 Finished candle/standard/monadic                                  1s  21MB
Dec 07 07:35:33 Starting candle/standard/ml_kernel
Dec 07 07:37:02 Finished candle/standard/ml_kernel                             1m29s   2GB
Dec 07 07:37:02 Starting candle/overloading/syntax
Dec 07 07:40:18 Finished candle/overloading/syntax                             3m15s   1GB
Dec 07 07:40:18 Starting candle/overloading/semantics
Dec 07 07:52:26 Finished candle/overloading/semantics                         12m07s   2GB
Dec 07 07:52:26 Starting candle/overloading/monadic
Dec 07 07:55:01 Finished candle/overloading/monadic                            2m34s   1GB
Dec 07 07:55:02 Starting candle/overloading/ml_kernel
Dec 07 08:02:29 Finished candle/overloading/ml_kernel                          7m27s   3GB
Dec 07 08:02:29 Starting candle/overloading/ml_checker
Dec 07 08:04:57 Finished candle/overloading/ml_checker                         2m27s   3GB
Dec 07 08:04:57 Starting candle/prover
Dec 07 08:14:36 Finished candle/prover                                         9m38s   3GB
Dec 07 08:14:36 Starting pancake
Dec 07 08:17:40 Finished pancake                                               3m03s   4GB
Dec 07 08:17:40 Starting pancake/ffi
Dec 07 08:17:41 Finished pancake/ffi                                              0s  13MB
Dec 07 08:17:41 Starting pancake/semantics
Dec 07 08:20:05 Finished pancake/semantics                                     2m23s   1GB
Dec 07 08:20:05 Starting pancake/proofs
Dec 07 08:23:07 Finished pancake/proofs                                        3m02s   2GB
Dec 07 08:23:07 Starting characteristic/examples
Dec 07 08:24:36 Finished characteristic/examples                               1m28s   1GB
Dec 07 08:24:37 Starting tutorial/solutions
Dec 07 08:39:45 Finished tutorial/solutions                                   15m08s   8GB
Dec 07 08:39:45 Starting translator/monadic/examples
Dec 07 08:43:36 Finished translator/monadic/examples                           3m50s   2GB
Dec 07 08:43:36 Starting examples
Dec 07 08:53:17 Finished examples                                              9m41s   3GB
Dec 07 08:53:17 Starting examples/compilation/x64
Dec 07 10:50:11 Finished examples/compilation/x64                           1h56m50s  14GB
Dec 07 10:50:11 Starting examples/compilation/x64/proofs
Dec 07 10:52:21 Finished examples/compilation/x64/proofs                       2m10s   3GB
Dec 07 10:52:21 Starting examples/compilation/ag32
Dec 07 11:21:51 Finished examples/compilation/ag32                            29m29s   8GB
Dec 07 11:21:52 Starting examples/compilation/ag32/proofs
Dec 07 11:22:41 Finished examples/compilation/ag32/proofs                        49s   3GB
Dec 07 11:22:42 Starting examples/compilation/to_word
Dec 07 11:25:40 Finished examples/compilation/to_word                          2m58s   6GB
Dec 07 11:25:40 Starting examples/lpr_checker
Dec 07 11:26:39 Finished examples/lpr_checker                                    58s   1GB
Dec 07 11:26:39 Starting examples/lpr_checker/array
Dec 07 12:01:18 Finished examples/lpr_checker/array                           34m37s   5GB
Dec 07 12:01:18 Starting examples/lpr_checker/array/compilation
Dec 07 12:40:09 Finished examples/lpr_checker/array/compilation               38m51s  25GB
Dec 07 12:40:09 Starting examples/lpr_checker/array/compilation/proofs
Dec 07 12:41:31 Finished examples/lpr_checker/array/compilation/proofs         1m21s   6GB
Dec 07 12:41:32 Starting examples/opentheory
Dec 07 12:51:58 Finished examples/opentheory                                  10m26s   3GB
Dec 07 12:51:58 Starting examples/opentheory
Dec 07 12:52:00 Finished examples/opentheory                                      1s  28MB
Dec 07 12:52:00 Starting examples/opentheory/compilation
Dec 07 13:27:55 Finished examples/opentheory/compilation                      35m53s  29GB
Dec 07 13:27:55 Starting examples/opentheory/compilation/proofs
Dec 07 13:28:43 Finished examples/opentheory/compilation/proofs                  48s   3GB
Dec 07 13:28:43 Starting examples/opentheory/compilation/ag32
Dec 07 14:01:53 Finished examples/opentheory/compilation/ag32                 33m09s  28GB
Dec 07 14:01:53 Starting examples/opentheory/compilation/ag32/proofs
Dec 07 14:03:34 Finished examples/opentheory/compilation/ag32/proofs           1m40s   5GB
Dec 07 14:03:34 Starting examples/sat_encodings
Dec 07 14:05:21 Finished examples/sat_encodings                                1m47s 815MB
Dec 07 14:05:22 Starting examples/sat_encodings/case_studies
Dec 07 14:06:59 Finished examples/sat_encodings/case_studies                   1m37s   1GB
Dec 07 14:06:59 Starting examples/sat_encodings/translation
Dec 07 14:12:42 Finished examples/sat_encodings/translation                    5m43s   3GB
Dec 07 14:12:42 Starting examples/sat_encodings/translation/compilation
Dec 07 14:57:19 Finished examples/sat_encodings/translation/compilation       44m35s  19GB
Dec 07 14:57:20 Starting examples/deflate
Dec 07 14:58:12 Finished examples/deflate                                        51s 795MB
Dec 07 14:58:12 Starting examples/deflate/translation
Dec 07 14:59:44 Finished examples/deflate/translation                          1m32s   2GB
Dec 07 14:59:45 Starting examples/deflate/translation/compilation
Dec 07 15:19:08 Finished examples/deflate/translation/compilation             19m23s  11GB
Dec 07 15:19:08 Starting translator/okasaki-examples
Dec 07 15:24:08 Finished translator/okasaki-examples                           4m59s   2GB
Dec 07 15:24:08 Starting translator/other-examples
Dec 07 15:24:54 Finished translator/other-examples                               45s   1GB
Dec 07 15:24:54 Starting compiler/parsing/tests
Dec 07 15:25:25 Finished compiler/parsing/tests                                  30s 671MB
Dec 07 15:25:25 Starting compiler/inference/tests
Dec 07 15:34:04 Finished compiler/inference/tests                              8m38s   3GB
Dec 07 15:34:04 Starting compiler/printing/test
Dec 07 15:37:34 Finished compiler/printing/test                                3m29s   3GB
Dec 07 15:37:34 Starting floatingPoint/tools/flover
Dec 07 16:10:03 Finished floatingPoint/tools/flover                           32m28s   1GB
Dec 07 16:10:03 Starting floatingPoint/icing/
Dec 07 17:10:01 Finished floatingPoint/icing/                                 59m57s   9GB
Dec 07 17:10:02 Starting floatingPoint/icing/examples
Dec 07 17:11:40 Finished floatingPoint/icing/examples                          1m37s   5GB
Dec 07 17:11:40 Starting floatingPoint/tools/dandelion
Dec 07 17:11:43 FAILED: floatingPoint/tools/dandelion
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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/finite_maps[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/examples/algebra/monoid[0m
Scanning [1m$(HOLDIR)/examples/algebra/group[0m
Scanning [1m$(HOLDIR)/examples/algebra/ring[0m
Scanning [1m$(HOLDIR)/examples/algebra/field[0m
Scanning [1m$(HOLDIR)/examples/algebra/polynomial[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/Infra[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/semantics[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover[0m
Scanned 23 directories
Starting work on README.md
Starting work on moreRealTheory
Starting work on renameTheory
Starting work on sollya
README.md                                                                                                                                                                       (0s)FAIL<1>
 ERROR! readme_gen.sml failed due to:
 sollya-8.0: unable to open file: /home/cug/hk324/cml-regression/cakeml-2060/floatingPoint/tools/dandelion/sollya-8.0/README.md
 These errors were in: /home/cug/hk324/cml-regression/cakeml-2060/floatingPoint/tools/dandelion
 
moreRealTheory                                                                                                                                                                  (0s)MKILLED
renameTheory                                                                                                                                                                    (0s)MKILLED
sollya                                                                                                                                                                          (0s)MKILLED