Job 2337

CakeML:74b152a08abe7ee2d1962cbe313a90d9f880f611
  Update for name change in mlintTheory [Mar 13 09:41:56]
#985 (cvunify)
Merging into:98d0d03c9e52b27a9895186563d385583deb75a2
  Merge pull request #984 from CakeML/compression [Mar 10 14:36:06]
HOL:3a51c81db857b7722efa0871ac507883adf6d440
  Remove compilerTheory (put its content at end of codegenTheory) [Mar 11 19:26:17]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Mar 13 09:47:05 Claimed job
Mar 13 09:47:07 Reusing HOL
Mar 13 09:47:48 Starting developers
Mar 13 09:47:53 Finished developers                                               5s 102MB
Mar 13 09:47:54 Starting developers/bin
Mar 13 09:48:00 Finished developers/bin                                           5s   1GB
Mar 13 09:48:00 Starting compiler/proofs
Mar 13 11:39:19 Finished compiler/proofs                                    1h51m18s  15GB
Mar 13 11:39:19 Starting compiler/bootstrap/translation
Mar 13 19:55:22 Finished compiler/bootstrap/translation                     8h16m03s  32GB
Mar 13 19:55:22 Starting semantics/ffi
Mar 13 19:55:27 Finished semantics/ffi                                            4s 387MB
Mar 13 19:55:27 Starting semantics
Mar 13 19:55:29 Finished semantics                                                1s  20MB
Mar 13 19:55:29 Starting semantics/proofs
Mar 13 19:56:01 Finished semantics/proofs                                        31s 819MB
Mar 13 19:56:01 Starting semantics/alt_semantics
Mar 13 19:56:33 Finished semantics/alt_semantics                                 31s 761MB
Mar 13 19:56:33 Starting semantics/alt_semantics/proofs
Mar 13 20:08:31 Finished semantics/alt_semantics/proofs                       11m57s   1GB
Mar 13 20:08:31 Starting basis/pure
Mar 13 20:08:32 Finished basis/pure                                               1s  20MB
Mar 13 20:08:32 Starting translator
Mar 13 20:10:21 Finished translator                                            1m48s   2GB
Mar 13 20:10:21 Starting compiler/parsing
Mar 13 20:10:23 Finished compiler/parsing                                         1s  23MB
Mar 13 20:10:23 Starting characteristic
Mar 13 20:10:25 Finished characteristic                                           1s  22MB
Mar 13 20:10:25 Starting translator/monadic
Mar 13 20:10:27 Finished translator/monadic                                       1s  26MB
Mar 13 20:10:27 Starting basis
Mar 13 20:14:08 Finished basis                                                 3m40s   3GB
Mar 13 20:14:08 Starting compiler/inference
Mar 13 20:14:11 Finished compiler/inference                                       2s  27MB
Mar 13 20:14:11 Starting compiler/backend/reg_alloc
Mar 13 20:14:12 Finished compiler/backend/reg_alloc                               1s  22MB
Mar 13 20:14:13 Starting compiler/backend/gc
Mar 13 20:14:15 Finished compiler/backend/gc                                      2s  24MB
Mar 13 20:14:15 Starting compiler/backend
Mar 13 20:14:28 Finished compiler/backend                                        12s 755MB
Mar 13 20:14:28 Starting compiler/encoders/asm
Mar 13 20:14:30 Finished compiler/encoders/asm                                    1s  21MB
Mar 13 20:14:30 Starting compiler/encoders/x64
Mar 13 20:14:32 Finished compiler/encoders/x64                                    1s  29MB
Mar 13 20:14:32 Starting compiler/encoders/arm7
Mar 13 20:14:33 Finished compiler/encoders/arm7                                   1s  28MB
Mar 13 20:14:34 Starting compiler/encoders/arm8
Mar 13 20:14:35 Finished compiler/encoders/arm8                                   1s  27MB
Mar 13 20:14:36 Starting compiler/encoders/arm8_asl
Mar 13 20:17:49 Finished compiler/encoders/arm8_asl                            3m13s   1GB
Mar 13 20:17:49 Starting compiler/encoders/mips
Mar 13 20:17:51 Finished compiler/encoders/mips                                   1s  27MB
Mar 13 20:17:51 Starting compiler/encoders/riscv
Mar 13 20:17:53 Finished compiler/encoders/riscv                                  1s  25MB
Mar 13 20:17:53 Starting compiler/encoders/ag32
Mar 13 20:17:55 Finished compiler/encoders/ag32                                   1s  21MB
Mar 13 20:17:55 Starting compiler/backend/x64
Mar 13 20:17:57 Finished compiler/backend/x64                                     2s  25MB
Mar 13 20:17:57 Starting compiler/backend/arm7
Mar 13 20:17:59 Finished compiler/backend/arm7                                    2s  28MB
Mar 13 20:17:59 Starting compiler/backend/arm8
Mar 13 20:18:02 Finished compiler/backend/arm8                                    2s  21MB
Mar 13 20:18:02 Starting compiler/backend/mips
Mar 13 20:18:04 Finished compiler/backend/mips                                    2s  22MB
Mar 13 20:18:04 Starting compiler/backend/riscv
Mar 13 20:18:06 Finished compiler/backend/riscv                                   2s  27MB
Mar 13 20:18:07 Starting compiler/backend/ag32
Mar 13 20:19:32 Finished compiler/backend/ag32                                 1m25s   1GB
Mar 13 20:19:32 Starting compiler/parsing/proofs
Mar 13 20:19:34 Finished compiler/parsing/proofs                                  1s  21MB
Mar 13 20:19:34 Starting compiler/inference/proofs
Mar 13 20:19:37 Finished compiler/inference/proofs                                2s  29MB
Mar 13 20:19:37 Starting compiler/backend/semantics
Mar 13 20:20:50 Finished compiler/backend/semantics                            1m13s   1GB
Mar 13 20:20:51 Starting compiler/backend/reg_alloc/proofs
Mar 13 20:20:52 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Mar 13 20:20:53 Starting compiler/backend/proofs
Mar 13 20:21:53 Finished compiler/backend/proofs                               1m00s   2GB
Mar 13 20:21:53 Starting compiler/backend/serialiser
Mar 13 20:21:56 Finished compiler/backend/serialiser                              2s  26MB
Mar 13 20:21:56 Starting compiler/encoders/x64/proofs
Mar 13 20:31:46 Finished compiler/encoders/x64/proofs                          9m49s   6GB
Mar 13 20:31:46 Starting compiler/encoders/arm7/proofs
Mar 13 20:45:40 Finished compiler/encoders/arm7/proofs                        13m53s   3GB
Mar 13 20:45:40 Starting compiler/encoders/arm8/proofs
Mar 13 20:52:39 Finished compiler/encoders/arm8/proofs                         6m58s   1GB
Mar 13 20:52:39 Starting compiler/encoders/arm8_asl/proofs
Mar 13 21:08:55 Finished compiler/encoders/arm8_asl/proofs                    16m15s   1GB
Mar 13 21:08:55 Starting compiler/encoders/mips/proofs
Mar 13 21:19:29 Finished compiler/encoders/mips/proofs                        10m34s   2GB
Mar 13 21:19:29 Starting compiler/encoders/riscv/proofs
Mar 13 21:28:29 Finished compiler/encoders/riscv/proofs                        8m59s   1GB
Mar 13 21:28:29 Starting compiler/encoders/ag32/proofs
Mar 13 21:31:02 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Mar 13 21:31:02 Starting compiler/backend/x64/proofs
Mar 13 21:31:34 Finished compiler/backend/x64/proofs                             31s   2GB
Mar 13 21:31:34 Starting compiler/backend/arm7/proofs
Mar 13 21:32:07 Finished compiler/backend/arm7/proofs                            32s   1GB
Mar 13 21:32:07 Starting compiler/backend/arm8/proofs
Mar 13 21:32:38 Finished compiler/backend/arm8/proofs                            30s   2GB
Mar 13 21:32:38 Starting compiler/backend/arm8_asl
Mar 13 21:33:03 Finished compiler/backend/arm8_asl                               24s   1GB
Mar 13 21:33:03 Starting compiler/backend/mips/proofs
Mar 13 21:33:34 Finished compiler/backend/mips/proofs                            31s   1GB
Mar 13 21:33:34 Starting compiler/backend/riscv/proofs
Mar 13 21:34:08 Finished compiler/backend/riscv/proofs                           33s   2GB
Mar 13 21:34:08 Starting compiler/backend/ag32/proofs
Mar 13 21:48:17 Finished compiler/backend/ag32/proofs                         14m08s   3GB
Mar 13 21:48:17 Starting candle/set-theory
Mar 13 21:48:56 Finished candle/set-theory                                       38s   1GB
Mar 13 21:48:56 Starting candle/syntax-lib
Mar 13 21:48:57 Finished candle/syntax-lib                                        1s  28MB
Mar 13 21:48:57 Starting candle/standard/syntax
Mar 13 21:49:08 Finished candle/standard/syntax                                  10s 733MB
Mar 13 21:49:09 Starting candle/standard/semantics
Mar 13 21:51:08 Finished candle/standard/semantics                             1m58s   1GB
Mar 13 21:51:08 Starting candle/standard/monadic
Mar 13 21:51:10 Finished candle/standard/monadic                                  1s  21MB
Mar 13 21:51:10 Starting candle/standard/ml_kernel
Mar 13 21:52:51 Finished candle/standard/ml_kernel                             1m40s   3GB
Mar 13 21:52:51 Starting candle/overloading/syntax
Mar 13 21:56:14 Finished candle/overloading/syntax                             3m22s   1GB
Mar 13 21:56:14 Starting candle/overloading/semantics
Mar 13 22:08:28 Finished candle/overloading/semantics                         12m13s   2GB
Mar 13 22:08:28 Starting candle/overloading/monadic
Mar 13 22:11:12 Finished candle/overloading/monadic                            2m44s   2GB
Mar 13 22:11:12 Starting candle/overloading/ml_kernel
Mar 13 22:19:14 Finished candle/overloading/ml_kernel                          8m01s   3GB
Mar 13 22:19:14 Starting candle/overloading/ml_checker
Mar 13 22:21:51 Finished candle/overloading/ml_checker                         2m37s   2GB
Mar 13 22:21:51 Starting candle/prover
Mar 13 22:31:58 Finished candle/prover                                        10m06s   3GB
Mar 13 22:31:58 Starting pancake
Mar 13 22:32:45 Finished pancake                                                 46s 900MB
Mar 13 22:32:45 Starting pancake/ffi
Mar 13 22:32:45 Finished pancake/ffi                                              0s  13MB
Mar 13 22:32:45 Starting pancake/semantics
Mar 13 22:35:10 Finished pancake/semantics                                     2m24s   1GB
Mar 13 22:35:10 Starting pancake/parser
Mar 13 22:35:33 Finished pancake/parser                                          22s 672MB
Mar 13 22:35:33 Starting pancake/proofs
Mar 13 23:09:02 Finished pancake/proofs                                       33m28s   5GB
Mar 13 23:09:02 Starting characteristic/examples
Mar 13 23:10:36 Finished characteristic/examples                               1m34s   3GB
Mar 13 23:10:36 Starting tutorial/solutions
Mar 13 23:25:36 Finished tutorial/solutions                                   14m59s  10GB
Mar 13 23:25:36 Starting translator/monadic/examples
Mar 13 23:29:45 Finished translator/monadic/examples                           4m08s   3GB
Mar 13 23:29:45 Starting examples
Mar 13 23:46:31 Finished examples                                             16m45s   4GB
Mar 13 23:46:31 Starting examples/compilation/x64
Mar 14 01:46:54 Finished examples/compilation/x64                           2h00m22s  21GB
Mar 14 01:46:54 Starting examples/compilation/x64/proofs
Mar 14 01:49:29 Finished examples/compilation/x64/proofs                       2m35s   4GB
Mar 14 01:49:29 Starting examples/compilation/ag32
Mar 14 02:19:55 Finished examples/compilation/ag32                            30m25s   7GB
Mar 14 02:19:55 Starting examples/compilation/ag32/proofs
Mar 14 02:20:58 Finished examples/compilation/ag32/proofs                      1m02s   3GB
Mar 14 02:20:58 Starting examples/compilation/to_word
Mar 14 02:24:19 Finished examples/compilation/to_word                          3m20s   6GB
Mar 14 02:24:19 Starting examples/lpr_checker
Mar 14 02:25:25 Finished examples/lpr_checker                                  1m06s   1GB
Mar 14 02:25:25 Starting examples/lpr_checker/array
Mar 14 02:58:03 Finished examples/lpr_checker/array                           32m37s   6GB
Mar 14 02:58:03 Starting examples/lpr_checker/array/compilation
Mar 14 03:49:00 Finished examples/lpr_checker/array/compilation               50m57s  23GB
Mar 14 03:49:00 Starting examples/lpr_checker/array/compilation/proofs
Mar 14 03:50:44 Finished examples/lpr_checker/array/compilation/proofs         1m43s   3GB
Mar 14 03:50:44 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 14 03:58:30 Finished examples/lpr_checker/array/compilation/proofsARM8     7m46s  18GB
Mar 14 03:58:30 Starting examples/xlrup_checker
Mar 14 03:59:28 Finished examples/xlrup_checker                                  58s   1GB
Mar 14 03:59:29 Starting examples/xlrup_checker/array
Mar 14 04:16:55 Finished examples/xlrup_checker/array                         17m25s   4GB
Mar 14 04:16:55 Starting examples/xlrup_checker/array/compilation
Mar 14 04:39:13 Finished examples/xlrup_checker/array/compilation             22m18s  19GB
Mar 14 04:39:13 Starting examples/xlrup_checker/array/compilation/proofs
Mar 14 04:40:13 Finished examples/xlrup_checker/array/compilation/proofs       1m00s   4GB
Mar 14 04:40:13 Starting examples/pseudo_bool
Mar 14 04:42:07 Finished examples/pseudo_bool                                  1m53s   1GB
Mar 14 04:42:07 Starting examples/pseudo_bool/cnf_encoding
Mar 14 04:42:35 Finished examples/pseudo_bool/cnf_encoding                       27s 825MB
Mar 14 04:42:35 Starting examples/pseudo_bool/graph_encoding
Mar 14 04:43:17 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
Mar 14 04:43:17 Starting examples/pseudo_bool/array
Mar 14 05:50:14 Finished examples/pseudo_bool/array                         1h06m57s   8GB
Mar 14 05:50:14 Starting examples/pseudo_bool/array/compilation
Mar 14 13:14:57 Finished examples/pseudo_bool/array/compilation             7h24m42s  64GB
Mar 14 13:14:58 Starting examples/pseudo_bool/array/compilation/proofs
Mar 14 13:17:32 Finished examples/pseudo_bool/array/compilation/proofs         2m34s   6GB
Mar 14 13:17:33 Starting examples/opentheory
Mar 14 13:28:40 Finished examples/opentheory                                  11m06s   4GB
Mar 14 13:28:40 Starting examples/opentheory
Mar 14 13:28:42 Finished examples/opentheory                                      1s  24MB
Mar 14 13:28:42 Starting examples/opentheory/compilation
Mar 14 14:06:42 Finished examples/opentheory/compilation                      38m00s  32GB
Mar 14 14:06:42 Starting examples/opentheory/compilation/proofs
Mar 14 14:07:44 Finished examples/opentheory/compilation/proofs                1m01s   5GB
Mar 14 14:07:44 Starting examples/opentheory/compilation/ag32
Mar 14 14:41:23 Finished examples/opentheory/compilation/ag32                 33m38s  32GB
Mar 14 14:41:24 Starting examples/opentheory/compilation/ag32/proofs
Mar 14 14:43:17 Finished examples/opentheory/compilation/ag32/proofs           1m53s   7GB
Mar 14 14:43:17 Starting examples/sat_encodings
Mar 14 14:45:20 Finished examples/sat_encodings                                2m03s 859MB
Mar 14 14:45:20 Starting examples/sat_encodings/case_studies
Mar 14 14:47:06 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Mar 14 14:47:06 Starting examples/sat_encodings/translation
Mar 14 14:53:27 Finished examples/sat_encodings/translation                    6m21s   4GB
Mar 14 14:53:27 Starting examples/sat_encodings/translation/compilation
Mar 14 15:40:04 Finished examples/sat_encodings/translation/compilation       46m36s  22GB
Mar 14 15:40:04 Starting examples/deflate
Mar 14 15:41:05 Finished examples/deflate                                      1m00s 950MB
Mar 14 15:41:05 Starting examples/deflate/translation
Mar 14 15:42:50 Finished examples/deflate/translation                          1m45s   4GB
Mar 14 15:42:50 Starting examples/deflate/translation/compilation
Mar 14 16:02:55 Finished examples/deflate/translation/compilation             20m04s  14GB
Mar 14 16:02:55 Starting examples/vipr
Mar 14 16:06:52 Finished examples/vipr                                         3m56s   3GB
Mar 14 16:06:52 Starting examples/vipr/compilation
Mar 14 16:27:38 Finished examples/vipr/compilation                            20m46s  20GB
Mar 14 16:27:38 Starting translator/okasaki-examples
Mar 14 16:32:49 Finished translator/okasaki-examples                           5m10s   2GB
Mar 14 16:32:50 Starting translator/other-examples
Mar 14 16:36:22 Finished translator/other-examples                             3m32s   1GB
Mar 14 16:36:22 Starting compiler/parsing/tests
Mar 14 16:36:54 Finished compiler/parsing/tests                                  32s 901MB
Mar 14 16:36:54 Starting compiler/inference/tests
Mar 14 16:37:25 Finished compiler/inference/tests                                30s   2GB
Mar 14 16:37:25 Starting compiler/printing/test
Mar 14 16:38:04 FAILED: compiler/printing/test
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)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/cv_compute[0m
Scanning [1m$(CAKEMLDIR)/cv_translator[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/tests[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanned 75 directories
Starting work on README.md
Starting work on printingTestTheory
README.md                                                                                                                                                                                                                         (0s)     OK
printingTestTheory                                                                                                                                                                                                               (33s)FAIL<1>
 /home/cug/hk324/cml-regression/cakeml-2337/compiler/printing/test/printingTestScript.sml:11: error: Structure (inferenceComputeLib) has not been declared
 Found near
   open preamble basicComputeLib inferenceComputeLib basisTypeCheckTheory
 error in quse /home/cug/hk324/cml-regression/cakeml-2337/compiler/printing/test/printingTestScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-2337/compiler/printing/test/printingTestScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"