Job 1991

CakeML:4cd953474ce72ae40ffdbb303741a04124d4fb2a
  prove word_to_word_compile_semantics [Sep 14 11:01:34]
#909 (word_to_word_Pancake)
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 21:31:09 Claimed job
Sep 17 21:31:10 Reusing HOL
Sep 17 21:31:25 Starting developers
Sep 17 21:31:30 Finished developers                                               4s  97MB
Sep 17 21:31:30 Starting developers/bin
Sep 17 21:31:36 Finished developers/bin                                           6s   1GB
Sep 17 21:31:36 Starting semantics/ffi
Sep 17 21:31:45 Finished semantics/ffi                                            8s 230MB
Sep 17 21:31:45 Starting semantics
Sep 17 21:34:07 Finished semantics                                             2m22s   1GB
Sep 17 21:34:07 Starting semantics/proofs
Sep 17 21:41:17 Finished semantics/proofs                                      7m09s   1GB
Sep 17 21:41:17 Starting semantics/alt_semantics
Sep 17 21:41:43 Finished semantics/alt_semantics                                 26s 558MB
Sep 17 21:41:43 Starting semantics/alt_semantics/proofs
Sep 17 21:53:22 Finished semantics/alt_semantics/proofs                       11m38s   1GB
Sep 17 21:53:22 Starting basis/pure
Sep 17 21:54:27 Finished basis/pure                                            1m04s 905MB
Sep 17 21:54:27 Starting translator
Sep 17 21:58:04 Finished translator                                            3m37s   1GB
Sep 17 21:58:04 Starting compiler/parsing
Sep 17 21:59:28 Finished compiler/parsing                                      1m23s   4GB
Sep 17 21:59:29 Starting characteristic
Sep 17 22:06:23 Finished characteristic                                        6m54s   1GB
Sep 17 22:06:23 Starting translator/monadic
Sep 17 22:08:18 Finished translator/monadic                                    1m54s   1GB
Sep 17 22:08:18 Starting basis
Sep 17 22:59:57 Finished basis                                                51m37s  15GB
Sep 17 22:59:57 Starting compiler/inference
Sep 17 23:01:27 Finished compiler/inference                                    1m29s   1GB
Sep 17 23:01:27 Starting compiler/backend/reg_alloc
Sep 17 23:03:11 Finished compiler/backend/reg_alloc                            1m44s   1GB
Sep 17 23:03:11 Starting compiler/backend/gc
Sep 17 23:07:28 Finished compiler/backend/gc                                   4m16s   1GB
Sep 17 23:07:28 Starting compiler/backend
Sep 17 23:13:02 Finished compiler/backend                                      5m34s   3GB
Sep 17 23:13:02 Starting compiler/encoders/asm
Sep 17 23:13:32 Finished compiler/encoders/asm                                   29s 904MB
Sep 17 23:13:32 Starting compiler/encoders/x64
Sep 17 23:14:01 Finished compiler/encoders/x64                                   28s   1GB
Sep 17 23:14:01 Starting compiler/encoders/arm7
Sep 17 23:14:55 Finished compiler/encoders/arm7                                  54s   1GB
Sep 17 23:14:55 Starting compiler/encoders/arm8
Sep 17 23:15:12 Finished compiler/encoders/arm8                                  16s 926MB
Sep 17 23:15:12 Starting compiler/encoders/arm8_asl
Sep 17 23:17:44 Finished compiler/encoders/arm8_asl                            2m31s   1GB
Sep 17 23:17:44 Starting compiler/encoders/mips
Sep 17 23:18:05 Finished compiler/encoders/mips                                  20s   1GB
Sep 17 23:18:05 Starting compiler/encoders/riscv
Sep 17 23:18:24 Finished compiler/encoders/riscv                                 19s 876MB
Sep 17 23:18:24 Starting compiler/encoders/ag32
Sep 17 23:18:45 Finished compiler/encoders/ag32                                  20s 614MB
Sep 17 23:18:45 Starting compiler/backend/x64
Sep 17 23:19:06 Finished compiler/backend/x64                                    20s   1GB
Sep 17 23:19:06 Starting compiler/backend/arm7
Sep 17 23:19:30 Finished compiler/backend/arm7                                   23s   1GB
Sep 17 23:19:30 Starting compiler/backend/arm8
Sep 17 23:19:51 Finished compiler/backend/arm8                                   20s   1GB
Sep 17 23:19:51 Starting compiler/backend/mips
Sep 17 23:20:13 Finished compiler/backend/mips                                   21s   1GB
Sep 17 23:20:13 Starting compiler/backend/riscv
Sep 17 23:20:34 Finished compiler/backend/riscv                                  21s   1GB
Sep 17 23:20:34 Starting compiler/backend/ag32
Sep 17 23:21:59 Finished compiler/backend/ag32                                 1m24s   2GB
Sep 17 23:21:59 Starting compiler/parsing/proofs
Sep 17 23:25:41 Finished compiler/parsing/proofs                               3m42s   1GB
Sep 17 23:25:41 Starting compiler/inference/proofs
Sep 17 23:28:23 Finished compiler/inference/proofs                             2m41s   1GB
Sep 17 23:28:23 Starting compiler/backend/semantics
Sep 17 23:54:01 Finished compiler/backend/semantics                           25m37s   2GB
Sep 17 23:54:02 Starting compiler/backend/reg_alloc/proofs
Sep 17 23:57:40 Finished compiler/backend/reg_alloc/proofs                     3m38s 788MB
Sep 17 23:57:40 Starting compiler/backend/proofs
Sep 18 00:53:08 Finished compiler/backend/proofs                              55m26s  15GB
Sep 18 00:53:08 Starting compiler/backend/serialiser
Sep 18 00:54:38 Finished compiler/backend/serialiser                           1m29s   1GB
Sep 18 00:54:38 Starting compiler/encoders/x64/proofs
Sep 18 01:04:31 Finished compiler/encoders/x64/proofs                          9m52s   4GB
Sep 18 01:04:31 Starting compiler/encoders/arm7/proofs
Sep 18 01:18:10 Finished compiler/encoders/arm7/proofs                        13m38s   3GB
Sep 18 01:18:10 Starting compiler/encoders/arm8/proofs
Sep 18 01:25:09 Finished compiler/encoders/arm8/proofs                         6m59s   1GB
Sep 18 01:25:10 Starting compiler/encoders/arm8_asl/proofs
Sep 18 01:40:59 Finished compiler/encoders/arm8_asl/proofs                    15m49s   2GB
Sep 18 01:40:59 Starting compiler/encoders/mips/proofs
Sep 18 01:51:16 Finished compiler/encoders/mips/proofs                        10m16s   2GB
Sep 18 01:51:16 Starting compiler/encoders/riscv/proofs
Sep 18 02:00:11 Finished compiler/encoders/riscv/proofs                        8m51s   1GB
Sep 18 02:00:11 Starting compiler/encoders/ag32/proofs
Sep 18 02:02:46 Finished compiler/encoders/ag32/proofs                         2m35s 864MB
Sep 18 02:02:47 Starting compiler/backend/x64/proofs
Sep 18 02:03:12 Finished compiler/backend/x64/proofs                             24s   1GB
Sep 18 02:03:12 Starting compiler/backend/arm7/proofs
Sep 18 02:03:40 Finished compiler/backend/arm7/proofs                            28s   1GB
Sep 18 02:03:40 Starting compiler/backend/arm8/proofs
Sep 18 02:04:07 Finished compiler/backend/arm8/proofs                            26s   1GB
Sep 18 02:04:07 Starting compiler/backend/arm8_asl
Sep 18 02:04:27 Finished compiler/backend/arm8_asl                               19s   1GB
Sep 18 02:04:27 Starting compiler/backend/mips/proofs
Sep 18 02:04:52 Finished compiler/backend/mips/proofs                            24s   1GB
Sep 18 02:04:52 Starting compiler/backend/riscv/proofs
Sep 18 02:05:18 Finished compiler/backend/riscv/proofs                           25s   1GB
Sep 18 02:05:18 Starting compiler/backend/ag32/proofs
Sep 18 02:18:44 Finished compiler/backend/ag32/proofs                         13m26s   3GB
Sep 18 02:18:45 Starting compiler/proofs
Sep 18 02:20:49 Finished compiler/proofs                                       2m04s   3GB
Sep 18 02:20:49 Starting candle/set-theory
Sep 18 02:21:23 Finished candle/set-theory                                       33s   1GB
Sep 18 02:21:23 Starting candle/syntax-lib
Sep 18 02:21:35 Finished candle/syntax-lib                                       12s 574MB
Sep 18 02:21:35 Starting candle/standard/syntax
Sep 18 02:23:36 Finished candle/standard/syntax                                2m00s   1GB
Sep 18 02:23:36 Starting candle/standard/semantics
Sep 18 02:25:20 Finished candle/standard/semantics                             1m43s   1GB
Sep 18 02:25:21 Starting candle/standard/monadic
Sep 18 02:27:14 Finished candle/standard/monadic                               1m53s   1GB
Sep 18 02:27:15 Starting candle/standard/ml_kernel
Sep 18 02:33:46 Finished candle/standard/ml_kernel                             6m31s   5GB
Sep 18 02:33:46 Starting candle/overloading/syntax
Sep 18 02:36:56 Finished candle/overloading/syntax                             3m10s   1GB
Sep 18 02:36:57 Starting candle/overloading/semantics
Sep 18 02:48:42 Finished candle/overloading/semantics                         11m45s   2GB
Sep 18 02:48:42 Starting candle/overloading/monadic
Sep 18 02:51:17 Finished candle/overloading/monadic                            2m34s   1GB
Sep 18 02:51:17 Starting candle/overloading/ml_kernel
Sep 18 02:58:30 Finished candle/overloading/ml_kernel                          7m12s   3GB
Sep 18 02:58:30 Starting candle/overloading/ml_checker
Sep 18 03:00:58 Finished candle/overloading/ml_checker                         2m26s   2GB
Sep 18 03:00:58 Starting candle/prover
Sep 18 03:15:57 Finished candle/prover                                        14m58s   5GB
Sep 18 03:15:57 Starting pancake
Sep 18 03:18:57 Finished pancake                                               3m00s   4GB
Sep 18 03:18:57 Starting pancake/ffi
Sep 18 03:18:58 Finished pancake/ffi                                              0s  25MB
Sep 18 03:18:58 Starting pancake/semantics
Sep 18 03:21:24 Finished pancake/semantics                                     2m26s   1GB
Sep 18 03:21:24 Starting pancake/proofs
Sep 18 03:33:45 Finished pancake/proofs                                       12m20s   6GB
Sep 18 03:33:45 Starting characteristic/examples
Sep 18 03:35:08 Finished characteristic/examples                               1m23s   2GB
Sep 18 03:35:08 Starting tutorial/solutions
Sep 18 03:51:10 Finished tutorial/solutions                                   16m01s   8GB
Sep 18 03:51:10 Starting translator/monadic/examples
Sep 18 03:54:54 Finished translator/monadic/examples                           3m44s   2GB
Sep 18 03:54:54 Starting examples
Sep 18 04:04:32 Finished examples                                              9m35s   4GB
Sep 18 04:04:32 Starting examples/compilation/x64
Sep 18 06:08:37 Finished examples/compilation/x64                           2h04m02s  15GB
Sep 18 06:08:38 Starting examples/compilation/x64/proofs
Sep 18 06:10:46 Finished examples/compilation/x64/proofs                       2m08s   3GB
Sep 18 06:10:46 Starting examples/compilation/ag32
Sep 18 06:43:46 Finished examples/compilation/ag32                            32m59s   8GB
Sep 18 06:43:46 Starting examples/compilation/ag32/proofs
Sep 18 06:44:35 Finished examples/compilation/ag32/proofs                        48s   3GB
Sep 18 06:44:35 Starting examples/lpr_checker
Sep 18 06:45:32 Finished examples/lpr_checker                                    56s   1GB
Sep 18 06:45:32 Starting examples/lpr_checker/array
Sep 18 07:19:23 Finished examples/lpr_checker/array                           33m50s  10GB
Sep 18 07:19:23 Starting examples/lpr_checker/array/compilation
Sep 18 07:58:45 Finished examples/lpr_checker/array/compilation               39m21s  26GB
Sep 18 07:58:45 Starting examples/lpr_checker/array/compilation/proofs
Sep 18 08:00:03 Finished examples/lpr_checker/array/compilation/proofs         1m18s   6GB
Sep 18 08:00:03 Starting examples/opentheory
Sep 18 08:10:19 Finished examples/opentheory                                  10m16s   5GB
Sep 18 08:10:20 Starting examples/opentheory
Sep 18 08:10:21 Finished examples/opentheory                                      1s 140MB
Sep 18 08:10:21 Starting examples/opentheory/compilation
Sep 18 08:47:04 Finished examples/opentheory/compilation                      36m41s  29GB
Sep 18 08:47:04 Starting examples/opentheory/compilation/proofs
Sep 18 08:47:50 Finished examples/opentheory/compilation/proofs                  46s   3GB
Sep 18 08:47:51 Starting examples/opentheory/compilation/ag32
Sep 18 09:22:23 Finished examples/opentheory/compilation/ag32                 34m32s  33GB
Sep 18 09:22:23 Starting examples/opentheory/compilation/ag32/proofs
Sep 18 09:24:10 Finished examples/opentheory/compilation/ag32/proofs           1m46s   6GB
Sep 18 09:24:10 Starting examples/sat_encodings
Sep 18 09:25:55 Finished examples/sat_encodings                                1m45s 763MB
Sep 18 09:25:55 Starting examples/sat_encodings/case_studies
Sep 18 09:27:32 Finished examples/sat_encodings/case_studies                   1m36s 715MB
Sep 18 09:27:32 Starting examples/sat_encodings/translation
Sep 18 09:33:23 Finished examples/sat_encodings/translation                    5m50s   3GB
Sep 18 09:33:23 Starting examples/sat_encodings/translation/compilation
Sep 18 10:21:05 Finished examples/sat_encodings/translation/compilation       47m40s  18GB
Sep 18 10:21:05 Starting examples/deflate
Sep 18 10:21:56 Finished examples/deflate                                        51s 729MB
Sep 18 10:21:57 Starting examples/deflate/translation
Sep 18 10:23:26 Finished examples/deflate/translation                          1m29s   2GB
Sep 18 10:23:27 Starting examples/deflate/translation/compilation
Sep 18 10:44:39 Finished examples/deflate/translation/compilation             21m12s  14GB
Sep 18 10:44:40 Starting translator/okasaki-examples
Sep 18 10:49:33 Finished translator/okasaki-examples                           4m53s   1GB
Sep 18 10:49:34 Starting translator/other-examples
Sep 18 10:50:19 Finished translator/other-examples                               45s   1GB
Sep 18 10:50:19 Starting compiler/parsing/tests
Sep 18 10:50:48 Finished compiler/parsing/tests                                  28s 588MB
Sep 18 10:50:49 Starting compiler/inference/tests
Sep 18 10:59:22 Finished compiler/inference/tests                              8m32s   5GB
Sep 18 10:59:22 Starting compiler/printing/test
Sep 18 11:03:03 Finished compiler/printing/test                                3m41s   2GB
Sep 18 11:03:04 Starting icing/flover
Sep 18 11:40:28 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)     OK
Starting work on MachineTypeTheory
sqrtApproxTheory                                                  icing/flover (25s)     OK
MachineTypeTheory                                           icing/flover/Infra (31s)     OK
Finished $(CAKEMLDIR)/icing/flover/Infra [#theories: 3]                           (53.070s) 
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]                       (78.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 (19s)     OK
Starting work on ErrorBoundsTheory
IntervalArithTheory                                               icing/flover (24s)     OK
TypeValidatorTheory                                               icing/flover (64s)     OK
Starting work on RealRangeArithTheory
ErrorBoundsTheory                                                 icing/flover (44s)     OK
RealRangeArithTheory                                              icing/flover  (7s)     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(999s)     OK
Starting work on FPRangeValidatorTheory
FPRangeValidatorTheory                                            icing/flover(947s)     OK
Starting work on CertificateCheckerTheory
CertificateCheckerTheory                                          icing/flover (17s)     OK
Starting work on IEEE_connectionTheory
IEEE_connectionTheory                                             icing/flover (17s)FAIL<1>
 <<HOL message: Created theory "IEEE_connection">>
 error in quse /home/cug/hk324/cml-regression/cakeml-1991/icing/flover/IEEE_connectionScript.sml : UNCHANGED
 error in load /home/cug/hk324/cml-regression/cakeml-1991/icing/flover/IEEE_connectionScript : UNCHANGED
 Uncaught exception: UNCHANGED