Job 1205

CakeML:7104ca1f213a86b2594c6c526332fb16a26fd7d8
  Make translator able to emit `Let NONE ... ...` [Mar 12 14:37:23]
#733 (trans-pure-seq)
Merging into:c42539bd7447e5469c5648b185e15ce5259957f8
  Merge pull request #731 from CakeML/source_assert [Mar 06 07:23:32]
HOL:ba25c5756203bd0ef0d73e04022916ccb291e1e5
  Write some comment-documentation [Mar 10 00:09:00]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Mar 12 15:43:46 Claimed job
Mar 12 15:43:54 Building HOL
Mar 12 15:55:50 Starting developers
Mar 12 15:55:53 Finished developers                                               2s  71MB
Mar 12 15:55:53 Starting developers/bin
Mar 12 15:56:00 Finished developers/bin                                           6s   1GB
Mar 12 15:56:00 Starting semantics/ffi
Mar 12 15:56:09 Finished semantics/ffi                                            8s 264MB
Mar 12 15:56:09 Starting semantics
Mar 12 15:57:45 Finished semantics                                             1m35s 970MB
Mar 12 15:57:45 Starting semantics/proofs
Mar 12 16:01:21 Finished semantics/proofs                                      3m35s   1GB
Mar 12 16:01:21 Starting semantics/alt_semantics
Mar 12 16:01:28 Finished semantics/alt_semantics                                  7s 325MB
Mar 12 16:01:29 Starting semantics/alt_semantics/proofs
Mar 12 16:03:41 Finished semantics/alt_semantics/proofs                        2m12s 852MB
Mar 12 16:03:41 Starting basis/pure
Mar 12 16:06:48 Finished basis/pure                                            3m06s 839MB
Mar 12 16:06:48 Starting translator
Mar 12 16:09:38 Finished translator                                            2m49s   1GB
Mar 12 16:09:39 Starting compiler/parsing
Mar 12 16:11:02 Finished compiler/parsing                                      1m23s   3GB
Mar 12 16:11:02 Starting characteristic
Mar 12 16:17:16 Finished characteristic                                        6m13s   1GB
Mar 12 16:17:16 Starting translator/monadic
Mar 12 16:18:58 Finished translator/monadic                                    1m42s   1GB
Mar 12 16:18:58 Starting basis
Mar 12 16:52:25 Finished basis                                                33m25s  18GB
Mar 12 16:52:26 Starting compiler/inference
Mar 12 16:53:31 Finished compiler/inference                                    1m05s   1GB
Mar 12 16:53:31 Starting compiler/backend/reg_alloc
Mar 12 16:54:34 Finished compiler/backend/reg_alloc                            1m02s   1GB
Mar 12 16:54:34 Starting compiler/backend/gc
Mar 12 16:57:55 Finished compiler/backend/gc                                   3m20s   2GB
Mar 12 16:57:55 Starting compiler/backend
Mar 12 17:02:23 Finished compiler/backend                                      4m28s   3GB
Mar 12 17:02:23 Starting compiler/encoders/asm
Mar 12 17:02:44 Finished compiler/encoders/asm                                   20s 745MB
Mar 12 17:02:44 Starting compiler/encoders/x64
Mar 12 17:03:39 Finished compiler/encoders/x64                                   54s 987MB
Mar 12 17:03:39 Starting compiler/encoders/arm7
Mar 12 17:05:27 Finished compiler/encoders/arm7                                1m47s   1GB
Mar 12 17:05:27 Starting compiler/encoders/arm8
Mar 12 17:05:58 Finished compiler/encoders/arm8                                  31s 887MB
Mar 12 17:05:58 Starting compiler/encoders/mips
Mar 12 17:07:06 Finished compiler/encoders/mips                                1m07s   1GB
Mar 12 17:07:06 Starting compiler/encoders/riscv
Mar 12 17:08:26 Finished compiler/encoders/riscv                               1m19s   1GB
Mar 12 17:08:26 Starting compiler/encoders/ag32
Mar 12 17:08:43 Finished compiler/encoders/ag32                                  16s 743MB
Mar 12 17:08:43 Starting compiler/backend/x64
Mar 12 17:09:01 Finished compiler/backend/x64                                    17s   1GB
Mar 12 17:09:01 Starting compiler/backend/arm7
Mar 12 17:09:20 Finished compiler/backend/arm7                                   18s   1GB
Mar 12 17:09:20 Starting compiler/backend/arm8
Mar 12 17:09:38 Finished compiler/backend/arm8                                   17s   1GB
Mar 12 17:09:38 Starting compiler/backend/mips
Mar 12 17:09:58 Finished compiler/backend/mips                                   18s   1GB
Mar 12 17:09:58 Starting compiler/backend/riscv
Mar 12 17:10:16 Finished compiler/backend/riscv                                  18s   1GB
Mar 12 17:10:16 Starting compiler/backend/ag32
Mar 12 17:11:24 Finished compiler/backend/ag32                                 1m07s   1GB
Mar 12 17:11:24 Starting compiler/parsing/proofs
Mar 12 17:17:08 Finished compiler/parsing/proofs                               5m43s   1GB
Mar 12 17:17:08 Starting compiler/inference/proofs
Mar 12 17:19:31 Finished compiler/inference/proofs                             2m22s   1GB
Mar 12 17:19:31 Starting compiler/backend/semantics
Mar 12 17:46:58 Finished compiler/backend/semantics                           27m26s   2GB
Mar 12 17:46:58 Starting compiler/backend/reg_alloc/proofs
Mar 12 17:50:23 Finished compiler/backend/reg_alloc/proofs                     3m24s 963MB
Mar 12 17:50:23 Starting compiler/backend/proofs
Mar 12 18:52:21 Finished compiler/backend/proofs                            1h01m58s  16GB
Mar 12 18:52:22 Starting compiler/encoders/x64/proofs
Mar 12 19:01:42 Finished compiler/encoders/x64/proofs                          9m20s   4GB
Mar 12 19:01:42 Starting compiler/encoders/arm7/proofs
Mar 12 19:14:16 Finished compiler/encoders/arm7/proofs                        12m33s   3GB
Mar 12 19:14:17 Starting compiler/encoders/arm8/proofs
Mar 12 19:20:35 Finished compiler/encoders/arm8/proofs                         6m17s   1GB
Mar 12 19:20:35 Starting compiler/encoders/mips/proofs
Mar 12 19:30:18 Finished compiler/encoders/mips/proofs                         9m43s   1GB
Mar 12 19:30:18 Starting compiler/encoders/riscv/proofs
Mar 12 19:39:01 Finished compiler/encoders/riscv/proofs                        8m42s   1GB
Mar 12 19:39:01 Starting compiler/encoders/ag32/proofs
Mar 12 19:41:28 Finished compiler/encoders/ag32/proofs                         2m26s 707MB
Mar 12 19:41:29 Starting compiler/backend/x64/proofs
Mar 12 19:41:47 Finished compiler/backend/x64/proofs                             18s 867MB
Mar 12 19:41:48 Starting compiler/backend/arm7/proofs
Mar 12 19:42:08 Finished compiler/backend/arm7/proofs                            20s   1GB
Mar 12 19:42:08 Starting compiler/backend/arm8/proofs
Mar 12 19:42:26 Finished compiler/backend/arm8/proofs                            18s 865MB
Mar 12 19:42:27 Starting compiler/backend/mips/proofs
Mar 12 19:42:47 Finished compiler/backend/mips/proofs                            20s   1GB
Mar 12 19:42:47 Starting compiler/backend/riscv/proofs
Mar 12 19:43:07 Finished compiler/backend/riscv/proofs                           20s   1GB
Mar 12 19:43:08 Starting compiler/backend/ag32/proofs
Mar 12 19:55:50 Finished compiler/backend/ag32/proofs                         12m41s   2GB
Mar 12 19:55:50 Starting compiler/proofs
Mar 12 19:57:33 Finished compiler/proofs                                       1m42s   2GB
Mar 12 19:57:33 Starting candle/set-theory
Mar 12 19:58:00 Finished candle/set-theory                                       27s   1GB
Mar 12 19:58:01 Starting candle/syntax-lib
Mar 12 19:58:10 Finished candle/syntax-lib                                        9s 656MB
Mar 12 19:58:11 Starting candle/standard/syntax
Mar 12 19:59:56 Finished candle/standard/syntax                                1m45s   1GB
Mar 12 19:59:57 Starting candle/standard/semantics
Mar 12 20:01:37 Finished candle/standard/semantics                             1m40s   1GB
Mar 12 20:01:37 Starting candle/standard/monadic
Mar 12 20:03:13 Finished candle/standard/monadic                               1m35s   1GB
Mar 12 20:03:13 Starting candle/standard/ml_kernel
Mar 12 20:08:17 Finished candle/standard/ml_kernel                             5m03s   6GB
Mar 12 20:08:17 Starting candle/standard/opentheory
Mar 12 20:17:02 Finished candle/standard/opentheory                            8m45s   4GB
Mar 12 20:17:03 Starting candle/standard/opentheory/compilation
Mar 12 20:49:14 Finished candle/standard/opentheory/compilation               32m11s  14GB
Mar 12 20:49:14 Starting candle/standard/opentheory/compilation/proofs
Mar 12 20:49:50 Finished candle/standard/opentheory/compilation/proofs           36s   3GB
Mar 12 20:49:51 Starting candle/overloading/syntax
Mar 12 20:52:51 Finished candle/overloading/syntax                             2m59s   1GB
Mar 12 20:52:51 Starting candle/overloading/semantics
Mar 12 20:59:39 Finished candle/overloading/semantics                          6m47s   3GB
Mar 12 20:59:39 Starting characteristic/examples
Mar 12 21:00:52 Finished characteristic/examples                               1m12s   3GB
Mar 12 21:00:52 Starting tutorial/solutions
Mar 12 21:15:26 Finished tutorial/solutions                                   14m33s   7GB
Mar 12 21:15:26 Starting translator/monadic/examples
Mar 12 21:18:31 Finished translator/monadic/examples                           3m04s   3GB
Mar 12 21:18:31 Starting examples
Mar 12 21:19:51 FAILED: examples
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
README.md                                                                                                                                                 real:    0s  user:    0s     OK
Starting work on lcsTheory
regexp_parserTheory                                                                                                                                       real:   13s  user:   13s     OK
Starting work on divTheory
lcsTheory                                                                                                                                                 real:   14s  user:   13s     OK
Starting work on diffTheory
diffTheory                                                                                                                                                real:   51s  user:   50s     OK
Starting work on diffProgTheory
divTheory                                                                                                                                                 real:   65s  user:   63sFAIL<1>
 
 Exception raised at TotalDefn.Define:
 between line 176, character 2 and line 183, character 49:
 at Defn.stdrec_defn:
 at Induction.mk_induction:
 at Induction.lpartition.part:
 cases missing in defn
 error in quse /home/myreen/regression/cakeml-1205/examples/divScript.sml : HOL_ERR {message = "between line 176, character 2 and line 183, character 49:\nat Defn.stdrec_defn:\nat Induction.mk_induction:\nat Induction.lpartition.part:\ncases missing in defn", origin_function = "Define", origin_structure = "TotalDefn"}
 error in load /home/myreen/regression/cakeml-1205/examples/divScript : HOL_ERR {message = "between line 176, character 2 and line 183, character 49:\nat Defn.stdrec_defn:\nat Induction.mk_induction:\nat Induction.lpartition.part:\ncases missing in defn", origin_function = "Define", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "between line 176, character 2 and line 183, character 49:\nat Defn.stdrec_defn:\nat Induction.mk_induction:\nat Induction.lpartition.part:\ncases missing in defn", origin_function = "Define", origin_structure = "TotalDefn"}
quicksortProgTheory                                                                                                                                                               M-KILLED
catProgTheory                                                                                                                                                                     M-KILLED
diffProgTheory                                                                                                                                                                    M-KILLED