Job 632

CakeML:754f13d79d430a756041b3c559ef3d12f709f4c4
  Fix a proof in iocatProg [Dec 16 12:31:16]
#583 (heapfree)
Merging into:9b366aa092a1e2c8100d95bbe3fa77b5fe513dc9
  Merge pull request #582 from CakeML/cleanup [Dec 14 06:05:52]
HOL:2300978321a15932fdaf49ff5e1365d09a9a1c3b
  Fix typo [Dec 13 15:46:26]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 16 16:42:04 Claimed job
Dec 16 16:42:08 Reusing HOL
Dec 16 16:42:57 Starting developers
Dec 16 16:43:00 Finished developers                                               2s  20MB
Dec 16 16:43:01 Starting developers/bin
Dec 16 16:44:07 Finished developers/bin                                        1m05s 916MB
Dec 16 16:44:08 Starting semantics/ffi
Dec 16 16:44:19 Finished semantics/ffi                                           10s 253MB
Dec 16 16:44:19 Starting semantics
Dec 16 16:45:45 Finished semantics                                             1m24s   1GB
Dec 16 16:45:46 Starting semantics/proofs
Dec 16 16:49:04 Finished semantics/proofs                                      3m17s   1GB
Dec 16 16:49:05 Starting basis/pure
Dec 16 16:49:59 Finished basis/pure                                              53s 605MB
Dec 16 16:49:59 Starting translator
Dec 16 16:51:39 Finished translator                                            1m39s   1GB
Dec 16 16:51:40 Starting compiler/parsing
Dec 16 16:52:44 Finished compiler/parsing                                      1m03s   2GB
Dec 16 16:52:45 Starting characteristic
Dec 16 16:56:08 Finished characteristic                                        3m23s   1GB
Dec 16 16:56:09 Starting translator/monadic
Dec 16 16:57:38 Finished translator/monadic                                    1m27s   2GB
Dec 16 16:57:38 Starting basis
Dec 16 17:13:56 Finished basis                                                16m17s   3GB
Dec 16 17:13:57 Starting compiler/inference
Dec 16 17:15:39 Finished compiler/inference                                    1m41s   1GB
Dec 16 17:15:40 Starting compiler/backend/reg_alloc
Dec 16 17:16:33 Finished compiler/backend/reg_alloc                              52s   1GB
Dec 16 17:16:34 Starting compiler/backend/gc
Dec 16 17:24:34 Finished compiler/backend/gc                                   7m59s   2GB
Dec 16 17:24:35 Starting compiler/backend
Dec 16 17:24:38 Finished compiler/backend                                         2s  24MB
Dec 16 17:24:39 Starting compiler/encoders/asm
Dec 16 17:24:40 Finished compiler/encoders/asm                                    1s  14MB
Dec 16 17:24:41 Starting compiler/encoders/x64
Dec 16 17:25:09 Finished compiler/encoders/x64                                   27s 906MB
Dec 16 17:25:09 Starting compiler/encoders/arm6
Dec 16 17:26:03 Finished compiler/encoders/arm6                                  53s 969MB
Dec 16 17:26:04 Starting compiler/encoders/arm8
Dec 16 17:26:18 Finished compiler/encoders/arm8                                  13s 883MB
Dec 16 17:26:19 Starting compiler/encoders/mips
Dec 16 17:26:37 Finished compiler/encoders/mips                                  17s   1GB
Dec 16 17:26:38 Starting compiler/encoders/riscv
Dec 16 17:26:54 Finished compiler/encoders/riscv                                 15s 919MB
Dec 16 17:26:55 Starting compiler/encoders/ag32
Dec 16 17:27:13 Finished compiler/encoders/ag32                                  17s 807MB
Dec 16 17:27:14 Starting compiler/backend/x64
Dec 16 17:27:31 Finished compiler/backend/x64                                    17s 791MB
Dec 16 17:27:32 Starting compiler/backend/arm6
Dec 16 17:27:53 Finished compiler/backend/arm6                                   20s   1GB
Dec 16 17:27:54 Starting compiler/backend/arm8
Dec 16 17:28:13 Finished compiler/backend/arm8                                   18s   1GB
Dec 16 17:28:13 Starting compiler/backend/mips
Dec 16 17:28:33 Finished compiler/backend/mips                                   19s   1GB
Dec 16 17:28:34 Starting compiler/backend/riscv
Dec 16 17:28:55 Finished compiler/backend/riscv                                  19s   1GB
Dec 16 17:28:55 Starting compiler/backend/ag32
Dec 16 17:30:09 Finished compiler/backend/ag32                                 1m13s   1GB
Dec 16 17:30:10 Starting compiler/parsing/proofs
Dec 16 17:36:23 Finished compiler/parsing/proofs                               6m12s 858MB
Dec 16 17:36:23 Starting compiler/inference/proofs
Dec 16 17:39:18 Finished compiler/inference/proofs                             2m54s   1GB
Dec 16 17:39:19 Starting compiler/backend/semantics
Dec 16 17:46:51 Finished compiler/backend/semantics                            7m31s   2GB
Dec 16 17:46:51 Starting compiler/backend/reg_alloc/proofs
Dec 16 17:49:35 Finished compiler/backend/reg_alloc/proofs                     2m43s 847MB
Dec 16 17:49:36 Starting compiler/backend/proofs
Dec 16 18:28:01 Finished compiler/backend/proofs                              38m24s   4GB
Dec 16 18:28:02 Starting compiler/encoders/x64/proofs
Dec 16 18:37:46 Finished compiler/encoders/x64/proofs                          9m43s   5GB
Dec 16 18:37:47 Starting compiler/encoders/arm6/proofs
Dec 16 18:51:29 Finished compiler/encoders/arm6/proofs                        13m41s   3GB
Dec 16 18:51:30 Starting compiler/encoders/arm8/proofs
Dec 16 18:57:24 Finished compiler/encoders/arm8/proofs                         5m53s   1GB
Dec 16 18:57:24 Starting compiler/encoders/mips/proofs
Dec 16 19:07:40 Finished compiler/encoders/mips/proofs                        10m14s   2GB
Dec 16 19:07:41 Starting compiler/encoders/riscv/proofs
Dec 16 19:15:34 Finished compiler/encoders/riscv/proofs                        7m52s   1GB
Dec 16 19:15:34 Starting compiler/encoders/ag32/proofs
Dec 16 19:18:15 Finished compiler/encoders/ag32/proofs                         2m40s 753MB
Dec 16 19:18:16 Starting compiler/backend/x64/proofs
Dec 16 19:18:37 Finished compiler/backend/x64/proofs                             20s   1GB
Dec 16 19:18:38 Starting compiler/backend/arm6/proofs
Dec 16 19:19:00 Finished compiler/backend/arm6/proofs                            22s 848MB
Dec 16 19:19:01 Starting compiler/backend/arm8/proofs
Dec 16 19:19:21 Finished compiler/backend/arm8/proofs                            19s 759MB
Dec 16 19:19:22 Starting compiler/backend/mips/proofs
Dec 16 19:19:43 Finished compiler/backend/mips/proofs                            20s 963MB
Dec 16 19:19:43 Starting compiler/backend/riscv/proofs
Dec 16 19:20:05 Finished compiler/backend/riscv/proofs                           20s   1GB
Dec 16 19:20:05 Starting compiler/backend/ag32/proofs
Dec 16 19:29:20 Finished compiler/backend/ag32/proofs                          9m14s   2GB
Dec 16 19:29:21 Starting compiler/proofs
Dec 16 19:30:41 Finished compiler/proofs                                       1m19s   3GB
Dec 16 19:30:42 Starting candle/set-theory
Dec 16 19:31:09 Finished candle/set-theory                                       27s 675MB
Dec 16 19:31:10 Starting candle/syntax-lib
Dec 16 19:31:21 Finished candle/syntax-lib                                       10s 664MB
Dec 16 19:31:22 Starting candle/standard/syntax
Dec 16 19:33:10 Finished candle/standard/syntax                                1m47s   1GB
Dec 16 19:33:11 Starting candle/standard/semantics
Dec 16 19:34:53 Finished candle/standard/semantics                             1m41s   1GB
Dec 16 19:34:54 Starting candle/standard/monadic
Dec 16 19:36:37 Finished candle/standard/monadic                               1m42s   1GB
Dec 16 19:36:37 Starting candle/standard/ml_kernel
Dec 16 19:51:46 Finished candle/standard/ml_kernel                            15m07s   2GB
Dec 16 19:51:47 Starting candle/standard/opentheory
Dec 16 20:00:29 Finished candle/standard/opentheory                            8m41s   4GB
Dec 16 20:00:29 Starting candle/standard/opentheory/compilation
Dec 16 20:29:20 Finished candle/standard/opentheory/compilation               28m50s  24GB
Dec 16 20:29:21 Starting candle/standard/opentheory/compilation/proofs
Dec 16 20:30:06 Finished candle/standard/opentheory/compilation/proofs           44s   4GB
Dec 16 20:30:07 Starting characteristic/examples
Dec 16 20:31:39 Finished characteristic/examples                               1m31s   2GB
Dec 16 20:31:40 Starting tutorial/solutions
Dec 16 20:44:39 Finished tutorial/solutions                                   12m58s   6GB
Dec 16 20:44:40 Starting translator/monadic/examples
Dec 16 20:46:49 Finished translator/monadic/examples                           2m07s   2GB
Dec 16 20:46:49 Starting examples
Dec 16 20:52:56 FAILED: examples
]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-632/basis]0;Holmake: ~/oven/regression/cakeml-632/basis/pure]0;Holmake: ~/oven/regression/cakeml-632/misc]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-632/misc]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-632/misc]0;Holmake: ~/oven/regression/cakeml-632/developers]0;Holmake: ~/oven/regression/cakeml-632/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-632/misc]0;Holmake: ~/oven/regression/cakeml-632/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-632/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-632/misc]0;Holmake: ~/oven/regression/cakeml-632/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-632/basis/pure]0;Holmake: ~/oven/regression/cakeml-632/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-632/basis]0;Holmake: ~/oven/regression/cakeml-632/characteristic]0;Holmake: ~/oven/regression/cakeml-632/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-632/semantics]0;Holmake: ~/oven/regression/cakeml-632/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-632/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-632/semantics]0;Holmake: ~/oven/regression/cakeml-632/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-632/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-632/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-632/characteristic]0;Holmake: ~/oven/regression/cakeml-632/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-632/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-632/characteristic]0;Holmake: ~/oven/regression/cakeml-632/translator]0;Holmake: ~/oven/regression/cakeml-632/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-632/characteristic]0;Holmake: ~/oven/regression/cakeml-632/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-632/basis]0;Holmake: ~/oven/regression/cakeml-632/translator/monadic]0;Holmake: ~/oven/regression/cakeml-632/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-632/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-632/translator/monadic]0;Holmake: ~/oven/regression/cakeml-632/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-632/basis]0;Holmake: ~/oven/regression/cakeml-632/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/examples
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on doubleProgTheory
lcsTheory                                                                    OK
Starting work on diffTheory
diffTheory                                                                   OK
Starting work on diffProgTheory
catProgTheory                                                                OK
Starting work on echoProgTheory
doubleProgTheory                                                             OK
Starting work on grepProgTheory
quicksortProgTheory                                                          OK
Starting work on array_searchProgTheory
echoProgTheory                                                               OK
Starting work on helloErrProgTheory
diffProgTheory                                                               OK
Starting work on helloProgTheory
helloProgTheory                                                              OK
Starting work on insertSortProgTheory
helloErrProgTheory                                                           OK
Starting work on iocatProgTheory
array_searchProgTheory                                                       OK
Starting work on patchProgTheory
insertSortProgTheory                                                         OK
Starting work on queueProgTheory
iocatProgTheory                                                              OK
Starting work on sortProgTheory
patchProgTheory                                                              OK
Starting work on splitwordsTheory
grepProgTheory                                                               OK
Starting work on stackProgTheory
splitwordsTheory                                                             OK
Starting work on wordcountProgTheory
sortProgTheory                                                      FAILED! <1>
               &(LIST_TYPE STRING_TYPE (REVERSE (... ... ) ++ ... ... acc)
                  strings_v  EVERY (inFS_fname fs  File) fnames))
          (e.
               STDIO fs *
               &(BadFileName_exn e  EVERY (inFS_fname fs  File) fnames))
          (n c b. &F))
 
 failed.
 Failed to prove theorem get_files_contents_spec.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 212) (THEN1 on line 213) (THEN1 on line 217)", origin_function = "THEN1", origin_structure = "Tactical"}
queueProgTheory                                                        M-KILLED
stackProgTheory                                                        M-KILLED
wordcountProgTheory                                                    M-KILLED
Don't know how to build necessary target(s): compilation/readmePrefix