Job 433

CakeML:42c919452dd418e7f3f60eec74e38fb6a9cc9d41
  Rename `flag` configuration type to `flagConf` [Aug 17 12:24:35]
#511 (argparse)
Merging into:e12dc542637af6649c97ecf8b12bc490db3840e1
  Fix more missing ERRs [Aug 19 08:01:39]
HOL:f59f1264f77465a8321b6b7c9115f007db7d2bc1
  Fix a missing ERR definition [Aug 18 19:10:45]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Aug 19 08:08:44 Claimed job
Aug 19 08:08:51 Reusing HOL
Aug 19 08:09:15 Starting developers/bin
Aug 19 08:09:25 Finished developers/bin                                           7s 142MB
Aug 19 08:09:27 Starting semantics/ffi
Aug 19 08:09:45 Finished semantics/ffi                                           16s 242MB
Aug 19 08:09:47 Starting semantics
Aug 19 08:11:46 Finished semantics                                             1m56s 824MB
Aug 19 08:11:48 Starting semantics/proofs
Aug 19 08:17:05 Finished semantics/proofs                                      5m15s   1GB
Aug 19 08:17:07 Starting basis/pure
Aug 19 08:18:40 Finished basis/pure                                            1m30s 714MB
Aug 19 08:18:41 Starting translator
Aug 19 08:21:32 Finished translator                                            2m48s 922MB
Aug 19 08:21:34 Starting compiler/parsing
Aug 19 08:23:51 Finished compiler/parsing                                      2m15s   2GB
Aug 19 08:23:53 Starting characteristic
Aug 19 08:28:17 Finished characteristic                                        4m22s   1GB
Aug 19 08:28:19 Starting translator/monadic
Aug 19 08:30:57 Finished translator/monadic                                    2m35s   1GB
Aug 19 08:30:59 Starting basis
Aug 19 09:01:43 Finished basis                                                30m42s   4GB
Aug 19 09:01:45 Starting compiler/inference
Aug 19 09:04:05 Finished compiler/inference                                    2m17s   1GB
Aug 19 09:04:07 Starting compiler/backend/reg_alloc
Aug 19 09:05:03 Finished compiler/backend/reg_alloc                              54s   1GB
Aug 19 09:05:05 Starting compiler/backend/gc
Aug 19 09:18:11 Finished compiler/backend/gc                                  13m02s   3GB
Aug 19 09:18:12 Starting compiler/backend
Aug 19 09:18:18 Finished compiler/backend                                         3s  14MB
Aug 19 09:18:19 Starting compiler/encoders/asm
Aug 19 09:18:22 Finished compiler/encoders/asm                                    0s  12MB
Aug 19 09:18:24 Starting compiler/encoders/x64
Aug 19 09:18:52 Finished compiler/encoders/x64                                   26s 405MB
Aug 19 09:18:54 Starting compiler/encoders/arm6
Aug 19 09:20:06 Finished compiler/encoders/arm6                                1m09s 374MB
Aug 19 09:20:08 Starting compiler/encoders/arm8
Aug 19 09:20:22 Finished compiler/encoders/arm8                                  11s 362MB
Aug 19 09:20:24 Starting compiler/encoders/mips
Aug 19 09:20:41 Finished compiler/encoders/mips                                  14s 499MB
Aug 19 09:20:42 Starting compiler/encoders/riscv
Aug 19 09:20:57 Finished compiler/encoders/riscv                                 12s 394MB
Aug 19 09:20:59 Starting compiler/backend/x64
Aug 19 09:21:32 Finished compiler/backend/x64                                    31s   1GB
Aug 19 09:21:34 Starting compiler/backend/arm6
Aug 19 09:22:10 Finished compiler/backend/arm6                                   33s   1GB
Aug 19 09:22:12 Starting compiler/backend/arm8
Aug 19 09:22:45 Finished compiler/backend/arm8                                   31s   1GB
Aug 19 09:22:47 Starting compiler/backend/mips
Aug 19 09:23:21 Finished compiler/backend/mips                                   31s   1GB
Aug 19 09:23:22 Starting compiler/backend/riscv
Aug 19 09:23:53 Finished compiler/backend/riscv                                  28s 748MB
Aug 19 09:23:55 Starting compiler/parsing/proofs
Aug 19 09:27:58 Finished compiler/parsing/proofs                               4m01s   1GB
Aug 19 09:28:00 Starting compiler/inference/proofs
Aug 19 09:32:49 Finished compiler/inference/proofs                             4m46s   1GB
Aug 19 09:32:51 Starting compiler/backend/semantics
Aug 19 09:47:19 Finished compiler/backend/semantics                           14m25s   2GB
Aug 19 09:47:21 Starting compiler/backend/reg_alloc/proofs
Aug 19 09:48:46 Finished compiler/backend/reg_alloc/proofs                     1m23s 398MB
Aug 19 09:48:48 Starting compiler/backend/proofs
Aug 19 10:43:34 Finished compiler/backend/proofs                              54m43s   3GB
Aug 19 10:43:36 Starting compiler/encoders/x64/proofs
Aug 19 10:53:29 Finished compiler/encoders/x64/proofs                          9m49s 910MB
Aug 19 10:53:31 Starting compiler/encoders/arm6/proofs
Aug 19 11:03:28 Finished compiler/encoders/arm6/proofs                         9m54s   1GB
Aug 19 11:03:30 Starting compiler/encoders/arm8/proofs
Aug 19 11:11:40 Finished compiler/encoders/arm8/proofs                         8m07s   1GB
Aug 19 11:11:41 Starting compiler/encoders/mips/proofs
Aug 19 11:23:26 Finished compiler/encoders/mips/proofs                        11m42s   2GB
Aug 19 11:23:28 Starting compiler/encoders/riscv/proofs
Aug 19 11:35:55 Finished compiler/encoders/riscv/proofs                       12m24s   1GB
Aug 19 11:35:57 Starting compiler/backend/x64/proofs
Aug 19 11:36:31 Finished compiler/backend/x64/proofs                             32s   1GB
Aug 19 11:36:33 Starting compiler/backend/arm6/proofs
Aug 19 11:37:11 Finished compiler/backend/arm6/proofs                            35s 993MB
Aug 19 11:37:13 Starting compiler/backend/arm8/proofs
Aug 19 11:37:48 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 19 11:37:50 Starting compiler/backend/mips/proofs
Aug 19 11:38:25 Finished compiler/backend/mips/proofs                            33s   1GB
Aug 19 11:38:27 Starting compiler/backend/riscv/proofs
Aug 19 11:39:02 Finished compiler/backend/riscv/proofs                           32s   1GB
Aug 19 11:39:04 Starting compiler/proofs
Aug 19 11:41:37 Finished compiler/proofs                                       2m31s   2GB
Aug 19 11:41:39 Starting candle/set-theory
Aug 19 11:42:25 Finished candle/set-theory                                       43s 591MB
Aug 19 11:42:27 Starting candle/syntax-lib
Aug 19 11:42:46 Finished candle/syntax-lib                                       17s 373MB
Aug 19 11:42:48 Starting candle/standard/syntax
Aug 19 11:45:35 Finished candle/standard/syntax                                2m45s 831MB
Aug 19 11:45:37 Starting candle/standard/semantics
Aug 19 11:47:58 Finished candle/standard/semantics                             2m19s   1GB
Aug 19 11:48:00 Starting candle/standard/monadic
Aug 19 11:50:20 Finished candle/standard/monadic                               2m17s   1GB
Aug 19 11:50:22 Starting candle/standard/ml_kernel
Aug 19 11:56:14 Finished candle/standard/ml_kernel                             5m48s   2GB
Aug 19 11:56:16 Starting candle/standard/opentheory
Aug 19 11:56:41 Finished candle/standard/opentheory                              23s 742MB
Aug 19 11:56:43 Starting characteristic/examples
Aug 19 11:59:34 Finished characteristic/examples                               2m48s   2GB
Aug 19 11:59:36 Starting tutorial/solutions
Aug 19 12:22:19 Finished tutorial/solutions                                   22m41s   6GB
Aug 19 12:22:21 Starting translator/monadic/examples
Aug 19 12:25:13 Finished translator/monadic/examples                           2m49s   2GB
Aug 19 12:25:15 Starting examples
Aug 19 12:28:06 FAILED: examples
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ../basis]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developers[1mWorking in ../developers[0m
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../misc]0;Holmake: ../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../basis]0;Holmake: ../characteristic]0;Holmake: ../compiler/parsing]0;Holmake: ../semantics]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../compiler/parsing]0;Holmake: ../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../characteristic]0;Holmake: ../translator]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../translator]0;Holmake: ../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../characteristic]0;Holmake: ../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../basis]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../basis]0;Holmake: ../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
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
diffTheory                                                                                                                                                OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                             OK
Starting work on helloProgTheory
helloErrProgTheory                                                                                                                                        OK
Starting work on insertSortProgTheory
grepProgTheory                                                                                                                                   FAILED! <1>
 Saved theorem _____ "regexp_matcher_with_limit_v_thm"
 Saved theorem _____ "tolist_fromlist_map_cancel"
 Updating regexp_matcher_with_limit_v_thm
 Saved theorem _____ "regexp_matcher_with_limit_v_thm"
 Saved theorem _____ "regexp_matcher_correct"
 Saved theorem _____ "INTRO_FLOOKUP"
 Translating coreloop_1
 error in quse /scratch/cakeml/regression/cakeml-433/examples/grepProgScript.sml : HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
 error in load grepProgScript : HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
 Uncaught exception: HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
diffProgTheory                                                                                                                                      M-KILLED
helloProgTheory                                                                                                                                     M-KILLED
insertSortProgTheory                                                                                                                                M-KILLED