Job 2336

CakeML:e0805b2e1acacb92de6b63dea47d6f1a6b6c1217
  Avoid a huge Theory.sig file [Mar 12 13:30:03]
#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 12 13:37:50 Claimed job
Mar 12 13:37:58 Building HOL
Mar 12 13:51:05 Starting developers
Mar 12 13:51:10 Finished developers                                               5s  96MB
Mar 12 13:51:10 Starting developers/bin
Mar 12 13:51:16 Finished developers/bin                                           5s   1GB
Mar 12 13:51:16 Starting compiler/proofs
Mar 12 15:45:22 Finished compiler/proofs                                    1h54m05s  25GB
Mar 12 15:45:22 Starting compiler/bootstrap/translation
Mar 12 23:55:36 Finished compiler/bootstrap/translation                     8h10m14s  43GB
Mar 12 23:55:36 Starting semantics/ffi
Mar 12 23:55:42 Finished semantics/ffi                                            5s 212MB
Mar 12 23:55:42 Starting semantics
Mar 12 23:55:44 Finished semantics                                                1s  20MB
Mar 12 23:55:44 Starting semantics/proofs
Mar 12 23:56:16 Finished semantics/proofs                                        32s 818MB
Mar 12 23:56:16 Starting semantics/alt_semantics
Mar 12 23:56:48 Finished semantics/alt_semantics                                 32s 761MB
Mar 12 23:56:49 Starting semantics/alt_semantics/proofs
Mar 13 00:08:49 Finished semantics/alt_semantics/proofs                       11m59s   1GB
Mar 13 00:08:49 Starting basis/pure
Mar 13 00:08:50 Finished basis/pure                                               1s  23MB
Mar 13 00:08:50 Starting translator
Mar 13 00:10:41 Finished translator                                            1m50s   1GB
Mar 13 00:10:41 Starting compiler/parsing
Mar 13 00:10:43 Finished compiler/parsing                                         1s  19MB
Mar 13 00:10:43 Starting characteristic
Mar 13 00:10:45 Finished characteristic                                           1s  24MB
Mar 13 00:10:45 Starting translator/monadic
Mar 13 00:10:47 Finished translator/monadic                                       1s  26MB
Mar 13 00:10:47 Starting basis
Mar 13 00:14:31 Finished basis                                                 3m44s   2GB
Mar 13 00:14:31 Starting compiler/inference
Mar 13 00:14:34 Finished compiler/inference                                       2s  33MB
Mar 13 00:14:34 Starting compiler/backend/reg_alloc
Mar 13 00:14:36 Finished compiler/backend/reg_alloc                               1s  22MB
Mar 13 00:14:36 Starting compiler/backend/gc
Mar 13 00:14:38 Finished compiler/backend/gc                                      2s  23MB
Mar 13 00:14:38 Starting compiler/backend
Mar 13 00:14:51 Finished compiler/backend                                        12s 769MB
Mar 13 00:14:51 Starting compiler/encoders/asm
Mar 13 00:14:53 Finished compiler/encoders/asm                                    1s  23MB
Mar 13 00:14:53 Starting compiler/encoders/x64
Mar 13 00:14:55 Finished compiler/encoders/x64                                    1s  21MB
Mar 13 00:14:55 Starting compiler/encoders/arm7
Mar 13 00:14:57 Finished compiler/encoders/arm7                                   1s  25MB
Mar 13 00:14:57 Starting compiler/encoders/arm8
Mar 13 00:14:59 Finished compiler/encoders/arm8                                   1s  24MB
Mar 13 00:14:59 Starting compiler/encoders/arm8_asl
Mar 13 02:42:50 Finished compiler/encoders/arm8_asl                         2h27m51s  49GB
Mar 13 02:42:50 Starting compiler/encoders/mips
Mar 13 02:42:52 Finished compiler/encoders/mips                                   1s  23MB
Mar 13 02:42:52 Starting compiler/encoders/riscv
Mar 13 02:42:54 Finished compiler/encoders/riscv                                  1s  25MB
Mar 13 02:42:54 Starting compiler/encoders/ag32
Mar 13 02:42:56 Finished compiler/encoders/ag32                                   1s  21MB
Mar 13 02:42:56 Starting compiler/backend/x64
Mar 13 02:42:58 Finished compiler/backend/x64                                     2s  28MB
Mar 13 02:42:58 Starting compiler/backend/arm7
Mar 13 02:43:00 Finished compiler/backend/arm7                                    2s  28MB
Mar 13 02:43:01 Starting compiler/backend/arm8
Mar 13 02:43:03 Finished compiler/backend/arm8                                    2s  26MB
Mar 13 02:43:03 Starting compiler/backend/mips
Mar 13 02:43:05 Finished compiler/backend/mips                                    2s  25MB
Mar 13 02:43:05 Starting compiler/backend/riscv
Mar 13 02:43:07 Finished compiler/backend/riscv                                   2s  24MB
Mar 13 02:43:08 Starting compiler/backend/ag32
Mar 13 02:44:33 Finished compiler/backend/ag32                                 1m25s   1GB
Mar 13 02:44:33 Starting compiler/parsing/proofs
Mar 13 02:44:34 Finished compiler/parsing/proofs                                  1s  18MB
Mar 13 02:44:35 Starting compiler/inference/proofs
Mar 13 02:44:37 Finished compiler/inference/proofs                                2s  35MB
Mar 13 02:44:37 Starting compiler/backend/semantics
Mar 13 02:45:53 Finished compiler/backend/semantics                            1m15s   1GB
Mar 13 02:45:53 Starting compiler/backend/reg_alloc/proofs
Mar 13 02:45:55 Finished compiler/backend/reg_alloc/proofs                        1s  27MB
Mar 13 02:45:55 Starting compiler/backend/proofs
Mar 13 02:46:55 Finished compiler/backend/proofs                               1m00s   3GB
Mar 13 02:46:55 Starting compiler/backend/serialiser
Mar 13 02:46:57 Finished compiler/backend/serialiser                              2s  24MB
Mar 13 02:46:57 Starting compiler/encoders/x64/proofs
Mar 13 02:56:47 Finished compiler/encoders/x64/proofs                          9m49s   6GB
Mar 13 02:56:47 Starting compiler/encoders/arm7/proofs
Mar 13 03:10:38 Finished compiler/encoders/arm7/proofs                        13m51s   3GB
Mar 13 03:10:38 Starting compiler/encoders/arm8/proofs
Mar 13 03:17:42 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Mar 13 03:17:42 Starting compiler/encoders/arm8_asl/proofs
Mar 13 04:10:17 Finished compiler/encoders/arm8_asl/proofs                    52m34s   7GB
Mar 13 04:10:17 Starting compiler/encoders/mips/proofs
Mar 13 04:20:48 Finished compiler/encoders/mips/proofs                        10m31s   2GB
Mar 13 04:20:48 Starting compiler/encoders/riscv/proofs
Mar 13 04:29:51 Finished compiler/encoders/riscv/proofs                        9m02s   1GB
Mar 13 04:29:51 Starting compiler/encoders/ag32/proofs
Mar 13 04:32:23 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Mar 13 04:32:23 Starting compiler/backend/x64/proofs
Mar 13 04:32:53 Finished compiler/backend/x64/proofs                             28s   1GB
Mar 13 04:32:53 Starting compiler/backend/arm7/proofs
Mar 13 04:33:25 Finished compiler/backend/arm7/proofs                            31s   1GB
Mar 13 04:33:25 Starting compiler/backend/arm8/proofs
Mar 13 04:33:55 Finished compiler/backend/arm8/proofs                            29s   1GB
Mar 13 04:33:55 Starting compiler/backend/arm8_asl
Mar 13 04:34:20 Finished compiler/backend/arm8_asl                               24s   1GB
Mar 13 04:34:20 Starting compiler/backend/mips/proofs
Mar 13 04:34:52 Finished compiler/backend/mips/proofs                            32s   1GB
Mar 13 04:34:52 Starting compiler/backend/riscv/proofs
Mar 13 04:35:27 Finished compiler/backend/riscv/proofs                           34s   2GB
Mar 13 04:35:27 Starting compiler/backend/ag32/proofs
Mar 13 04:49:28 Finished compiler/backend/ag32/proofs                         14m01s   3GB
Mar 13 04:49:28 Starting candle/set-theory
Mar 13 04:50:06 Finished candle/set-theory                                       38s   1GB
Mar 13 04:50:07 Starting candle/syntax-lib
Mar 13 04:50:08 Finished candle/syntax-lib                                        1s  19MB
Mar 13 04:50:08 Starting candle/standard/syntax
Mar 13 04:50:19 Finished candle/standard/syntax                                  10s 733MB
Mar 13 04:50:19 Starting candle/standard/semantics
Mar 13 04:52:18 Finished candle/standard/semantics                             1m58s   1GB
Mar 13 04:52:18 Starting candle/standard/monadic
Mar 13 04:52:20 Finished candle/standard/monadic                                  1s  20MB
Mar 13 04:52:20 Starting candle/standard/ml_kernel
Mar 13 04:54:01 Finished candle/standard/ml_kernel                             1m40s   3GB
Mar 13 04:54:01 Starting candle/overloading/syntax
Mar 13 04:57:22 Finished candle/overloading/syntax                             3m20s   1GB
Mar 13 04:57:22 Starting candle/overloading/semantics
Mar 13 05:09:52 Finished candle/overloading/semantics                         12m30s   2GB
Mar 13 05:09:52 Starting candle/overloading/monadic
Mar 13 05:12:38 Finished candle/overloading/monadic                            2m45s   2GB
Mar 13 05:12:38 Starting candle/overloading/ml_kernel
Mar 13 05:20:40 Finished candle/overloading/ml_kernel                          8m02s   3GB
Mar 13 05:20:41 Starting candle/overloading/ml_checker
Mar 13 05:23:18 Finished candle/overloading/ml_checker                         2m37s   2GB
Mar 13 05:23:18 Starting candle/prover
Mar 13 05:33:19 Finished candle/prover                                        10m00s   3GB
Mar 13 05:33:19 Starting pancake
Mar 13 05:34:05 Finished pancake                                                 45s 900MB
Mar 13 05:34:05 Starting pancake/ffi
Mar 13 05:34:05 Finished pancake/ffi                                              0s  13MB
Mar 13 05:34:05 Starting pancake/semantics
Mar 13 05:36:33 Finished pancake/semantics                                     2m26s   1GB
Mar 13 05:36:33 Starting pancake/parser
Mar 13 05:36:57 Finished pancake/parser                                          23s   1GB
Mar 13 05:36:57 Starting pancake/proofs
Mar 13 06:10:07 Finished pancake/proofs                                       33m10s   5GB
Mar 13 06:10:07 Starting characteristic/examples
Mar 13 06:11:42 Finished characteristic/examples                               1m34s   3GB
Mar 13 06:11:42 Starting tutorial/solutions
Mar 13 06:13:22 FAILED: tutorial/solutions
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[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/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/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$(CAKEMLDIR)/compiler/backend/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$(CAKEMLDIR)/compiler/backend/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$(CAKEMLDIR)/compiler/backend/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$(CAKEMLDIR)/compiler/backend/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/x64[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$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/cv_compute[0m
Scanning [1m$(CAKEMLDIR)/cv_translator[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Scanned 90 directories
Finished $(CAKEMLDIR)/compiler                                                                                                                                                                                                       (0.000s) 
Starting work on README.md
Starting work on make_ex
Starting work on simple_bstTheory
Starting work on splitwordsTheory
README.md                                                                                                                                                                                                     tutorial/solutions  (0s)     OK
make_ex                                                                                                                                                                                                       tutorial/solutions  (0s)     OK
Starting work on exercises
exercises                                                                                                                                                                                                     tutorial/solutions  (0s)     OK
splitwordsTheory                                                                                                                                                                                              tutorial/solutions (11s)     OK
Starting work on wordfreqProgTheory
simple_bstTheory                                                                                                                                                                                              tutorial/solutions (12s)     OK
wordfreqProgTheory                                                                                                                                                                                            tutorial/solutions (75s)     OK
Starting work on wordfreqCompileTheory
wordfreqCompileTheory                                                                                                                                                                                         tutorial/solutions  (4s)FAIL<1>
 Found near
   [
      mlstringTheory.implode_def,
      mlstringTheory.str_def,
      mlstringTheory.concat_thm,
      mlstringTheory.explode_thm,
      mloptionTheory.getOpt_def,
      ...
      ]
 Uncaught exception: Fail "Static Errors"