Job 1007

CakeML:c63c2eee4cfca18c11e8781d51eb44a3ffda9ac1
  Insert a few old_drule calls to fix readerProof [Aug 17 07:49:57]
HOL:8cc876e8e492e4f4045670ff53549a04cf1fdc65
  Further document drule breakage by linking to CakeML's old_drule [Aug 16 01:09:50]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 17 07:53:23 Claimed job
Aug 17 07:56:57 Building HOL
Aug 17 08:04:55 Starting developers
Aug 17 08:04:56 Finished developers                                               0s  30MB
Aug 17 08:04:56 Starting developers/bin
Aug 17 08:06:29 Finished developers/bin                                        1m32s 164MB
Aug 17 08:06:29 Starting semantics/ffi
Aug 17 08:07:02 Finished semantics/ffi                                           32s 388MB
Aug 17 08:07:03 Starting semantics
Aug 17 08:08:32 Finished semantics                                             1m28s   1GB
Aug 17 08:08:32 Starting semantics/proofs
Aug 17 08:11:31 Finished semantics/proofs                                      2m58s   1GB
Aug 17 08:11:32 Starting semantics/alt_semantics
Aug 17 08:11:38 Finished semantics/alt_semantics                                  5s 279MB
Aug 17 08:11:39 Starting semantics/alt_semantics/proofs
Aug 17 08:13:27 Finished semantics/alt_semantics/proofs                        1m47s 797MB
Aug 17 08:13:27 Starting basis/pure
Aug 17 08:16:58 Finished basis/pure                                            3m29s 804MB
Aug 17 08:16:58 Starting translator
Aug 17 08:18:41 Finished translator                                            1m42s   1GB
Aug 17 08:18:41 Starting compiler/parsing
Aug 17 08:19:38 Finished compiler/parsing                                        56s   1GB
Aug 17 08:19:38 Starting characteristic
Aug 17 08:24:45 Finished characteristic                                        5m06s   1GB
Aug 17 08:24:46 Starting translator/monadic
Aug 17 08:26:10 Finished translator/monadic                                    1m23s   1GB
Aug 17 08:26:10 Starting basis
Aug 17 08:44:02 Finished basis                                                17m51s   2GB
Aug 17 08:44:03 Starting compiler/inference
Aug 17 08:45:54 Finished compiler/inference                                    1m50s   1GB
Aug 17 08:45:55 Starting compiler/backend/reg_alloc
Aug 17 08:46:52 Finished compiler/backend/reg_alloc                              57s   1GB
Aug 17 08:46:53 Starting compiler/backend/gc
Aug 17 08:55:56 Finished compiler/backend/gc                                   9m02s   2GB
Aug 17 08:55:56 Starting compiler/backend
Aug 17 08:55:57 Finished compiler/backend                                         0s  41MB
Aug 17 08:55:58 Starting compiler/encoders/asm
Aug 17 08:55:58 Finished compiler/encoders/asm                                    0s  38MB
Aug 17 08:55:59 Starting compiler/encoders/x64
Aug 17 08:56:56 Finished compiler/encoders/x64                                   57s 938MB
Aug 17 08:56:57 Starting compiler/encoders/arm7
Aug 17 08:58:34 Finished compiler/encoders/arm7                                1m36s   1GB
Aug 17 08:58:35 Starting compiler/encoders/arm8
Aug 17 08:59:04 Finished compiler/encoders/arm8                                  28s 878MB
Aug 17 08:59:04 Starting compiler/encoders/mips
Aug 17 09:00:07 Finished compiler/encoders/mips                                1m03s 796MB
Aug 17 09:00:08 Starting compiler/encoders/riscv
Aug 17 09:01:24 Finished compiler/encoders/riscv                               1m15s 860MB
Aug 17 09:01:24 Starting compiler/encoders/ag32
Aug 17 09:01:39 Finished compiler/encoders/ag32                                  14s 620MB
Aug 17 09:01:40 Starting compiler/backend/x64
Aug 17 09:01:56 Finished compiler/backend/x64                                    15s   1GB
Aug 17 09:01:56 Starting compiler/backend/arm7
Aug 17 09:02:13 Finished compiler/backend/arm7                                   16s   1GB
Aug 17 09:02:13 Starting compiler/backend/arm8
Aug 17 09:02:29 Finished compiler/backend/arm8                                   15s   1GB
Aug 17 09:02:30 Starting compiler/backend/mips
Aug 17 09:02:46 Finished compiler/backend/mips                                   15s   1GB
Aug 17 09:02:46 Starting compiler/backend/riscv
Aug 17 09:03:03 Finished compiler/backend/riscv                                  16s   1GB
Aug 17 09:03:03 Starting compiler/backend/ag32
Aug 17 09:04:10 Finished compiler/backend/ag32                                 1m06s   1GB
Aug 17 09:04:11 Starting compiler/parsing/proofs
Aug 17 09:09:42 Finished compiler/parsing/proofs                               5m31s 958MB
Aug 17 09:09:43 Starting compiler/inference/proofs
Aug 17 09:12:24 Finished compiler/inference/proofs                             2m40s   1GB
Aug 17 09:12:24 Starting compiler/backend/semantics
Aug 17 09:19:28 Finished compiler/backend/semantics                            7m03s   1GB
Aug 17 09:19:29 Starting compiler/backend/reg_alloc/proofs
Aug 17 09:22:40 Finished compiler/backend/reg_alloc/proofs                     3m11s 673MB
Aug 17 09:22:41 Starting compiler/backend/proofs
Aug 17 10:00:53 Finished compiler/backend/proofs                              38m11s   3GB
Aug 17 10:00:53 Starting compiler/encoders/x64/proofs
Aug 17 10:10:52 Finished compiler/encoders/x64/proofs                          9m59s   5GB
Aug 17 10:10:53 Starting compiler/encoders/arm7/proofs
Aug 17 10:24:15 Finished compiler/encoders/arm7/proofs                        13m21s   3GB
Aug 17 10:24:15 Starting compiler/encoders/arm8/proofs
Aug 17 10:30:58 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Aug 17 10:30:58 Starting compiler/encoders/mips/proofs
Aug 17 10:40:52 Finished compiler/encoders/mips/proofs                         9m53s   2GB
Aug 17 10:40:53 Starting compiler/encoders/riscv/proofs
Aug 17 10:49:07 Finished compiler/encoders/riscv/proofs                        8m14s   1GB
Aug 17 10:49:08 Starting compiler/encoders/ag32/proofs
Aug 17 10:51:36 Finished compiler/encoders/ag32/proofs                         2m27s 702MB
Aug 17 10:51:36 Starting compiler/backend/x64/proofs
Aug 17 10:51:53 Finished compiler/backend/x64/proofs                             16s   1GB
Aug 17 10:51:53 Starting compiler/backend/arm7/proofs
Aug 17 10:52:12 Finished compiler/backend/arm7/proofs                            18s   1GB
Aug 17 10:52:13 Starting compiler/backend/arm8/proofs
Aug 17 10:52:29 Finished compiler/backend/arm8/proofs                            16s   1GB
Aug 17 10:52:30 Starting compiler/backend/mips/proofs
Aug 17 10:52:48 Finished compiler/backend/mips/proofs                            17s   1GB
Aug 17 10:52:49 Starting compiler/backend/riscv/proofs
Aug 17 10:53:05 Finished compiler/backend/riscv/proofs                           16s 999MB
Aug 17 10:53:05 Starting compiler/backend/ag32/proofs
Aug 17 11:01:57 Finished compiler/backend/ag32/proofs                          8m51s   2GB
Aug 17 11:01:57 Starting compiler/proofs
Aug 17 11:03:36 Finished compiler/proofs                                       1m38s   2GB
Aug 17 11:03:37 Starting candle/set-theory
Aug 17 11:04:03 Finished candle/set-theory                                       25s 884MB
Aug 17 11:04:04 Starting candle/syntax-lib
Aug 17 11:04:13 Finished candle/syntax-lib                                        9s 591MB
Aug 17 11:04:13 Starting candle/standard/syntax
Aug 17 11:05:53 Finished candle/standard/syntax                                1m39s 825MB
Aug 17 11:05:54 Starting candle/standard/semantics
Aug 17 11:07:26 Finished candle/standard/semantics                             1m32s 992MB
Aug 17 11:07:26 Starting candle/standard/monadic
Aug 17 11:08:58 Finished candle/standard/monadic                               1m31s   1GB
Aug 17 11:08:59 Starting candle/standard/ml_kernel
Aug 17 11:12:43 Finished candle/standard/ml_kernel                             3m43s   5GB
Aug 17 11:12:43 Starting candle/standard/opentheory
Aug 17 11:21:03 Finished candle/standard/opentheory                            8m20s   4GB
Aug 17 11:21:04 Starting candle/standard/opentheory/compilation
Aug 17 11:51:20 Finished candle/standard/opentheory/compilation               30m15s  18GB
Aug 17 11:51:20 Starting candle/standard/opentheory/compilation/proofs
Aug 17 11:52:02 Finished candle/standard/opentheory/compilation/proofs           42s   2GB
Aug 17 11:52:03 Starting characteristic/examples
Aug 17 11:53:27 Finished characteristic/examples                               1m23s   1GB
Aug 17 11:53:27 Starting tutorial/solutions
Aug 17 12:06:26 Finished tutorial/solutions                                   12m58s   5GB
Aug 17 12:06:27 Starting translator/monadic/examples
Aug 17 12:09:14 Finished translator/monadic/examples                           2m46s   2GB
Aug 17 12:09:14 Starting examples
Aug 17 12:14:38 FAILED: examples
]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-1007/basis]0;Holmake: ~/regression/cakeml-1007/basis/pure]0;Holmake: ~/regression/cakeml-1007/misc]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-1007/misc]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-1007/misc]0;Holmake: ~/regression/cakeml-1007/developers]0;Holmake: ~/regression/cakeml-1007/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-1007/misc]0;Holmake: ~/regression/cakeml-1007/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1007/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1007/misc]0;Holmake: ~/regression/cakeml-1007/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-1007/basis/pure]0;Holmake: ~/regression/cakeml-1007/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-1007/basis]0;Holmake: ~/regression/cakeml-1007/characteristic]0;Holmake: ~/regression/cakeml-1007/compiler/parsing]0;Holmake: ~/regression/cakeml-1007/semantics]0;Holmake: ~/regression/cakeml-1007/semantics/ffi]0;Holmake: ~/regression/cakeml-1007/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-1007/semantics]0;Holmake: ~/regression/cakeml-1007/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-1007/compiler/parsing]0;Holmake: ~/regression/cakeml-1007/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-1007/characteristic]0;Holmake: ~/regression/cakeml-1007/semantics/proofs]0;Holmake: ~/regression/cakeml-1007/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-1007/characteristic]0;Holmake: ~/regression/cakeml-1007/translator]0;Holmake: ~/regression/cakeml-1007/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-1007/characteristic]0;Holmake: ~/regression/cakeml-1007/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-1007/basis]0;Holmake: ~/regression/cakeml-1007/translator/monadic]0;Holmake: ~/regression/cakeml-1007/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-1007/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-1007/translator/monadic]0;Holmake: ~/regression/cakeml-1007/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-1007/basis]0;Holmake: ~/regression/cakeml-1007/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on divTheory
lcsTheory                                                                                                                                                                         OK
Starting work on diffTheory
diffTheory                                                                                                                                                                        OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                                                     OK
Starting work on doubleProgTheory
quicksortProgTheory                                                                                                                                                               OK
Starting work on array_searchProgTheory
diffProgTheory                                                                                                                                                                    OK
Starting work on echoProgTheory
divTheory                                                                                                                                                                         OK
Starting work on filterProgTheory
doubleProgTheory                                                                                                                                                                  OK
Starting work on grepProgTheory
echoProgTheory                                                                                                                                                                    OK
Starting work on helloErrProgTheory
array_searchProgTheory                                                                                                                                                            OK
Starting work on helloProgTheory
filterProgTheory                                                                                                                                                         FAILED! <1>
   (LFILTER (language  MAP (CHR  w2n)  cut_at_null_w) inl)
 
 failed.
 Failed to prove theorem semantics_finite_filter.
 
 Exception raised at Thm_cont.DISCH_THEN:
 
 error in quse /home/myreen/regression/cakeml-1007/examples/filterProgScript.sml : HOL_ERR {message = "", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
 error in load filterProgScript : HOL_ERR {message = "", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
 Uncaught exception: HOL_ERR {message = "", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
grepProgTheory                                                                                                                                                              M-KILLED
helloErrProgTheory                                                                                                                                                          M-KILLED
helloProgTheory                                                                                                                                                             M-KILLED