Job 465

CakeML:747a323c230d3c8f26d9ff8769b6fba15056be00
  Update HOL_STORE precondition theorem [Aug 28 11:11:46]
#511 (argparse)
Merging into:f6d8ed2ee71091a75c6c7c634490380e8abe11a9
  Fix typo [Aug 28 07:46:30]
HOL:cc8f983f09c21e413738c986d6ce54b256e8feef
  Promote more functions from Isabelle Library into Portable [Aug 30 02:04:45]
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux

Aug 30 15:16:03 Claimed job
Aug 30 15:16:14 Building HOL
Aug 30 15:29:53 Starting developers/bin
Aug 30 15:30:03 Finished developers/bin                                           7s 144MB
Aug 30 15:30:05 Starting semantics/ffi
Aug 30 15:31:05 Finished semantics/ffi                                           57s 382MB
Aug 30 15:31:07 Starting semantics
Aug 30 15:33:30 Finished semantics                                             2m21s 804MB
Aug 30 15:33:32 Starting semantics/proofs
Aug 30 15:38:43 Finished semantics/proofs                                      5m08s   1GB
Aug 30 15:38:44 Starting basis/pure
Aug 30 15:44:34 Finished basis/pure                                            5m47s 640MB
Aug 30 15:44:36 Starting translator
Aug 30 15:46:33 Finished translator                                            1m54s 882MB
Aug 30 15:46:35 Starting compiler/parsing
Aug 30 15:48:55 Finished compiler/parsing                                      2m17s   2GB
Aug 30 15:48:57 Starting characteristic
Aug 30 15:53:26 Finished characteristic                                        4m26s   1GB
Aug 30 15:53:28 Starting translator/monadic
Aug 30 15:56:05 Finished translator/monadic                                    2m35s   1GB
Aug 30 15:56:07 Starting basis
Aug 30 16:27:23 Finished basis                                                31m13s   4GB
Aug 30 16:27:26 Starting compiler/inference
Aug 30 16:30:11 Finished compiler/inference                                    2m43s   1GB
Aug 30 16:30:13 Starting compiler/backend/reg_alloc
Aug 30 16:31:37 Finished compiler/backend/reg_alloc                            1m21s   1GB
Aug 30 16:31:39 Starting compiler/backend/gc
Aug 30 16:46:33 Finished compiler/backend/gc                                  14m52s   3GB
Aug 30 16:46:35 Starting compiler/backend
Aug 30 16:46:40 Finished compiler/backend                                         3s  21MB
Aug 30 16:46:42 Starting compiler/encoders/asm
Aug 30 16:46:46 Finished compiler/encoders/asm                                    0s  11MB
Aug 30 16:46:48 Starting compiler/encoders/x64
Aug 30 16:48:17 Finished compiler/encoders/x64                                 1m27s 613MB
Aug 30 16:48:19 Starting compiler/encoders/arm6
Aug 30 16:51:16 Finished compiler/encoders/arm6                                2m54s   1GB
Aug 30 16:51:18 Starting compiler/encoders/arm8
Aug 30 16:52:02 Finished compiler/encoders/arm8                                  42s 413MB
Aug 30 16:52:04 Starting compiler/encoders/mips
Aug 30 16:53:41 Finished compiler/encoders/mips                                1m34s 712MB
Aug 30 16:53:43 Starting compiler/encoders/riscv
Aug 30 16:55:19 Finished compiler/encoders/riscv                               1m34s 495MB
Aug 30 16:55:21 Starting compiler/backend/x64
Aug 30 16:55:51 Finished compiler/backend/x64                                    28s 765MB
Aug 30 16:55:53 Starting compiler/backend/arm6
Aug 30 16:56:27 Finished compiler/backend/arm6                                   31s   1GB
Aug 30 16:56:29 Starting compiler/backend/arm8
Aug 30 16:57:01 Finished compiler/backend/arm8                                   30s   1GB
Aug 30 16:57:03 Starting compiler/backend/mips
Aug 30 16:57:37 Finished compiler/backend/mips                                   32s   1GB
Aug 30 16:57:39 Starting compiler/backend/riscv
Aug 30 16:58:13 Finished compiler/backend/riscv                                  32s   1GB
Aug 30 16:58:15 Starting compiler/parsing/proofs
Aug 30 17:02:17 Finished compiler/parsing/proofs                               3m59s 936MB
Aug 30 17:02:19 Starting compiler/inference/proofs
Aug 30 17:07:08 Finished compiler/inference/proofs                             4m47s   1GB
Aug 30 17:07:10 Starting compiler/backend/semantics
Aug 30 17:21:37 Finished compiler/backend/semantics                           14m25s   3GB
Aug 30 17:21:39 Starting compiler/backend/reg_alloc/proofs
Aug 30 17:33:23 Finished compiler/backend/reg_alloc/proofs                    11m40s 593MB
Aug 30 17:33:26 Starting compiler/backend/proofs
Aug 30 18:28:10 Finished compiler/backend/proofs                              54m40s   3GB
Aug 30 18:28:12 Starting compiler/encoders/x64/proofs
Aug 30 18:39:51 Finished compiler/encoders/x64/proofs                         11m37s   1GB
Aug 30 18:39:53 Starting compiler/encoders/arm6/proofs
Aug 30 18:52:00 Finished compiler/encoders/arm6/proofs                        12m04s   2GB
Aug 30 18:52:02 Starting compiler/encoders/arm8/proofs
Aug 30 19:00:26 Finished compiler/encoders/arm8/proofs                         8m21s 882MB
Aug 30 19:00:28 Starting compiler/encoders/mips/proofs
Aug 30 19:12:13 Finished compiler/encoders/mips/proofs                        11m42s   1GB
Aug 30 19:12:15 Starting compiler/encoders/riscv/proofs
Aug 30 19:24:49 Finished compiler/encoders/riscv/proofs                       12m32s 863MB
Aug 30 19:24:51 Starting compiler/backend/x64/proofs
Aug 30 19:25:27 Finished compiler/backend/x64/proofs                             33s   1GB
Aug 30 19:25:29 Starting compiler/backend/arm6/proofs
Aug 30 19:26:08 Finished compiler/backend/arm6/proofs                            37s   1GB
Aug 30 19:26:10 Starting compiler/backend/arm8/proofs
Aug 30 19:26:45 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 30 19:26:47 Starting compiler/backend/mips/proofs
Aug 30 19:27:24 Finished compiler/backend/mips/proofs                            35s   1GB
Aug 30 19:27:26 Starting compiler/backend/riscv/proofs
Aug 30 19:28:03 Finished compiler/backend/riscv/proofs                           34s   1GB
Aug 30 19:28:05 Starting compiler/proofs
Aug 30 19:30:41 Finished compiler/proofs                                       2m33s   2GB
Aug 30 19:30:43 Starting candle/set-theory
Aug 30 19:31:40 Finished candle/set-theory                                       55s 555MB
Aug 30 19:31:42 Starting candle/syntax-lib
Aug 30 19:32:03 Finished candle/syntax-lib                                       17s 582MB
Aug 30 19:32:05 Starting candle/standard/syntax
Aug 30 19:34:48 Finished candle/standard/syntax                                2m41s 614MB
Aug 30 19:34:50 Starting candle/standard/semantics
Aug 30 19:37:05 Finished candle/standard/semantics                             2m12s 779MB
Aug 30 19:37:08 Starting candle/standard/monadic
Aug 30 19:39:47 Finished candle/standard/monadic                               2m36s   1GB
Aug 30 19:39:49 Starting candle/standard/ml_kernel
Aug 30 20:11:16 Finished candle/standard/ml_kernel                            31m25s   5GB
Aug 30 20:11:18 Starting candle/standard/opentheory
Aug 30 20:26:53 Finished candle/standard/opentheory                           15m33s   5GB
Aug 30 20:26:55 Starting characteristic/examples
Aug 30 20:29:54 Finished characteristic/examples                               2m56s   2GB
Aug 30 20:29:56 Starting tutorial/solutions
Aug 30 20:52:49 Finished tutorial/solutions                                   22m50s   5GB
Aug 30 20:52:51 Starting translator/monadic/examples
Aug 30 20:55:45 Finished translator/monadic/examples                           2m51s   3GB
Aug 30 20:55:47 Starting examples
Aug 30 21:04:37 Finished examples                                              8m48s   5GB
Aug 30 21:04:39 Starting examples/compilation
Aug 31 00:13:19 Finished examples/compilation                               3h08m37s   8GB
Aug 31 00:13:21 Starting examples/compilation/proofs
Aug 31 00:17:19 Finished examples/compilation/proofs                           3m56s   3GB
Aug 31 00:17:21 Starting compiler/benchmarks
Aug 31 00:17:23 Finished compiler/benchmarks                                      0s   4MB
Aug 31 00:17:25 Starting translator/okasaki-examples
Aug 31 00:23:49 Finished translator/okasaki-examples                           6m21s   1GB
Aug 31 00:23:51 Starting translator/other-examples
Aug 31 00:30:33 Finished translator/other-examples                             6m39s 945MB
Aug 31 00:30:35 Starting compiler/parsing/tests
Aug 31 00:31:18 Finished compiler/parsing/tests                                  40s 341MB
Aug 31 00:31:20 Starting compiler/inference/tests
Aug 31 21:38:27 FAILED: compiler/inference/tests
]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/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-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/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-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/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-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-cc8f983f09c21e413738c986d6ce54b256e8feef/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-465/compiler/inference/unifyLib.sml:35: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /scratch/cakeml/regression/cakeml-465/compiler/inference/unifyLib.sml:53: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /scratch/cakeml/regression/cakeml-465/compiler/inference/unifyLib.sml:59: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /scratch/cakeml/regression/cakeml-465/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-465/compiler/inference/tests/basisTypeCheckScript.sml : Interrupt
 error in load basisTypeCheckScript : Interrupt
 Uncaught exception: Interrupt