CakeML Regression Test

Job 2059

CakeML:30067de2abd290d9760b464ba7cf3c32d6d6f465
  Tweak Holmakefile more to build proper README's [Dec 05 07:49:40]
#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 05 08:04:39 Claimed job
Dec 05 08:04:43 Reusing HOL
Dec 05 08:05:23 Starting developers
Dec 05 08:05:28 Finished developers                                               5s 162MB
Dec 05 08:05:28 Starting developers/bin
Dec 05 08:05:34 Finished developers/bin                                           5s   1GB
Dec 05 08:05:35 Starting compiler/proofs
Dec 05 09:50:21 Finished compiler/proofs                                    1h44m45s  16GB
Dec 05 09:50:21 Starting compiler/bootstrap/translation
Dec 05 15:18:39 Finished compiler/bootstrap/translation                     5h28m16s  63GB
Dec 05 15:18:39 Starting semantics/ffi
Dec 05 15:18:44 Finished semantics/ffi                                            4s 140MB
Dec 05 15:18:44 Starting semantics
Dec 05 15:18:46 Finished semantics                                                1s  18MB
Dec 05 15:18:46 Starting semantics/proofs
Dec 05 15:19:18 Finished semantics/proofs                                        31s 881MB
Dec 05 15:19:18 Starting semantics/alt_semantics
Dec 05 15:19:45 Finished semantics/alt_semantics                                 27s 523MB
Dec 05 15:19:45 Starting semantics/alt_semantics/proofs
Dec 05 15:31:53 Finished semantics/alt_semantics/proofs                       12m07s   1GB
Dec 05 15:31:53 Starting basis/pure
Dec 05 15:31:55 Finished basis/pure                                               1s  34MB
Dec 05 15:31:55 Starting translator
Dec 05 15:33:44 Finished translator                                            1m49s   2GB
Dec 05 15:33:45 Starting compiler/parsing
Dec 05 15:33:46 Finished compiler/parsing                                         1s  18MB
Dec 05 15:33:46 Starting characteristic
Dec 05 15:33:48 Finished characteristic                                           1s  24MB
Dec 05 15:33:48 Starting translator/monadic
Dec 05 15:33:50 Finished translator/monadic                                       1s  34MB
Dec 05 15:33:50 Starting basis
Dec 05 15:37:25 Finished basis                                                 3m34s   2GB
Dec 05 15:37:25 Starting compiler/inference
Dec 05 15:37:27 Finished compiler/inference                                       1s  18MB
Dec 05 15:37:27 Starting compiler/backend/reg_alloc
Dec 05 15:37:29 Finished compiler/backend/reg_alloc                               1s  35MB
Dec 05 15:37:29 Starting compiler/backend/gc
Dec 05 15:37:31 Finished compiler/backend/gc                                      2s  35MB
Dec 05 15:37:31 Starting compiler/backend
Dec 05 15:37:42 Finished compiler/backend                                        10s 620MB
Dec 05 15:37:43 Starting compiler/encoders/asm
Dec 05 15:37:44 Finished compiler/encoders/asm                                    1s  19MB
Dec 05 15:37:44 Starting compiler/encoders/x64
Dec 05 15:37:46 Finished compiler/encoders/x64                                    1s  26MB
Dec 05 15:37:46 Starting compiler/encoders/arm7
Dec 05 15:37:48 Finished compiler/encoders/arm7                                   1s  20MB
Dec 05 15:37:48 Starting compiler/encoders/arm8
Dec 05 15:37:50 Finished compiler/encoders/arm8                                   1s  25MB
Dec 05 15:37:50 Starting compiler/encoders/arm8_asl
Dec 05 15:41:27 Finished compiler/encoders/arm8_asl                            3m37s   1GB
Dec 05 15:41:28 Starting compiler/encoders/mips
Dec 05 15:41:30 Finished compiler/encoders/mips                                   2s  19MB
Dec 05 15:41:30 Starting compiler/encoders/riscv
Dec 05 15:41:33 Finished compiler/encoders/riscv                                  2s  24MB
Dec 05 15:41:33 Starting compiler/encoders/ag32
Dec 05 15:41:35 Finished compiler/encoders/ag32                                   1s  21MB
Dec 05 15:41:35 Starting compiler/backend/x64
Dec 05 15:41:38 Finished compiler/backend/x64                                     2s  23MB
Dec 05 15:41:38 Starting compiler/backend/arm7
Dec 05 15:41:41 Finished compiler/backend/arm7                                    2s  28MB
Dec 05 15:41:41 Starting compiler/backend/arm8
Dec 05 15:41:44 Finished compiler/backend/arm8                                    2s  24MB
Dec 05 15:41:44 Starting compiler/backend/mips
Dec 05 15:41:47 Finished compiler/backend/mips                                    2s  35MB
Dec 05 15:41:47 Starting compiler/backend/riscv
Dec 05 15:41:49 Finished compiler/backend/riscv                                   2s  24MB
Dec 05 15:41:50 Starting compiler/backend/ag32
Dec 05 15:43:46 Finished compiler/backend/ag32                                 1m56s   1GB
Dec 05 15:43:46 Starting compiler/parsing/proofs
Dec 05 15:43:49 Finished compiler/parsing/proofs                                  1s  34MB
Dec 05 15:43:49 Starting compiler/inference/proofs
Dec 05 15:43:51 Finished compiler/inference/proofs                                2s  22MB
Dec 05 15:43:51 Starting compiler/backend/semantics
Dec 05 15:45:25 Finished compiler/backend/semantics                            1m33s   1GB
Dec 05 15:45:25 Starting compiler/backend/reg_alloc/proofs
Dec 05 15:45:27 Finished compiler/backend/reg_alloc/proofs                        1s  35MB
Dec 05 15:45:27 Starting compiler/backend/proofs
Dec 05 15:46:28 Finished compiler/backend/proofs                               1m00s   2GB
Dec 05 15:46:28 Starting compiler/backend/serialiser
Dec 05 15:46:31 Finished compiler/backend/serialiser                              2s  34MB
Dec 05 15:46:31 Starting compiler/encoders/x64/proofs
Dec 05 15:59:51 Finished compiler/encoders/x64/proofs                         13m19s   5GB
Dec 05 15:59:51 Starting compiler/encoders/arm7/proofs
Dec 05 16:20:16 Finished compiler/encoders/arm7/proofs                        20m23s   1GB
Dec 05 16:20:16 Starting compiler/encoders/arm8/proofs
Dec 05 16:27:33 Finished compiler/encoders/arm8/proofs                         7m17s   1GB
Dec 05 16:27:33 Starting compiler/encoders/arm8_asl/proofs
Dec 05 16:45:36 Finished compiler/encoders/arm8_asl/proofs                    18m02s   2GB
Dec 05 16:45:36 Starting compiler/encoders/mips/proofs
Dec 05 16:56:40 Finished compiler/encoders/mips/proofs                        11m04s   2GB
Dec 05 16:56:41 Starting compiler/encoders/riscv/proofs
Dec 05 17:06:07 Finished compiler/encoders/riscv/proofs                        9m26s   1GB
Dec 05 17:06:07 Starting compiler/encoders/ag32/proofs
Dec 05 17:08:55 Finished compiler/encoders/ag32/proofs                         2m47s 964MB
Dec 05 17:08:55 Starting compiler/backend/x64/proofs
Dec 05 17:09:22 Finished compiler/backend/x64/proofs                             27s   1GB
Dec 05 17:09:23 Starting compiler/backend/arm7/proofs
Dec 05 17:09:51 Finished compiler/backend/arm7/proofs                            28s   1GB
Dec 05 17:09:51 Starting compiler/backend/arm8/proofs
Dec 05 17:10:18 Finished compiler/backend/arm8/proofs                            27s   1GB
Dec 05 17:10:19 Starting compiler/backend/arm8_asl
Dec 05 17:10:49 Finished compiler/backend/arm8_asl                               30s   1GB
Dec 05 17:10:49 Starting compiler/backend/mips/proofs
Dec 05 17:11:15 Finished compiler/backend/mips/proofs                            26s   1GB
Dec 05 17:11:16 Starting compiler/backend/riscv/proofs
Dec 05 17:11:43 Finished compiler/backend/riscv/proofs                           26s   2GB
Dec 05 17:11:43 Starting compiler/backend/ag32/proofs
Dec 05 17:25:07 Finished compiler/backend/ag32/proofs                         13m23s   2GB
Dec 05 17:25:07 Starting candle/set-theory
Dec 05 17:25:42 Finished candle/set-theory                                       34s 971MB
Dec 05 17:25:42 Starting candle/syntax-lib
Dec 05 17:25:44 Finished candle/syntax-lib                                        1s  20MB
Dec 05 17:25:44 Starting candle/standard/syntax
Dec 05 17:25:53 Finished candle/standard/syntax                                   9s 552MB
Dec 05 17:25:53 Starting candle/standard/semantics
Dec 05 17:27:38 Finished candle/standard/semantics                             1m44s   1GB
Dec 05 17:27:39 Starting candle/standard/monadic
Dec 05 17:27:41 Finished candle/standard/monadic                                  1s  35MB
Dec 05 17:27:41 Starting candle/standard/ml_kernel
Dec 05 17:29:11 Finished candle/standard/ml_kernel                             1m30s   2GB
Dec 05 17:29:11 Starting candle/overloading/syntax
Dec 05 17:32:22 Finished candle/overloading/syntax                             3m10s   1GB
Dec 05 17:32:22 Starting candle/overloading/semantics
Dec 05 17:44:23 Finished candle/overloading/semantics                         12m00s   2GB
Dec 05 17:44:23 Starting candle/overloading/monadic
Dec 05 17:47:01 Finished candle/overloading/monadic                            2m37s   1GB
Dec 05 17:47:01 Starting candle/overloading/ml_kernel
Dec 05 17:54:37 Finished candle/overloading/ml_kernel                          7m35s   3GB
Dec 05 17:54:37 Starting candle/overloading/ml_checker
Dec 05 17:57:07 Finished candle/overloading/ml_checker                         2m29s   2GB
Dec 05 17:57:07 Starting candle/prover
Dec 05 18:06:53 Finished candle/prover                                         9m45s   3GB
Dec 05 18:06:53 Starting pancake
Dec 05 18:09:56 Finished pancake                                               3m02s   3GB
Dec 05 18:09:56 Starting pancake/ffi
Dec 05 18:09:57 Finished pancake/ffi                                              0s  13MB
Dec 05 18:09:57 Starting pancake/semantics
Dec 05 18:12:20 Finished pancake/semantics                                     2m22s   1GB
Dec 05 18:12:20 Starting pancake/proofs
Dec 05 18:15:24 Finished pancake/proofs                                        3m03s   2GB
Dec 05 18:15:24 Starting characteristic/examples
Dec 05 18:16:50 Finished characteristic/examples                               1m25s   3GB
Dec 05 18:16:50 Starting tutorial/solutions
Dec 05 18:32:06 Finished tutorial/solutions                                   15m15s   8GB
Dec 05 18:32:06 Starting translator/monadic/examples
Dec 05 18:35:59 Finished translator/monadic/examples                           3m52s   3GB
Dec 05 18:36:00 Starting examples
Dec 05 18:45:48 Finished examples                                              9m48s   4GB
Dec 05 18:45:48 Starting examples/compilation/x64
Dec 05 20:43:24 Finished examples/compilation/x64                           1h57m34s  14GB
Dec 05 20:43:24 Starting examples/compilation/x64/proofs
Dec 05 20:45:28 Finished examples/compilation/x64/proofs                       2m03s   3GB
Dec 05 20:45:28 Starting examples/compilation/ag32
Dec 05 21:15:10 Finished examples/compilation/ag32                            29m42s   7GB
Dec 05 21:15:11 Starting examples/compilation/ag32/proofs
Dec 05 21:16:02 Finished examples/compilation/ag32/proofs                        51s   5GB
Dec 05 21:16:03 Starting examples/compilation/to_word
Dec 05 21:19:05 Finished examples/compilation/to_word                          3m01s   5GB
Dec 05 21:19:05 Starting examples/lpr_checker
Dec 05 21:20:04 Finished examples/lpr_checker                                    58s   1GB
Dec 05 21:20:04 Starting examples/lpr_checker/array
Dec 05 21:55:00 Finished examples/lpr_checker/array                           34m54s   5GB
Dec 05 21:55:00 Starting examples/lpr_checker/array/compilation
Dec 05 22:33:33 Finished examples/lpr_checker/array/compilation               38m33s  21GB
Dec 05 22:33:33 Starting examples/lpr_checker/array/compilation/proofs
Dec 05 22:34:53 Finished examples/lpr_checker/array/compilation/proofs         1m20s   6GB
Dec 05 22:34:53 Starting examples/opentheory
Dec 05 22:45:05 Finished examples/opentheory                                  10m11s   5GB
Dec 05 22:45:05 Starting examples/opentheory
Dec 05 22:45:07 Finished examples/opentheory                                      1s  35MB
Dec 05 22:45:07 Starting examples/opentheory/compilation
Dec 05 23:20:55 Finished examples/opentheory/compilation                      35m46s  28GB
Dec 05 23:20:55 Starting examples/opentheory/compilation/proofs
Dec 05 23:22:07 Finished examples/opentheory/compilation/proofs                1m11s   3GB
Dec 05 23:22:07 Starting examples/opentheory/compilation/ag32
Dec 05 23:54:57 Finished examples/opentheory/compilation/ag32                 32m50s  27GB
Dec 05 23:54:58 Starting examples/opentheory/compilation/ag32/proofs
Dec 05 23:56:40 Finished examples/opentheory/compilation/ag32/proofs           1m42s   6GB
Dec 05 23:56:40 Starting examples/sat_encodings
Dec 05 23:58:28 Finished examples/sat_encodings                                1m47s   1GB
Dec 05 23:58:28 Starting examples/sat_encodings/case_studies
Dec 06 00:00:04 Finished examples/sat_encodings/case_studies                   1m36s   1GB
Dec 06 00:00:04 Starting examples/sat_encodings/translation
Dec 06 00:05:59 Finished examples/sat_encodings/translation                    5m54s   4GB
Dec 06 00:05:59 Starting examples/sat_encodings/translation/compilation
Dec 06 00:50:52 Finished examples/sat_encodings/translation/compilation       44m50s  19GB
Dec 06 00:50:52 Starting examples/deflate
Dec 06 00:51:44 Finished examples/deflate                                        51s 791MB
Dec 06 00:51:44 Starting examples/deflate/translation
Dec 06 00:53:18 Finished examples/deflate/translation                          1m33s   3GB
Dec 06 00:53:18 Starting examples/deflate/translation/compilation
Dec 06 01:13:06 Finished examples/deflate/translation/compilation             19m47s  10GB
Dec 06 01:13:06 Starting translator/okasaki-examples
Dec 06 01:18:05 Finished translator/okasaki-examples                           4m59s   3GB
Dec 06 01:18:06 Starting translator/other-examples
Dec 06 01:18:53 Finished translator/other-examples                               46s   1GB
Dec 06 01:18:53 Starting compiler/parsing/tests
Dec 06 01:19:23 Finished compiler/parsing/tests                                  30s 671MB
Dec 06 01:19:24 Starting compiler/inference/tests
Dec 06 01:28:09 Finished compiler/inference/tests                              8m45s   3GB
Dec 06 01:28:09 Starting compiler/printing/test
Dec 06 01:31:41 Finished compiler/printing/test                                3m32s   3GB
Dec 06 01:31:42 Starting floatingPoint/tools/flover
Dec 06 02:03:33 Finished floatingPoint/tools/flover                           31m48s   1GB
Dec 06 02:03:33 Starting floatingPoint/icing/
Dec 06 03:03:30 Finished floatingPoint/icing/                                 59m57s   9GB
Dec 06 03:03:30 Starting floatingPoint/icing/examples
Dec 06 03:05:07 Finished floatingPoint/icing/examples                          1m35s   6GB
Dec 06 03:05:07 Starting floatingPoint/tools/dandelion
Dec 06 03:05:13 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)     OK
sollya                                                                                                                                                                          (1s)FAIL<1>
 checking that pdflatex comes with the necessary packages... yes
 checking for pkg-config... pkg-config
 checking for library containing xmlTextReaderIsEmptyElement... -lxml2
 checking for dlopen in -lc... yes
 checking for __gmpz_init in -lgmp... yes
 checking for __gmpz_fac_ui in -lgmp... yes
 checking for __gmpz_bin_uiui in -lgmp... yes
 checking for __gmpz_export in -lgmp... yes
 checking for mpfr_init in -lmpfr... configure: error: libmpfr unusable
 no
moreRealTheory                                                                                                                                                                  (2s)MKILLED
renameTheory                                                                                                                                                                    (2s)MKILLED