Job 1941

CakeML:099c12cd5cc72f05c5be3d73a4a72a8c7f076e54
  Fixes for name change abs_1_v --> abs_v [Jun 22 21:13:52]
#892 (double-type-new)
Merging into:3edf3dfb5230ae6668e0082093cc00b303838e59
  Merge pull request #884 from CakeML/let-lift [Jun 22 20:28:35]
HOL:3810cf53c6050c5b2748cb042415145bd842957f
  Make parsing in RealField properly independent of context [Jun 21 00:55:21]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jun 23 05:11:15 Claimed job
Jun 23 05:11:17 Reusing HOL
Jun 23 05:11:31 Starting developers
Jun 23 05:11:36 Finished developers                                               4s 142MB
Jun 23 05:11:36 Starting developers/bin
Jun 23 05:11:42 Finished developers/bin                                           6s   1GB
Jun 23 05:11:42 Starting semantics/ffi
Jun 23 05:11:52 Finished semantics/ffi                                            9s 236MB
Jun 23 05:11:52 Starting semantics
Jun 23 05:14:21 Finished semantics                                             2m28s   1GB
Jun 23 05:14:21 Starting semantics/proofs
Jun 23 05:21:18 Finished semantics/proofs                                      6m57s   1GB
Jun 23 05:21:18 Starting semantics/alt_semantics
Jun 23 05:21:46 Finished semantics/alt_semantics                                 27s 581MB
Jun 23 05:21:46 Starting semantics/alt_semantics/proofs
Jun 23 05:33:18 Finished semantics/alt_semantics/proofs                       11m30s   1GB
Jun 23 05:33:18 Starting basis/pure
Jun 23 05:34:25 Finished basis/pure                                            1m06s 980MB
Jun 23 05:34:25 Starting translator
Jun 23 05:38:05 Finished translator                                            3m40s   1GB
Jun 23 05:38:05 Starting compiler/parsing
Jun 23 05:39:28 Finished compiler/parsing                                      1m22s   3GB
Jun 23 05:39:28 Starting characteristic
Jun 23 05:46:31 Finished characteristic                                        7m03s   2GB
Jun 23 05:46:31 Starting translator/monadic
Jun 23 05:48:34 Finished translator/monadic                                    2m01s   1GB
Jun 23 05:48:34 Starting basis
Jun 23 06:39:58 Finished basis                                                51m21s  11GB
Jun 23 06:39:58 Starting compiler/inference
Jun 23 06:41:30 Finished compiler/inference                                    1m31s   1GB
Jun 23 06:41:30 Starting compiler/backend/reg_alloc
Jun 23 06:43:15 Finished compiler/backend/reg_alloc                            1m45s   1GB
Jun 23 06:43:15 Starting compiler/backend/gc
Jun 23 06:47:45 Finished compiler/backend/gc                                   4m29s   1GB
Jun 23 06:47:45 Starting compiler/backend
Jun 23 06:53:59 Finished compiler/backend                                      6m13s   3GB
Jun 23 06:53:59 Starting compiler/encoders/asm
Jun 23 06:54:30 Finished compiler/encoders/asm                                   30s 718MB
Jun 23 06:54:30 Starting compiler/encoders/x64
Jun 23 06:55:00 Finished compiler/encoders/x64                                   29s   1GB
Jun 23 06:55:00 Starting compiler/encoders/arm7
Jun 23 06:55:59 Finished compiler/encoders/arm7                                  59s 861MB
Jun 23 06:55:59 Starting compiler/encoders/arm8
Jun 23 06:56:17 Finished compiler/encoders/arm8                                  17s 773MB
Jun 23 06:56:17 Starting compiler/encoders/arm8_asl
Jun 23 06:58:54 Finished compiler/encoders/arm8_asl                            2m37s 944MB
Jun 23 06:58:55 Starting compiler/encoders/mips
Jun 23 06:59:16 Finished compiler/encoders/mips                                  21s   1GB
Jun 23 06:59:16 Starting compiler/encoders/riscv
Jun 23 06:59:36 Finished compiler/encoders/riscv                                 19s 898MB
Jun 23 06:59:36 Starting compiler/encoders/ag32
Jun 23 06:59:58 Finished compiler/encoders/ag32                                  21s 750MB
Jun 23 06:59:58 Starting compiler/backend/x64
Jun 23 07:00:21 Finished compiler/backend/x64                                    22s   1GB
Jun 23 07:00:21 Starting compiler/backend/arm7
Jun 23 07:00:45 Finished compiler/backend/arm7                                   23s   1GB
Jun 23 07:00:45 Starting compiler/backend/arm8
Jun 23 07:01:08 Finished compiler/backend/arm8                                   23s   1GB
Jun 23 07:01:09 Starting compiler/backend/mips
Jun 23 07:01:32 Finished compiler/backend/mips                                   23s   1GB
Jun 23 07:01:33 Starting compiler/backend/riscv
Jun 23 07:01:57 Finished compiler/backend/riscv                                  24s   1GB
Jun 23 07:01:57 Starting compiler/backend/ag32
Jun 23 07:03:21 Finished compiler/backend/ag32                                 1m23s   1GB
Jun 23 07:03:21 Starting compiler/parsing/proofs
Jun 23 07:07:07 Finished compiler/parsing/proofs                               3m45s   1GB
Jun 23 07:07:07 Starting compiler/inference/proofs
Jun 23 07:09:53 Finished compiler/inference/proofs                             2m45s   1GB
Jun 23 07:09:53 Starting compiler/backend/semantics
Jun 23 07:35:59 Finished compiler/backend/semantics                           26m06s   2GB
Jun 23 07:35:59 Starting compiler/backend/reg_alloc/proofs
Jun 23 07:39:33 Finished compiler/backend/reg_alloc/proofs                     3m33s 873MB
Jun 23 07:39:33 Starting compiler/backend/proofs
Jun 23 08:34:50 Finished compiler/backend/proofs                              55m15s  24GB
Jun 23 08:34:50 Starting compiler/backend/serialiser
Jun 23 08:36:33 Finished compiler/backend/serialiser                           1m43s   1GB
Jun 23 08:36:33 Starting compiler/encoders/x64/proofs
Jun 23 08:46:00 Finished compiler/encoders/x64/proofs                          9m26s   5GB
Jun 23 08:46:00 Starting compiler/encoders/arm7/proofs
Jun 23 08:59:19 Finished compiler/encoders/arm7/proofs                        13m18s   4GB
Jun 23 08:59:19 Starting compiler/encoders/arm8/proofs
Jun 23 09:06:02 Finished compiler/encoders/arm8/proofs                         6m42s   1GB
Jun 23 09:06:02 Starting compiler/encoders/arm8_asl/proofs
Jun 23 09:21:13 Finished compiler/encoders/arm8_asl/proofs                    15m11s   2GB
Jun 23 09:21:13 Starting compiler/encoders/mips/proofs
Jun 23 09:31:27 Finished compiler/encoders/mips/proofs                        10m13s   2GB
Jun 23 09:31:27 Starting compiler/encoders/riscv/proofs
Jun 23 09:40:18 Finished compiler/encoders/riscv/proofs                        8m49s   1GB
Jun 23 09:40:18 Starting compiler/encoders/ag32/proofs
Jun 23 09:42:54 Finished compiler/encoders/ag32/proofs                         2m35s 740MB
Jun 23 09:42:54 Starting compiler/backend/x64/proofs
Jun 23 09:43:24 Finished compiler/backend/x64/proofs                             29s   1GB
Jun 23 09:43:24 Starting compiler/backend/arm7/proofs
Jun 23 09:43:53 Finished compiler/backend/arm7/proofs                            29s   1GB
Jun 23 09:43:54 Starting compiler/backend/arm8/proofs
Jun 23 09:44:22 Finished compiler/backend/arm8/proofs                            28s   1GB
Jun 23 09:44:22 Starting compiler/backend/arm8_asl
Jun 23 09:44:45 Finished compiler/backend/arm8_asl                               22s   1GB
Jun 23 09:44:45 Starting compiler/backend/mips/proofs
Jun 23 09:45:14 Finished compiler/backend/mips/proofs                            29s   2GB
Jun 23 09:45:15 Starting compiler/backend/riscv/proofs
Jun 23 09:45:44 Finished compiler/backend/riscv/proofs                           28s   1GB
Jun 23 09:45:44 Starting compiler/backend/ag32/proofs
Jun 23 09:59:19 Finished compiler/backend/ag32/proofs                         13m34s   2GB
Jun 23 09:59:19 Starting compiler/proofs
Jun 23 10:01:31 Finished compiler/proofs                                       2m12s   3GB
Jun 23 10:01:31 Starting candle/set-theory
Jun 23 10:02:06 Finished candle/set-theory                                       35s   1GB
Jun 23 10:02:07 Starting candle/syntax-lib
Jun 23 10:02:20 Finished candle/syntax-lib                                       13s 614MB
Jun 23 10:02:20 Starting candle/standard/syntax
Jun 23 10:04:24 Finished candle/standard/syntax                                2m03s   1GB
Jun 23 10:04:24 Starting candle/standard/semantics
Jun 23 10:06:14 Finished candle/standard/semantics                             1m50s   1GB
Jun 23 10:06:15 Starting candle/standard/monadic
Jun 23 10:08:11 Finished candle/standard/monadic                               1m56s   1GB
Jun 23 10:08:11 Starting candle/standard/ml_kernel
Jun 23 10:14:35 Finished candle/standard/ml_kernel                             6m23s   2GB
Jun 23 10:14:35 Starting candle/overloading/syntax
Jun 23 10:17:46 Finished candle/overloading/syntax                             3m10s   1GB
Jun 23 10:17:46 Starting candle/overloading/semantics
Jun 23 10:29:40 Finished candle/overloading/semantics                         11m53s   2GB
Jun 23 10:29:40 Starting candle/overloading/monadic
Jun 23 10:32:17 Finished candle/overloading/monadic                            2m36s   1GB
Jun 23 10:32:17 Starting candle/overloading/ml_kernel
Jun 23 10:39:51 Finished candle/overloading/ml_kernel                          7m34s   3GB
Jun 23 10:39:52 Starting candle/overloading/ml_checker
Jun 23 10:42:18 Finished candle/overloading/ml_checker                         2m23s   2GB
Jun 23 10:42:18 Starting candle/prover
Jun 23 10:53:00 Finished candle/prover                                        10m41s   2GB
Jun 23 10:53:00 Starting pancake
Jun 23 10:56:53 Finished pancake                                               3m52s   4GB
Jun 23 10:56:53 Starting pancake/ffi
Jun 23 10:56:53 Finished pancake/ffi                                              0s  35MB
Jun 23 10:56:53 Starting pancake/semantics
Jun 23 10:59:25 Finished pancake/semantics                                     2m31s   1GB
Jun 23 10:59:25 Starting pancake/proofs
Jun 23 11:11:17 Finished pancake/proofs                                       11m51s   6GB
Jun 23 11:11:17 Starting characteristic/examples
Jun 23 11:12:43 Finished characteristic/examples                               1m26s   2GB
Jun 23 11:12:43 Starting tutorial/solutions
Jun 23 11:28:35 Finished tutorial/solutions                                   15m51s  10GB
Jun 23 11:28:35 Starting translator/monadic/examples
Jun 23 11:32:34 Finished translator/monadic/examples                           3m59s   2GB
Jun 23 11:32:34 Starting examples
Jun 23 11:42:14 Finished examples                                              9m39s   3GB
Jun 23 11:42:14 Starting examples/compilation/x64
Jun 23 13:45:49 Finished examples/compilation/x64                           2h03m32s  17GB
Jun 23 13:45:49 Starting examples/compilation/x64/proofs
Jun 23 13:48:23 Finished examples/compilation/x64/proofs                       2m33s   2GB
Jun 23 13:48:23 Starting examples/compilation/ag32
Jun 23 14:21:33 Finished examples/compilation/ag32                            33m09s   8GB
Jun 23 14:21:33 Starting examples/compilation/ag32/proofs
Jun 23 14:22:29 Finished examples/compilation/ag32/proofs                        55s   2GB
Jun 23 14:22:29 Starting examples/lpr_checker
Jun 23 14:23:32 Finished examples/lpr_checker                                  1m02s   1GB
Jun 23 14:23:32 Starting examples/lpr_checker/array
Jun 23 14:56:23 Finished examples/lpr_checker/array                           32m50s   5GB
Jun 23 14:56:23 Starting examples/lpr_checker/array/compilation
Jun 23 15:34:49 Finished examples/lpr_checker/array/compilation               38m25s  23GB
Jun 23 15:34:49 Starting examples/lpr_checker/array/compilation/proofs
Jun 23 15:36:15 Finished examples/lpr_checker/array/compilation/proofs         1m25s   6GB
Jun 23 15:36:15 Starting examples/opentheory
Jun 23 15:46:38 Finished examples/opentheory                                  10m22s   4GB
Jun 23 15:46:38 Starting examples/opentheory
Jun 23 15:46:39 Finished examples/opentheory                                      1s 132MB
Jun 23 15:46:39 Starting examples/opentheory/compilation
Jun 23 16:24:34 Finished examples/opentheory/compilation                      37m53s  30GB
Jun 23 16:24:34 Starting examples/opentheory/compilation/proofs
Jun 23 16:25:29 Finished examples/opentheory/compilation/proofs                  54s   4GB
Jun 23 16:25:29 Starting examples/opentheory/compilation/ag32
Jun 23 16:59:52 Finished examples/opentheory/compilation/ag32                 34m22s  27GB
Jun 23 16:59:52 Starting examples/opentheory/compilation/ag32/proofs
Jun 23 17:02:16 Finished examples/opentheory/compilation/ag32/proofs           2m24s   7GB
Jun 23 17:02:17 Starting examples/sat_encodings
Jun 23 17:04:18 Finished examples/sat_encodings                                2m01s   1GB
Jun 23 17:04:18 Starting examples/sat_encodings/case_studies
Jun 23 17:06:00 Finished examples/sat_encodings/case_studies                   1m41s 787MB
Jun 23 17:06:00 Starting examples/sat_encodings/translation
Jun 23 17:11:49 Finished examples/sat_encodings/translation                    5m48s   5GB
Jun 23 17:11:49 Starting examples/sat_encodings/translation/compilation
Jun 23 17:58:25 Finished examples/sat_encodings/translation/compilation       46m35s  18GB
Jun 23 17:58:25 Starting examples/deflate
Jun 23 17:59:24 Finished examples/deflate                                        58s 882MB
Jun 23 17:59:24 Starting examples/deflate/translation
Jun 23 18:00:58 Finished examples/deflate/translation                          1m33s   3GB
Jun 23 18:00:58 Starting examples/deflate/translation/compilation
Jun 23 18:21:57 Finished examples/deflate/translation/compilation             20m58s  11GB
Jun 23 18:21:57 Starting translator/okasaki-examples
Jun 23 18:26:57 Finished translator/okasaki-examples                           4m59s   3GB
Jun 23 18:26:57 Starting translator/other-examples
Jun 23 18:27:47 Finished translator/other-examples                               49s   1GB
Jun 23 18:27:47 Starting compiler/parsing/tests
Jun 23 18:28:17 Finished compiler/parsing/tests                                  29s 583MB
Jun 23 18:28:17 Starting compiler/inference/tests
Jun 23 18:36:42 Finished compiler/inference/tests                              8m24s   5GB
Jun 23 18:36:42 Starting compiler/printing/test
Jun 23 18:40:25 Finished compiler/printing/test                                3m43s   3GB
Jun 23 18:40:26 Starting icing/flover
Jun 23 18:40:42 FAILED: icing/flover
Scanning [1m$(CAKEMLDIR)/icing/flover/semantics[0m
Scanned 3 directories
Starting work on RealSimpsTheory
Starting work on ResultsTheory
Starting work on sqrtApproxTheory
Starting work on README.md
README.md                                                                                     icing/flover  (0s)     OK
ResultsTheory                                                                           icing/flover/Infra  (7s)     OK
RealSimpsTheory                                                                         icing/flover/Infra (14s)FAIL<1>
 <<HOL message: Created theory "RealSimps">>
 error in quse /home/cug/hk324/cml-regression/cakeml-1941/icing/flover/Infra/RealSimpsScript.sml : HOL_ERR {message = "\"abs\" not found in theory \"real\"", origin_function = "prim_mk_const", origin_structure = "Term"}
 error in load /home/cug/hk324/cml-regression/cakeml-1941/icing/flover/Infra/RealSimpsScript : HOL_ERR {message = "\"abs\" not found in theory \"real\"", origin_function = "prim_mk_const", origin_structure = "Term"}
 Uncaught exception: HOL_ERR {message = "\"abs\" not found in theory \"real\"", origin_function = "prim_mk_const", origin_structure = "Term"}
sqrtApproxTheory                                                                              icing/flover (15s)MKILLED