Job 472

CakeML:747a323c230d3c8f26d9ff8769b6fba15056be00
  Update HOL_STORE precondition theorem [Aug 28 11:11:46]
#511 (argparse)
Merging into:1bb8663a0aeb377eb22aeb600de4bc536e647744
  Merge pull request #519 from CakeML/basis_ffi-fix [Sep 05 07:26:39]
HOL:daf1c4e85558a55c5bf4812c6ca711acea77f763
  Document ee54b084d's change in release notes [Sep 05 01:00:03]
Machine:oven1 (2) 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Sep 05 09:46:31 Claimed job
Sep 05 09:46:57 Building HOL
Sep 05 09:56:25 Starting developers/bin
Sep 05 09:57:01 Finished developers/bin                                          36s 912MB
Sep 05 09:57:02 Starting semantics/ffi
Sep 05 09:57:41 Finished semantics/ffi                                           38s 387MB
Sep 05 09:57:42 Starting semantics
Sep 05 09:59:07 Finished semantics                                             1m24s 919MB
Sep 05 09:59:08 Starting semantics/proofs
Sep 05 10:01:50 Finished semantics/proofs                                      2m41s   1GB
Sep 05 10:01:51 Starting basis/pure
Sep 05 10:05:25 Finished basis/pure                                            3m33s 765MB
Sep 05 10:05:26 Starting translator
Sep 05 10:06:32 Finished translator                                            1m05s   1GB
Sep 05 10:06:33 Starting compiler/parsing
Sep 05 10:08:07 Finished compiler/parsing                                      1m33s   2GB
Sep 05 10:08:08 Starting characteristic
Sep 05 10:10:36 Finished characteristic                                        2m27s   1GB
Sep 05 10:10:37 Starting translator/monadic
Sep 05 10:12:04 Finished translator/monadic                                    1m26s   1GB
Sep 05 10:12:05 Starting basis
Sep 05 10:30:34 Finished basis                                                18m28s   5GB
Sep 05 10:30:35 Starting compiler/inference
Sep 05 10:32:17 Finished compiler/inference                                    1m41s   1GB
Sep 05 10:32:18 Starting compiler/backend/reg_alloc
Sep 05 10:33:06 Finished compiler/backend/reg_alloc                              47s 882MB
Sep 05 10:33:06 Starting compiler/backend/gc
Sep 05 10:41:59 Finished compiler/backend/gc                                   8m52s   3GB
Sep 05 10:42:00 Starting compiler/backend
Sep 05 10:42:03 Finished compiler/backend                                         2s  15MB
Sep 05 10:42:04 Starting compiler/encoders/asm
Sep 05 10:42:06 Finished compiler/encoders/asm                                    1s  11MB
Sep 05 10:42:07 Starting compiler/encoders/x64
Sep 05 10:42:59 Finished compiler/encoders/x64                                   52s 602MB
Sep 05 10:43:00 Starting compiler/encoders/arm6
Sep 05 10:44:47 Finished compiler/encoders/arm6                                1m46s   1GB
Sep 05 10:44:48 Starting compiler/encoders/arm8
Sep 05 10:45:14 Finished compiler/encoders/arm8                                  25s 483MB
Sep 05 10:45:15 Starting compiler/encoders/mips
Sep 05 10:46:13 Finished compiler/encoders/mips                                  57s 898MB
Sep 05 10:46:14 Starting compiler/encoders/riscv
Sep 05 10:47:15 Finished compiler/encoders/riscv                               1m00s 680MB
Sep 05 10:47:15 Starting compiler/backend/x64
Sep 05 10:47:34 Finished compiler/backend/x64                                    18s   1GB
Sep 05 10:47:35 Starting compiler/backend/arm6
Sep 05 10:47:54 Finished compiler/backend/arm6                                   18s   1GB
Sep 05 10:47:55 Starting compiler/backend/arm8
Sep 05 10:48:14 Finished compiler/backend/arm8                                   18s   1GB
Sep 05 10:48:15 Starting compiler/backend/mips
Sep 05 10:48:33 Finished compiler/backend/mips                                   17s 808MB
Sep 05 10:48:34 Starting compiler/backend/riscv
Sep 05 10:48:54 Finished compiler/backend/riscv                                  18s   1GB
Sep 05 10:48:54 Starting compiler/parsing/proofs
Sep 05 10:55:05 Finished compiler/parsing/proofs                               6m10s 770MB
Sep 05 10:55:06 Starting compiler/inference/proofs
Sep 05 10:57:56 Finished compiler/inference/proofs                             2m49s   1GB
Sep 05 10:57:57 Starting compiler/backend/semantics
Sep 05 11:06:56 Finished compiler/backend/semantics                            8m58s   2GB
Sep 05 11:06:57 Starting compiler/backend/reg_alloc/proofs
Sep 05 11:14:23 Finished compiler/backend/reg_alloc/proofs                     7m25s 855MB
Sep 05 11:14:24 Starting compiler/backend/proofs
Sep 05 11:49:39 Finished compiler/backend/proofs                              35m14s   3GB
Sep 05 11:49:39 Starting compiler/encoders/x64/proofs
Sep 05 11:57:12 Finished compiler/encoders/x64/proofs                          7m31s   5GB
Sep 05 11:57:13 Starting compiler/encoders/arm6/proofs
Sep 05 12:04:46 Finished compiler/encoders/arm6/proofs                         7m32s   2GB
Sep 05 12:04:46 Starting compiler/encoders/arm8/proofs
Sep 05 12:10:01 Finished compiler/encoders/arm8/proofs                         5m14s   1GB
Sep 05 12:10:02 Starting compiler/encoders/mips/proofs
Sep 05 12:17:22 Finished compiler/encoders/mips/proofs                         7m19s   2GB
Sep 05 12:17:23 Starting compiler/encoders/riscv/proofs
Sep 05 12:25:30 Finished compiler/encoders/riscv/proofs                        8m06s 673MB
Sep 05 12:25:31 Starting compiler/backend/x64/proofs
Sep 05 12:25:51 Finished compiler/backend/x64/proofs                             19s   1GB
Sep 05 12:25:52 Starting compiler/backend/arm6/proofs
Sep 05 12:26:15 Finished compiler/backend/arm6/proofs                            22s 952MB
Sep 05 12:26:16 Starting compiler/backend/arm8/proofs
Sep 05 12:26:37 Finished compiler/backend/arm8/proofs                            19s   1GB
Sep 05 12:26:37 Starting compiler/backend/mips/proofs
Sep 05 12:26:58 Finished compiler/backend/mips/proofs                            20s   1GB
Sep 05 12:26:59 Starting compiler/backend/riscv/proofs
Sep 05 12:27:21 Finished compiler/backend/riscv/proofs                           21s 970MB
Sep 05 12:27:22 Starting compiler/proofs
Sep 05 12:28:43 Finished compiler/proofs                                       1m20s   2GB
Sep 05 12:28:44 Starting candle/set-theory
Sep 05 12:29:15 Finished candle/set-theory                                       30s 589MB
Sep 05 12:29:15 Starting candle/syntax-lib
Sep 05 12:29:26 Finished candle/syntax-lib                                       10s 419MB
Sep 05 12:29:27 Starting candle/standard/syntax
Sep 05 12:31:00 Finished candle/standard/syntax                                1m32s 633MB
Sep 05 12:31:01 Starting candle/standard/semantics
Sep 05 12:32:21 Finished candle/standard/semantics                             1m19s 874MB
Sep 05 12:32:21 Starting candle/standard/monadic
Sep 05 12:33:54 Finished candle/standard/monadic                               1m32s   1GB
Sep 05 12:33:55 Starting candle/standard/ml_kernel
Sep 05 12:54:09 Finished candle/standard/ml_kernel                            20m13s   8GB
Sep 05 12:54:10 Starting candle/standard/opentheory
Sep 05 13:03:22 Finished candle/standard/opentheory                            9m11s   9GB
Sep 05 13:03:23 Starting characteristic/examples
Sep 05 13:05:12 Finished characteristic/examples                               1m47s   2GB
Sep 05 13:05:12 Starting tutorial/solutions
Sep 05 13:19:56 Finished tutorial/solutions                                   14m43s   7GB
Sep 05 13:19:57 Starting translator/monadic/examples
Sep 05 13:21:45 Finished translator/monadic/examples                           1m47s   2GB
Sep 05 13:21:46 Starting examples
Sep 05 13:27:51 Finished examples                                              6m04s   3GB
Sep 05 13:27:51 Starting examples/compilation
Sep 05 15:35:53 Finished examples/compilation                               2h08m00s   9GB
Sep 05 15:35:54 Starting examples/compilation/proofs
Sep 05 15:37:54 Finished examples/compilation/proofs                           2m00s   3GB
Sep 05 15:37:55 Starting compiler/benchmarks
Sep 05 15:37:56 Finished compiler/benchmarks                                      0s   4MB
Sep 05 15:37:57 Starting translator/okasaki-examples
Sep 05 15:41:26 Finished translator/okasaki-examples                           3m28s   1GB
Sep 05 15:41:26 Starting translator/other-examples
Sep 11 15:10:54 Resuming translator/other-examples
Sep 11 15:11:05 FAILED: translator/other-examples
Starting work on README.md
README.md                                                                                                                                                                            OK
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/formal-languages/context-free]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
Starting work on libTheory
libTheory                                                                                                                                                                            OK
]0;Holmake: ../../misc]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/machine-code/hoare-triple]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
Starting work on README.md
README.md                                                                                                                                                                            OK
]0;Holmake: ../../basis/pure]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/balanced_bst]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/formal-languages]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-daf1c4e85558a55c5bf4812c6ca711acea77f763/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../basis/pure]0;Holmake: ../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
Starting work on mlnumTheory
mlnumTheory                                                                                                                                                                 FAILED! <1>
 error in quse /home/cake/regression/cakeml-472/misc/miscTheory.sml : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 error in load $(CAKEMLDIR)/misc/miscTheory : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 error in load $(CAKEMLDIR)/misc/preamble : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 error in load mlnumScript : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 <<HOL message: link_parents: the following parents of "misc"
   should already be in the theory graph (but aren't): ("lib",1536141455,844224)>>
 Exception- HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"} raised
 Uncaught exception: HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
]0;Holmake: ../../basis]0;Holmake: .