Job 546

CakeML:7ec3d29ad8687ebf32ed1df8b94ad5c70a1036be
  Add a comment to ArgParse [Oct 23 08:36:07]
#511 (argparse)
Merging into:33e99acd8473d0f3b26811cff129818bb6b04743
  Merge pull request #545 from CakeML/explorer [Oct 21 01:02:30]
HOL:ad8ad6f4b07521a5c63799c5f1a3d582824cb21f
  Merge pull request #605 from thtuerk/ltl_translations [Oct 24 11:17:16]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Oct 25 01:28:15 Claimed job
Oct 25 01:31:01 Building HOL
Oct 25 01:40:20 Starting developers/bin
Oct 25 01:41:36 Finished developers/bin                                        1m15s 916MB
Oct 25 01:41:37 Starting semantics/ffi
Oct 25 01:42:16 Finished semantics/ffi                                           38s 367MB
Oct 25 01:42:16 Starting semantics
Oct 25 01:43:44 Finished semantics                                             1m26s 804MB
Oct 25 01:43:45 Starting semantics/proofs
Oct 25 01:46:29 Finished semantics/proofs                                      2m43s   1GB
Oct 25 01:46:29 Starting basis/pure
Oct 25 01:50:01 Finished basis/pure                                            3m30s 834MB
Oct 25 01:50:02 Starting translator
Oct 25 01:53:04 Finished translator                                            3m01s   1GB
Oct 25 01:53:04 Starting compiler/parsing
Oct 25 01:54:20 Finished compiler/parsing                                      1m15s   2GB
Oct 25 01:54:21 Starting characteristic
Oct 25 01:56:52 Finished characteristic                                        2m29s   1GB
Oct 25 01:56:52 Starting translator/monadic
Oct 25 01:58:18 Finished translator/monadic                                    1m24s   1GB
Oct 25 01:58:18 Starting basis
Oct 25 02:16:54 Finished basis                                                18m35s   5GB
Oct 25 02:16:55 Starting compiler/inference
Oct 25 02:18:36 Finished compiler/inference                                    1m40s   1GB
Oct 25 02:18:37 Starting compiler/backend/reg_alloc
Oct 25 02:19:25 Finished compiler/backend/reg_alloc                              47s   1GB
Oct 25 02:19:26 Starting compiler/backend/gc
Oct 25 02:26:43 Finished compiler/backend/gc                                   7m16s   1GB
Oct 25 02:26:44 Starting compiler/backend
Oct 25 02:26:48 Finished compiler/backend                                         3s  18MB
Oct 25 02:26:49 Starting compiler/encoders/asm
Oct 25 02:26:51 Finished compiler/encoders/asm                                    1s  14MB
Oct 25 02:26:51 Starting compiler/encoders/x64
Oct 25 02:27:44 Finished compiler/encoders/x64                                   51s 604MB
Oct 25 02:27:44 Starting compiler/encoders/arm6
Oct 25 02:29:28 Finished compiler/encoders/arm6                                1m43s   1GB
Oct 25 02:29:29 Starting compiler/encoders/arm8
Oct 25 02:29:56 Finished compiler/encoders/arm8                                  26s 466MB
Oct 25 02:29:57 Starting compiler/encoders/mips
Oct 25 02:30:56 Finished compiler/encoders/mips                                  58s   1GB
Oct 25 02:30:56 Starting compiler/encoders/riscv
Oct 25 02:31:58 Finished compiler/encoders/riscv                               1m00s 677MB
Oct 25 02:31:58 Starting compiler/backend/x64
Oct 25 02:32:17 Finished compiler/backend/x64                                    17s 769MB
Oct 25 02:32:17 Starting compiler/backend/arm6
Oct 25 02:32:37 Finished compiler/backend/arm6                                   19s   1GB
Oct 25 02:32:38 Starting compiler/backend/arm8
Oct 25 02:32:58 Finished compiler/backend/arm8                                   18s 952MB
Oct 25 02:32:58 Starting compiler/backend/mips
Oct 25 02:33:18 Finished compiler/backend/mips                                   19s   1GB
Oct 25 02:33:19 Starting compiler/backend/riscv
Oct 25 02:33:39 Finished compiler/backend/riscv                                  19s   1GB
Oct 25 02:33:40 Starting compiler/parsing/proofs
Oct 25 02:39:42 Finished compiler/parsing/proofs                               6m02s 826MB
Oct 25 02:39:43 Starting compiler/inference/proofs
Oct 25 02:42:35 Finished compiler/inference/proofs                             2m51s   1GB
Oct 25 02:42:36 Starting compiler/backend/semantics
Oct 25 02:51:28 Finished compiler/backend/semantics                            8m51s   2GB
Oct 25 02:51:29 Starting compiler/backend/reg_alloc/proofs
Oct 25 02:58:33 Finished compiler/backend/reg_alloc/proofs                     7m03s 587MB
Oct 25 02:58:33 Starting compiler/backend/proofs
Oct 25 03:39:23 Finished compiler/backend/proofs                              40m48s   4GB
Oct 25 03:39:24 Starting compiler/encoders/x64/proofs
Oct 25 03:46:46 Finished compiler/encoders/x64/proofs                          7m21s   3GB
Oct 25 03:46:47 Starting compiler/encoders/arm6/proofs
Oct 25 03:54:20 Finished compiler/encoders/arm6/proofs                         7m32s   3GB
Oct 25 03:54:20 Starting compiler/encoders/arm8/proofs
Oct 25 03:59:41 Finished compiler/encoders/arm8/proofs                         5m19s   1GB
Oct 25 03:59:42 Starting compiler/encoders/mips/proofs
Oct 25 04:06:59 Finished compiler/encoders/mips/proofs                         7m17s   2GB
Oct 25 04:07:00 Starting compiler/encoders/riscv/proofs
Oct 25 04:14:52 Finished compiler/encoders/riscv/proofs                        7m51s 750MB
Oct 25 04:14:53 Starting compiler/backend/x64/proofs
Oct 25 04:15:14 Finished compiler/backend/x64/proofs                             21s   1GB
Oct 25 04:15:15 Starting compiler/backend/arm6/proofs
Oct 25 04:15:40 Finished compiler/backend/arm6/proofs                            23s   1GB
Oct 25 04:15:40 Starting compiler/backend/arm8/proofs
Oct 25 04:16:01 Finished compiler/backend/arm8/proofs                            20s   1GB
Oct 25 04:16:02 Starting compiler/backend/mips/proofs
Oct 25 04:16:25 Finished compiler/backend/mips/proofs                            21s   1GB
Oct 25 04:16:25 Starting compiler/backend/riscv/proofs
Oct 25 04:16:47 Finished compiler/backend/riscv/proofs                           21s   1GB
Oct 25 04:16:48 Starting compiler/proofs
Oct 25 04:18:13 Finished compiler/proofs                                       1m25s   2GB
Oct 25 04:18:14 Starting candle/set-theory
Oct 25 04:18:46 Finished candle/set-theory                                       31s 591MB
Oct 25 04:18:47 Starting candle/syntax-lib
Oct 25 04:18:57 Finished candle/syntax-lib                                       10s 427MB
Oct 25 04:18:58 Starting candle/standard/syntax
Oct 25 04:20:31 Finished candle/standard/syntax                                1m32s 566MB
Oct 25 04:20:32 Starting candle/standard/semantics
Oct 25 04:21:56 Finished candle/standard/semantics                             1m23s 849MB
Oct 25 04:21:56 Starting candle/standard/monadic
Oct 25 04:23:32 Finished candle/standard/monadic                               1m34s 928MB
Oct 25 04:23:32 Starting candle/standard/ml_kernel
Oct 25 04:43:38 Finished candle/standard/ml_kernel                            20m04s   6GB
Oct 25 04:43:38 Starting candle/standard/opentheory
Oct 25 04:52:48 Finished candle/standard/opentheory                            9m09s   6GB
Oct 25 04:52:49 Starting candle/standard/opentheory/compilation
Oct 25 05:28:57 Finished candle/standard/opentheory/compilation               36m07s  18GB
Oct 25 05:28:58 Starting candle/standard/opentheory/compilation/proofs
Oct 25 05:29:34 Finished candle/standard/opentheory/compilation/proofs           34s   4GB
Oct 25 05:29:34 Starting characteristic/examples
Oct 25 05:31:21 Finished characteristic/examples                               1m46s   2GB
Oct 25 05:31:22 Starting tutorial/solutions
Oct 25 05:45:55 Finished tutorial/solutions                                   14m32s   6GB
Oct 25 05:45:55 Starting translator/monadic/examples
Oct 25 05:47:46 Finished translator/monadic/examples                           1m50s   3GB
Oct 25 05:47:47 Starting examples
Oct 25 05:53:56 Finished examples                                              6m07s   4GB
Oct 25 05:53:56 Starting examples/compilation
Oct 25 07:59:13 Finished examples/compilation                               2h05m15s  10GB
Oct 25 07:59:14 Starting examples/compilation/proofs
Oct 25 08:01:19 Finished examples/compilation/proofs                           2m04s   3GB
Oct 25 08:01:20 Starting compiler/benchmarks
Oct 25 08:01:21 Finished compiler/benchmarks                                      0s   5MB
Oct 25 08:01:21 Starting translator/okasaki-examples
Oct 25 08:04:51 Finished translator/okasaki-examples                           3m29s   1GB
Oct 25 08:04:52 Starting translator/other-examples
Oct 25 08:08:22 Finished translator/other-examples                             3m29s 864MB
Oct 25 08:08:22 Starting compiler/parsing/tests
Oct 25 08:08:48 Finished compiler/parsing/tests                                  25s 313MB
Oct 25 08:08:49 Starting compiler/inference/tests
Oct 31 05:22:41 FAILED: compiler/inference/tests
]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/balanced_bst]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/formal-languages]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/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: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semantics[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/alt_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: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/unification/triangular]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-ad8ad6f4b07521a5c63799c5f1a3d582824cb21f/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>>
 /home/cake/regression/cakeml-546/compiler/inference/unifyLib.sml:35: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cake/regression/cakeml-546/compiler/inference/unifyLib.sml:53: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cake/regression/cakeml-546/compiler/inference/unifyLib.sml:59: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cake/regression/cakeml-546/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 /home/cake/regression/cakeml-546/compiler/inference/tests/basisTypeCheckScript.sml : Interrupt
 error in load basisTypeCheckScript : Interrupt
 Uncaught exception: Interrupt