Job 510

CakeML:747a323c230d3c8f26d9ff8769b6fba15056be00
  Update HOL_STORE precondition theorem [Aug 28 11:11:46]
#511 (argparse)
Merging into:153ef4270fca8b5a3d6e9652f1f11edbad70406a
  Add reader compilation theories to build-sequence [Sep 26 17:48:15]
HOL:b42a4b729800b9a771bd1820e31e0ada14653ffb
  Document strange uninterruptibility of {PROVE,METIS}_TAC in comment [Oct 02 06:56:54]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Oct 03 06:04:42 Claimed job
Oct 03 06:04:53 Building HOL
Oct 03 06:19:34 Starting developers/bin
Oct 03 06:19:44 Finished developers/bin                                           8s 148MB
Oct 03 06:19:46 Starting semantics/ffi
Oct 03 06:20:52 Finished semantics/ffi                                         1m04s 399MB
Oct 03 06:20:54 Starting semantics
Oct 03 06:23:16 Finished semantics                                             2m19s 844MB
Oct 03 06:23:18 Starting semantics/proofs
Oct 03 06:27:30 Finished semantics/proofs                                      4m10s 994MB
Oct 03 06:27:32 Starting basis/pure
Oct 03 06:33:11 Finished basis/pure                                            5m36s 799MB
Oct 03 06:33:13 Starting translator
Oct 03 06:35:04 Finished translator                                            1m49s 985MB
Oct 03 06:35:06 Starting compiler/parsing
Oct 03 06:37:27 Finished compiler/parsing                                      2m18s   1GB
Oct 03 06:37:29 Starting characteristic
Oct 03 06:41:31 Finished characteristic                                        4m00s   1GB
Oct 03 06:41:33 Starting translator/monadic
Oct 03 06:44:00 Finished translator/monadic                                    2m25s   1GB
Oct 03 06:44:02 Starting basis
Oct 03 07:13:48 Finished basis                                                29m43s   4GB
Oct 03 07:13:50 Starting compiler/inference
Oct 03 07:16:33 Finished compiler/inference                                    2m41s   1GB
Oct 03 07:16:35 Starting compiler/backend/reg_alloc
Oct 03 07:17:55 Finished compiler/backend/reg_alloc                            1m18s   1GB
Oct 03 07:17:57 Starting compiler/backend/gc
Oct 03 07:32:09 Finished compiler/backend/gc                                  14m08s   3GB
Oct 03 07:32:11 Starting compiler/backend
Oct 03 07:32:16 Finished compiler/backend                                         3s  17MB
Oct 03 07:32:18 Starting compiler/encoders/asm
Oct 03 07:32:22 Finished compiler/encoders/asm                                    1s  11MB
Oct 03 07:32:24 Starting compiler/encoders/x64
Oct 03 07:33:58 Finished compiler/encoders/x64                                 1m32s 629MB
Oct 03 07:34:00 Starting compiler/encoders/arm6
Oct 03 07:37:02 Finished compiler/encoders/arm6                                2m59s   1GB
Oct 03 07:37:04 Starting compiler/encoders/arm8
Oct 03 07:37:53 Finished compiler/encoders/arm8                                  46s 476MB
Oct 03 07:37:55 Starting compiler/encoders/mips
Oct 03 07:39:32 Finished compiler/encoders/mips                                1m35s 857MB
Oct 03 07:39:34 Starting compiler/encoders/riscv
Oct 03 07:41:15 Finished compiler/encoders/riscv                               1m39s 860MB
Oct 03 07:41:17 Starting compiler/backend/x64
Oct 03 07:41:48 Finished compiler/backend/x64                                    28s   1GB
Oct 03 07:41:50 Starting compiler/backend/arm6
Oct 03 07:42:21 Finished compiler/backend/arm6                                   29s   1GB
Oct 03 07:42:23 Starting compiler/backend/arm8
Oct 03 07:42:54 Finished compiler/backend/arm8                                   29s   1GB
Oct 03 07:42:56 Starting compiler/backend/mips
Oct 03 07:43:28 Finished compiler/backend/mips                                   30s   1GB
Oct 03 07:43:30 Starting compiler/backend/riscv
Oct 03 07:44:02 Finished compiler/backend/riscv                                  29s 930MB
Oct 03 07:44:04 Starting compiler/parsing/proofs
Oct 03 07:54:11 Finished compiler/parsing/proofs                              10m05s 945MB
Oct 03 07:54:13 Starting compiler/inference/proofs
Oct 03 07:58:41 Finished compiler/inference/proofs                             4m25s   1GB
Oct 03 07:58:43 Starting compiler/backend/semantics
Oct 03 08:12:28 Finished compiler/backend/semantics                           13m43s   2GB
Oct 03 08:12:30 Starting compiler/backend/reg_alloc/proofs
Oct 03 08:23:44 Finished compiler/backend/reg_alloc/proofs                    11m11s 464MB
Oct 03 08:23:46 Starting compiler/backend/proofs
Oct 03 09:17:02 Finished compiler/backend/proofs                              53m14s   3GB
Oct 03 09:17:04 Starting compiler/encoders/x64/proofs
Oct 03 09:29:10 Finished compiler/encoders/x64/proofs                         12m03s   4GB
Oct 03 09:29:12 Starting compiler/encoders/arm6/proofs
Oct 03 09:41:04 Finished compiler/encoders/arm6/proofs                        11m49s   2GB
Oct 03 09:41:06 Starting compiler/encoders/arm8/proofs
Oct 03 09:49:35 Finished compiler/encoders/arm8/proofs                         8m27s   1GB
Oct 03 09:49:37 Starting compiler/encoders/mips/proofs
Oct 03 10:01:21 Finished compiler/encoders/mips/proofs                        11m41s   1GB
Oct 03 10:01:23 Starting compiler/encoders/riscv/proofs
Oct 03 10:14:01 Finished compiler/encoders/riscv/proofs                       12m35s 928MB
Oct 03 10:14:03 Starting compiler/backend/x64/proofs
Oct 03 10:14:40 Finished compiler/backend/x64/proofs                             34s 731MB
Oct 03 10:14:42 Starting compiler/backend/arm6/proofs
Oct 03 10:15:19 Finished compiler/backend/arm6/proofs                            35s   1GB
Oct 03 10:15:21 Starting compiler/backend/arm8/proofs
Oct 03 10:15:55 Finished compiler/backend/arm8/proofs                            32s   1GB
Oct 03 10:15:57 Starting compiler/backend/mips/proofs
Oct 03 10:16:30 Finished compiler/backend/mips/proofs                            31s   1GB
Oct 03 10:16:32 Starting compiler/backend/riscv/proofs
Oct 03 10:17:07 Finished compiler/backend/riscv/proofs                           32s   1GB
Oct 03 10:17:09 Starting compiler/proofs
Oct 03 10:19:43 Finished compiler/proofs                                       2m31s   2GB
Oct 03 10:19:45 Starting candle/set-theory
Oct 03 10:20:39 Finished candle/set-theory                                       51s 598MB
Oct 03 10:20:41 Starting candle/syntax-lib
Oct 03 10:20:58 Finished candle/syntax-lib                                       15s 564MB
Oct 03 10:21:00 Starting candle/standard/syntax
Oct 03 10:23:33 Finished candle/standard/syntax                                2m31s 963MB
Oct 03 10:23:35 Starting candle/standard/semantics
Oct 03 10:25:51 Finished candle/standard/semantics                             2m14s 892MB
Oct 03 10:25:53 Starting candle/standard/monadic
Oct 03 10:28:23 Finished candle/standard/monadic                               2m28s 948MB
Oct 03 10:28:25 Starting candle/standard/ml_kernel
Oct 03 10:59:39 Finished candle/standard/ml_kernel                            31m11s   6GB
Oct 03 10:59:41 Starting candle/standard/opentheory
Oct 03 11:14:38 Finished candle/standard/opentheory                           14m54s   7GB
Oct 03 11:14:40 Starting candle/standard/opentheory/compilation
Oct 03 12:06:56 Finished candle/standard/opentheory/compilation               52m14s  18GB
Oct 03 12:06:58 Starting characteristic/examples
Oct 03 12:09:52 Finished characteristic/examples                               2m51s   2GB
Oct 03 12:09:54 Starting tutorial/solutions
Oct 03 12:33:28 Finished tutorial/solutions                                   23m32s   7GB
Oct 03 12:33:30 Starting translator/monadic/examples
Oct 03 12:36:09 Finished translator/monadic/examples                           2m36s   2GB
Oct 03 12:36:11 Starting examples
Oct 03 12:44:30 Finished examples                                              8m17s   6GB
Oct 03 12:44:32 Starting examples/compilation
Oct 03 16:02:34 Finished examples/compilation                               3h17m59s  11GB
Oct 03 16:02:36 Starting examples/compilation/proofs
Oct 03 16:06:10 Finished examples/compilation/proofs                           3m32s   3GB
Oct 03 16:06:12 Starting compiler/benchmarks
Oct 03 16:06:15 Finished compiler/benchmarks                                      0s   4MB
Oct 03 16:06:17 Starting translator/okasaki-examples
Oct 03 16:11:43 Finished translator/okasaki-examples                           5m24s   1GB
Oct 03 16:11:45 Starting translator/other-examples
Oct 03 16:17:36 Finished translator/other-examples                             5m48s 843MB
Oct 03 16:17:38 Starting compiler/parsing/tests
Oct 03 16:18:20 Finished compiler/parsing/tests                                  39s 359MB
Oct 03 16:18:22 Starting compiler/inference/tests
Oct 03 16:50:18 FAILED: compiler/inference/tests
]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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: ..]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/inference/tests[0m
Starting work on basisTypeCheckTheory
basisTypeCheckTheory                                                                                                                              FAILED! <1>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 /scratch/cakeml/regression/cakeml-510/compiler/inference/unifyLib.sml:35: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /scratch/cakeml/regression/cakeml-510/compiler/inference/unifyLib.sml:53: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /scratch/cakeml/regression/cakeml-510/compiler/inference/unifyLib.sml:59: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /scratch/cakeml/regression/cakeml-510/compiler/inference/unifyLib.sml:65: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 <<HOL message: Created theory "basisTypeCheck">>
 Warning - Unable to increase stack - interrupting thread
 error in quse /scratch/cakeml/regression/cakeml-510/compiler/inference/tests/basisTypeCheckScript.sml : Interrupt
 error in load basisTypeCheckScript : Interrupt
 Uncaught exception: Interrupt