Job 1088

CakeML:b618263721be9f7297903418b3a32f3220620c6c
  Fix a CF example [Nov 12 20:29:18]
#702 (bufferedio)
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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 13 11:30:02 Claimed job
Nov 13 11:30:09 Reusing HOL
Nov 13 11:31:02 Starting developers
Nov 13 11:31:06 Finished developers                                               3s  62MB
Nov 13 11:31:07 Starting developers/bin
Nov 13 11:31:13 Finished developers/bin                                           6s 960MB
Nov 13 11:31:14 Starting semantics/ffi
Nov 13 11:31:23 Finished semantics/ffi                                            9s 224MB
Nov 13 11:31:23 Starting semantics
Nov 13 11:32:41 Finished semantics                                             1m17s   1GB
Nov 13 11:32:41 Starting semantics/proofs
Nov 13 11:35:41 Finished semantics/proofs                                      2m59s 882MB
Nov 13 11:35:41 Starting semantics/alt_semantics
Nov 13 11:35:48 Finished semantics/alt_semantics                                  7s 275MB
Nov 13 11:35:48 Starting semantics/alt_semantics/proofs
Nov 13 11:37:37 Finished semantics/alt_semantics/proofs                        1m48s 693MB
Nov 13 11:37:37 Starting basis/pure
Nov 13 11:38:23 Finished basis/pure                                              45s 615MB
Nov 13 11:38:23 Starting translator
Nov 13 11:40:09 Finished translator                                            1m45s   1GB
Nov 13 11:40:09 Starting compiler/parsing
Nov 13 11:41:07 Finished compiler/parsing                                        57s   1GB
Nov 13 11:41:07 Starting characteristic
Nov 13 11:46:19 Finished characteristic                                        5m11s   2GB
Nov 13 11:46:19 Starting translator/monadic
Nov 13 11:47:49 Finished translator/monadic                                    1m29s   1GB
Nov 13 11:47:49 Starting basis
Nov 13 12:20:09 Finished basis                                                32m19s  15GB
Nov 13 12:20:09 Starting compiler/inference
Nov 13 12:21:49 Finished compiler/inference                                    1m39s   1GB
Nov 13 12:21:49 Starting compiler/backend/reg_alloc
Nov 13 12:22:48 Finished compiler/backend/reg_alloc                              58s   1GB
Nov 13 12:22:48 Starting compiler/backend/gc
Nov 13 12:25:46 Finished compiler/backend/gc                                   2m57s   2GB
Nov 13 12:25:46 Starting compiler/backend
Nov 13 12:29:30 Finished compiler/backend                                      3m43s   1GB
Nov 13 12:29:30 Starting compiler/encoders/asm
Nov 13 12:29:50 Finished compiler/encoders/asm                                   20s 774MB
Nov 13 12:29:50 Starting compiler/encoders/x64
Nov 13 12:30:14 Finished compiler/encoders/x64                                   23s 559MB
Nov 13 12:30:14 Starting compiler/encoders/arm7
Nov 13 12:30:59 Finished compiler/encoders/arm7                                  44s 805MB
Nov 13 12:31:00 Starting compiler/encoders/arm8
Nov 13 12:31:12 Finished compiler/encoders/arm8                                  12s 548MB
Nov 13 12:31:12 Starting compiler/encoders/mips
Nov 13 12:31:28 Finished compiler/encoders/mips                                  15s 783MB
Nov 13 12:31:29 Starting compiler/encoders/riscv
Nov 13 12:31:42 Finished compiler/encoders/riscv                                 13s 851MB
Nov 13 12:31:42 Starting compiler/encoders/ag32
Nov 13 12:31:59 Finished compiler/encoders/ag32                                  16s 523MB
Nov 13 12:32:00 Starting compiler/backend/x64
Nov 13 12:32:17 Finished compiler/backend/x64                                    16s   1GB
Nov 13 12:32:17 Starting compiler/backend/arm7
Nov 13 12:32:35 Finished compiler/backend/arm7                                   17s   1GB
Nov 13 12:32:35 Starting compiler/backend/arm8
Nov 13 12:32:52 Finished compiler/backend/arm8                                   16s   1GB
Nov 13 12:32:52 Starting compiler/backend/mips
Nov 13 12:33:10 Finished compiler/backend/mips                                   17s   1GB
Nov 13 12:33:10 Starting compiler/backend/riscv
Nov 13 12:33:28 Finished compiler/backend/riscv                                  17s   1GB
Nov 13 12:33:28 Starting compiler/backend/ag32
Nov 13 12:34:32 Finished compiler/backend/ag32                                 1m04s   1GB
Nov 13 12:34:33 Starting compiler/parsing/proofs
Nov 13 12:40:12 Finished compiler/parsing/proofs                               5m38s 819MB
Nov 13 12:40:12 Starting compiler/inference/proofs
Nov 13 12:42:57 Finished compiler/inference/proofs                             2m44s   1GB
Nov 13 12:42:57 Starting compiler/backend/semantics
Nov 13 12:48:49 Finished compiler/backend/semantics                            5m52s   2GB
Nov 13 12:48:49 Starting compiler/backend/reg_alloc/proofs
Nov 13 12:52:04 Finished compiler/backend/reg_alloc/proofs                     3m14s 798MB
Nov 13 12:52:04 Starting compiler/backend/proofs
Nov 13 13:32:08 Finished compiler/backend/proofs                              40m03s   4GB
Nov 13 13:32:08 Starting compiler/encoders/x64/proofs
Nov 13 13:41:05 Finished compiler/encoders/x64/proofs                          8m55s   5GB
Nov 13 13:41:05 Starting compiler/encoders/arm7/proofs
Nov 13 13:53:21 Finished compiler/encoders/arm7/proofs                        12m15s   3GB
Nov 13 13:53:21 Starting compiler/encoders/arm8/proofs
Nov 13 13:59:27 Finished compiler/encoders/arm8/proofs                         6m06s   1GB
Nov 13 13:59:27 Starting compiler/encoders/mips/proofs
Nov 13 14:08:41 Finished compiler/encoders/mips/proofs                         9m13s   3GB
Nov 13 14:08:41 Starting compiler/encoders/riscv/proofs
Nov 13 14:16:56 Finished compiler/encoders/riscv/proofs                        8m14s 968MB
Nov 13 14:16:56 Starting compiler/encoders/ag32/proofs
Nov 13 14:19:21 Finished compiler/encoders/ag32/proofs                         2m24s 628MB
Nov 13 14:19:21 Starting compiler/backend/x64/proofs
Nov 13 14:19:39 Finished compiler/backend/x64/proofs                             17s   1GB
Nov 13 14:19:39 Starting compiler/backend/arm7/proofs
Nov 13 14:19:58 Finished compiler/backend/arm7/proofs                            19s   1GB
Nov 13 14:19:58 Starting compiler/backend/arm8/proofs
Nov 13 14:20:15 Finished compiler/backend/arm8/proofs                            16s 803MB
Nov 13 14:20:15 Starting compiler/backend/mips/proofs
Nov 13 14:20:33 Finished compiler/backend/mips/proofs                            18s 923MB
Nov 13 14:20:33 Starting compiler/backend/riscv/proofs
Nov 13 14:20:52 Finished compiler/backend/riscv/proofs                           18s   1GB
Nov 13 14:20:52 Starting compiler/backend/ag32/proofs
Nov 13 14:29:38 Finished compiler/backend/ag32/proofs                          8m45s   2GB
Nov 13 14:29:38 Starting compiler/proofs
Nov 13 14:31:25 Finished compiler/proofs                                       1m47s   3GB
Nov 13 14:31:25 Starting candle/set-theory
Nov 13 14:31:52 Finished candle/set-theory                                       26s 827MB
Nov 13 14:31:52 Starting candle/syntax-lib
Nov 13 14:32:02 Finished candle/syntax-lib                                       10s 667MB
Nov 13 14:32:02 Starting candle/standard/syntax
Nov 13 14:33:45 Finished candle/standard/syntax                                1m42s   1GB
Nov 13 14:33:46 Starting candle/standard/semantics
Nov 13 14:35:23 Finished candle/standard/semantics                             1m36s   1GB
Nov 13 14:35:23 Starting candle/standard/monadic
Nov 13 14:36:55 Finished candle/standard/monadic                               1m32s   1GB
Nov 13 14:36:56 Starting candle/standard/ml_kernel
Nov 13 14:40:44 Finished candle/standard/ml_kernel                             3m48s   4GB
Nov 13 14:40:44 Starting candle/standard/opentheory
Nov 13 14:49:23 Finished candle/standard/opentheory                            8m39s   4GB
Nov 13 14:49:24 Starting candle/standard/opentheory/compilation
Nov 13 15:19:14 Finished candle/standard/opentheory/compilation               29m50s  16GB
Nov 13 15:19:14 Starting candle/standard/opentheory/compilation/proofs
Nov 13 15:20:03 Finished candle/standard/opentheory/compilation/proofs           48s   3GB
Nov 13 15:20:03 Starting characteristic/examples
Nov 13 15:21:38 Finished characteristic/examples                               1m35s   1GB
Nov 13 15:21:38 Starting tutorial/solutions
Nov 13 15:34:39 Finished tutorial/solutions                                   12m59s   7GB
Nov 13 15:34:39 Starting translator/monadic/examples
Nov 13 15:37:34 Finished translator/monadic/examples                           2m55s   2GB
Nov 13 15:37:34 Starting examples
Nov 13 15:38:21 FAILED: examples
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
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:   14s  user:   13s     OK
Starting work on diffTheory
catProgTheory                                   real:   45s  user:   43sFAIL<1>
          (u.
               SEP_EXISTS content ino.
                   &UNIT_TYPE () u * &(ALOOKUP ... .files fnm = SOME ino) *
                   &(ALOOKUP fs.inode_tbl (File ino) = SOME content) *
                   STDIO (add_stdout fs (implode content)))
          (e. &BadFileName_exn e * &inFS_fname fs fnm * STDIO fs))
 
 failed.
 Failed to prove theorem do_onefile_spec.
 Uncaught exception: HOL_ERR {message = "Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
quicksortProgTheory                                                     M-KILLED
divTheory                                                               M-KILLED
diffTheory                                                              M-KILLED