Job 1069

CakeML:dc73bd8f21601e06bdc92eb303865a3992673970
  Merge pull request #694 from CakeML/remove-oom [Oct 13 07:36:28]
HOL:63cafe0c6fe8ccc9745d4df57ceeeed75f009fc2
  Holmake: prevent starred dependencies from spawning 2 jobs [Nov 05 03:23:34]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Nov 06 00:32:17 Claimed job
Nov 06 00:32:23 Building HOL
Nov 06 00:42:39 Starting developers
Nov 06 00:42:43 Finished developers                                               3s 100MB
Nov 06 00:42:43 Starting developers/bin
Nov 06 00:42:49 Finished developers/bin                                           5s 964MB
Nov 06 00:42:49 Starting semantics/ffi
Nov 06 00:42:58 Finished semantics/ffi                                            8s 248MB
Nov 06 00:42:58 Starting semantics
Nov 06 00:44:20 Finished semantics                                             1m21s   1GB
Nov 06 00:44:20 Starting semantics/proofs
Nov 06 00:47:13 Finished semantics/proofs                                      2m53s   1GB
Nov 06 00:47:14 Starting semantics/alt_semantics
Nov 06 00:47:21 Finished semantics/alt_semantics                                  7s 291MB
Nov 06 00:47:21 Starting semantics/alt_semantics/proofs
Nov 06 00:49:05 Finished semantics/alt_semantics/proofs                        1m44s 708MB
Nov 06 00:49:05 Starting basis/pure
Nov 06 00:51:43 Finished basis/pure                                            2m37s 745MB
Nov 06 00:51:43 Starting translator
Nov 06 00:53:24 Finished translator                                            1m41s   1GB
Nov 06 00:53:24 Starting compiler/parsing
Nov 06 00:54:18 Finished compiler/parsing                                        54s   2GB
Nov 06 00:54:18 Starting characteristic
Nov 06 00:59:25 Finished characteristic                                        5m06s   1GB
Nov 06 00:59:25 Starting translator/monadic
Nov 06 01:00:49 Finished translator/monadic                                    1m24s   1GB
Nov 06 01:00:50 Starting basis
Nov 06 01:19:42 Finished basis                                                18m52s   2GB
Nov 06 01:19:43 Starting compiler/inference
Nov 06 01:21:22 Finished compiler/inference                                    1m39s   2GB
Nov 06 01:21:22 Starting compiler/backend/reg_alloc
Nov 06 01:22:20 Finished compiler/backend/reg_alloc                              57s   1GB
Nov 06 01:22:20 Starting compiler/backend/gc
Nov 06 01:25:21 Finished compiler/backend/gc                                   3m00s   1GB
Nov 06 01:25:21 Starting compiler/backend
Nov 06 01:28:47 Finished compiler/backend                                      3m25s   2GB
Nov 06 01:28:47 Starting compiler/encoders/asm
Nov 06 01:29:06 Finished compiler/encoders/asm                                   19s 818MB
Nov 06 01:29:06 Starting compiler/encoders/x64
Nov 06 01:29:58 Finished compiler/encoders/x64                                   51s 734MB
Nov 06 01:29:58 Starting compiler/encoders/arm7
Nov 06 01:31:31 Finished compiler/encoders/arm7                                1m33s   1GB
Nov 06 01:31:32 Starting compiler/encoders/arm8
Nov 06 01:32:02 Finished compiler/encoders/arm8                                  30s 585MB
Nov 06 01:32:02 Starting compiler/encoders/mips
Nov 06 01:33:06 Finished compiler/encoders/mips                                1m03s   1GB
Nov 06 01:33:06 Starting compiler/encoders/riscv
Nov 06 01:34:19 Finished compiler/encoders/riscv                               1m13s 757MB
Nov 06 01:34:19 Starting compiler/encoders/ag32
Nov 06 01:34:35 Finished compiler/encoders/ag32                                  15s 831MB
Nov 06 01:34:35 Starting compiler/backend/x64
Nov 06 01:34:52 Finished compiler/backend/x64                                    16s   1GB
Nov 06 01:34:52 Starting compiler/backend/arm7
Nov 06 01:35:10 Finished compiler/backend/arm7                                   17s   1GB
Nov 06 01:35:10 Starting compiler/backend/arm8
Nov 06 01:35:26 Finished compiler/backend/arm8                                   16s   1GB
Nov 06 01:35:26 Starting compiler/backend/mips
Nov 06 01:35:43 Finished compiler/backend/mips                                   16s   1GB
Nov 06 01:35:43 Starting compiler/backend/riscv
Nov 06 01:35:59 Finished compiler/backend/riscv                                  16s   1GB
Nov 06 01:35:59 Starting compiler/backend/ag32
Nov 06 01:37:01 Finished compiler/backend/ag32                                 1m01s   1GB
Nov 06 01:37:01 Starting compiler/parsing/proofs
Nov 06 01:42:29 Finished compiler/parsing/proofs                               5m27s   1GB
Nov 06 01:42:29 Starting compiler/inference/proofs
Nov 06 01:45:06 Finished compiler/inference/proofs                             2m37s   1GB
Nov 06 01:45:06 Starting compiler/backend/semantics
Nov 06 01:50:36 Finished compiler/backend/semantics                            5m29s   2GB
Nov 06 01:50:36 Starting compiler/backend/reg_alloc/proofs
Nov 06 01:53:43 Finished compiler/backend/reg_alloc/proofs                     3m06s 850MB
Nov 06 01:53:43 Starting compiler/backend/proofs
Nov 06 02:30:18 Finished compiler/backend/proofs                              36m34s   4GB
Nov 06 02:30:18 Starting compiler/encoders/x64/proofs
Nov 06 02:38:58 Finished compiler/encoders/x64/proofs                          8m38s   4GB
Nov 06 02:38:58 Starting compiler/encoders/arm7/proofs
Nov 06 02:50:32 Finished compiler/encoders/arm7/proofs                        11m34s   3GB
Nov 06 02:50:32 Starting compiler/encoders/arm8/proofs
Nov 06 02:56:24 Finished compiler/encoders/arm8/proofs                         5m52s   1GB
Nov 06 02:56:24 Starting compiler/encoders/mips/proofs
Nov 06 03:05:26 Finished compiler/encoders/mips/proofs                         9m01s   2GB
Nov 06 03:05:26 Starting compiler/encoders/riscv/proofs
Nov 06 03:13:19 Finished compiler/encoders/riscv/proofs                        7m53s   1GB
Nov 06 03:13:20 Starting compiler/encoders/ag32/proofs
Nov 06 03:15:36 Finished compiler/encoders/ag32/proofs                         2m16s 738MB
Nov 06 03:15:36 Starting compiler/backend/x64/proofs
Nov 06 03:15:53 Finished compiler/backend/x64/proofs                             16s 977MB
Nov 06 03:15:53 Starting compiler/backend/arm7/proofs
Nov 06 03:16:10 Finished compiler/backend/arm7/proofs                            16s 868MB
Nov 06 03:16:10 Starting compiler/backend/arm8/proofs
Nov 06 03:16:27 Finished compiler/backend/arm8/proofs                            17s   1GB
Nov 06 03:16:27 Starting compiler/backend/mips/proofs
Nov 06 03:16:44 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 06 03:16:44 Starting compiler/backend/riscv/proofs
Nov 06 03:17:02 Finished compiler/backend/riscv/proofs                           17s   1GB
Nov 06 03:17:02 Starting compiler/backend/ag32/proofs
Nov 06 03:25:21 Finished compiler/backend/ag32/proofs                          8m19s   1GB
Nov 06 03:25:22 Starting compiler/proofs
Nov 06 03:26:59 Finished compiler/proofs                                       1m37s   4GB
Nov 06 03:26:59 Starting candle/set-theory
Nov 06 03:27:26 Finished candle/set-theory                                       26s 951MB
Nov 06 03:27:26 Starting candle/syntax-lib
Nov 06 03:27:35 Finished candle/syntax-lib                                        9s 627MB
Nov 06 03:27:35 Starting candle/standard/syntax
Nov 06 03:29:14 Finished candle/standard/syntax                                1m38s 948MB
Nov 06 03:29:14 Starting candle/standard/semantics
Nov 06 03:30:48 Finished candle/standard/semantics                             1m32s   1GB
Nov 06 03:30:48 Starting candle/standard/monadic
Nov 06 03:32:18 Finished candle/standard/monadic                               1m29s   1GB
Nov 06 03:32:18 Starting candle/standard/ml_kernel
Nov 06 03:36:03 Finished candle/standard/ml_kernel                             3m45s   3GB
Nov 06 03:36:03 Starting candle/standard/opentheory
Nov 06 03:44:17 Finished candle/standard/opentheory                            8m13s   4GB
Nov 06 03:44:17 Starting candle/standard/opentheory/compilation
Nov 06 04:12:08 Finished candle/standard/opentheory/compilation               27m51s  21GB
Nov 06 04:12:08 Starting candle/standard/opentheory/compilation/proofs
Nov 06 04:12:53 Finished candle/standard/opentheory/compilation/proofs           44s   3GB
Nov 06 04:12:53 Starting characteristic/examples
Nov 06 04:14:17 Finished characteristic/examples                               1m24s   2GB
Nov 06 04:14:17 Starting tutorial/solutions
Nov 06 04:26:56 Finished tutorial/solutions                                   12m38s   6GB
Nov 06 04:26:56 Starting translator/monadic/examples
Nov 06 04:29:41 Finished translator/monadic/examples                           2m44s   3GB
Nov 06 04:29:41 Starting examples
Nov 06 04:34:46 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 README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
README.md                                       real:    0s  user:    0s     OK
Starting work on lcsTheory
regexp_parserTheory                             real:   12s  user:   11s     OK
Starting work on divTheory
lcsTheory                                       real:   13s  user:   12s     OK
Starting work on diffTheory
diffTheory                                      real:   45s  user:   44s     OK
Starting work on diffProgTheory
catProgTheory                                   real:   78s  user:   76s     OK
Starting work on doubleProgTheory
quicksortProgTheory                             real:  104s  user:  103s     OK
Starting work on array_searchProgTheory
diffProgTheory                                  real:   90s  user:   88s     OK
Starting work on echoProgTheory
divTheory                                       real:  153s  user:  151s     OK
Starting work on filterProgTheory
doubleProgTheory                                real:  100s  user:   99s     OK
Starting work on grepProgTheory
array_searchProgTheory                          real:  104s  user:  102s     OK
Starting work on helloErrProgTheory
echoProgTheory                                  real:   61s  user:   60s     OK
Starting work on helloProgTheory
helloErrProgTheory                              real:   54s  user:   53s     OK
Starting work on insertSortProgTheory
helloProgTheory                                 real:   53s  user:   51s     OK
Starting work on iocatProgTheory
filterProgTheory                                real:  100s  user:   97s     OK
Starting work on patchProgTheory
iocatProgTheory                                 real:   39s  user:   37sFAIL<1>
 Proof of 
 
 fns fnsv fs.
     LIST_TYPE FILENAME fns fnsv  EVERY (inFS_fname fs) fns  hasFreeFD fs 
     app p cat_v [fnsv] (STDIO fs)
       (POSTv u.
            &UNIT_TYPE () u * STDIO (add_stdout fs (catfiles_string fs fns)))
 
 failed.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 68) (THEN1 on line 74) (THEN1 on line 75) (THEN1 on line 83)", origin_function = "THEN1", origin_structure = "Tactical"}
grepProgTheory                                                          M-KILLED
insertSortProgTheory                                                    M-KILLED
patchProgTheory                                                         M-KILLED