Job 2054

CakeML:eab9fb49e2e2645f23933918b56a49432bf08292
  Fix a minor annoyance in Holmakefile [Nov 30 07:30:42]
#911 (libm_gen)
Merging into:3687487b0ceaa28ee5ceff431d51fa5303742e1f
  Merge pull request #918 from CakeML/clos-interpreter [Nov 29 06:06:35]
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 02 10:36:05 Claimed job
Dec 02 10:36:14 Building HOL
Dec 02 10:47:35 Starting developers
Dec 02 10:47:40 Finished developers                                               5s 153MB
Dec 02 10:47:40 Starting developers/bin
Dec 02 10:47:48 Finished developers/bin                                           7s   1GB
Dec 02 10:47:48 Starting compiler/proofs
Dec 02 12:36:10 Finished compiler/proofs                                    1h48m20s  16GB
Dec 02 12:36:10 Starting compiler/bootstrap/translation
Dec 02 17:31:15 Finished compiler/bootstrap/translation                     4h55m01s  59GB
Dec 02 17:31:15 Starting semantics/ffi
Dec 02 17:31:19 Finished semantics/ffi                                            3s 203MB
Dec 02 17:31:19 Starting semantics
Dec 02 17:31:20 Finished semantics                                                1s  18MB
Dec 02 17:31:20 Starting semantics/proofs
Dec 02 17:31:52 Finished semantics/proofs                                        31s 834MB
Dec 02 17:31:52 Starting semantics/alt_semantics
Dec 02 17:32:19 Finished semantics/alt_semantics                                 26s 686MB
Dec 02 17:32:19 Starting semantics/alt_semantics/proofs
Dec 02 17:44:12 Finished semantics/alt_semantics/proofs                       11m52s   1GB
Dec 02 17:44:12 Starting basis/pure
Dec 02 17:44:13 Finished basis/pure                                               1s  19MB
Dec 02 17:44:14 Starting translator
Dec 02 17:45:59 Finished translator                                            1m45s   1GB
Dec 02 17:46:00 Starting compiler/parsing
Dec 02 17:46:01 Finished compiler/parsing                                         1s  34MB
Dec 02 17:46:01 Starting characteristic
Dec 02 17:46:03 Finished characteristic                                           1s  23MB
Dec 02 17:46:03 Starting translator/monadic
Dec 02 17:46:05 Finished translator/monadic                                       1s  34MB
Dec 02 17:46:05 Starting basis
Dec 02 17:49:32 Finished basis                                                 3m26s   2GB
Dec 02 17:49:32 Starting compiler/inference
Dec 02 17:49:34 Finished compiler/inference                                       1s  22MB
Dec 02 17:49:34 Starting compiler/backend/reg_alloc
Dec 02 17:49:36 Finished compiler/backend/reg_alloc                               1s  28MB
Dec 02 17:49:36 Starting compiler/backend/gc
Dec 02 17:49:38 Finished compiler/backend/gc                                      2s  24MB
Dec 02 17:49:38 Starting compiler/backend
Dec 02 17:49:49 Finished compiler/backend                                        10s 678MB
Dec 02 17:49:49 Starting compiler/encoders/asm
Dec 02 17:49:51 Finished compiler/encoders/asm                                    1s  20MB
Dec 02 17:49:51 Starting compiler/encoders/x64
Dec 02 17:49:53 Finished compiler/encoders/x64                                    1s  20MB
Dec 02 17:49:53 Starting compiler/encoders/arm7
Dec 02 17:49:55 Finished compiler/encoders/arm7                                   1s  20MB
Dec 02 17:49:55 Starting compiler/encoders/arm8
Dec 02 17:49:57 Finished compiler/encoders/arm8                                   1s  33MB
Dec 02 17:49:57 Starting compiler/encoders/arm8_asl
Dec 02 20:10:55 Finished compiler/encoders/arm8_asl                         2h20m56s  26GB
Dec 02 20:10:55 Starting compiler/encoders/mips
Dec 02 20:10:57 Finished compiler/encoders/mips                                   1s  22MB
Dec 02 20:10:57 Starting compiler/encoders/riscv
Dec 02 20:10:59 Finished compiler/encoders/riscv                                  1s  21MB
Dec 02 20:10:59 Starting compiler/encoders/ag32
Dec 02 20:11:01 Finished compiler/encoders/ag32                                   1s  19MB
Dec 02 20:11:01 Starting compiler/backend/x64
Dec 02 20:11:03 Finished compiler/backend/x64                                     2s  33MB
Dec 02 20:11:03 Starting compiler/backend/arm7
Dec 02 20:11:05 Finished compiler/backend/arm7                                    2s  22MB
Dec 02 20:11:05 Starting compiler/backend/arm8
Dec 02 20:11:08 Finished compiler/backend/arm8                                    2s  24MB
Dec 02 20:11:08 Starting compiler/backend/mips
Dec 02 20:11:10 Finished compiler/backend/mips                                    2s  33MB
Dec 02 20:11:10 Starting compiler/backend/riscv
Dec 02 20:11:12 Finished compiler/backend/riscv                                   2s  31MB
Dec 02 20:11:12 Starting compiler/backend/ag32
Dec 02 20:12:38 Finished compiler/backend/ag32                                 1m25s   1GB
Dec 02 20:12:38 Starting compiler/parsing/proofs
Dec 02 20:12:40 Finished compiler/parsing/proofs                                  1s  19MB
Dec 02 20:12:40 Starting compiler/inference/proofs
Dec 02 20:12:42 Finished compiler/inference/proofs                                1s  35MB
Dec 02 20:12:42 Starting compiler/backend/semantics
Dec 02 20:13:50 Finished compiler/backend/semantics                            1m07s   1GB
Dec 02 20:13:50 Starting compiler/backend/reg_alloc/proofs
Dec 02 20:13:52 Finished compiler/backend/reg_alloc/proofs                        1s  35MB
Dec 02 20:13:52 Starting compiler/backend/proofs
Dec 02 20:14:47 Finished compiler/backend/proofs                                 54s   2GB
Dec 02 20:14:47 Starting compiler/backend/serialiser
Dec 02 20:14:49 Finished compiler/backend/serialiser                              2s  34MB
Dec 02 20:14:50 Starting compiler/encoders/x64/proofs
Dec 02 20:24:45 Finished compiler/encoders/x64/proofs                          9m55s   5GB
Dec 02 20:24:45 Starting compiler/encoders/arm7/proofs
Dec 02 20:38:34 Finished compiler/encoders/arm7/proofs                        13m48s   4GB
Dec 02 20:38:34 Starting compiler/encoders/arm8/proofs
Dec 02 20:45:42 Finished compiler/encoders/arm8/proofs                         7m07s   1GB
Dec 02 20:45:42 Starting compiler/encoders/arm8_asl/proofs
Dec 02 21:38:12 Finished compiler/encoders/arm8_asl/proofs                    52m29s   5GB
Dec 02 21:38:12 Starting compiler/encoders/mips/proofs
Dec 02 21:49:02 Finished compiler/encoders/mips/proofs                        10m49s   2GB
Dec 02 21:49:02 Starting compiler/encoders/riscv/proofs
Dec 02 21:58:16 Finished compiler/encoders/riscv/proofs                        9m13s   1GB
Dec 02 21:58:16 Starting compiler/encoders/ag32/proofs
Dec 02 22:00:58 Finished compiler/encoders/ag32/proofs                         2m41s 793MB
Dec 02 22:00:58 Starting compiler/backend/x64/proofs
Dec 02 22:01:25 Finished compiler/backend/x64/proofs                             26s   1GB
Dec 02 22:01:25 Starting compiler/backend/arm7/proofs
Dec 02 22:01:52 Finished compiler/backend/arm7/proofs                            27s   1GB
Dec 02 22:01:52 Starting compiler/backend/arm8/proofs
Dec 02 22:02:19 Finished compiler/backend/arm8/proofs                            26s   1GB
Dec 02 22:02:19 Starting compiler/backend/arm8_asl
Dec 02 22:02:40 Finished compiler/backend/arm8_asl                               20s   1GB
Dec 02 22:02:40 Starting compiler/backend/mips/proofs
Dec 02 22:03:07 Finished compiler/backend/mips/proofs                            27s   2GB
Dec 02 22:03:07 Starting compiler/backend/riscv/proofs
Dec 02 22:03:33 Finished compiler/backend/riscv/proofs                           26s   1GB
Dec 02 22:03:34 Starting compiler/backend/ag32/proofs
Dec 02 22:17:13 Finished compiler/backend/ag32/proofs                         13m39s   2GB
Dec 02 22:17:13 Starting candle/set-theory
Dec 02 22:17:48 Finished candle/set-theory                                       34s 969MB
Dec 02 22:17:49 Starting candle/syntax-lib
Dec 02 22:17:50 Finished candle/syntax-lib                                        1s  34MB
Dec 02 22:17:50 Starting candle/standard/syntax
Dec 02 22:17:59 Finished candle/standard/syntax                                   8s 552MB
Dec 02 22:17:59 Starting candle/standard/semantics
Dec 02 22:19:46 Finished candle/standard/semantics                             1m46s   1GB
Dec 02 22:19:46 Starting candle/standard/monadic
Dec 02 22:19:48 Finished candle/standard/monadic                                  1s  34MB
Dec 02 22:19:48 Starting candle/standard/ml_kernel
Dec 02 22:21:17 Finished candle/standard/ml_kernel                             1m29s   2GB
Dec 02 22:21:17 Starting candle/overloading/syntax
Dec 02 22:24:33 Finished candle/overloading/syntax                             3m15s   1GB
Dec 02 22:24:33 Starting candle/overloading/semantics
Dec 02 22:36:39 Finished candle/overloading/semantics                         12m05s   2GB
Dec 02 22:36:39 Starting candle/overloading/monadic
Dec 02 22:39:19 Finished candle/overloading/monadic                            2m39s   1GB
Dec 02 22:39:19 Starting candle/overloading/ml_kernel
Dec 02 22:46:59 Finished candle/overloading/ml_kernel                          7m39s   3GB
Dec 02 22:46:59 Starting candle/overloading/ml_checker
Dec 02 22:49:28 Finished candle/overloading/ml_checker                         2m28s   3GB
Dec 02 22:49:28 Starting candle/prover
Dec 02 22:59:03 Finished candle/prover                                         9m34s   3GB
Dec 02 22:59:03 Starting pancake
Dec 02 23:02:12 Finished pancake                                               3m09s   5GB
Dec 02 23:02:12 Starting pancake/ffi
Dec 02 23:02:13 Finished pancake/ffi                                              0s  13MB
Dec 02 23:02:13 Starting pancake/semantics
Dec 02 23:04:35 Finished pancake/semantics                                     2m21s   1GB
Dec 02 23:04:35 Starting pancake/proofs
Dec 02 23:07:35 Finished pancake/proofs                                        2m59s   2GB
Dec 02 23:07:35 Starting characteristic/examples
Dec 02 23:09:15 Finished characteristic/examples                               1m39s   2GB
Dec 02 23:09:15 Starting tutorial/solutions
Dec 02 23:24:41 Finished tutorial/solutions                                   15m25s   8GB
Dec 02 23:24:41 Starting translator/monadic/examples
Dec 02 23:28:31 Finished translator/monadic/examples                           3m50s   2GB
Dec 02 23:28:32 Starting examples
Dec 02 23:38:39 Finished examples                                             10m07s   4GB
Dec 02 23:38:40 Starting examples/compilation/x64
Dec 03 01:37:05 Finished examples/compilation/x64                           1h58m24s  17GB
Dec 03 01:37:05 Starting examples/compilation/x64/proofs
Dec 03 01:39:20 Finished examples/compilation/x64/proofs                       2m14s   3GB
Dec 03 01:39:20 Starting examples/compilation/ag32
Dec 03 02:09:10 Finished examples/compilation/ag32                            29m49s   8GB
Dec 03 02:09:10 Starting examples/compilation/ag32/proofs
Dec 03 02:10:00 Finished examples/compilation/ag32/proofs                        49s   3GB
Dec 03 02:10:00 Starting examples/compilation/to_word
Dec 03 02:13:03 Finished examples/compilation/to_word                          3m02s   5GB
Dec 03 02:13:03 Starting examples/lpr_checker
Dec 03 02:14:03 Finished examples/lpr_checker                                    59s   1GB
Dec 03 02:14:03 Starting examples/lpr_checker/array
Dec 03 02:48:58 Finished examples/lpr_checker/array                           34m53s   5GB
Dec 03 02:48:59 Starting examples/lpr_checker/array/compilation
Dec 03 03:26:16 Finished examples/lpr_checker/array/compilation               37m16s  26GB
Dec 03 03:26:16 Starting examples/lpr_checker/array/compilation/proofs
Dec 03 03:27:37 Finished examples/lpr_checker/array/compilation/proofs         1m20s   5GB
Dec 03 03:27:37 Starting examples/opentheory
Dec 03 03:38:03 Finished examples/opentheory                                  10m26s   4GB
Dec 03 03:38:04 Starting examples/opentheory
Dec 03 03:38:05 Finished examples/opentheory                                      1s  34MB
Dec 03 03:38:05 Starting examples/opentheory/compilation
Dec 03 04:14:11 Finished examples/opentheory/compilation                      36m04s  28GB
Dec 03 04:14:11 Starting examples/opentheory/compilation/proofs
Dec 03 04:14:58 Finished examples/opentheory/compilation/proofs                  46s   3GB
Dec 03 04:14:58 Starting examples/opentheory/compilation/ag32
Dec 03 04:48:03 Finished examples/opentheory/compilation/ag32                 33m05s  27GB
Dec 03 04:48:03 Starting examples/opentheory/compilation/ag32/proofs
Dec 03 04:49:50 Finished examples/opentheory/compilation/ag32/proofs           1m46s   7GB
Dec 03 04:49:50 Starting examples/sat_encodings
Dec 03 04:51:36 Finished examples/sat_encodings                                1m46s 690MB
Dec 03 04:51:37 Starting examples/sat_encodings/case_studies
Dec 03 04:53:14 Finished examples/sat_encodings/case_studies                   1m37s 846MB
Dec 03 04:53:14 Starting examples/sat_encodings/translation
Dec 03 04:59:05 Finished examples/sat_encodings/translation                    5m50s   4GB
Dec 03 04:59:05 Starting examples/sat_encodings/translation/compilation
Dec 03 05:43:48 Finished examples/sat_encodings/translation/compilation       44m41s  17GB
Dec 03 05:43:48 Starting examples/deflate
Dec 03 05:44:40 Finished examples/deflate                                        52s 831MB
Dec 03 05:44:40 Starting examples/deflate/translation
Dec 03 05:46:14 Finished examples/deflate/translation                          1m33s   3GB
Dec 03 05:46:15 Starting examples/deflate/translation/compilation
Dec 03 06:06:20 Finished examples/deflate/translation/compilation             20m05s  12GB
Dec 03 06:06:20 Starting translator/okasaki-examples
Dec 03 06:11:15 Finished translator/okasaki-examples                           4m55s   3GB
Dec 03 06:11:16 Starting translator/other-examples
Dec 03 06:13:36 Finished translator/other-examples                             2m20s   1GB
Dec 03 06:13:36 Starting compiler/parsing/tests
Dec 03 06:14:07 Finished compiler/parsing/tests                                  30s 553MB
Dec 03 06:14:07 Starting compiler/inference/tests
Dec 03 06:22:50 Finished compiler/inference/tests                              8m42s   4GB
Dec 03 06:22:50 Starting compiler/printing/test
Dec 03 06:26:26 Finished compiler/printing/test                                3m35s   3GB
Dec 03 06:26:26 Starting floatingPoint/tools/flover
Dec 03 06:58:39 Finished floatingPoint/tools/flover                           32m10s   1GB
Dec 03 06:58:39 Starting floatingPoint/icing/
Dec 03 07:58:06 Finished floatingPoint/icing/                                 59m26s   9GB
Dec 03 07:58:06 Starting floatingPoint/icing/examples
Dec 03 07:59:49 Finished floatingPoint/icing/examples                          1m40s   5GB
Dec 03 07:59:50 Starting floatingPoint/tools/dandelion
Dec 03 07:59:53 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-2054/floatingPoint/tools/dandelion/sollya-8.0/README.md
 These errors were in: /home/cug/hk324/cml-regression/cakeml-2054/floatingPoint/tools/dandelion
 
moreRealTheory                                                                                              (0s)MKILLED
renameTheory                                                                                                (0s)MKILLED
sollya                                                                                                      (0s)MKILLED