Job 1987

CakeML:e1a091a98456edccc763187c818c3e290eb52abb
  Fix some parsing issues [Sep 14 20:27:21]
#908 (common-sub-exp-elim)
Merging into:8f9eeb4f6d657077aca5ed92c7f20bd8c35befef
  Remove failing diminish_srw_ss [Sep 16 18:41:10]
HOL:893dead4b6f59a9be7fc251533d0a5ee77e12e56
  Add some simple test for bitArithLib and document in next-release.md [Sep 15 04:32:27]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Sep 17 04:04:46 Claimed job
Sep 17 04:04:52 Building HOL
Sep 17 04:16:05 Starting developers
Sep 17 04:16:10 Finished developers                                               4s  71MB
Sep 17 04:16:10 Starting developers/bin
Sep 17 04:16:16 Finished developers/bin                                           6s   1GB
Sep 17 04:16:17 Starting semantics/ffi
Sep 17 04:16:25 Finished semantics/ffi                                            8s 231MB
Sep 17 04:16:26 Starting semantics
Sep 17 04:18:57 Finished semantics                                             2m31s   1GB
Sep 17 04:18:58 Starting semantics/proofs
Sep 17 04:26:08 Finished semantics/proofs                                      7m10s   1GB
Sep 17 04:26:08 Starting semantics/alt_semantics
Sep 17 04:26:34 Finished semantics/alt_semantics                                 25s 558MB
Sep 17 04:26:35 Starting semantics/alt_semantics/proofs
Sep 17 04:38:17 Finished semantics/alt_semantics/proofs                       11m42s   1GB
Sep 17 04:38:17 Starting basis/pure
Sep 17 04:41:49 Finished basis/pure                                            3m32s 940MB
Sep 17 04:41:50 Starting translator
Sep 17 04:45:26 Finished translator                                            3m36s   2GB
Sep 17 04:45:26 Starting compiler/parsing
Sep 17 04:46:54 Finished compiler/parsing                                      1m28s   3GB
Sep 17 04:46:55 Starting characteristic
Sep 17 04:53:46 Finished characteristic                                        6m51s   1GB
Sep 17 04:53:46 Starting translator/monadic
Sep 17 04:55:46 Finished translator/monadic                                    1m59s   2GB
Sep 17 04:55:46 Starting basis
Sep 17 05:47:34 Finished basis                                                51m46s  13GB
Sep 17 05:47:34 Starting compiler/inference
Sep 17 05:49:12 Finished compiler/inference                                    1m38s   1GB
Sep 17 05:49:12 Starting compiler/backend/reg_alloc
Sep 17 05:50:57 Finished compiler/backend/reg_alloc                            1m44s   1GB
Sep 17 05:50:57 Starting compiler/backend/gc
Sep 17 05:55:16 Finished compiler/backend/gc                                   4m19s   1GB
Sep 17 05:55:16 Starting compiler/backend
Sep 17 06:00:53 Finished compiler/backend                                      5m36s   2GB
Sep 17 06:00:53 Starting compiler/encoders/asm
Sep 17 06:01:23 Finished compiler/encoders/asm                                   29s 882MB
Sep 17 06:01:23 Starting compiler/encoders/x64
Sep 17 06:02:30 Finished compiler/encoders/x64                                 1m07s 737MB
Sep 17 06:02:30 Starting compiler/encoders/arm7
Sep 17 06:04:34 Finished compiler/encoders/arm7                                2m03s   1GB
Sep 17 06:04:35 Starting compiler/encoders/arm8
Sep 17 06:05:16 Finished compiler/encoders/arm8                                  41s   1GB
Sep 17 06:05:17 Starting compiler/encoders/arm8_asl
Sep 17 08:22:46 Finished compiler/encoders/arm8_asl                         2h17m28s  25GB
Sep 17 08:22:46 Starting compiler/encoders/mips
Sep 17 08:24:18 Finished compiler/encoders/mips                                1m31s   1GB
Sep 17 08:24:18 Starting compiler/encoders/riscv
Sep 17 08:26:07 Finished compiler/encoders/riscv                               1m48s 876MB
Sep 17 08:26:07 Starting compiler/encoders/ag32
Sep 17 08:26:27 Finished compiler/encoders/ag32                                  20s 614MB
Sep 17 08:26:28 Starting compiler/backend/x64
Sep 17 08:26:48 Finished compiler/backend/x64                                    20s   1GB
Sep 17 08:26:49 Starting compiler/backend/arm7
Sep 17 08:27:12 Finished compiler/backend/arm7                                   23s   1GB
Sep 17 08:27:12 Starting compiler/backend/arm8
Sep 17 08:27:33 Finished compiler/backend/arm8                                   21s   1GB
Sep 17 08:27:33 Starting compiler/backend/mips
Sep 17 08:27:54 Finished compiler/backend/mips                                   20s   1GB
Sep 17 08:27:55 Starting compiler/backend/riscv
Sep 17 08:28:16 Finished compiler/backend/riscv                                  21s   1GB
Sep 17 08:28:16 Starting compiler/backend/ag32
Sep 17 08:29:42 Finished compiler/backend/ag32                                 1m26s   1GB
Sep 17 08:29:42 Starting compiler/parsing/proofs
Sep 17 08:33:29 Finished compiler/parsing/proofs                               3m46s   1GB
Sep 17 08:33:29 Starting compiler/inference/proofs
Sep 17 08:36:09 Finished compiler/inference/proofs                             2m40s   1GB
Sep 17 08:36:10 Starting compiler/backend/semantics
Sep 17 09:02:19 Finished compiler/backend/semantics                           26m09s   1GB
Sep 17 09:02:19 Starting compiler/backend/reg_alloc/proofs
Sep 17 09:05:51 Finished compiler/backend/reg_alloc/proofs                     3m32s   1GB
Sep 17 09:05:52 Starting compiler/backend/proofs
Sep 17 10:01:59 Finished compiler/backend/proofs                              56m06s  24GB
Sep 17 10:01:59 Starting compiler/backend/serialiser
Sep 17 10:03:29 Finished compiler/backend/serialiser                           1m30s   1GB
Sep 17 10:03:29 Starting compiler/encoders/x64/proofs
Sep 17 10:13:21 Finished compiler/encoders/x64/proofs                          9m52s   4GB
Sep 17 10:13:22 Starting compiler/encoders/arm7/proofs
Sep 17 10:27:01 Finished compiler/encoders/arm7/proofs                        13m39s   3GB
Sep 17 10:27:01 Starting compiler/encoders/arm8/proofs
Sep 17 10:34:01 Finished compiler/encoders/arm8/proofs                         7m00s   1GB
Sep 17 10:34:02 Starting compiler/encoders/arm8_asl/proofs
Sep 17 11:24:52 Finished compiler/encoders/arm8_asl/proofs                    50m49s   5GB
Sep 17 11:24:53 Starting compiler/encoders/mips/proofs
Sep 17 11:35:29 Finished compiler/encoders/mips/proofs                        10m36s   2GB
Sep 17 11:35:29 Starting compiler/encoders/riscv/proofs
Sep 17 11:44:31 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Sep 17 11:44:31 Starting compiler/encoders/ag32/proofs
Sep 17 11:47:11 Finished compiler/encoders/ag32/proofs                         2m39s 850MB
Sep 17 11:47:11 Starting compiler/backend/x64/proofs
Sep 17 11:47:36 Finished compiler/backend/x64/proofs                             24s   1GB
Sep 17 11:47:36 Starting compiler/backend/arm7/proofs
Sep 17 11:48:03 Finished compiler/backend/arm7/proofs                            26s   2GB
Sep 17 11:48:03 Starting compiler/backend/arm8/proofs
Sep 17 11:48:29 Finished compiler/backend/arm8/proofs                            25s   1GB
Sep 17 11:48:29 Starting compiler/backend/arm8_asl
Sep 17 11:48:49 Finished compiler/backend/arm8_asl                               19s   1GB
Sep 17 11:48:49 Starting compiler/backend/mips/proofs
Sep 17 11:49:13 Finished compiler/backend/mips/proofs                            24s   1GB
Sep 17 11:49:14 Starting compiler/backend/riscv/proofs
Sep 17 11:49:39 Finished compiler/backend/riscv/proofs                           25s   1GB
Sep 17 11:49:39 Starting compiler/backend/ag32/proofs
Sep 17 12:02:57 Finished compiler/backend/ag32/proofs                         13m17s   3GB
Sep 17 12:02:57 Starting compiler/proofs
Sep 17 12:05:17 Finished compiler/proofs                                       2m19s   3GB
Sep 17 12:05:17 Starting candle/set-theory
Sep 17 12:05:51 Finished candle/set-theory                                       33s   1GB
Sep 17 12:05:51 Starting candle/syntax-lib
Sep 17 12:06:04 Finished candle/syntax-lib                                       12s 639MB
Sep 17 12:06:04 Starting candle/standard/syntax
Sep 17 12:08:04 Finished candle/standard/syntax                                1m59s   1GB
Sep 17 12:08:04 Starting candle/standard/semantics
Sep 17 12:09:49 Finished candle/standard/semantics                             1m44s   1GB
Sep 17 12:09:49 Starting candle/standard/monadic
Sep 17 12:11:43 Finished candle/standard/monadic                               1m53s   1GB
Sep 17 12:11:43 Starting candle/standard/ml_kernel
Sep 17 12:18:20 Finished candle/standard/ml_kernel                             6m36s   2GB
Sep 17 12:18:20 Starting candle/overloading/syntax
Sep 17 12:21:31 Finished candle/overloading/syntax                             3m10s   1GB
Sep 17 12:21:31 Starting candle/overloading/semantics
Sep 17 12:33:31 Finished candle/overloading/semantics                         11m58s   2GB
Sep 17 12:33:31 Starting candle/overloading/monadic
Sep 17 12:36:06 Finished candle/overloading/monadic                            2m34s   1GB
Sep 17 12:36:06 Starting candle/overloading/ml_kernel
Sep 17 12:43:25 Finished candle/overloading/ml_kernel                          7m18s   3GB
Sep 17 12:43:25 Starting candle/overloading/ml_checker
Sep 17 12:45:54 Finished candle/overloading/ml_checker                         2m29s   2GB
Sep 17 12:45:54 Starting candle/prover
Sep 17 13:01:06 Finished candle/prover                                        15m11s   4GB
Sep 17 13:01:06 Starting pancake
Sep 17 13:04:09 Finished pancake                                               3m02s   3GB
Sep 17 13:04:09 Starting pancake/ffi
Sep 17 13:04:09 Finished pancake/ffi                                              0s  25MB
Sep 17 13:04:09 Starting pancake/semantics
Sep 17 13:06:32 Finished pancake/semantics                                     2m22s   1GB
Sep 17 13:06:32 Starting pancake/proofs
Sep 17 13:18:42 Finished pancake/proofs                                       12m09s   6GB
Sep 17 13:18:42 Starting characteristic/examples
Sep 17 13:20:08 Finished characteristic/examples                               1m26s   3GB
Sep 17 13:20:08 Starting tutorial/solutions
Sep 17 13:36:11 Finished tutorial/solutions                                   16m01s   9GB
Sep 17 13:36:11 Starting translator/monadic/examples
Sep 17 13:39:57 Finished translator/monadic/examples                           3m45s   2GB
Sep 17 13:39:57 Starting examples
Sep 17 13:49:47 Finished examples                                              9m49s   4GB
Sep 17 13:49:47 Starting examples/compilation/x64
Sep 17 15:53:12 Finished examples/compilation/x64                           2h03m23s  16GB
Sep 17 15:53:12 Starting examples/compilation/x64/proofs
Sep 17 15:55:28 Finished examples/compilation/x64/proofs                       2m15s   3GB
Sep 17 15:55:28 Starting examples/compilation/ag32
Sep 17 16:28:17 Finished examples/compilation/ag32                            32m48s   8GB
Sep 17 16:28:17 Starting examples/compilation/ag32/proofs
Sep 17 16:29:06 Finished examples/compilation/ag32/proofs                        49s   3GB
Sep 17 16:29:07 Starting examples/compilation/to_word
Sep 17 16:32:05 Finished examples/compilation/to_word                          2m57s   5GB
Sep 17 16:32:05 Starting examples/lpr_checker
Sep 17 16:33:02 Finished examples/lpr_checker                                    56s 997MB
Sep 17 16:33:02 Starting examples/lpr_checker/array
Sep 17 17:06:49 Finished examples/lpr_checker/array                           33m45s   5GB
Sep 17 17:06:49 Starting examples/lpr_checker/array/compilation
Sep 17 17:51:38 Finished examples/lpr_checker/array/compilation               44m49s   9GB
Sep 17 17:51:38 Starting examples/lpr_checker/array/compilation/proofs
Sep 17 17:52:58 Finished examples/lpr_checker/array/compilation/proofs         1m19s   6GB
Sep 17 17:52:58 Starting examples/opentheory
Sep 17 18:03:15 Finished examples/opentheory                                  10m16s   6GB
Sep 17 18:03:15 Starting examples/opentheory
Sep 17 18:03:16 Finished examples/opentheory                                      1s 140MB
Sep 17 18:03:16 Starting examples/opentheory/compilation
Sep 17 18:39:58 Finished examples/opentheory/compilation                      36m39s  29GB
Sep 17 18:39:59 Starting examples/opentheory/compilation/proofs
Sep 17 18:40:44 Finished examples/opentheory/compilation/proofs                  44s   3GB
Sep 17 18:40:44 Starting examples/opentheory/compilation/ag32
Sep 17 19:14:22 Finished examples/opentheory/compilation/ag32                 33m37s  27GB
Sep 17 19:14:22 Starting examples/opentheory/compilation/ag32/proofs
Sep 17 19:16:15 Finished examples/opentheory/compilation/ag32/proofs           1m52s   6GB
Sep 17 19:16:15 Starting examples/sat_encodings
Sep 17 19:18:02 Finished examples/sat_encodings                                1m46s 764MB
Sep 17 19:18:02 Starting examples/sat_encodings/case_studies
Sep 17 19:19:37 Finished examples/sat_encodings/case_studies                   1m34s 804MB
Sep 17 19:19:37 Starting examples/sat_encodings/translation
Sep 17 19:25:13 Finished examples/sat_encodings/translation                    5m36s   5GB
Sep 17 19:25:13 Starting examples/sat_encodings/translation/compilation
Sep 17 20:11:49 Finished examples/sat_encodings/translation/compilation       46m34s  21GB
Sep 17 20:11:49 Starting examples/deflate
Sep 17 20:12:40 Finished examples/deflate                                        51s 730MB
Sep 17 20:12:41 Starting examples/deflate/translation
Sep 17 20:14:11 Finished examples/deflate/translation                          1m30s   2GB
Sep 17 20:14:11 Starting examples/deflate/translation/compilation
Sep 17 20:34:53 Finished examples/deflate/translation/compilation             20m41s  12GB
Sep 17 20:34:53 Starting translator/okasaki-examples
Sep 17 20:39:48 Finished translator/okasaki-examples                           4m54s   1GB
Sep 17 20:39:48 Starting translator/other-examples
Sep 17 20:42:06 Finished translator/other-examples                             2m18s   1GB
Sep 17 20:42:06 Starting compiler/parsing/tests
Sep 17 20:42:35 Finished compiler/parsing/tests                                  28s 616MB
Sep 17 20:42:36 Starting compiler/inference/tests
Sep 17 20:50:57 Finished compiler/inference/tests                              8m21s   6GB
Sep 17 20:50:57 Starting compiler/printing/test
Sep 17 20:54:41 Finished compiler/printing/test                                3m43s   3GB
Sep 17 20:54:41 Starting icing/flover
Sep 17 21:31:07 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 (15s)     OK
Starting work on MachineTypeTheory
sqrtApproxTheory                                                  icing/flover (26s)     OK
MachineTypeTheory                                           icing/flover/Infra (30s)     OK
Finished $(CAKEMLDIR)/icing/flover/Infra [#theories: 3]                           (52.640s) 
Starting work on AbbrevsTheory
AbbrevsTheory                                           icing/flover/semantics (14s)     OK
Starting work on ExpressionsTheory
ExpressionsTheory                                       icing/flover/semantics (16s)     OK
Starting work on FloverMapTheory
FloverMapTheory                                         icing/flover/semantics  (7s)     OK
Starting work on ExpressionAbbrevsTheory
ExpressionAbbrevsTheory                                 icing/flover/semantics  (6s)     OK
Starting work on ExpressionSemanticsTheory
ExpressionSemanticsTheory                               icing/flover/semantics (18s)     OK
Starting work on CommandsTheory
CommandsTheory                                          icing/flover/semantics (14s)     OK
Finished $(CAKEMLDIR)/icing/flover/semantics [#theories: 6]                       (77.680s) 
Starting work on EnvironmentsTheory
Starting work on IntervalArithTheory
Starting work on TypeValidatorTheory
Starting work on ssaPrgsTheory
ssaPrgsTheory                                                     icing/flover  (8s)     OK
EnvironmentsTheory                                                icing/flover (17s)     OK
Starting work on ErrorBoundsTheory
IntervalArithTheory                                               icing/flover (26s)     OK
TypeValidatorTheory                                               icing/flover (61s)     OK
Starting work on RealRangeArithTheory
ErrorBoundsTheory                                                 icing/flover (44s)     OK
RealRangeArithTheory                                              icing/flover  (8s)     OK
Starting work on IntervalValidationTheory
Starting work on RealIntervalInferenceTheory
RealIntervalInferenceTheory                                       icing/flover (17s)     OK
IntervalValidationTheory                                          icing/flover (29s)     OK
Starting work on ErrorValidationTheory
Starting work on ErrorIntervalInferenceTheory
ErrorIntervalInferenceTheory                                      icing/flover (18s)     OK
Starting work on CertificateGeneratorTheory
CertificateGeneratorTheory                                        icing/flover  (8s)     OK
ErrorValidationTheory                                             icing/flover(946s)     OK
Starting work on FPRangeValidatorTheory
FPRangeValidatorTheory                                            icing/flover(949s)     OK
Starting work on CertificateCheckerTheory
CertificateCheckerTheory                                          icing/flover (17s)     OK
Starting work on IEEE_connectionTheory
IEEE_connectionTheory                                             icing/flover (16s)FAIL<1>
 <<HOL message: Created theory "IEEE_connection">>
 error in quse /home/cug/hk324/cml-regression/cakeml-1987/icing/flover/IEEE_connectionScript.sml : UNCHANGED
 error in load /home/cug/hk324/cml-regression/cakeml-1987/icing/flover/IEEE_connectionScript : UNCHANGED
 Uncaught exception: UNCHANGED