Job 1066

CakeML:082af7d3d4a197a141c24adde12493785bf9e74c
  Fix grievous bug that prevented ! from being a valid symbol [Nov 01 06:14:49]
#695 (ocaml-infixes)
Merging into:dc73bd8f21601e06bdc92eb303865a3992673970
  Merge pull request #694 from CakeML/remove-oom [Oct 13 07:36:28]
HOL:9f88723b3e280ac1295c98de7a91ecb67eed7728
  Emacs mode: start on movement commands for navigating script buffers [Nov 04 05:23:11]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Nov 04 09:21:10 Claimed job
Nov 04 09:21:13 Building HOL
Nov 04 09:31:30 Starting developers
Nov 04 09:31:34 Finished developers                                               3s 137MB
Nov 04 09:31:34 Starting developers/bin
Nov 04 09:31:40 Finished developers/bin                                           5s 964MB
Nov 04 09:31:40 Starting semantics/ffi
Nov 04 09:31:49 Finished semantics/ffi                                            8s 241MB
Nov 04 09:31:49 Starting semantics
Nov 04 09:33:11 Finished semantics                                             1m21s   1GB
Nov 04 09:33:11 Starting semantics/proofs
Nov 04 09:36:01 Finished semantics/proofs                                      2m49s 836MB
Nov 04 09:36:01 Starting semantics/alt_semantics
Nov 04 09:36:08 Finished semantics/alt_semantics                                  6s 291MB
Nov 04 09:36:08 Starting semantics/alt_semantics/proofs
Nov 04 09:37:51 Finished semantics/alt_semantics/proofs                        1m43s 807MB
Nov 04 09:37:51 Starting basis/pure
Nov 04 09:40:28 Finished basis/pure                                            2m37s 745MB
Nov 04 09:40:29 Starting translator
Nov 04 09:42:11 Finished translator                                            1m42s   1GB
Nov 04 09:42:11 Starting compiler/parsing
Nov 04 09:43:12 Finished compiler/parsing                                      1m01s   2GB
Nov 04 09:43:12 Starting characteristic
Nov 04 09:48:15 Finished characteristic                                        5m02s   1GB
Nov 04 09:48:15 Starting translator/monadic
Nov 04 09:49:42 Finished translator/monadic                                    1m27s   1GB
Nov 04 09:49:42 Starting basis
Nov 04 10:08:25 Finished basis                                                18m42s   2GB
Nov 04 10:08:25 Starting compiler/inference
Nov 04 10:10:06 Finished compiler/inference                                    1m40s   1GB
Nov 04 10:10:06 Starting compiler/backend/reg_alloc
Nov 04 10:11:03 Finished compiler/backend/reg_alloc                              56s   1GB
Nov 04 10:11:03 Starting compiler/backend/gc
Nov 04 10:14:02 Finished compiler/backend/gc                                   2m58s   1GB
Nov 04 10:14:02 Starting compiler/backend
Nov 04 10:17:34 Finished compiler/backend                                      3m31s   2GB
Nov 04 10:17:34 Starting compiler/encoders/asm
Nov 04 10:17:53 Finished compiler/encoders/asm                                   19s 851MB
Nov 04 10:17:53 Starting compiler/encoders/x64
Nov 04 10:18:45 Finished compiler/encoders/x64                                   51s 782MB
Nov 04 10:18:45 Starting compiler/encoders/arm7
Nov 04 10:20:19 Finished compiler/encoders/arm7                                1m33s   1GB
Nov 04 10:20:19 Starting compiler/encoders/arm8
Nov 04 10:20:48 Finished compiler/encoders/arm8                                  29s 874MB
Nov 04 10:20:48 Starting compiler/encoders/mips
Nov 04 10:21:54 Finished compiler/encoders/mips                                1m05s 921MB
Nov 04 10:21:54 Starting compiler/encoders/riscv
Nov 04 10:23:11 Finished compiler/encoders/riscv                               1m17s   1GB
Nov 04 10:23:11 Starting compiler/encoders/ag32
Nov 04 10:23:27 Finished compiler/encoders/ag32                                  15s 752MB
Nov 04 10:23:27 Starting compiler/backend/x64
Nov 04 10:23:44 Finished compiler/backend/x64                                    16s   1GB
Nov 04 10:23:44 Starting compiler/backend/arm7
Nov 04 10:24:02 Finished compiler/backend/arm7                                   17s   1GB
Nov 04 10:24:02 Starting compiler/backend/arm8
Nov 04 10:24:19 Finished compiler/backend/arm8                                   16s   1GB
Nov 04 10:24:19 Starting compiler/backend/mips
Nov 04 10:24:36 Finished compiler/backend/mips                                   17s   1GB
Nov 04 10:24:36 Starting compiler/backend/riscv
Nov 04 10:24:54 Finished compiler/backend/riscv                                  17s   1GB
Nov 04 10:24:54 Starting compiler/backend/ag32
Nov 04 10:26:02 Finished compiler/backend/ag32                                 1m07s   1GB
Nov 04 10:26:02 Starting compiler/parsing/proofs
Nov 04 10:31:38 Finished compiler/parsing/proofs                               5m36s   1GB
Nov 04 10:31:38 Starting compiler/inference/proofs
Nov 04 10:34:17 Finished compiler/inference/proofs                             2m38s   1GB
Nov 04 10:34:17 Starting compiler/backend/semantics
Nov 04 10:43:17 Finished compiler/backend/semantics                            8m59s   1GB
Nov 04 10:43:17 Starting compiler/backend/reg_alloc/proofs
Nov 04 10:47:59 Finished compiler/backend/reg_alloc/proofs                     4m42s 766MB
Nov 04 10:47:59 Starting compiler/backend/proofs
Nov 04 11:27:11 Finished compiler/backend/proofs                              39m11s   4GB
Nov 04 11:27:11 Starting compiler/encoders/x64/proofs
Nov 04 11:36:02 Finished compiler/encoders/x64/proofs                          8m50s   5GB
Nov 04 11:36:02 Starting compiler/encoders/arm7/proofs
Nov 04 11:47:53 Finished compiler/encoders/arm7/proofs                        11m51s   3GB
Nov 04 11:47:53 Starting compiler/encoders/arm8/proofs
Nov 04 11:53:58 Finished compiler/encoders/arm8/proofs                         6m04s   1GB
Nov 04 11:53:58 Starting compiler/encoders/mips/proofs
Nov 04 12:03:00 Finished compiler/encoders/mips/proofs                         9m01s   3GB
Nov 04 12:03:00 Starting compiler/encoders/riscv/proofs
Nov 04 12:10:53 Finished compiler/encoders/riscv/proofs                        7m53s   1GB
Nov 04 12:10:53 Starting compiler/encoders/ag32/proofs
Nov 04 12:13:09 Finished compiler/encoders/ag32/proofs                         2m15s 643MB
Nov 04 12:13:09 Starting compiler/backend/x64/proofs
Nov 04 12:13:26 Finished compiler/backend/x64/proofs                             16s 784MB
Nov 04 12:13:26 Starting compiler/backend/arm7/proofs
Nov 04 12:13:44 Finished compiler/backend/arm7/proofs                            17s 852MB
Nov 04 12:13:44 Starting compiler/backend/arm8/proofs
Nov 04 12:14:00 Finished compiler/backend/arm8/proofs                            16s   1GB
Nov 04 12:14:01 Starting compiler/backend/mips/proofs
Nov 04 12:14:18 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 04 12:14:18 Starting compiler/backend/riscv/proofs
Nov 04 12:14:34 Finished compiler/backend/riscv/proofs                           16s 841MB
Nov 04 12:14:34 Starting compiler/backend/ag32/proofs
Nov 04 12:23:00 Finished compiler/backend/ag32/proofs                          8m25s   2GB
Nov 04 12:23:00 Starting compiler/proofs
Nov 04 12:24:37 Finished compiler/proofs                                       1m37s   3GB
Nov 04 12:24:37 Starting candle/set-theory
Nov 04 12:25:03 Finished candle/set-theory                                       25s 704MB
Nov 04 12:25:03 Starting candle/syntax-lib
Nov 04 12:25:12 Finished candle/syntax-lib                                        9s 694MB
Nov 04 12:25:13 Starting candle/standard/syntax
Nov 04 12:26:52 Finished candle/standard/syntax                                1m39s   1GB
Nov 04 12:26:53 Starting candle/standard/semantics
Nov 04 12:28:25 Finished candle/standard/semantics                             1m32s   1GB
Nov 04 12:28:25 Starting candle/standard/monadic
Nov 04 12:29:55 Finished candle/standard/monadic                               1m29s   1GB
Nov 04 12:29:55 Starting candle/standard/ml_kernel
Nov 04 12:33:36 Finished candle/standard/ml_kernel                             3m40s   3GB
Nov 04 12:33:36 Starting candle/standard/opentheory
Nov 04 12:41:56 Finished candle/standard/opentheory                            8m20s   3GB
Nov 04 12:41:56 Starting candle/standard/opentheory/compilation
Nov 04 13:09:26 Finished candle/standard/opentheory/compilation               27m30s  19GB
Nov 04 13:09:26 Starting candle/standard/opentheory/compilation/proofs
Nov 04 13:09:58 Finished candle/standard/opentheory/compilation/proofs           32s   2GB
Nov 04 13:09:58 Starting characteristic/examples
Nov 04 13:11:23 Finished characteristic/examples                               1m24s   2GB
Nov 04 13:11:23 Starting tutorial/solutions
Nov 04 13:24:04 Finished tutorial/solutions                                   12m40s   7GB
Nov 04 13:24:04 Starting translator/monadic/examples
Nov 04 13:26:42 Finished translator/monadic/examples                           2m37s   1GB
Nov 04 13:26:42 Starting examples
Nov 04 13:31: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:   12s  user:   11s     OK
Starting work on diffTheory
diffTheory                                      real:   43s  user:   42s     OK
Starting work on diffProgTheory
catProgTheory                                   real:   70s  user:   69s     OK
Starting work on doubleProgTheory
quicksortProgTheory                             real:  103s  user:  101s     OK
Starting work on array_searchProgTheory
diffProgTheory                                  real:   81s  user:   80s     OK
Starting work on echoProgTheory
divTheory                                       real:  151s  user:  149s     OK
Starting work on filterProgTheory
doubleProgTheory                                real:  105s  user:  103s     OK
Starting work on grepProgTheory
echoProgTheory                                  real:   60s  user:   59s     OK
Starting work on helloErrProgTheory
array_searchProgTheory                          real:  103s  user:  101s     OK
Starting work on helloProgTheory
helloErrProgTheory                              real:   54s  user:   52s     OK
Starting work on insertSortProgTheory
helloProgTheory                                 real:   53s  user:   52s     OK
Starting work on iocatProgTheory
filterProgTheory                                real:  103s  user:  101s     OK
Starting work on patchProgTheory
iocatProgTheory                                 real:   41s  user:   40sFAIL<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