Job 1937

CakeML:cb0e2ef96602bb903072c5e781bfe859a664a563
  Update perms_ok file for changes to QSORT in basis [Jun 22 06:48:54]
#891 (boot-trans)
Merging into:326efcaf26f0481002d76a507c159a04166d0232
  Another change caused by movement of real constants in HOL master [Jun 21 04:33:56]
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 22 12:30:10 Claimed job
Jun 22 12:30:16 Building HOL
Jun 22 12:41:26 Starting developers
Jun 22 12:41:30 Finished developers                                               4s  77MB
Jun 22 12:41:30 Starting developers/bin
Jun 22 12:41:37 Finished developers/bin                                           6s   1GB
Jun 22 12:41:37 Starting semantics/ffi
Jun 22 12:41:47 Finished semantics/ffi                                           10s 239MB
Jun 22 12:41:47 Starting semantics
Jun 22 12:44:26 Finished semantics                                             2m38s   1GB
Jun 22 12:44:26 Starting semantics/proofs
Jun 22 12:51:34 Finished semantics/proofs                                      7m07s   1GB
Jun 22 12:51:34 Starting semantics/alt_semantics
Jun 22 12:52:02 Finished semantics/alt_semantics                                 27s 606MB
Jun 22 12:52:02 Starting semantics/alt_semantics/proofs
Jun 22 13:03:22 Finished semantics/alt_semantics/proofs                       11m20s   1GB
Jun 22 13:03:23 Starting basis/pure
Jun 22 13:06:53 Finished basis/pure                                            3m30s   1GB
Jun 22 13:06:53 Starting translator
Jun 22 13:10:35 Finished translator                                            3m41s   1GB
Jun 22 13:10:35 Starting compiler/parsing
Jun 22 13:12:03 Finished compiler/parsing                                      1m28s   3GB
Jun 22 13:12:03 Starting characteristic
Jun 22 13:19:02 Finished characteristic                                        6m58s   1GB
Jun 22 13:19:02 Starting translator/monadic
Jun 22 13:21:04 Finished translator/monadic                                    2m01s   1GB
Jun 22 13:21:04 Starting basis
Jun 22 14:12:17 Finished basis                                                51m12s  25GB
Jun 22 14:12:17 Starting compiler/inference
Jun 22 14:13:56 Finished compiler/inference                                    1m38s   1GB
Jun 22 14:13:56 Starting compiler/backend/reg_alloc
Jun 22 14:15:41 Finished compiler/backend/reg_alloc                            1m44s   1GB
Jun 22 14:15:41 Starting compiler/backend/gc
Jun 22 14:20:14 Finished compiler/backend/gc                                   4m33s   2GB
Jun 22 14:20:14 Starting compiler/backend
Jun 22 14:26:13 Finished compiler/backend                                      5m58s   2GB
Jun 22 14:26:13 Starting compiler/encoders/asm
Jun 22 14:26:43 Finished compiler/encoders/asm                                   30s 695MB
Jun 22 14:26:44 Starting compiler/encoders/x64
Jun 22 14:27:52 Finished compiler/encoders/x64                                 1m08s 734MB
Jun 22 14:27:52 Starting compiler/encoders/arm7
Jun 22 14:30:01 Finished compiler/encoders/arm7                                2m09s   1GB
Jun 22 14:30:01 Starting compiler/encoders/arm8
Jun 22 14:30:44 Finished compiler/encoders/arm8                                  42s 829MB
Jun 22 14:30:44 Starting compiler/encoders/arm8_asl
Jun 22 16:48:43 Finished compiler/encoders/arm8_asl                         2h17m57s  32GB
Jun 22 16:48:43 Starting compiler/encoders/mips
Jun 22 16:50:15 Finished compiler/encoders/mips                                1m31s   1GB
Jun 22 16:50:15 Starting compiler/encoders/riscv
Jun 22 16:52:04 Finished compiler/encoders/riscv                               1m49s   1GB
Jun 22 16:52:05 Starting compiler/encoders/ag32
Jun 22 16:52:27 Finished compiler/encoders/ag32                                  21s   1GB
Jun 22 16:52:27 Starting compiler/backend/x64
Jun 22 16:52:50 Finished compiler/backend/x64                                    23s   1GB
Jun 22 16:52:50 Starting compiler/backend/arm7
Jun 22 16:53:15 Finished compiler/backend/arm7                                   24s   1GB
Jun 22 16:53:15 Starting compiler/backend/arm8
Jun 22 16:53:37 Finished compiler/backend/arm8                                   22s   1GB
Jun 22 16:53:37 Starting compiler/backend/mips
Jun 22 16:54:02 Finished compiler/backend/mips                                   24s   1GB
Jun 22 16:54:02 Starting compiler/backend/riscv
Jun 22 16:54:25 Finished compiler/backend/riscv                                  22s   1GB
Jun 22 16:54:25 Starting compiler/backend/ag32
Jun 22 16:55:51 Finished compiler/backend/ag32                                 1m26s   1GB
Jun 22 16:55:51 Starting compiler/parsing/proofs
Jun 22 16:59:37 Finished compiler/parsing/proofs                               3m45s   1GB
Jun 22 16:59:37 Starting compiler/inference/proofs
Jun 22 17:02:30 Finished compiler/inference/proofs                             2m52s   1GB
Jun 22 17:02:30 Starting compiler/backend/semantics
Jun 22 17:29:39 Finished compiler/backend/semantics                           27m08s   2GB
Jun 22 17:29:39 Starting compiler/backend/reg_alloc/proofs
Jun 22 17:33:19 Finished compiler/backend/reg_alloc/proofs                     3m40s   1GB
Jun 22 17:33:20 Starting compiler/backend/proofs
Jun 22 18:27:55 Finished compiler/backend/proofs                              54m33s  14GB
Jun 22 18:27:57 Starting compiler/backend/serialiser
Jun 22 18:29:40 Finished compiler/backend/serialiser                           1m42s   1GB
Jun 22 18:29:40 Starting compiler/encoders/x64/proofs
Jun 22 18:39:07 Finished compiler/encoders/x64/proofs                          9m26s   5GB
Jun 22 18:39:07 Starting compiler/encoders/arm7/proofs
Jun 22 18:52:29 Finished compiler/encoders/arm7/proofs                        13m21s   3GB
Jun 22 18:52:29 Starting compiler/encoders/arm8/proofs
Jun 22 18:59:19 Finished compiler/encoders/arm8/proofs                         6m50s   1GB
Jun 22 18:59:19 Starting compiler/encoders/arm8_asl/proofs
Jun 22 19:50:02 Finished compiler/encoders/arm8_asl/proofs                    50m40s   7GB
Jun 22 19:50:02 Starting compiler/encoders/mips/proofs
Jun 22 20:00:02 Finished compiler/encoders/mips/proofs                        10m00s   2GB
Jun 22 20:00:02 Starting compiler/encoders/riscv/proofs
Jun 22 20:08:50 Finished compiler/encoders/riscv/proofs                        8m48s   1GB
Jun 22 20:08:51 Starting compiler/encoders/ag32/proofs
Jun 22 20:11:28 Finished compiler/encoders/ag32/proofs                         2m36s 718MB
Jun 22 20:11:28 Starting compiler/backend/x64/proofs
Jun 22 20:11:56 Finished compiler/backend/x64/proofs                             28s   1GB
Jun 22 20:11:56 Starting compiler/backend/arm7/proofs
Jun 22 20:12:26 Finished compiler/backend/arm7/proofs                            29s   1GB
Jun 22 20:12:26 Starting compiler/backend/arm8/proofs
Jun 22 20:12:55 Finished compiler/backend/arm8/proofs                            29s   1GB
Jun 22 20:12:55 Starting compiler/backend/arm8_asl
Jun 22 20:13:20 Finished compiler/backend/arm8_asl                               24s   1GB
Jun 22 20:13:20 Starting compiler/backend/mips/proofs
Jun 22 20:13:49 Finished compiler/backend/mips/proofs                            28s   1GB
Jun 22 20:13:49 Starting compiler/backend/riscv/proofs
Jun 22 20:14:18 Finished compiler/backend/riscv/proofs                           28s   1GB
Jun 22 20:14:18 Starting compiler/backend/ag32/proofs
Jun 22 20:28:11 Finished compiler/backend/ag32/proofs                         13m52s   2GB
Jun 22 20:28:11 Starting compiler/proofs
Jun 22 20:30:39 Finished compiler/proofs                                       2m28s   3GB
Jun 22 20:30:40 Starting candle/set-theory
Jun 22 20:31:14 Finished candle/set-theory                                       34s 959MB
Jun 22 20:31:15 Starting candle/syntax-lib
Jun 22 20:31:28 Finished candle/syntax-lib                                       13s 655MB
Jun 22 20:31:28 Starting candle/standard/syntax
Jun 22 20:33:32 Finished candle/standard/syntax                                2m04s   1GB
Jun 22 20:33:32 Starting candle/standard/semantics
Jun 22 20:35:22 Finished candle/standard/semantics                             1m50s 956MB
Jun 22 20:35:23 Starting candle/standard/monadic
Jun 22 20:37:16 Finished candle/standard/monadic                               1m52s   1GB
Jun 22 20:37:16 Starting candle/standard/ml_kernel
Jun 22 20:43:50 Finished candle/standard/ml_kernel                             6m34s   3GB
Jun 22 20:43:50 Starting candle/overloading/syntax
Jun 22 20:47:01 Finished candle/overloading/syntax                             3m10s   1GB
Jun 22 20:47:01 Starting candle/overloading/semantics
Jun 22 20:58:50 Finished candle/overloading/semantics                         11m47s   2GB
Jun 22 20:58:50 Starting candle/overloading/monadic
Jun 22 21:01:28 Finished candle/overloading/monadic                            2m37s   1GB
Jun 22 21:01:28 Starting candle/overloading/ml_kernel
Jun 22 21:08:56 Finished candle/overloading/ml_kernel                          7m28s   3GB
Jun 22 21:08:56 Starting candle/overloading/ml_checker
Jun 22 21:11:21 Finished candle/overloading/ml_checker                         2m24s   3GB
Jun 22 21:11:21 Starting candle/prover
Jun 22 21:22:13 Finished candle/prover                                        10m51s   3GB
Jun 22 21:22:13 Starting pancake
Jun 22 21:26:06 Finished pancake                                               3m52s   4GB
Jun 22 21:26:06 Starting pancake/ffi
Jun 22 21:26:06 Finished pancake/ffi                                              0s  35MB
Jun 22 21:26:06 Starting pancake/semantics
Jun 22 21:28:37 Finished pancake/semantics                                     2m30s   1GB
Jun 22 21:28:37 Starting pancake/proofs
Jun 22 21:40:43 Finished pancake/proofs                                       12m05s   7GB
Jun 22 21:40:43 Starting characteristic/examples
Jun 22 21:42:07 Finished characteristic/examples                               1m23s   2GB
Jun 22 21:42:07 Starting tutorial/solutions
Jun 22 21:58:21 Finished tutorial/solutions                                   16m14s   8GB
Jun 22 21:58:21 Starting translator/monadic/examples
Jun 22 22:02:18 Finished translator/monadic/examples                           3m54s   2GB
Jun 22 22:02:19 Starting examples
Jun 22 22:12:18 Finished examples                                              9m59s   3GB
Jun 22 22:12:18 Starting examples/compilation/x64
Jun 23 00:16:09 Finished examples/compilation/x64                           2h03m49s  13GB
Jun 23 00:16:09 Starting examples/compilation/x64/proofs
Jun 23 00:18:23 Finished examples/compilation/x64/proofs                       2m13s   3GB
Jun 23 00:18:23 Starting examples/compilation/ag32
Jun 23 00:51:07 Finished examples/compilation/ag32                            32m43s   8GB
Jun 23 00:51:07 Starting examples/compilation/ag32/proofs
Jun 23 00:52:02 Finished examples/compilation/ag32/proofs                        54s   3GB
Jun 23 00:52:02 Starting examples/lpr_checker
Jun 23 00:53:04 Finished examples/lpr_checker                                  1m02s   1GB
Jun 23 00:53:05 Starting examples/lpr_checker/array
Jun 23 01:25:29 Finished examples/lpr_checker/array                           32m22s   6GB
Jun 23 01:25:30 Starting examples/lpr_checker/array/compilation
Jun 23 02:04:50 Finished examples/lpr_checker/array/compilation               39m20s  24GB
Jun 23 02:04:51 Starting examples/lpr_checker/array/compilation/proofs
Jun 23 02:06:13 Finished examples/lpr_checker/array/compilation/proofs         1m22s   5GB
Jun 23 02:06:14 Starting examples/opentheory
Jun 23 02:16:50 Finished examples/opentheory                                  10m36s   6GB
Jun 23 02:16:50 Starting examples/opentheory
Jun 23 02:16:51 Finished examples/opentheory                                      1s 132MB
Jun 23 02:16:51 Starting examples/opentheory/compilation
Jun 23 02:53:27 Finished examples/opentheory/compilation                      36m35s  29GB
Jun 23 02:53:28 Starting examples/opentheory/compilation/proofs
Jun 23 02:54:22 Finished examples/opentheory/compilation/proofs                  54s   4GB
Jun 23 02:54:22 Starting examples/opentheory/compilation/ag32
Jun 23 03:29:26 Finished examples/opentheory/compilation/ag32                 35m04s  29GB
Jun 23 03:29:27 Starting examples/opentheory/compilation/ag32/proofs
Jun 23 03:31:14 Finished examples/opentheory/compilation/ag32/proofs           1m47s   6GB
Jun 23 03:31:14 Starting examples/sat_encodings
Jun 23 03:33:17 Finished examples/sat_encodings                                2m02s 900MB
Jun 23 03:33:17 Starting examples/sat_encodings/case_studies
Jun 23 03:35:00 Finished examples/sat_encodings/case_studies                   1m42s 735MB
Jun 23 03:35:00 Starting examples/sat_encodings/translation
Jun 23 03:40:46 Finished examples/sat_encodings/translation                    5m46s   3GB
Jun 23 03:40:47 Starting examples/sat_encodings/translation/compilation
Jun 23 04:27:28 Finished examples/sat_encodings/translation/compilation       46m39s  17GB
Jun 23 04:27:28 Starting examples/deflate
Jun 23 04:28:26 Finished examples/deflate                                        58s 742MB
Jun 23 04:28:26 Starting examples/deflate/translation
Jun 23 04:29:59 Finished examples/deflate/translation                          1m33s   2GB
Jun 23 04:30:00 Starting examples/deflate/translation/compilation
Jun 23 04:50:36 Finished examples/deflate/translation/compilation             20m36s  12GB
Jun 23 04:50:36 Starting translator/okasaki-examples
Jun 23 04:55:42 Finished translator/okasaki-examples                           5m05s   2GB
Jun 23 04:55:42 Starting translator/other-examples
Jun 23 04:58:04 Finished translator/other-examples                             2m22s   1GB
Jun 23 04:58:04 Starting compiler/parsing/tests
Jun 23 04:58:34 Finished compiler/parsing/tests                                  29s 539MB
Jun 23 04:58:34 Starting compiler/inference/tests
Jun 23 05:07:05 Finished compiler/inference/tests                              8m31s   3GB
Jun 23 05:07:06 Starting compiler/printing/test
Jun 23 05:10:57 Finished compiler/printing/test                                3m51s   3GB
Jun 23 05:10:57 Starting icing/flover
Jun 23 05:11:14 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  (6s)     OK
RealSimpsTheory                                                                         icing/flover/Infra (14s)FAIL<1>
 <<HOL message: Created theory "RealSimps">>
 error in quse /home/cug/hk324/cml-regression/cakeml-1937/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-1937/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