CakeML Regression Test

Job 2043

CakeML:b1f08888ac7132052616812b01cdfb07925943e2
  Fix another bug related to readme_gen [Nov 23 11:37:16]
#911 (libm_gen)
Merging into:3d27e77937edd037e810801a4e7849352300104f
  Add [schematic] to a definition (suggested by @mn200) [Nov 07 20:36:24]
HOL:126d898e2a2195a717f5757375b93570965286f1
  Cleanup and tweak release notes for next version in a few places [Nov 03 06:41:06]
Machine:oven3

Nov 23 11:37:36 Claimed job
Nov 23 11:37:38 Reusing HOL
Nov 23 11:38:30 Starting developers
Nov 23 11:38:39 Finished developers                                               8s 156MB
Nov 23 11:38:40 Starting developers/bin
Nov 23 11:38:53 Finished developers/bin                                          12s   1GB
Nov 23 11:38:53 Starting compiler/proofs
Nov 23 15:04:33 Finished compiler/proofs                                    3h25m39s  24GB
Nov 23 15:04:34 Starting compiler/bootstrap/translation
Nov 24 01:29:19 Finished compiler/bootstrap/translation                    10h24m45s  44GB
Nov 24 01:29:19 Starting semantics/ffi
Nov 24 01:29:28 Finished semantics/ffi                                            8s 231MB
Nov 24 01:29:28 Starting semantics
Nov 24 01:29:31 Finished semantics                                                2s  18MB
Nov 24 01:29:31 Starting semantics/proofs
Nov 24 01:30:44 Finished semantics/proofs                                      1m12s 953MB
Nov 24 01:30:44 Starting semantics/alt_semantics
Nov 24 01:31:40 Finished semantics/alt_semantics                                 56s 546MB
Nov 24 01:31:41 Starting semantics/alt_semantics/proofs
Nov 24 01:57:37 Finished semantics/alt_semantics/proofs                       25m56s   1GB
Nov 24 01:57:38 Starting basis/pure
Nov 24 01:57:40 Finished basis/pure                                               2s  32MB
Nov 24 01:57:40 Starting translator
Nov 24 02:01:18 Finished translator                                            3m38s   2GB
Nov 24 02:01:19 Starting compiler/parsing
Nov 24 02:01:21 Finished compiler/parsing                                         2s  34MB
Nov 24 02:01:21 Starting characteristic
Nov 24 02:01:25 Finished characteristic                                           3s  33MB
Nov 24 02:01:25 Starting translator/monadic
Nov 24 02:01:28 Finished translator/monadic                                       2s  25MB
Nov 24 02:01:28 Starting basis
Nov 24 02:08:53 Finished basis                                                 7m24s   2GB
Nov 24 02:08:53 Starting compiler/inference
Nov 24 02:08:56 Finished compiler/inference                                       2s  28MB
Nov 24 02:08:56 Starting compiler/backend/reg_alloc
Nov 24 02:08:59 Finished compiler/backend/reg_alloc                               2s  17MB
Nov 24 02:08:59 Starting compiler/backend/gc
Nov 24 02:09:03 Finished compiler/backend/gc                                      3s  33MB
Nov 24 02:09:03 Starting compiler/backend
Nov 24 02:09:29 Finished compiler/backend                                        26s 509MB
Nov 24 02:09:30 Starting compiler/encoders/asm
Nov 24 02:09:33 Finished compiler/encoders/asm                                    2s  32MB
Nov 24 02:09:33 Starting compiler/encoders/x64
Nov 24 02:09:36 Finished compiler/encoders/x64                                    2s  32MB
Nov 24 02:09:36 Starting compiler/encoders/arm7
Nov 24 02:09:39 Finished compiler/encoders/arm7                                   2s  31MB
Nov 24 02:09:39 Starting compiler/encoders/arm8
Nov 24 02:09:42 Finished compiler/encoders/arm8                                   2s  33MB
Nov 24 02:09:42 Starting compiler/encoders/arm8_asl
Nov 24 02:16:44 Finished compiler/encoders/arm8_asl                            7m01s   1GB
Nov 24 02:16:44 Starting compiler/encoders/mips
Nov 24 02:16:47 Finished compiler/encoders/mips                                   2s  33MB
Nov 24 02:16:48 Starting compiler/encoders/riscv
Nov 24 02:16:50 Finished compiler/encoders/riscv                                  2s  26MB
Nov 24 02:16:51 Starting compiler/encoders/ag32
Nov 24 02:16:54 Finished compiler/encoders/ag32                                   2s  27MB
Nov 24 02:16:54 Starting compiler/backend/x64
Nov 24 02:16:58 Finished compiler/backend/x64                                     3s  27MB
Nov 24 02:16:58 Starting compiler/backend/arm7
Nov 24 02:17:02 Finished compiler/backend/arm7                                    3s  33MB
Nov 24 02:17:02 Starting compiler/backend/arm8
Nov 24 02:17:06 Finished compiler/backend/arm8                                    3s  31MB
Nov 24 02:17:06 Starting compiler/backend/mips
Nov 24 02:17:10 Finished compiler/backend/mips                                    3s  34MB
Nov 24 02:17:10 Starting compiler/backend/riscv
Nov 24 02:17:14 Finished compiler/backend/riscv                                   3s  33MB
Nov 24 02:17:14 Starting compiler/backend/ag32
Nov 24 02:20:12 Finished compiler/backend/ag32                                 2m57s   1GB
Nov 24 02:20:13 Starting compiler/parsing/proofs
Nov 24 02:20:15 Finished compiler/parsing/proofs                                  2s  32MB
Nov 24 02:20:16 Starting compiler/inference/proofs
Nov 24 02:20:19 Finished compiler/inference/proofs                                2s  30MB
Nov 24 02:20:19 Starting compiler/backend/semantics
Nov 24 02:22:41 Finished compiler/backend/semantics                            2m21s   1GB
Nov 24 02:22:41 Starting compiler/backend/reg_alloc/proofs
Nov 24 02:22:44 Finished compiler/backend/reg_alloc/proofs                        3s  34MB
Nov 24 02:22:45 Starting compiler/backend/proofs
Nov 24 02:24:37 Finished compiler/backend/proofs                               1m52s   3GB
Nov 24 02:24:38 Starting compiler/backend/serialiser
Nov 24 02:24:42 Finished compiler/backend/serialiser                              4s  33MB
Nov 24 02:24:43 Starting compiler/encoders/x64/proofs
Nov 24 02:47:02 Finished compiler/encoders/x64/proofs                         22m19s   4GB
Nov 24 02:47:03 Starting compiler/encoders/arm7/proofs
Nov 24 03:17:47 Finished compiler/encoders/arm7/proofs                        30m44s   6GB
Nov 24 03:17:47 Starting compiler/encoders/arm8/proofs
Nov 24 03:33:29 Finished compiler/encoders/arm8/proofs                        15m41s   1GB
Nov 24 03:33:30 Starting compiler/encoders/arm8_asl/proofs
Nov 24 04:10:09 Finished compiler/encoders/arm8_asl/proofs                    36m38s   1GB
Nov 24 04:10:09 Starting compiler/encoders/mips/proofs
Nov 24 04:34:30 Finished compiler/encoders/mips/proofs                        24m20s   2GB
Nov 24 04:34:30 Starting compiler/encoders/riscv/proofs
Nov 24 04:54:44 Finished compiler/encoders/riscv/proofs                       20m13s   1GB
Nov 24 04:54:44 Starting compiler/encoders/ag32/proofs
Nov 24 05:00:38 Finished compiler/encoders/ag32/proofs                         5m54s 876MB
Nov 24 05:00:38 Starting compiler/backend/x64/proofs
Nov 24 05:01:35 Finished compiler/backend/x64/proofs                             56s   1GB
Nov 24 05:01:35 Starting compiler/backend/arm7/proofs
Nov 24 05:02:34 Finished compiler/backend/arm7/proofs                            58s   2GB
Nov 24 05:02:34 Starting compiler/backend/arm8/proofs
Nov 24 05:03:30 Finished compiler/backend/arm8/proofs                            55s   1GB
Nov 24 05:03:30 Starting compiler/backend/arm8_asl
Nov 24 05:04:17 Finished compiler/backend/arm8_asl                               46s   1GB
Nov 24 05:04:17 Starting compiler/backend/mips/proofs
Nov 24 05:05:12 Finished compiler/backend/mips/proofs                            54s   1GB
Nov 24 05:05:13 Starting compiler/backend/riscv/proofs
Nov 24 05:06:14 Finished compiler/backend/riscv/proofs                         1m01s   1GB
Nov 24 05:06:14 Starting compiler/backend/ag32/proofs
Nov 24 05:36:24 Finished compiler/backend/ag32/proofs                         30m09s   2GB
Nov 24 05:36:24 Starting candle/set-theory
Nov 24 05:37:32 Finished candle/set-theory                                     1m08s 977MB
Nov 24 05:37:33 Starting candle/syntax-lib
Nov 24 05:37:35 Finished candle/syntax-lib                                        2s  17MB
Nov 24 05:37:35 Starting candle/standard/syntax
Nov 24 05:37:55 Finished candle/standard/syntax                                  19s 548MB
Nov 24 05:37:55 Starting candle/standard/semantics
Nov 24 05:41:49 Finished candle/standard/semantics                             3m53s   1GB
Nov 24 05:41:49 Starting candle/standard/monadic
Nov 24 05:41:53 Finished candle/standard/monadic                                  3s  26MB
Nov 24 05:41:53 Starting candle/standard/ml_kernel
Nov 24 05:44:54 Finished candle/standard/ml_kernel                             3m01s   3GB
Nov 24 05:44:54 Starting candle/overloading/syntax
Nov 24 05:52:05 Finished candle/overloading/syntax                             7m10s   1GB
Nov 24 05:52:05 Starting candle/overloading/semantics
Nov 24 06:19:07 Finished candle/overloading/semantics                         27m01s   2GB
Nov 24 06:19:08 Starting candle/overloading/monadic
Nov 24 06:24:42 Finished candle/overloading/monadic                            5m34s   1GB
Nov 24 06:24:43 Starting candle/overloading/ml_kernel
Nov 24 06:40:34 Finished candle/overloading/ml_kernel                         15m50s   3GB
Nov 24 06:40:34 Starting candle/overloading/ml_checker
Nov 24 06:45:53 Finished candle/overloading/ml_checker                         5m18s   3GB
Nov 24 06:45:53 Starting candle/prover
Nov 24 07:07:21 Finished candle/prover                                        21m27s   3GB
Nov 24 07:07:21 Starting pancake
Nov 24 07:13:45 Finished pancake                                               6m23s   4GB
Nov 24 07:13:46 Starting pancake/ffi
Nov 24 07:13:46 Finished pancake/ffi                                              0s  11MB
Nov 24 07:13:46 Starting pancake/semantics
Nov 24 07:19:06 Finished pancake/semantics                                     5m19s   1GB
Nov 24 07:19:07 Starting pancake/proofs
Nov 24 07:25:18 Finished pancake/proofs                                        6m10s   2GB
Nov 24 07:25:18 Starting characteristic/examples
Nov 24 07:28:21 Finished characteristic/examples                               3m02s   3GB
Nov 24 07:28:21 Starting tutorial/solutions
Nov 24 08:03:34 Finished tutorial/solutions                                   35m12s   7GB
Nov 24 08:03:35 Starting translator/monadic/examples
Nov 24 08:10:24 Finished translator/monadic/examples                           6m48s   3GB
Nov 24 08:10:24 Starting examples
Nov 24 08:29:24 Finished examples                                             18m59s   3GB
Nov 24 08:29:24 Starting examples/compilation/x64
Nov 24 13:07:26 Finished examples/compilation/x64                           4h38m01s  18GB
Nov 24 13:07:26 Starting examples/compilation/x64/proofs
Nov 24 13:12:02 Finished examples/compilation/x64/proofs                       4m34s   3GB
Nov 24 13:12:02 Starting examples/compilation/ag32
Nov 24 14:27:37 Finished examples/compilation/ag32                          1h15m34s   9GB
Nov 24 14:27:37 Starting examples/compilation/ag32/proofs
Nov 24 14:29:20 Finished examples/compilation/ag32/proofs                      1m42s   3GB
Nov 24 14:29:21 Starting examples/compilation/to_word
Nov 24 14:36:07 Finished examples/compilation/to_word                          6m45s   6GB
Nov 24 14:36:07 Starting examples/lpr_checker
Nov 24 14:38:04 Finished examples/lpr_checker                                  1m56s   1GB
Nov 24 14:38:04 Starting examples/lpr_checker/array
Nov 24 15:58:02 Finished examples/lpr_checker/array                         1h19m57s   5GB
Nov 24 15:58:02 Starting examples/lpr_checker/array/compilation
Nov 24 17:19:28 Finished examples/lpr_checker/array/compilation             1h21m25s  34GB
Nov 24 17:19:28 Starting examples/lpr_checker/array/compilation/proofs
Nov 24 17:22:49 Finished examples/lpr_checker/array/compilation/proofs         3m20s   6GB
Nov 24 17:22:49 Starting examples/opentheory
Nov 24 17:44:58 Finished examples/opentheory                                  22m08s   5GB
Nov 24 17:44:59 Starting examples/opentheory
Nov 24 17:45:02 Finished examples/opentheory                                      3s  33MB
Nov 24 17:45:02 Starting examples/opentheory/compilation
Nov 24 19:13:03 Finished examples/opentheory/compilation                    1h28m00s  41GB
Nov 24 19:13:04 Starting examples/opentheory/compilation/proofs
Nov 24 19:15:04 Finished examples/opentheory/compilation/proofs                1m59s   3GB
Nov 24 19:15:04 Starting examples/opentheory/compilation/ag32
Nov 24 20:33:13 Finished examples/opentheory/compilation/ag32               1h18m08s  29GB
Nov 24 20:33:13 Starting examples/opentheory/compilation/ag32/proofs
Nov 24 20:36:50 Finished examples/opentheory/compilation/ag32/proofs           3m36s   5GB
Nov 24 20:36:50 Starting examples/sat_encodings
Nov 24 20:40:37 Finished examples/sat_encodings                                3m46s 790MB
Nov 24 20:40:37 Starting examples/sat_encodings/case_studies
Nov 24 20:44:10 Finished examples/sat_encodings/case_studies                   3m32s   1GB
Nov 24 20:44:10 Starting examples/sat_encodings/translation
Nov 24 20:56:01 Finished examples/sat_encodings/translation                   11m50s   4GB
Nov 24 20:56:01 Starting examples/sat_encodings/translation/compilation
Nov 24 22:20:19 Finished examples/sat_encodings/translation/compilation     1h24m17s  20GB
Nov 24 22:20:19 Starting examples/deflate
Nov 24 22:22:03 Finished examples/deflate                                      1m43s 807MB
Nov 24 22:22:04 Starting examples/deflate/translation
Nov 24 22:24:57 Finished examples/deflate/translation                          2m52s   3GB
Nov 24 22:24:57 Starting examples/deflate/translation/compilation
Nov 24 23:04:03 Finished examples/deflate/translation/compilation             39m05s  14GB
Nov 24 23:04:03 Starting translator/okasaki-examples
Nov 24 23:13:56 Finished translator/okasaki-examples                           9m52s   3GB
Nov 24 23:13:57 Starting translator/other-examples
Nov 24 23:15:21 Finished translator/other-examples                             1m24s   1GB
Nov 24 23:15:22 Starting compiler/parsing/tests
Nov 24 23:16:30 Finished compiler/parsing/tests                                1m08s 723MB
Nov 24 23:16:30 Starting compiler/inference/tests
Nov 24 23:33:22 Finished compiler/inference/tests                             16m51s   7GB
Nov 24 23:33:22 Starting compiler/printing/test
Nov 24 23:40:32 Finished compiler/printing/test                                7m09s   2GB
Nov 24 23:40:32 Starting floatingPoint/tools/flover
Nov 25 00:47:49 Finished floatingPoint/tools/flover                         1h07m16s   1GB
Nov 25 00:47:49 Starting floatingPoint/icing/
Nov 25 03:03:48 Finished floatingPoint/icing/                               2h15m58s   7GB
Nov 25 03:03:48 Starting floatingPoint/icing/examples
Nov 25 03:07:04 Finished floatingPoint/icing/examples                          3m15s   3GB
Nov 25 03:07:04 Starting floatingPoint/tools/dandelion
Nov 25 03:07:16 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                                                                                                                                                                                                (3s)FAIL<1>
 checking bison supports all required features... yes
 checking for pkg-config... pkg-config
 checking for dlopen in -lc... no
 checking for dlopen in -ldl... (cached) 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                                                                                                                                                                                        (5s)MKILLED
renameTheory                                                                                                                                                                                          (5s)MKILLED