Job 1075

CakeML:5b4a50112136b93e58c86f4bc8beb12c388c3bd1
  merge with master [Nov 11 14:32:54]
#701 (strlit-implode)
Merging into:a0a73be366a40123567f97a747fbaffa114b6352
  Merge pull request #700 from CakeML/iocatprog-fix [Nov 10 16:39:33]
HOL:63cafe0c6fe8ccc9745d4df57ceeeed75f009fc2
  Holmake: prevent starred dependencies from spawning 2 jobs [Nov 05 03:23:34]
Machine:oven3 4.19.67.1.amd64-smp

Nov 11 14:51:48 Claimed job
Nov 11 14:51:53 Reusing HOL
Nov 11 14:52:50 Starting developers
Nov 11 14:52:57 Finished developers                                               6s 125MB
Nov 11 14:52:57 Starting developers/bin
Nov 11 14:53:10 Finished developers/bin                                          13s 972MB
Nov 11 14:53:10 Starting semantics/ffi
Nov 11 14:53:32 Finished semantics/ffi                                           21s 258MB
Nov 11 14:53:32 Starting semantics
Nov 11 14:56:09 Finished semantics                                             2m36s   1GB
Nov 11 14:56:09 Starting semantics/proofs
Nov 11 15:02:46 Finished semantics/proofs                                      6m36s   1GB
Nov 11 15:02:46 Starting semantics/alt_semantics
Nov 11 15:03:04 Finished semantics/alt_semantics                                 17s 295MB
Nov 11 15:03:04 Starting semantics/alt_semantics/proofs
Nov 11 15:06:56 Finished semantics/alt_semantics/proofs                        3m51s 859MB
Nov 11 15:06:56 Starting basis/pure
Nov 11 15:08:38 Finished basis/pure                                            1m40s 726MB
Nov 11 15:08:38 Starting translator
Nov 11 15:12:26 Finished translator                                            3m47s   1GB
Nov 11 15:12:26 Starting compiler/parsing
Nov 11 15:14:23 Finished compiler/parsing                                      1m56s   1GB
Nov 11 15:14:23 Starting characteristic
Nov 11 15:25:52 Finished characteristic                                       11m28s   1GB
Nov 11 15:25:52 Starting translator/monadic
Nov 11 15:28:59 Finished translator/monadic                                    3m06s   1GB
Nov 11 15:28:59 Starting basis
Nov 11 16:10:26 Finished basis                                                41m26s   2GB
Nov 11 16:10:26 Starting compiler/inference
Nov 11 16:13:57 Finished compiler/inference                                    3m31s   1GB
Nov 11 16:13:57 Starting compiler/backend/reg_alloc
Nov 11 16:15:49 Finished compiler/backend/reg_alloc                            1m51s   1GB
Nov 11 16:15:49 Starting compiler/backend/gc
Nov 11 16:21:43 Finished compiler/backend/gc                                   5m53s   2GB
Nov 11 16:21:44 Starting compiler/backend
Nov 11 16:28:41 Finished compiler/backend                                      6m57s   2GB
Nov 11 16:28:41 Starting compiler/encoders/asm
Nov 11 16:29:26 Finished compiler/encoders/asm                                   44s 817MB
Nov 11 16:29:26 Starting compiler/encoders/x64
Nov 11 16:30:21 Finished compiler/encoders/x64                                   55s 746MB
Nov 11 16:30:22 Starting compiler/encoders/arm7
Nov 11 16:32:09 Finished compiler/encoders/arm7                                1m47s 701MB
Nov 11 16:32:10 Starting compiler/encoders/arm8
Nov 11 16:32:39 Finished compiler/encoders/arm8                                  28s 609MB
Nov 11 16:32:39 Starting compiler/encoders/mips
Nov 11 16:33:15 Finished compiler/encoders/mips                                  36s 956MB
Nov 11 16:33:15 Starting compiler/encoders/riscv
Nov 11 16:33:46 Finished compiler/encoders/riscv                                 30s 943MB
Nov 11 16:33:47 Starting compiler/encoders/ag32
Nov 11 16:34:22 Finished compiler/encoders/ag32                                  35s 561MB
Nov 11 16:34:22 Starting compiler/backend/x64
Nov 11 16:34:59 Finished compiler/backend/x64                                    36s   1GB
Nov 11 16:34:59 Starting compiler/backend/arm7
Nov 11 16:35:37 Finished compiler/backend/arm7                                   37s   1GB
Nov 11 16:35:38 Starting compiler/backend/arm8
Nov 11 16:36:15 Finished compiler/backend/arm8                                   36s   1GB
Nov 11 16:36:15 Starting compiler/backend/mips
Nov 11 16:36:51 Finished compiler/backend/mips                                   35s   1GB
Nov 11 16:36:51 Starting compiler/backend/riscv
Nov 11 16:37:29 Finished compiler/backend/riscv                                  37s   1GB
Nov 11 16:37:29 Starting compiler/backend/ag32
Nov 11 16:39:47 Finished compiler/backend/ag32                                 2m17s   1GB
Nov 11 16:39:47 Starting compiler/parsing/proofs
Nov 11 16:51:47 Finished compiler/parsing/proofs                              11m59s   1GB
Nov 11 16:51:47 Starting compiler/inference/proofs
Nov 11 16:58:06 Finished compiler/inference/proofs                             6m18s   1GB
Nov 11 16:58:06 Starting compiler/backend/semantics
Nov 11 17:09:51 Finished compiler/backend/semantics                           11m44s   1GB
Nov 11 17:09:51 Starting compiler/backend/reg_alloc/proofs
Nov 11 17:17:03 Finished compiler/backend/reg_alloc/proofs                     7m10s   1GB
Nov 11 17:17:03 Starting compiler/backend/proofs
Nov 11 18:33:28 Finished compiler/backend/proofs                            1h16m24s   4GB
Nov 11 18:33:28 Starting compiler/encoders/x64/proofs
Nov 11 18:53:57 Finished compiler/encoders/x64/proofs                         20m29s   4GB
Nov 11 18:53:58 Starting compiler/encoders/arm7/proofs
Nov 11 19:21:46 Finished compiler/encoders/arm7/proofs                        27m48s   3GB
Nov 11 19:21:46 Starting compiler/encoders/arm8/proofs
Nov 11 19:35:51 Finished compiler/encoders/arm8/proofs                        14m04s   1GB
Nov 11 19:35:51 Starting compiler/encoders/mips/proofs
Nov 11 19:57:01 Finished compiler/encoders/mips/proofs                        21m09s   2GB
Nov 11 19:57:01 Starting compiler/encoders/riscv/proofs
Nov 11 20:15:33 Finished compiler/encoders/riscv/proofs                       18m31s   1GB
Nov 11 20:15:33 Starting compiler/encoders/ag32/proofs
Nov 11 20:20:56 Finished compiler/encoders/ag32/proofs                         5m23s 913MB
Nov 11 20:20:57 Starting compiler/backend/x64/proofs
Nov 11 20:21:37 Finished compiler/backend/x64/proofs                             40s   1GB
Nov 11 20:21:37 Starting compiler/backend/arm7/proofs
Nov 11 20:22:17 Finished compiler/backend/arm7/proofs                            39s 857MB
Nov 11 20:22:17 Starting compiler/backend/arm8/proofs
Nov 11 20:22:58 Finished compiler/backend/arm8/proofs                            40s 787MB
Nov 11 20:22:59 Starting compiler/backend/mips/proofs
Nov 11 20:23:39 Finished compiler/backend/mips/proofs                            40s   1GB
Nov 11 20:23:39 Starting compiler/backend/riscv/proofs
Nov 11 20:24:18 Finished compiler/backend/riscv/proofs                           38s 849MB
Nov 11 20:24:18 Starting compiler/backend/ag32/proofs
Nov 11 20:43:25 Finished compiler/backend/ag32/proofs                         19m06s   2GB
Nov 11 20:43:25 Starting compiler/proofs
Nov 11 20:46:04 Finished compiler/proofs                                       2m38s   4GB
Nov 11 20:46:05 Starting candle/set-theory
Nov 11 20:47:00 Finished candle/set-theory                                       55s 735MB
Nov 11 20:47:00 Starting candle/syntax-lib
Nov 11 20:47:23 Finished candle/syntax-lib                                       22s 654MB
Nov 11 20:47:23 Starting candle/standard/syntax
Nov 11 20:51:02 Finished candle/standard/syntax                                3m39s   1GB
Nov 11 20:51:03 Starting candle/standard/semantics
Nov 11 20:54:37 Finished candle/standard/semantics                             3m34s   1GB
Nov 11 20:54:37 Starting candle/standard/monadic
Nov 11 20:58:01 Finished candle/standard/monadic                               3m24s   1GB
Nov 11 20:58:02 Starting candle/standard/ml_kernel
Nov 11 21:06:28 Finished candle/standard/ml_kernel                             8m25s   3GB
Nov 11 21:06:28 Starting candle/standard/opentheory
Nov 11 21:24:51 Finished candle/standard/opentheory                           18m22s   4GB
Nov 11 21:24:51 Starting candle/standard/opentheory/compilation
Nov 11 22:27:06 Finished candle/standard/opentheory/compilation             1h02m14s  17GB
Nov 11 22:27:06 Starting candle/standard/opentheory/compilation/proofs
Nov 11 22:28:38 Finished candle/standard/opentheory/compilation/proofs         1m31s   2GB
Nov 11 22:28:38 Starting characteristic/examples
Nov 11 22:31:40 Finished characteristic/examples                               3m01s   2GB
Nov 11 22:31:40 Starting tutorial/solutions
Nov 11 23:00:37 Finished tutorial/solutions                                   28m57s   7GB
Nov 11 23:00:38 Starting translator/monadic/examples
Nov 11 23:05:45 Finished translator/monadic/examples                           5m07s   2GB
Nov 11 23:05:45 Starting examples
Nov 11 23:06:39 FAILED: examples
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)/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/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
README.md                                                                                                                                                                          real:    0s  user:    0s     OK
Starting work on divTheory
lcsTheory                                                                                                                                                                          real:   26s  user:   24s     OK
Starting work on diffTheory
diffTheory                                                                                                                                                                         real:   23s  user:   21sFAIL<1>
          strsub (ml_num_toString n')
            (strlen l''  (strlen (ml_num_toString n) + 1))
      else
        strsub (str #"\n")
          (strlen l'' 
           (strlen (ml_num_toString n) + (strlen (ml_num_toString n') + 1)))) =
     #"a"
 
 Failed to prove theorem parse_header_cancel.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
quicksortProgTheory                                                                                                                                                                                        M-KILLED
catProgTheory                                                                                                                                                                                              M-KILLED
divTheory                                                                                                                                                                                                  M-KILLED