Job 331

CakeML:62c0fbc6dcb3ba0aef8825680714ac56b2877e26
  Rename kernel.ml.txt so it gets gitignored [May 31 09:31:48]
HOL:4f2fc0f852c2307a56657ba660203833d7be0944
  Convert some llist theorems to use polyscripter in DESCRIPTION [May 31 06:45:04]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

May 31 09:32:37 Claimed job
May 31 09:32:46 Building HOL
May 31 09:44:21 Starting developers/bin
May 31 09:44:42 Finished developers/bin                                          19s 224MB
May 31 09:44:44 Starting semantics/ffi
May 31 09:45:45 Finished semantics/ffi                                           59s 303MB
May 31 09:45:47 Starting semantics
May 31 09:48:10 Finished semantics                                             2m20s   1GB
May 31 09:48:12 Starting semantics/proofs
May 31 09:51:24 Finished semantics/proofs                                      3m10s   1GB
May 31 09:51:26 Starting basis/pure
May 31 09:57:14 Finished basis/pure                                            5m45s 734MB
May 31 09:57:16 Starting translator
May 31 10:04:00 Finished translator                                            6m41s   1GB
May 31 10:04:02 Starting compiler/parsing
May 31 10:06:12 Finished compiler/parsing                                      2m08s   1GB
May 31 10:06:14 Starting characteristic
May 31 10:10:38 Finished characteristic                                        4m22s   1GB
May 31 10:10:40 Starting basis
May 31 10:39:20 Finished basis                                                28m37s   2GB
May 31 10:39:22 Starting translator/monadic
May 31 10:39:26 Finished translator/monadic                                       2s  12MB
May 31 10:39:28 Starting compiler/inference
May 31 10:42:10 Finished compiler/inference                                    2m39s 951MB
May 31 10:42:12 Starting compiler/backend/reg_alloc
May 31 10:43:09 Finished compiler/backend/reg_alloc                              54s   1GB
May 31 10:43:11 Starting compiler/backend/gc
May 31 10:57:58 Finished compiler/backend/gc                                  14m44s   3GB
May 31 10:57:59 Starting compiler/backend
May 31 10:58:05 Finished compiler/backend                                         3s  14MB
May 31 10:58:07 Starting compiler/encoders/asm
May 31 10:58:10 Finished compiler/encoders/asm                                    0s  11MB
May 31 10:58:12 Starting compiler/encoders/x64
May 31 10:59:40 Finished compiler/encoders/x64                                 1m25s 498MB
May 31 10:59:42 Starting compiler/encoders/arm6
May 31 11:02:37 Finished compiler/encoders/arm6                                2m53s   1GB
May 31 11:02:39 Starting compiler/encoders/arm8
May 31 11:03:24 Finished compiler/encoders/arm8                                  42s 399MB
May 31 11:03:26 Starting compiler/encoders/mips
May 31 11:05:01 Finished compiler/encoders/mips                                1m32s 725MB
May 31 11:05:03 Starting compiler/encoders/riscv
May 31 11:06:39 Finished compiler/encoders/riscv                               1m34s 728MB
May 31 11:06:41 Starting compiler/backend/x64
May 31 11:07:14 Finished compiler/backend/x64                                    31s   1GB
May 31 11:07:16 Starting compiler/backend/arm6
May 31 11:07:51 Finished compiler/backend/arm6                                   33s   1GB
May 31 11:07:53 Starting compiler/backend/arm8
May 31 11:08:28 Finished compiler/backend/arm8                                   32s   1GB
May 31 11:08:30 Starting compiler/backend/mips
May 31 11:09:06 Finished compiler/backend/mips                                   33s   1GB
May 31 11:09:08 Starting compiler/backend/riscv
May 31 11:09:42 Finished compiler/backend/riscv                                  32s   1GB
May 31 11:09:44 Starting compiler/parsing/proofs
May 31 11:13:51 Finished compiler/parsing/proofs                               4m04s 854MB
May 31 11:13:53 Starting compiler/inference/proofs
May 31 11:17:53 Finished compiler/inference/proofs                             3m57s   1GB
May 31 11:17:55 Starting compiler/backend/semantics
May 31 11:36:22 Finished compiler/backend/semantics                           18m25s   2GB
May 31 11:36:24 Starting compiler/backend/reg_alloc/proofs
May 31 11:37:50 Finished compiler/backend/reg_alloc/proofs                     1m23s 382MB
May 31 11:37:52 Starting compiler/backend/proofs
May 31 12:32:54 Finished compiler/backend/proofs                              55m00s   4GB
May 31 12:32:56 Starting compiler/encoders/x64/proofs
May 31 12:44:32 Finished compiler/encoders/x64/proofs                         11m33s   1GB
May 31 12:44:34 Starting compiler/encoders/arm6/proofs
May 31 12:56:27 Finished compiler/encoders/arm6/proofs                        11m51s   2GB
May 31 12:56:29 Starting compiler/encoders/arm8/proofs
May 31 13:04:51 Finished compiler/encoders/arm8/proofs                         8m19s   1GB
May 31 13:04:53 Starting compiler/encoders/mips/proofs
May 31 13:16:30 Finished compiler/encoders/mips/proofs                        11m34s   1GB
May 31 13:16:32 Starting compiler/encoders/riscv/proofs
May 31 13:28:57 Finished compiler/encoders/riscv/proofs                       12m23s   1GB
May 31 13:28:59 Starting compiler/backend/x64/proofs
May 31 13:29:36 Finished compiler/backend/x64/proofs                             34s   1GB
May 31 13:29:37 Starting compiler/backend/arm6/proofs
May 31 13:30:16 Finished compiler/backend/arm6/proofs                            36s   1GB
May 31 13:30:18 Starting compiler/backend/arm8/proofs
May 31 13:30:54 Finished compiler/backend/arm8/proofs                            34s   1GB
May 31 13:30:56 Starting compiler/backend/mips/proofs
May 31 13:31:34 Finished compiler/backend/mips/proofs                            36s   1GB
May 31 13:31:36 Starting compiler/backend/riscv/proofs
May 31 13:32:13 Finished compiler/backend/riscv/proofs                           34s   1GB
May 31 13:32:15 Starting compiler/proofs
May 31 13:34:36 Finished compiler/proofs                                       2m18s   2GB
May 31 13:34:38 Starting candle/set-theory
May 31 13:36:17 Finished candle/set-theory                                     1m36s 550MB
May 31 13:36:19 Starting candle/syntax-lib
May 31 13:36:37 Finished candle/syntax-lib                                       16s 390MB
May 31 13:36:39 Starting candle/standard/syntax
May 31 13:39:20 Finished candle/standard/syntax                                2m39s 606MB
May 31 13:39:22 Starting candle/standard/semantics
May 31 13:41:38 Finished candle/standard/semantics                             2m13s 754MB
May 31 13:41:40 Starting candle/standard/monadic
May 31 13:44:02 Finished candle/standard/monadic                               2m20s 899MB
May 31 13:44:04 Starting candle/standard/ml_kernel
May 31 13:54:23 Finished candle/standard/ml_kernel                            10m17s   2GB
May 31 13:54:25 Starting candle/standard/opentheory
May 31 13:54:51 Finished candle/standard/opentheory                              24s 640MB
May 31 13:54:53 Starting characteristic/examples
May 31 13:57:18 Finished characteristic/examples                               2m22s   1GB
May 31 13:57:20 Starting tutorial/solutions
May 31 14:31:38 Finished tutorial/solutions                                   34m16s  10GB
May 31 14:31:40 Starting translator/monadic/examples
May 31 14:34:39 Finished translator/monadic/examples                           2m56s   2GB
May 31 14:34:41 Starting examples
May 31 14:37:58 FAILED: examples
]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: .]0;Holmake: ../basis]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-4f2fc0f852c2307a56657ba660203833d7be0944/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developersWorking in ../developers
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../misc]0;Holmake: ../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ../basis]0;Holmake: ../characteristic]0;Holmake: ../compiler/parsing]0;Holmake: ../semantics]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../compiler/parsing]0;Holmake: ../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../characteristic]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../characteristic]0;Holmake: ../translator]0;Holmake: ../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../characteristic]0;Holmake: ../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../basis]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../basis]0;Holmake: ../basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/examples
Starting work on heap
Starting work on README.md
README.md                                                                                       OK
heap                                                                                            OK
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on echoProgTheory
Starting work on grepProgTheory
lcsTheory                                                                                       OK
Starting work on diffTheory
echoProgTheory                                                                                  OK
Starting work on helloErrProgTheory
catProgTheory                                                                                   OK
Starting work on helloProgTheory
diffTheory                                                                                      OK
Starting work on diffProgTheory
helloErrProgTheory                                                                              OK
Starting work on insertSortProgTheory
helloProgTheory                                                                                 OK
Starting work on iocatProgTheory
iocatProgTheory                                                                        FAILED! <1>
            SEP_EXISTS nr.
                &NUM nr nrv * &(nr  MIN 2048 (STRLEN c1  pos1)) *
                &(nr = 0  eof fd1 fs = SOME T) *
                STDIO
                  (fsupdate (... ... (... + ... ) c1) fd2 0 (STRLEN c2 + nr)
                     (STRCAT c2 (TAKE nr (DROP pos1 c1)))))
 
 failed.
 Failed to prove theorem pipe_2048_spec.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 75) (THEN1 on line 81) (THEN1 on line 74) (THEN1 on line 82) (THEN1 on line 73) (THEN1 on line 84) (THEN1 on line 91) (THEN1 on line 92)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
grepProgTheory                                                                            M-KILLED
diffProgTheory                                                                            M-KILLED
insertSortProgTheory                                                                      M-KILLED