Job 1045

CakeML:30193e4df86fc6ee1df59c8baf4b125c84ba01d4
  Merge pull request #690 from CakeML/close-files [Sep 13 07:50:45]
HOL:fdba23b05ca01a36aa6d330d2adeb55601b76924
  Optimization of proof-based regexp compiler [Sep 27 22:31:07]
Machine:oven3 4.19.67.1.amd64-smp

Oct 01 05:33:26 Claimed job
Oct 01 05:33:34 Building HOL
Oct 01 05:56:39 Starting developers
Oct 01 05:56:46 Finished developers                                               6s 127MB
Oct 01 05:56:46 Starting developers/bin
Oct 01 05:57:00 Finished developers/bin                                          13s 964MB
Oct 01 05:57:00 Starting semantics/ffi
Oct 01 05:58:27 Finished semantics/ffi                                         1m26s 673MB
Oct 01 05:58:27 Starting semantics
Oct 01 06:01:49 Finished semantics                                             3m21s   1GB
Oct 01 06:01:49 Starting semantics/proofs
Oct 01 06:08:42 Finished semantics/proofs                                      6m52s   1GB
Oct 01 06:08:43 Starting semantics/alt_semantics
Oct 01 06:09:00 Finished semantics/alt_semantics                                 17s 332MB
Oct 01 06:09:00 Starting semantics/alt_semantics/proofs
Oct 01 06:13:00 Finished semantics/alt_semantics/proofs                        3m58s 817MB
Oct 01 06:13:00 Starting basis/pure
Oct 01 06:21:13 Finished basis/pure                                            8m13s 686MB
Oct 01 06:21:13 Starting translator
Oct 01 06:24:56 Finished translator                                            3m42s   1GB
Oct 01 06:24:56 Starting compiler/parsing
Oct 01 06:26:56 Finished compiler/parsing                                      2m00s   2GB
Oct 01 06:26:57 Starting characteristic
Oct 01 06:38:31 Finished characteristic                                       11m34s   2GB
Oct 01 06:38:31 Starting translator/monadic
Oct 01 06:41:36 Finished translator/monadic                                    3m04s   1GB
Oct 01 06:41:36 Starting basis
Oct 01 07:22:23 Finished basis                                                40m46s   2GB
Oct 01 07:22:23 Starting compiler/inference
Oct 01 07:26:40 Finished compiler/inference                                    4m16s   1GB
Oct 01 07:26:40 Starting compiler/backend/reg_alloc
Oct 01 07:28:32 Finished compiler/backend/reg_alloc                            1m51s   1GB
Oct 01 07:28:32 Starting compiler/backend/gc
Oct 01 07:47:16 Finished compiler/backend/gc                                  18m42s   2GB
Oct 01 07:47:16 Starting compiler/backend
Oct 01 07:47:19 Finished compiler/backend                                         2s  48MB
Oct 01 07:47:19 Starting compiler/encoders/asm
Oct 01 07:47:20 Finished compiler/encoders/asm                                    1s  15MB
Oct 01 07:47:21 Starting compiler/encoders/x64
Oct 01 07:49:40 Finished compiler/encoders/x64                                 2m19s 969MB
Oct 01 07:49:40 Starting compiler/encoders/arm7
Oct 01 07:53:24 Finished compiler/encoders/arm7                                3m44s   1GB
Oct 01 07:53:25 Starting compiler/encoders/arm8
Oct 01 07:54:37 Finished compiler/encoders/arm8                                1m11s 633MB
Oct 01 07:54:37 Starting compiler/encoders/mips
Oct 01 07:57:12 Finished compiler/encoders/mips                                2m34s   1GB
Oct 01 07:57:12 Starting compiler/encoders/riscv
Oct 01 08:00:12 Finished compiler/encoders/riscv                               2m59s 907MB
Oct 01 08:00:12 Starting compiler/encoders/ag32
Oct 01 08:00:48 Finished compiler/encoders/ag32                                  36s 518MB
Oct 01 08:00:48 Starting compiler/backend/x64
Oct 01 08:01:23 Finished compiler/backend/x64                                    34s 869MB
Oct 01 08:01:23 Starting compiler/backend/arm7
Oct 01 08:02:05 Finished compiler/backend/arm7                                   41s   1GB
Oct 01 08:02:05 Starting compiler/backend/arm8
Oct 01 08:02:47 Finished compiler/backend/arm8                                   41s   1GB
Oct 01 08:02:47 Starting compiler/backend/mips
Oct 01 08:03:26 Finished compiler/backend/mips                                   38s   1GB
Oct 01 08:03:26 Starting compiler/backend/riscv
Oct 01 08:04:05 Finished compiler/backend/riscv                                  37s   1GB
Oct 01 08:04:05 Starting compiler/backend/ag32
Oct 01 08:06:28 Finished compiler/backend/ag32                                 2m22s   1GB
Oct 01 08:06:28 Starting compiler/parsing/proofs
Oct 01 08:18:42 Finished compiler/parsing/proofs                              12m13s 893MB
Oct 01 08:18:42 Starting compiler/inference/proofs
Oct 01 08:24:53 Finished compiler/inference/proofs                             6m10s   1GB
Oct 01 08:24:53 Starting compiler/backend/semantics
Oct 01 08:36:30 Finished compiler/backend/semantics                           11m36s   2GB
Oct 01 08:36:30 Starting compiler/backend/reg_alloc/proofs
Oct 01 08:44:04 Finished compiler/backend/reg_alloc/proofs                     7m33s   1GB
Oct 01 08:44:04 Starting compiler/backend/proofs
Oct 01 10:00:21 Finished compiler/backend/proofs                            1h16m16s   4GB
Oct 01 10:00:21 Starting compiler/encoders/x64/proofs
Oct 01 10:22:27 Finished compiler/encoders/x64/proofs                         22m05s   5GB
Oct 01 10:22:27 Starting compiler/encoders/arm7/proofs
Oct 01 10:51:52 Finished compiler/encoders/arm7/proofs                        29m24s   6GB
Oct 01 10:51:52 Starting compiler/encoders/arm8/proofs
Oct 01 11:06:53 Finished compiler/encoders/arm8/proofs                        14m59s   1GB
Oct 01 11:06:53 Starting compiler/encoders/mips/proofs
Oct 01 11:28:47 Finished compiler/encoders/mips/proofs                        21m53s   2GB
Oct 01 11:28:47 Starting compiler/encoders/riscv/proofs
Oct 01 11:47:56 Finished compiler/encoders/riscv/proofs                       19m08s   1GB
Oct 01 11:47:56 Starting compiler/encoders/ag32/proofs
Oct 01 11:53:26 Finished compiler/encoders/ag32/proofs                         5m29s 769MB
Oct 01 11:53:26 Starting compiler/backend/x64/proofs
Oct 01 11:54:06 Finished compiler/backend/x64/proofs                             39s   1GB
Oct 01 11:54:06 Starting compiler/backend/arm7/proofs
Oct 01 11:54:45 Finished compiler/backend/arm7/proofs                            39s   1GB
Oct 01 11:54:46 Starting compiler/backend/arm8/proofs
Oct 01 11:55:23 Finished compiler/backend/arm8/proofs                            37s   1GB
Oct 01 11:55:23 Starting compiler/backend/mips/proofs
Oct 01 11:56:03 Finished compiler/backend/mips/proofs                            39s   1GB
Oct 01 11:56:03 Starting compiler/backend/riscv/proofs
Oct 01 11:56:42 Finished compiler/backend/riscv/proofs                           38s   1GB
Oct 01 11:56:42 Starting compiler/backend/ag32/proofs
Oct 01 12:15:58 Finished compiler/backend/ag32/proofs                         19m15s   2GB
Oct 01 12:15:59 Starting compiler/proofs
Oct 01 12:18:42 Finished compiler/proofs                                       2m42s   2GB
Oct 01 12:18:42 Starting candle/set-theory
Oct 01 12:19:37 Finished candle/set-theory                                       54s 883MB
Oct 01 12:19:37 Starting candle/syntax-lib
Oct 01 12:19:58 Finished candle/syntax-lib                                       20s 525MB
Oct 01 12:19:58 Starting candle/standard/syntax
Oct 01 12:23:45 Finished candle/standard/syntax                                3m47s   1GB
Oct 01 12:23:45 Starting candle/standard/semantics
Oct 01 12:27:19 Finished candle/standard/semantics                             3m33s   1GB
Oct 01 12:27:19 Starting candle/standard/monadic
Oct 01 12:30:41 Finished candle/standard/monadic                               3m21s   1GB
Oct 01 12:30:41 Starting candle/standard/ml_kernel
Oct 01 12:38:49 Finished candle/standard/ml_kernel                             8m07s   3GB
Oct 01 12:38:49 Starting candle/standard/opentheory
Oct 01 12:57:52 Finished candle/standard/opentheory                           19m02s   3GB
Oct 01 12:57:52 Starting candle/standard/opentheory/compilation
Oct 01 14:00:37 Finished candle/standard/opentheory/compilation             1h02m44s  15GB
Oct 01 14:00:38 Starting candle/standard/opentheory/compilation/proofs
Oct 01 14:02:13 Finished candle/standard/opentheory/compilation/proofs         1m34s   2GB
Oct 01 14:02:13 Starting characteristic/examples
Oct 01 14:05:13 Finished characteristic/examples                               3m00s   2GB
Oct 01 14:05:13 Starting tutorial/solutions
Oct 01 14:34:05 Finished tutorial/solutions                                   28m51s   7GB
Oct 01 14:34:05 Starting translator/monadic/examples
Oct 01 14:39:21 Finished translator/monadic/examples                           5m15s   2GB
Oct 01 14:39:21 Starting examples
Oct 01 14:44:54 FAILED: examples
]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/formal-languages]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-1045/basis]0;Holmake: ~/regression/cakeml-1045/basis/pure]0;Holmake: ~/regression/cakeml-1045/misc]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-1045/misc]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-fdba23b05ca01a36aa6d330d2adeb55601b76924/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-1045/misc]0;Holmake: ~/regression/cakeml-1045/developers]0;Holmake: ~/regression/cakeml-1045/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-1045/misc]0;Holmake: ~/regression/cakeml-1045/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1045/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1045/misc]0;Holmake: ~/regression/cakeml-1045/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-1045/basis/pure]0;Holmake: ~/regression/cakeml-1045/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-1045/basis]0;Holmake: ~/regression/cakeml-1045/characteristic]0;Holmake: ~/regression/cakeml-1045/compiler/parsing]0;Holmake: ~/regression/cakeml-1045/semantics]0;Holmake: ~/regression/cakeml-1045/semantics/ffi]0;Holmake: ~/regression/cakeml-1045/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-1045/semantics]0;Holmake: ~/regression/cakeml-1045/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-1045/compiler/parsing]0;Holmake: ~/regression/cakeml-1045/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-1045/characteristic]0;Holmake: ~/regression/cakeml-1045/semantics/proofs]0;Holmake: ~/regression/cakeml-1045/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-1045/characteristic]0;Holmake: ~/regression/cakeml-1045/translator]0;Holmake: ~/regression/cakeml-1045/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-1045/characteristic]0;Holmake: ~/regression/cakeml-1045/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-1045/basis]0;Holmake: ~/regression/cakeml-1045/translator/monadic]0;Holmake: ~/regression/cakeml-1045/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-1045/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-1045/translator/monadic]0;Holmake: ~/regression/cakeml-1045/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-1045/basis]0;Holmake: ~/regression/cakeml-1045/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                                                                                                                                                                          real:   26s  user:   24s     OK
Starting work on diffTheory
diffTheory                                                                                                                                                                         real:   83s  user:   81s     OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                                                      real:  146s  user:  141s     OK
Starting work on doubleProgTheory
quicksortProgTheory                                                                                                                                                                real:  205s  user:  199s     OK
Starting work on array_searchProgTheory
divTheory                                                                                                                                                                          real:  263s  user:  256s     OK
Starting work on echoProgTheory
diffProgTheory                                                                                                                                                                     real:  155s  user:  149s     OK
Starting work on filterProgTheory
doubleProgTheory                                                                                                                                                                   real:  182s  user:  178s     OK
Starting work on grepProgTheory
filterProgTheory                                                                                                                                                                   real:   64s  user:   60sFAIL<1>
   pattern completion has added 1 clause to the original specification.>>
 <<HOL message: mk_functional: 
   pattern completion has added 1 clause to the original specification.>>
 error in quse /root/regression/cakeml-1045/examples/filterProgScript.sml : Fail "Static Errors"
 error in load filterProgScript : Fail "Static Errors"
 <<HOL message: Created theory "filterProg">>
 Loading translation: MapProg ... done.
 /root/regression/cakeml-1045/examples/filterProgScript.sml:26: error: Value or constructor (regexp_compset) has not been declared in structure regexpLib
 Found near regexpLib.regexp_compset ()
 Uncaught exception: Fail "Static Errors"
array_searchProgTheory                                                                                                                                                                                     M-KILLED
echoProgTheory                                                                                                                                                                                             M-KILLED
grepProgTheory                                                                                                                                                                                             M-KILLED