CakeML Regression Test

Job 2057

CakeML:eab9fb49e2e2645f23933918b56a49432bf08292
  Fix a minor annoyance in Holmakefile [Nov 30 07:30:42]
#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 04 12:50:43 Claimed job
Dec 04 12:50:44 Reusing HOL
Dec 04 12:51:24 Starting developers
Dec 04 12:51:29 Finished developers                                               5s  91MB
Dec 04 12:51:30 Starting developers/bin
Dec 04 12:51:36 Finished developers/bin                                           5s   1GB
Dec 04 12:51:36 Starting compiler/proofs
Dec 04 14:36:57 Finished compiler/proofs                                    1h45m19s  18GB
Dec 04 14:36:57 Starting compiler/bootstrap/translation
Dec 04 19:31:26 Finished compiler/bootstrap/translation                     4h54m28s  42GB
Dec 04 19:31:26 Starting semantics/ffi
Dec 04 19:31:31 Finished semantics/ffi                                            4s 140MB
Dec 04 19:31:31 Starting semantics
Dec 04 19:31:33 Finished semantics                                                1s  19MB
Dec 04 19:31:33 Starting semantics/proofs
Dec 04 19:32:04 Finished semantics/proofs                                        31s 882MB
Dec 04 19:32:04 Starting semantics/alt_semantics
Dec 04 19:32:31 Finished semantics/alt_semantics                                 26s 686MB
Dec 04 19:32:31 Starting semantics/alt_semantics/proofs
Dec 04 19:44:27 Finished semantics/alt_semantics/proofs                       11m56s   1GB
Dec 04 19:44:27 Starting basis/pure
Dec 04 19:44:29 Finished basis/pure                                               1s  32MB
Dec 04 19:44:29 Starting translator
Dec 04 19:46:19 Finished translator                                            1m49s   2GB
Dec 04 19:46:19 Starting compiler/parsing
Dec 04 19:46:20 Finished compiler/parsing                                         1s  34MB
Dec 04 19:46:20 Starting characteristic
Dec 04 19:46:22 Finished characteristic                                           1s  23MB
Dec 04 19:46:22 Starting translator/monadic
Dec 04 19:46:24 Finished translator/monadic                                       1s  34MB
Dec 04 19:46:24 Starting basis
Dec 04 19:49:50 Finished basis                                                 3m25s   2GB
Dec 04 19:49:50 Starting compiler/inference
Dec 04 19:49:52 Finished compiler/inference                                       1s  24MB
Dec 04 19:49:52 Starting compiler/backend/reg_alloc
Dec 04 19:49:54 Finished compiler/backend/reg_alloc                               1s  20MB
Dec 04 19:49:54 Starting compiler/backend/gc
Dec 04 19:49:56 Finished compiler/backend/gc                                      2s  34MB
Dec 04 19:49:56 Starting compiler/backend
Dec 04 19:50:07 Finished compiler/backend                                        10s 618MB
Dec 04 19:50:07 Starting compiler/encoders/asm
Dec 04 19:50:08 Finished compiler/encoders/asm                                    1s  24MB
Dec 04 19:50:09 Starting compiler/encoders/x64
Dec 04 19:50:10 Finished compiler/encoders/x64                                    1s  33MB
Dec 04 19:50:10 Starting compiler/encoders/arm7
Dec 04 19:50:12 Finished compiler/encoders/arm7                                   1s  35MB
Dec 04 19:50:12 Starting compiler/encoders/arm8
Dec 04 19:50:14 Finished compiler/encoders/arm8                                   1s  35MB
Dec 04 19:50:14 Starting compiler/encoders/arm8_asl
Dec 04 19:53:23 Finished compiler/encoders/arm8_asl                            3m08s   1GB
Dec 04 19:53:23 Starting compiler/encoders/mips
Dec 04 19:53:25 Finished compiler/encoders/mips                                   1s  31MB
Dec 04 19:53:25 Starting compiler/encoders/riscv
Dec 04 19:53:27 Finished compiler/encoders/riscv                                  1s  20MB
Dec 04 19:53:27 Starting compiler/encoders/ag32
Dec 04 19:53:28 Finished compiler/encoders/ag32                                   1s  24MB
Dec 04 19:53:29 Starting compiler/backend/x64
Dec 04 19:53:31 Finished compiler/backend/x64                                     2s  36MB
Dec 04 19:53:31 Starting compiler/backend/arm7
Dec 04 19:53:33 Finished compiler/backend/arm7                                    2s  39MB
Dec 04 19:53:33 Starting compiler/backend/arm8
Dec 04 19:53:35 Finished compiler/backend/arm8                                    2s  25MB
Dec 04 19:53:35 Starting compiler/backend/mips
Dec 04 19:53:38 Finished compiler/backend/mips                                    2s  34MB
Dec 04 19:53:38 Starting compiler/backend/riscv
Dec 04 19:53:40 Finished compiler/backend/riscv                                   2s  34MB
Dec 04 19:53:40 Starting compiler/backend/ag32
Dec 04 19:55:05 Finished compiler/backend/ag32                                 1m24s   1GB
Dec 04 19:55:05 Starting compiler/parsing/proofs
Dec 04 19:55:07 Finished compiler/parsing/proofs                                  1s  20MB
Dec 04 19:55:07 Starting compiler/inference/proofs
Dec 04 19:55:09 Finished compiler/inference/proofs                                1s  19MB
Dec 04 19:55:09 Starting compiler/backend/semantics
Dec 04 19:56:14 Finished compiler/backend/semantics                            1m05s   1GB
Dec 04 19:56:14 Starting compiler/backend/reg_alloc/proofs
Dec 04 19:56:16 Finished compiler/backend/reg_alloc/proofs                        1s  35MB
Dec 04 19:56:16 Starting compiler/backend/proofs
Dec 04 19:57:10 Finished compiler/backend/proofs                                 53s   2GB
Dec 04 19:57:10 Starting compiler/backend/serialiser
Dec 04 19:57:13 Finished compiler/backend/serialiser                              2s  30MB
Dec 04 19:57:13 Starting compiler/encoders/x64/proofs
Dec 04 20:07:05 Finished compiler/encoders/x64/proofs                          9m51s   4GB
Dec 04 20:07:06 Starting compiler/encoders/arm7/proofs
Dec 04 20:20:55 Finished compiler/encoders/arm7/proofs                        13m49s   4GB
Dec 04 20:20:55 Starting compiler/encoders/arm8/proofs
Dec 04 20:27:55 Finished compiler/encoders/arm8/proofs                         6m59s   1GB
Dec 04 20:27:55 Starting compiler/encoders/arm8_asl/proofs
Dec 04 20:43:57 Finished compiler/encoders/arm8_asl/proofs                    16m01s   2GB
Dec 04 20:43:58 Starting compiler/encoders/mips/proofs
Dec 04 20:54:45 Finished compiler/encoders/mips/proofs                        10m47s   2GB
Dec 04 20:54:45 Starting compiler/encoders/riscv/proofs
Dec 04 21:03:57 Finished compiler/encoders/riscv/proofs                        9m11s   1GB
Dec 04 21:03:57 Starting compiler/encoders/ag32/proofs
Dec 04 21:06:39 Finished compiler/encoders/ag32/proofs                         2m41s 797MB
Dec 04 21:06:39 Starting compiler/backend/x64/proofs
Dec 04 21:07:04 Finished compiler/backend/x64/proofs                             25s   1GB
Dec 04 21:07:04 Starting compiler/backend/arm7/proofs
Dec 04 21:07:32 Finished compiler/backend/arm7/proofs                            27s   1GB
Dec 04 21:07:33 Starting compiler/backend/arm8/proofs
Dec 04 21:08:00 Finished compiler/backend/arm8/proofs                            26s   1GB
Dec 04 21:08:00 Starting compiler/backend/arm8_asl
Dec 04 21:08:22 Finished compiler/backend/arm8_asl                               21s   1GB
Dec 04 21:08:22 Starting compiler/backend/mips/proofs
Dec 04 21:08:49 Finished compiler/backend/mips/proofs                            27s   2GB
Dec 04 21:08:49 Starting compiler/backend/riscv/proofs
Dec 04 21:09:17 Finished compiler/backend/riscv/proofs                           27s   2GB
Dec 04 21:09:17 Starting compiler/backend/ag32/proofs
Dec 04 21:22:43 Finished compiler/backend/ag32/proofs                         13m25s   2GB
Dec 04 21:22:43 Starting candle/set-theory
Dec 04 21:23:18 Finished candle/set-theory                                       35s 903MB
Dec 04 21:23:18 Starting candle/syntax-lib
Dec 04 21:23:20 Finished candle/syntax-lib                                        1s  20MB
Dec 04 21:23:20 Starting candle/standard/syntax
Dec 04 21:23:29 Finished candle/standard/syntax                                   8s 551MB
Dec 04 21:23:29 Starting candle/standard/semantics
Dec 04 21:25:15 Finished candle/standard/semantics                             1m45s   1GB
Dec 04 21:25:15 Starting candle/standard/monadic
Dec 04 21:25:17 Finished candle/standard/monadic                                  1s  35MB
Dec 04 21:25:17 Starting candle/standard/ml_kernel
Dec 04 21:26:46 Finished candle/standard/ml_kernel                             1m29s   2GB
Dec 04 21:26:47 Starting candle/overloading/syntax
Dec 04 21:29:56 Finished candle/overloading/syntax                             3m09s   1GB
Dec 04 21:29:57 Starting candle/overloading/semantics
Dec 04 21:42:16 Finished candle/overloading/semantics                         12m18s   2GB
Dec 04 21:42:16 Starting candle/overloading/monadic
Dec 04 21:44:58 Finished candle/overloading/monadic                            2m38s   1GB
Dec 04 21:44:58 Starting candle/overloading/ml_kernel
Dec 04 21:52:27 Finished candle/overloading/ml_kernel                          7m28s   3GB
Dec 04 21:52:27 Starting candle/overloading/ml_checker
Dec 04 21:55:05 Finished candle/overloading/ml_checker                         2m37s   2GB
Dec 04 21:55:05 Starting candle/prover
Dec 04 22:04:40 Finished candle/prover                                         9m34s   3GB
Dec 04 22:04:40 Starting pancake
Dec 04 22:07:42 Finished pancake                                               3m01s   3GB
Dec 04 22:07:42 Starting pancake/ffi
Dec 04 22:07:43 Finished pancake/ffi                                              0s  13MB
Dec 04 22:07:43 Starting pancake/semantics
Dec 04 22:10:10 Finished pancake/semantics                                     2m27s   1GB
Dec 04 22:10:10 Starting pancake/proofs
Dec 04 22:13:15 Finished pancake/proofs                                        3m04s   2GB
Dec 04 22:13:15 Starting characteristic/examples
Dec 04 22:14:42 Finished characteristic/examples                               1m26s   2GB
Dec 04 22:14:42 Starting tutorial/solutions
Dec 04 22:29:59 Finished tutorial/solutions                                   15m17s   7GB
Dec 04 22:30:00 Starting translator/monadic/examples
Dec 04 22:33:50 Finished translator/monadic/examples                           3m50s   2GB
Dec 04 22:33:50 Starting examples
Dec 04 22:43:45 Finished examples                                              9m54s   4GB
Dec 04 22:43:46 Starting examples/compilation/x64
Dec 05 00:42:18 Finished examples/compilation/x64                           1h58m31s  14GB
Dec 05 00:42:18 Starting examples/compilation/x64/proofs
Dec 05 00:44:27 Finished examples/compilation/x64/proofs                       2m08s   3GB
Dec 05 00:44:27 Starting examples/compilation/ag32
Dec 05 01:13:57 Finished examples/compilation/ag32                            29m29s   7GB
Dec 05 01:13:57 Starting examples/compilation/ag32/proofs
Dec 05 01:14:47 Finished examples/compilation/ag32/proofs                        49s   3GB
Dec 05 01:14:47 Starting examples/compilation/to_word
Dec 05 01:17:58 Finished examples/compilation/to_word                          3m10s   4GB
Dec 05 01:17:58 Starting examples/lpr_checker
Dec 05 01:18:56 Finished examples/lpr_checker                                    58s   1GB
Dec 05 01:18:57 Starting examples/lpr_checker/array
Dec 05 01:54:07 Finished examples/lpr_checker/array                           35m09s   7GB
Dec 05 01:54:07 Starting examples/lpr_checker/array/compilation
Dec 05 02:31:44 Finished examples/lpr_checker/array/compilation               37m36s  25GB
Dec 05 02:31:44 Starting examples/lpr_checker/array/compilation/proofs
Dec 05 02:33:05 Finished examples/lpr_checker/array/compilation/proofs         1m20s   6GB
Dec 05 02:33:05 Starting examples/opentheory
Dec 05 02:44:12 Finished examples/opentheory                                  11m06s   3GB
Dec 05 02:44:12 Starting examples/opentheory
Dec 05 02:44:14 Finished examples/opentheory                                      1s  34MB
Dec 05 02:44:14 Starting examples/opentheory/compilation
Dec 05 03:20:30 Finished examples/opentheory/compilation                      36m15s  30GB
Dec 05 03:20:30 Starting examples/opentheory/compilation/proofs
Dec 05 03:21:17 Finished examples/opentheory/compilation/proofs                  46s   3GB
Dec 05 03:21:17 Starting examples/opentheory/compilation/ag32
Dec 05 03:53:58 Finished examples/opentheory/compilation/ag32                 32m40s  28GB
Dec 05 03:53:58 Starting examples/opentheory/compilation/ag32/proofs
Dec 05 03:55:42 Finished examples/opentheory/compilation/ag32/proofs           1m44s   6GB
Dec 05 03:55:43 Starting examples/sat_encodings
Dec 05 03:57:29 Finished examples/sat_encodings                                1m46s   1GB
Dec 05 03:57:29 Starting examples/sat_encodings/case_studies
Dec 05 03:59:06 Finished examples/sat_encodings/case_studies                   1m36s 972MB
Dec 05 03:59:06 Starting examples/sat_encodings/translation
Dec 05 04:04:53 Finished examples/sat_encodings/translation                    5m46s   5GB
Dec 05 04:04:54 Starting examples/sat_encodings/translation/compilation
Dec 05 04:49:31 Finished examples/sat_encodings/translation/compilation       44m36s  19GB
Dec 05 04:49:31 Starting examples/deflate
Dec 05 04:50:24 Finished examples/deflate                                        52s 811MB
Dec 05 04:50:24 Starting examples/deflate/translation
Dec 05 04:51:58 Finished examples/deflate/translation                          1m33s   3GB
Dec 05 04:51:58 Starting examples/deflate/translation/compilation
Dec 05 05:11:21 Finished examples/deflate/translation/compilation             19m22s  13GB
Dec 05 05:11:21 Starting translator/okasaki-examples
Dec 05 05:16:22 Finished translator/okasaki-examples                           5m01s   2GB
Dec 05 05:16:23 Starting translator/other-examples
Dec 05 05:17:09 Finished translator/other-examples                               46s   1GB
Dec 05 05:17:09 Starting compiler/parsing/tests
Dec 05 05:17:40 Finished compiler/parsing/tests                                  30s 592MB
Dec 05 05:17:40 Starting compiler/inference/tests
Dec 05 05:26:23 Finished compiler/inference/tests                              8m43s   3GB
Dec 05 05:26:24 Starting compiler/printing/test
Dec 05 05:29:58 Finished compiler/printing/test                                3m33s   3GB
Dec 05 05:29:58 Starting floatingPoint/tools/flover
Dec 05 06:02:50 Finished floatingPoint/tools/flover                           32m51s   1GB
Dec 05 06:02:51 Starting floatingPoint/icing/
Dec 05 07:02:52 Finished floatingPoint/icing/                               1h00m00s   5GB
Dec 05 07:02:52 Starting floatingPoint/icing/examples
Dec 05 07:04:33 Finished floatingPoint/icing/examples                          1m41s   3GB
Dec 05 07:04:33 Starting floatingPoint/tools/dandelion
Dec 05 07:04:36 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-2057/floatingPoint/tools/dandelion/sollya-8.0/README.md
 These errors were in: /home/cug/hk324/cml-regression/cakeml-2057/floatingPoint/tools/dandelion
 
moreRealTheory                                                                                                                                                                  (0s)MKILLED
renameTheory                                                                                                                                                                    (0s)MKILLED
sollya                                                                                                                                                                          (0s)MKILLED