Job 1082

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:98729fa718256b0fa48d19ca8a978029674fe5a9
  Clean an AKS theory for --expk; examples/AKS now builds there [Nov 11 23:10:55]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 12 23:54:24 Claimed job
Nov 12 23:54:29 Building HOL
Nov 13 00:04:03 Starting developers
Nov 13 00:04:04 Finished developers                                               0s  21MB
Nov 13 00:04:04 Starting developers/bin
Nov 13 00:04:08 Finished developers/bin                                           3s 164MB
Nov 13 00:04:08 Starting semantics/ffi
Nov 13 00:04:16 Finished semantics/ffi                                            7s 231MB
Nov 13 00:04:16 Starting semantics
Nov 13 00:05:40 Finished semantics                                             1m23s   1GB
Nov 13 00:05:41 Starting semantics/proofs
Nov 13 00:08:42 Finished semantics/proofs                                      3m01s   1GB
Nov 13 00:08:42 Starting semantics/alt_semantics
Nov 13 00:08:49 Finished semantics/alt_semantics                                  6s 282MB
Nov 13 00:08:49 Starting semantics/alt_semantics/proofs
Nov 13 00:10:38 Finished semantics/alt_semantics/proofs                        1m48s 704MB
Nov 13 00:10:38 Starting basis/pure
Nov 13 00:13:31 Finished basis/pure                                            2m52s 915MB
Nov 13 00:13:32 Starting translator
Nov 13 00:15:22 Finished translator                                            1m49s   1GB
Nov 13 00:15:22 Starting compiler/parsing
Nov 13 00:16:22 Finished compiler/parsing                                        59s   2GB
Nov 13 00:16:22 Starting characteristic
Nov 13 00:21:35 Finished characteristic                                        5m12s   2GB
Nov 13 00:21:35 Starting translator/monadic
Nov 13 00:23:02 Finished translator/monadic                                    1m27s   1GB
Nov 13 00:23:03 Starting basis
Nov 13 00:42:45 Finished basis                                                19m41s   2GB
Nov 13 00:42:45 Starting compiler/inference
Nov 13 00:44:31 Finished compiler/inference                                    1m45s   1GB
Nov 13 00:44:31 Starting compiler/backend/reg_alloc
Nov 13 00:45:31 Finished compiler/backend/reg_alloc                              59s   1GB
Nov 13 00:45:32 Starting compiler/backend/gc
Nov 13 00:48:48 Finished compiler/backend/gc                                   3m15s   1GB
Nov 13 00:48:48 Starting compiler/backend
Nov 13 00:52:33 Finished compiler/backend                                      3m44s   2GB
Nov 13 00:52:33 Starting compiler/encoders/asm
Nov 13 00:52:53 Finished compiler/encoders/asm                                   18s 794MB
Nov 13 00:52:53 Starting compiler/encoders/x64
Nov 13 00:53:45 Finished compiler/encoders/x64                                   51s 675MB
Nov 13 00:53:46 Starting compiler/encoders/arm7
Nov 13 00:55:23 Finished compiler/encoders/arm7                                1m37s   1GB
Nov 13 00:55:24 Starting compiler/encoders/arm8
Nov 13 00:55:54 Finished compiler/encoders/arm8                                  30s 539MB
Nov 13 00:55:54 Starting compiler/encoders/mips
Nov 13 00:56:59 Finished compiler/encoders/mips                                1m04s 811MB
Nov 13 00:56:59 Starting compiler/encoders/riscv
Nov 13 00:58:19 Finished compiler/encoders/riscv                               1m19s 798MB
Nov 13 00:58:19 Starting compiler/encoders/ag32
Nov 13 00:58:35 Finished compiler/encoders/ag32                                  15s 782MB
Nov 13 00:58:35 Starting compiler/backend/x64
Nov 13 00:58:51 Finished compiler/backend/x64                                    16s   1GB
Nov 13 00:58:52 Starting compiler/backend/arm7
Nov 13 00:59:10 Finished compiler/backend/arm7                                   17s   1GB
Nov 13 00:59:10 Starting compiler/backend/arm8
Nov 13 00:59:26 Finished compiler/backend/arm8                                   15s 965MB
Nov 13 00:59:26 Starting compiler/backend/mips
Nov 13 00:59:43 Finished compiler/backend/mips                                   16s   1GB
Nov 13 00:59:44 Starting compiler/backend/riscv
Nov 13 01:00:01 Finished compiler/backend/riscv                                  17s   1GB
Nov 13 01:00:02 Starting compiler/backend/ag32
Nov 13 01:01:09 Finished compiler/backend/ag32                                 1m06s   1GB
Nov 13 01:01:09 Starting compiler/parsing/proofs
Nov 13 01:06:48 Finished compiler/parsing/proofs                               5m39s 827MB
Nov 13 01:06:49 Starting compiler/inference/proofs
Nov 13 01:09:31 Finished compiler/inference/proofs                             2m42s 924MB
Nov 13 01:09:31 Starting compiler/backend/semantics
Nov 13 01:15:43 Finished compiler/backend/semantics                            6m11s   2GB
Nov 13 01:15:44 Starting compiler/backend/reg_alloc/proofs
Nov 13 01:19:03 Finished compiler/backend/reg_alloc/proofs                     3m18s 771MB
Nov 13 01:19:03 Starting compiler/backend/proofs
Nov 13 02:00:44 Finished compiler/backend/proofs                              41m40s   3GB
Nov 13 02:00:44 Starting compiler/encoders/x64/proofs
Nov 13 02:10:08 Finished compiler/encoders/x64/proofs                          9m23s   4GB
Nov 13 02:10:08 Starting compiler/encoders/arm7/proofs
Nov 13 02:23:05 Finished compiler/encoders/arm7/proofs                        12m56s   3GB
Nov 13 02:23:06 Starting compiler/encoders/arm8/proofs
Nov 13 02:29:23 Finished compiler/encoders/arm8/proofs                         6m17s   1GB
Nov 13 02:29:23 Starting compiler/encoders/mips/proofs
Nov 13 02:39:03 Finished compiler/encoders/mips/proofs                         9m38s   2GB
Nov 13 02:39:03 Starting compiler/encoders/riscv/proofs
Nov 13 02:47:30 Finished compiler/encoders/riscv/proofs                        8m26s   1GB
Nov 13 02:47:30 Starting compiler/encoders/ag32/proofs
Nov 13 02:49:58 Finished compiler/encoders/ag32/proofs                         2m26s 750MB
Nov 13 02:49:58 Starting compiler/backend/x64/proofs
Nov 13 02:50:15 Finished compiler/backend/x64/proofs                             16s   1GB
Nov 13 02:50:16 Starting compiler/backend/arm7/proofs
Nov 13 02:50:35 Finished compiler/backend/arm7/proofs                            18s   1GB
Nov 13 02:50:35 Starting compiler/backend/arm8/proofs
Nov 13 02:50:52 Finished compiler/backend/arm8/proofs                            16s   1GB
Nov 13 02:50:52 Starting compiler/backend/mips/proofs
Nov 13 02:51:10 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 13 02:51:11 Starting compiler/backend/riscv/proofs
Nov 13 02:51:29 Finished compiler/backend/riscv/proofs                           17s   1GB
Nov 13 02:51:29 Starting compiler/backend/ag32/proofs
Nov 13 03:00:43 Finished compiler/backend/ag32/proofs                          9m13s   2GB
Nov 13 03:00:43 Starting compiler/proofs
Nov 13 03:02:21 Finished compiler/proofs                                       1m37s   2GB
Nov 13 03:02:21 Starting candle/set-theory
Nov 13 03:02:48 Finished candle/set-theory                                       26s 679MB
Nov 13 03:02:48 Starting candle/syntax-lib
Nov 13 03:02:57 Finished candle/syntax-lib                                        9s 708MB
Nov 13 03:02:58 Starting candle/standard/syntax
Nov 13 03:04:40 Finished candle/standard/syntax                                1m42s 945MB
Nov 13 03:04:41 Starting candle/standard/semantics
Nov 13 03:06:15 Finished candle/standard/semantics                             1m34s   1GB
Nov 13 03:06:16 Starting candle/standard/monadic
Nov 13 03:07:49 Finished candle/standard/monadic                               1m32s   1GB
Nov 13 03:07:49 Starting candle/standard/ml_kernel
Nov 13 03:11:50 Finished candle/standard/ml_kernel                             4m00s   6GB
Nov 13 03:11:50 Starting candle/standard/opentheory
Nov 13 03:20:31 Finished candle/standard/opentheory                            8m40s   4GB
Nov 13 03:20:31 Starting candle/standard/opentheory/compilation
Nov 13 03:50:48 Finished candle/standard/opentheory/compilation               30m16s  19GB
Nov 13 03:50:48 Starting candle/standard/opentheory/compilation/proofs
Nov 13 03:51:27 Finished candle/standard/opentheory/compilation/proofs           38s   3GB
Nov 13 03:51:27 Starting characteristic/examples
Nov 13 03:52:57 Finished characteristic/examples                               1m29s   2GB
Nov 13 03:52:58 Starting tutorial/solutions
Nov 13 04:06:13 Finished tutorial/solutions                                   13m15s   7GB
Nov 13 04:06:14 Starting translator/monadic/examples
Nov 13 04:09:11 Finished translator/monadic/examples                           2m56s   2GB
Nov 13 04:09:11 Starting examples
Nov 13 04:09:41 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 regexp_parserTheory
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
lcsTheory                                                                                                                                           real:   14s  user:   13s     OK
Starting work on diffTheory
regexp_parserTheory                                                                                                                                 real:   14s  user:   13s     OK
Starting work on divTheory
diffTheory                                                                                                                                          real:   14s  user:   13sFAIL<1>
           (strlen (ml_num_toString n) + (strlen (ml_num_toString n') + 1)))) =
     #"a"
 
 Failed to prove theorem parse_header_cancel.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/myreen/regression/cakeml-1082/examples/diffScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1082/examples/diffScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
quicksortProgTheory                                                                                                                                                         M-KILLED
catProgTheory                                                                                                                                                               M-KILLED
divTheory                                                                                                                                                                   M-KILLED