Job 2338

CakeML:0797ca2d7b7f55b3387a4a2b8e69dd2c74d069ae
  Add a couple of tests [Mar 13 15:44:02]
#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:lammington

Mar 13 21:49:15 Claimed job
Mar 13 21:49:20 Building HOL
Mar 13 22:03:22 Starting developers
Mar 13 22:03:26 Finished developers                                               2s 213MB
Mar 13 22:03:26 Starting developers/bin
Mar 13 22:03:38 Finished developers/bin                                          10s   1GB
Mar 13 22:03:38 Starting compiler/proofs
Mar 13 23:49:15 Finished compiler/proofs                                    1h45m36s  46GB
Mar 13 23:49:16 Starting compiler/bootstrap/translation
Mar 14 07:50:41 Finished compiler/bootstrap/translation                     8h01m23s  60GB
Mar 14 07:50:42 Starting semantics/ffi
Mar 14 07:50:50 Finished semantics/ffi                                            7s 660MB
Mar 14 07:50:51 Starting semantics
Mar 14 07:50:52 Finished semantics                                                0s  67MB
Mar 14 07:50:53 Starting semantics/proofs
Mar 14 07:51:30 Finished semantics/proofs                                        35s   1GB
Mar 14 07:51:31 Starting semantics/alt_semantics
Mar 14 07:52:11 Finished semantics/alt_semantics                                 38s   1GB
Mar 14 07:52:11 Starting semantics/alt_semantics/proofs
Mar 14 08:03:08 Finished semantics/alt_semantics/proofs                       10m55s   5GB
Mar 14 08:03:09 Starting basis/pure
Mar 14 08:03:11 Finished basis/pure                                               0s  69MB
Mar 14 08:03:12 Starting translator
Mar 14 08:05:01 Finished translator                                            1m48s   3GB
Mar 14 08:05:02 Starting compiler/parsing
Mar 14 08:05:03 Finished compiler/parsing                                         0s  69MB
Mar 14 08:05:04 Starting characteristic
Mar 14 08:05:06 Finished characteristic                                           0s  87MB
Mar 14 08:05:06 Starting translator/monadic
Mar 14 08:05:08 Finished translator/monadic                                       0s  97MB
Mar 14 08:05:09 Starting basis
Mar 14 08:08:52 Finished basis                                                 3m42s  10GB
Mar 14 08:08:53 Starting compiler/inference
Mar 14 08:08:55 Finished compiler/inference                                       1s 177MB
Mar 14 08:08:56 Starting compiler/backend/reg_alloc
Mar 14 08:08:57 Finished compiler/backend/reg_alloc                               0s  69MB
Mar 14 08:08:58 Starting compiler/backend/gc
Mar 14 08:09:00 Finished compiler/backend/gc                                      0s 134MB
Mar 14 08:09:01 Starting compiler/backend
Mar 14 08:09:18 Finished compiler/backend                                        16s   1GB
Mar 14 08:09:19 Starting compiler/encoders/asm
Mar 14 08:09:21 Finished compiler/encoders/asm                                    0s  84MB
Mar 14 08:09:22 Starting compiler/encoders/x64
Mar 14 08:09:23 Finished compiler/encoders/x64                                    0s  88MB
Mar 14 08:09:24 Starting compiler/encoders/arm7
Mar 14 08:09:25 Finished compiler/encoders/arm7                                   0s  96MB
Mar 14 08:09:26 Starting compiler/encoders/arm8
Mar 14 08:09:28 Finished compiler/encoders/arm8                                   0s  92MB
Mar 14 08:09:29 Starting compiler/encoders/arm8_asl
Mar 14 10:19:33 Finished compiler/encoders/arm8_asl                         2h10m03s  40GB
Mar 14 10:19:34 Starting compiler/encoders/mips
Mar 14 10:19:36 Finished compiler/encoders/mips                                   0s  97MB
Mar 14 10:19:37 Starting compiler/encoders/riscv
Mar 14 10:19:38 Finished compiler/encoders/riscv                                  0s  88MB
Mar 14 10:19:39 Starting compiler/encoders/ag32
Mar 14 10:19:41 Finished compiler/encoders/ag32                                   0s  90MB
Mar 14 10:19:41 Starting compiler/backend/x64
Mar 14 10:19:43 Finished compiler/backend/x64                                     0s 131MB
Mar 14 10:19:44 Starting compiler/backend/arm7
Mar 14 10:19:46 Finished compiler/backend/arm7                                    0s 131MB
Mar 14 10:19:47 Starting compiler/backend/arm8
Mar 14 10:19:49 Finished compiler/backend/arm8                                    0s 131MB
Mar 14 10:19:49 Starting compiler/backend/mips
Mar 14 10:19:51 Finished compiler/backend/mips                                    0s 131MB
Mar 14 10:19:52 Starting compiler/backend/riscv
Mar 14 10:19:54 Finished compiler/backend/riscv                                   0s 131MB
Mar 14 10:19:55 Starting compiler/backend/ag32
Mar 14 10:21:12 Finished compiler/backend/ag32                                 1m16s   2GB
Mar 14 10:21:13 Starting compiler/parsing/proofs
Mar 14 10:21:14 Finished compiler/parsing/proofs                                  0s  71MB
Mar 14 10:21:15 Starting compiler/inference/proofs
Mar 14 10:21:17 Finished compiler/inference/proofs                                1s 180MB
Mar 14 10:21:18 Starting compiler/backend/semantics
Mar 14 10:22:43 Finished compiler/backend/semantics                            1m24s   2GB
Mar 14 10:22:44 Starting compiler/backend/reg_alloc/proofs
Mar 14 10:22:46 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Mar 14 10:22:47 Starting compiler/backend/proofs
Mar 14 10:23:49 Finished compiler/backend/proofs                               1m01s   3GB
Mar 14 10:23:50 Starting compiler/backend/serialiser
Mar 14 10:23:52 Finished compiler/backend/serialiser                              0s 129MB
Mar 14 10:23:53 Starting compiler/encoders/x64/proofs
Mar 14 10:33:16 Finished compiler/encoders/x64/proofs                          9m22s   5GB
Mar 14 10:33:17 Starting compiler/encoders/arm7/proofs
Mar 14 10:45:59 Finished compiler/encoders/arm7/proofs                        12m41s   7GB
Mar 14 10:46:00 Starting compiler/encoders/arm8/proofs
Mar 14 10:52:23 Finished compiler/encoders/arm8/proofs                         6m21s   5GB
Mar 14 10:52:24 Starting compiler/encoders/arm8_asl/proofs
Mar 14 11:39:40 Finished compiler/encoders/arm8_asl/proofs                    47m15s  10GB
Mar 14 11:39:41 Starting compiler/encoders/mips/proofs
Mar 14 11:49:42 Finished compiler/encoders/mips/proofs                         9m59s   8GB
Mar 14 11:49:43 Starting compiler/encoders/riscv/proofs
Mar 14 11:58:07 Finished compiler/encoders/riscv/proofs                        8m23s   3GB
Mar 14 11:58:08 Starting compiler/encoders/ag32/proofs
Mar 14 12:00:29 Finished compiler/encoders/ag32/proofs                         2m19s   2GB
Mar 14 12:00:30 Starting compiler/backend/x64/proofs
Mar 14 12:01:10 Finished compiler/backend/x64/proofs                             38s   3GB
Mar 14 12:01:10 Starting compiler/backend/arm7/proofs
Mar 14 12:01:53 Finished compiler/backend/arm7/proofs                            41s   2GB
Mar 14 12:01:54 Starting compiler/backend/arm8/proofs
Mar 14 12:02:31 Finished compiler/backend/arm8/proofs                            36s   2GB
Mar 14 12:02:32 Starting compiler/backend/arm8_asl
Mar 14 12:03:01 Finished compiler/backend/arm8_asl                               27s   2GB
Mar 14 12:03:02 Starting compiler/backend/mips/proofs
Mar 14 12:03:45 Finished compiler/backend/mips/proofs                            41s   3GB
Mar 14 12:03:46 Starting compiler/backend/riscv/proofs
Mar 14 12:04:36 Finished compiler/backend/riscv/proofs                           49s   3GB
Mar 14 12:04:37 Starting compiler/backend/ag32/proofs
Mar 14 12:17:50 Finished compiler/backend/ag32/proofs                         13m12s   6GB
Mar 14 12:17:51 Starting candle/set-theory
Mar 14 12:18:36 Finished candle/set-theory                                       44s   1GB
Mar 14 12:18:37 Starting candle/syntax-lib
Mar 14 12:18:38 Finished candle/syntax-lib                                        0s  74MB
Mar 14 12:18:39 Starting candle/standard/syntax
Mar 14 12:18:55 Finished candle/standard/syntax                                  15s   1GB
Mar 14 12:18:56 Starting candle/standard/semantics
Mar 14 12:21:20 Finished candle/standard/semantics                             2m23s   2GB
Mar 14 12:21:21 Starting candle/standard/monadic
Mar 14 12:21:23 Finished candle/standard/monadic                                  0s  99MB
Mar 14 12:21:24 Starting candle/standard/ml_kernel
Mar 14 12:23:12 Finished candle/standard/ml_kernel                             1m47s   5GB
Mar 14 12:23:13 Starting candle/overloading/syntax
Mar 14 12:26:38 Finished candle/overloading/syntax                             3m23s   2GB
Mar 14 12:26:39 Starting candle/overloading/semantics
Mar 14 12:38:14 Finished candle/overloading/semantics                         11m34s   7GB
Mar 14 12:38:15 Starting candle/overloading/monadic
Mar 14 12:40:52 Finished candle/overloading/monadic                            2m35s   3GB
Mar 14 12:40:53 Starting candle/overloading/ml_kernel
Mar 14 12:48:38 Finished candle/overloading/ml_kernel                          7m43s   6GB
Mar 14 12:48:39 Starting candle/overloading/ml_checker
Mar 14 12:51:15 Finished candle/overloading/ml_checker                         2m35s   7GB
Mar 14 12:51:16 Starting candle/prover
Mar 14 13:01:13 Finished candle/prover                                         9m56s   5GB
Mar 14 13:01:14 Starting pancake
Mar 14 13:02:16 Finished pancake                                               1m00s   1GB
Mar 14 13:02:17 Starting pancake/ffi
Mar 14 13:02:18 Finished pancake/ffi                                              0s  23MB
Mar 14 13:02:19 Starting pancake/semantics
Mar 14 13:04:45 Finished pancake/semantics                                     2m25s   2GB
Mar 14 13:04:46 Starting pancake/parser
Mar 14 13:05:13 Finished pancake/parser                                          25s   2GB
Mar 14 13:05:14 Starting pancake/proofs
Mar 14 13:35:14 Finished pancake/proofs                                       29m59s   8GB
Mar 14 13:35:15 Starting characteristic/examples
Mar 14 13:36:51 Finished characteristic/examples                               1m35s   5GB
Mar 14 13:36:52 Starting tutorial/solutions
Mar 14 13:52:58 Finished tutorial/solutions                                   16m04s  24GB
Mar 14 13:52:59 Starting translator/monadic/examples
Mar 14 13:56:41 Finished translator/monadic/examples                           3m41s   5GB
Mar 14 13:56:42 Starting examples
Mar 14 14:11:10 Finished examples                                             14m27s   7GB
Mar 14 14:11:11 Starting examples/compilation/x64
Mar 14 16:07:35 Finished examples/compilation/x64                           1h56m22s  39GB
Mar 14 16:07:36 Starting examples/compilation/x64/proofs
Mar 14 16:11:24 Finished examples/compilation/x64/proofs                       3m47s   6GB
Mar 14 16:11:25 Starting examples/compilation/ag32
Mar 14 16:40:56 Finished examples/compilation/ag32                            29m29s  12GB
Mar 14 16:40:56 Starting examples/compilation/ag32/proofs
Mar 14 16:42:27 Finished examples/compilation/ag32/proofs                      1m30s   6GB
Mar 14 16:42:28 Starting examples/compilation/to_word
Mar 14 16:46:16 Finished examples/compilation/to_word                          3m46s  12GB
Mar 14 16:46:17 Starting examples/lpr_checker
Mar 14 16:47:32 Finished examples/lpr_checker                                  1m14s   2GB
Mar 14 16:47:33 Starting examples/lpr_checker/array
Mar 14 17:17:52 Finished examples/lpr_checker/array                           30m17s  24GB
Mar 14 17:17:53 Starting examples/lpr_checker/array/compilation
Mar 14 17:57:35 Finished examples/lpr_checker/array/compilation               39m41s  77GB
Mar 14 17:57:35 Starting examples/lpr_checker/array/compilation/proofs
Mar 14 17:59:15 Finished examples/lpr_checker/array/compilation/proofs         1m38s   8GB
Mar 14 17:59:16 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 14 18:10:49 Finished examples/lpr_checker/array/compilation/proofsARM8    11m32s  33GB
Mar 14 18:10:50 Starting examples/xlrup_checker
Mar 14 18:11:58 Finished examples/xlrup_checker                                1m07s   1GB
Mar 14 18:11:59 Starting examples/xlrup_checker/array
Mar 14 18:28:07 Finished examples/xlrup_checker/array                         16m06s   7GB
Mar 14 18:28:08 Starting examples/xlrup_checker/array/compilation
Mar 14 18:49:27 Finished examples/xlrup_checker/array/compilation             21m18s  36GB
Mar 14 18:49:28 Starting examples/xlrup_checker/array/compilation/proofs
Mar 14 18:50:57 Finished examples/xlrup_checker/array/compilation/proofs       1m28s   6GB
Mar 14 18:50:58 Starting examples/pseudo_bool
Mar 14 18:53:01 Finished examples/pseudo_bool                                  2m01s   2GB
Mar 14 18:53:02 Starting examples/pseudo_bool/cnf_encoding
Mar 14 18:53:37 Finished examples/pseudo_bool/cnf_encoding                       34s   1GB
Mar 14 18:53:38 Starting examples/pseudo_bool/graph_encoding
Mar 14 18:54:25 Finished examples/pseudo_bool/graph_encoding                     45s   1GB
Mar 14 18:54:26 Starting examples/pseudo_bool/array
Mar 14 19:57:31 Finished examples/pseudo_bool/array                         1h03m04s  38GB
Mar 14 19:57:32 Starting examples/pseudo_bool/array/compilation
Mar 15 03:12:51 Finished examples/pseudo_bool/array/compilation             7h15m18s 133GB
Mar 15 03:12:52 Starting examples/pseudo_bool/array/compilation/proofs
Mar 15 03:16:08 Finished examples/pseudo_bool/array/compilation/proofs         3m15s   7GB
Mar 15 03:16:09 Starting examples/opentheory
Mar 15 03:26:40 Finished examples/opentheory                                  10m30s   8GB
Mar 15 03:26:41 Starting examples/opentheory
Mar 15 03:26:43 Finished examples/opentheory                                      0s 122MB
Mar 15 03:26:44 Starting examples/opentheory/compilation
Mar 15 04:02:33 Finished examples/opentheory/compilation                      35m47s  50GB
Mar 15 04:02:34 Starting examples/opentheory/compilation/proofs
Mar 15 04:04:02 Finished examples/opentheory/compilation/proofs                1m27s   6GB
Mar 15 04:04:03 Starting examples/opentheory/compilation/ag32
Mar 15 04:35:34 Finished examples/opentheory/compilation/ag32                 31m30s  36GB
Mar 15 04:35:35 Starting examples/opentheory/compilation/ag32/proofs
Mar 15 04:37:50 Finished examples/opentheory/compilation/ag32/proofs           2m14s  11GB
Mar 15 04:37:51 Starting examples/sat_encodings
Mar 15 04:40:24 Finished examples/sat_encodings                                2m32s   1GB
Mar 15 04:40:25 Starting examples/sat_encodings/case_studies
Mar 15 04:42:24 Finished examples/sat_encodings/case_studies                   1m58s   2GB
Mar 15 04:42:25 Starting examples/sat_encodings/translation
Mar 15 04:48:27 Finished examples/sat_encodings/translation                    6m01s   7GB
Mar 15 04:48:28 Starting examples/sat_encodings/translation/compilation
Mar 15 05:24:19 Finished examples/sat_encodings/translation/compilation       35m50s  37GB
Mar 15 05:24:20 Starting examples/deflate
Mar 15 05:25:36 Finished examples/deflate                                      1m15s   1GB
Mar 15 05:25:37 Starting examples/deflate/translation
Mar 15 05:27:15 Finished examples/deflate/translation                          1m37s   7GB
Mar 15 05:27:16 Starting examples/deflate/translation/compilation
Mar 15 05:44:02 Finished examples/deflate/translation/compilation             16m44s  22GB
Mar 15 05:44:02 Starting examples/vipr
Mar 15 05:48:04 Finished examples/vipr                                         4m00s   7GB
Mar 15 05:48:05 Starting examples/vipr/compilation
Mar 15 06:08:23 Finished examples/vipr/compilation                            20m16s  44GB
Mar 15 06:08:23 Starting translator/okasaki-examples
Mar 15 06:13:22 Finished translator/okasaki-examples                           4m57s   4GB
Mar 15 06:13:23 Starting translator/other-examples
Mar 15 06:18:06 Finished translator/other-examples                             4m41s   3GB
Mar 15 06:18:07 Starting compiler/parsing/tests
Mar 15 06:18:40 Finished compiler/parsing/tests                                  32s   1GB
Mar 15 06:18:41 Starting compiler/inference/tests
Mar 15 06:19:20 Finished compiler/inference/tests                                37s   2GB
Mar 15 06:19:21 Starting compiler/printing/test
Mar 15 06:20:08 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                                                 (39s)FAIL<1>
 /scratch/cakeml/regression2/cakeml-2338/compiler/printing/test/printingTestScript.sml:11: error: Structure (inferenceComputeLib) has not been declared
 Found near
   open preamble basicComputeLib inferenceComputeLib basisTypeCheckTheory
 error in quse /scratch/cakeml/regression2/cakeml-2338/compiler/printing/test/printingTestScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression2/cakeml-2338/compiler/printing/test/printingTestScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"