Job 1198

CakeML:fcce77b65b0ef3e3a17536720597ebf2fc3b88bc
  Refactor assert into RuntimeProg [Mar 03 10:19:02]
#731 (source_assert)
Merging into:e601a7b5e675a8f4f760735cee79c04e1692598d
  Merge pull request #724 from talsewell/constrain_op_case [Feb 23 19:40:17]
HOL:72f6abae3df1a87d5c1b26e309f5d2a379929e63
  Fix off-by-one error in RISC-V DecodeRVC [Mar 01 19:20:54]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Mar 03 10:42:26 Claimed job
Mar 03 10:42:32 Building HOL
Mar 03 10:54:13 Starting developers
Mar 03 10:54:17 Finished developers                                               4s 106MB
Mar 03 10:54:17 Starting developers/bin
Mar 03 10:54:24 Finished developers/bin                                           6s   1GB
Mar 03 10:54:25 Starting semantics/ffi
Mar 03 10:54:35 Finished semantics/ffi                                            9s 246MB
Mar 03 10:54:35 Starting semantics
Mar 03 10:56:00 Finished semantics                                             1m25s   1GB
Mar 03 10:56:01 Starting semantics/proofs
Mar 03 10:59:13 Finished semantics/proofs                                      3m12s   1GB
Mar 03 10:59:13 Starting semantics/alt_semantics
Mar 03 10:59:21 Finished semantics/alt_semantics                                  7s 333MB
Mar 03 10:59:21 Starting semantics/alt_semantics/proofs
Mar 03 11:01:19 Finished semantics/alt_semantics/proofs                        1m58s   1GB
Mar 03 11:01:19 Starting basis/pure
Mar 03 11:04:05 Finished basis/pure                                            2m46s 898MB
Mar 03 11:04:05 Starting translator
Mar 03 11:06:33 Finished translator                                            2m27s   1GB
Mar 03 11:06:33 Starting compiler/parsing
Mar 03 11:07:34 Finished compiler/parsing                                      1m01s   3GB
Mar 03 11:07:34 Starting characteristic
Mar 03 11:13:16 Finished characteristic                                        5m41s   2GB
Mar 03 11:13:16 Starting translator/monadic
Mar 03 11:14:50 Finished translator/monadic                                    1m34s   1GB
Mar 03 11:14:50 Starting basis
Mar 03 11:45:03 Finished basis                                                30m12s  14GB
Mar 03 11:45:03 Starting compiler/inference
Mar 03 11:46:09 Finished compiler/inference                                    1m06s   1GB
Mar 03 11:46:09 Starting compiler/backend/reg_alloc
Mar 03 11:47:09 Finished compiler/backend/reg_alloc                              59s   1GB
Mar 03 11:47:09 Starting compiler/backend/gc
Mar 03 11:50:17 Finished compiler/backend/gc                                   3m07s   2GB
Mar 03 11:50:17 Starting compiler/backend
Mar 03 11:54:25 Finished compiler/backend                                      4m08s   4GB
Mar 03 11:54:26 Starting compiler/encoders/asm
Mar 03 11:54:47 Finished compiler/encoders/asm                                   21s 851MB
Mar 03 11:54:47 Starting compiler/encoders/x64
Mar 03 11:55:42 Finished compiler/encoders/x64                                   54s 964MB
Mar 03 11:55:42 Starting compiler/encoders/arm7
Mar 03 11:57:20 Finished compiler/encoders/arm7                                1m37s   1GB
Mar 03 11:57:20 Starting compiler/encoders/arm8
Mar 03 11:57:51 Finished compiler/encoders/arm8                                  31s 616MB
Mar 03 11:57:52 Starting compiler/encoders/mips
Mar 03 11:58:56 Finished compiler/encoders/mips                                1m04s   1GB
Mar 03 11:58:56 Starting compiler/encoders/riscv
Mar 03 12:00:16 Finished compiler/encoders/riscv                               1m20s   1GB
Mar 03 12:00:16 Starting compiler/encoders/ag32
Mar 03 12:00:33 Finished compiler/encoders/ag32                                  16s 786MB
Mar 03 12:00:33 Starting compiler/backend/x64
Mar 03 12:00:51 Finished compiler/backend/x64                                    18s   1GB
Mar 03 12:00:51 Starting compiler/backend/arm7
Mar 03 12:01:10 Finished compiler/backend/arm7                                   19s   1GB
Mar 03 12:01:11 Starting compiler/backend/arm8
Mar 03 12:01:27 Finished compiler/backend/arm8                                   16s   1GB
Mar 03 12:01:27 Starting compiler/backend/mips
Mar 03 12:01:45 Finished compiler/backend/mips                                   18s   1GB
Mar 03 12:01:46 Starting compiler/backend/riscv
Mar 03 12:02:04 Finished compiler/backend/riscv                                  18s   1GB
Mar 03 12:02:05 Starting compiler/backend/ag32
Mar 03 12:03:10 Finished compiler/backend/ag32                                 1m05s 945MB
Mar 03 12:03:10 Starting compiler/parsing/proofs
Mar 03 12:08:43 Finished compiler/parsing/proofs                               5m32s 993MB
Mar 03 12:08:43 Starting compiler/inference/proofs
Mar 03 12:11:00 Finished compiler/inference/proofs                             2m17s   1GB
Mar 03 12:11:00 Starting compiler/backend/semantics
Mar 03 12:37:09 Finished compiler/backend/semantics                           26m08s   2GB
Mar 03 12:37:09 Starting compiler/backend/reg_alloc/proofs
Mar 03 12:40:25 Finished compiler/backend/reg_alloc/proofs                     3m15s   1GB
Mar 03 12:40:25 Starting compiler/backend/proofs
Mar 03 13:37:36 Finished compiler/backend/proofs                              57m10s  17GB
Mar 03 13:37:36 Starting compiler/encoders/x64/proofs
Mar 03 13:46:30 Finished compiler/encoders/x64/proofs                          8m54s   4GB
Mar 03 13:46:30 Starting compiler/encoders/arm7/proofs
Mar 03 13:58:43 Finished compiler/encoders/arm7/proofs                        12m13s   3GB
Mar 03 13:58:44 Starting compiler/encoders/arm8/proofs
Mar 03 14:04:43 Finished compiler/encoders/arm8/proofs                         5m58s   1GB
Mar 03 14:04:43 Starting compiler/encoders/mips/proofs
Mar 03 14:13:56 Finished compiler/encoders/mips/proofs                         9m13s   2GB
Mar 03 14:13:56 Starting compiler/encoders/riscv/proofs
Mar 03 14:21:52 Finished compiler/encoders/riscv/proofs                        7m56s   1GB
Mar 03 14:21:52 Starting compiler/encoders/ag32/proofs
Mar 03 14:24:17 Finished compiler/encoders/ag32/proofs                         2m24s 682MB
Mar 03 14:24:17 Starting compiler/backend/x64/proofs
Mar 03 14:24:36 Finished compiler/backend/x64/proofs                             19s   1GB
Mar 03 14:24:36 Starting compiler/backend/arm7/proofs
Mar 03 14:24:57 Finished compiler/backend/arm7/proofs                            20s   1GB
Mar 03 14:24:57 Starting compiler/backend/arm8/proofs
Mar 03 14:25:16 Finished compiler/backend/arm8/proofs                            19s   1GB
Mar 03 14:25:16 Starting compiler/backend/mips/proofs
Mar 03 14:25:36 Finished compiler/backend/mips/proofs                            20s   1GB
Mar 03 14:25:36 Starting compiler/backend/riscv/proofs
Mar 03 14:25:56 Finished compiler/backend/riscv/proofs                           19s   1GB
Mar 03 14:25:56 Starting compiler/backend/ag32/proofs
Mar 03 14:38:07 Finished compiler/backend/ag32/proofs                         12m10s   1GB
Mar 03 14:38:07 Starting compiler/proofs
Mar 03 14:39:49 Finished compiler/proofs                                       1m41s   4GB
Mar 03 14:39:49 Starting candle/set-theory
Mar 03 14:40:17 Finished candle/set-theory                                       27s 816MB
Mar 03 14:40:17 Starting candle/syntax-lib
Mar 03 14:40:27 Finished candle/syntax-lib                                       10s 650MB
Mar 03 14:40:27 Starting candle/standard/syntax
Mar 03 14:42:11 Finished candle/standard/syntax                                1m43s   1GB
Mar 03 14:42:11 Starting candle/standard/semantics
Mar 03 14:43:50 Finished candle/standard/semantics                             1m38s   1GB
Mar 03 14:43:50 Starting candle/standard/monadic
Mar 03 14:45:22 Finished candle/standard/monadic                               1m31s   1GB
Mar 03 14:45:22 Starting candle/standard/ml_kernel
Mar 03 14:50:19 Finished candle/standard/ml_kernel                             4m56s   5GB
Mar 03 14:50:19 Starting candle/standard/opentheory
Mar 03 14:58:44 Finished candle/standard/opentheory                            8m25s   4GB
Mar 03 14:58:44 Starting candle/standard/opentheory/compilation
Mar 03 15:28:02 Finished candle/standard/opentheory/compilation               29m18s  15GB
Mar 03 15:28:03 Starting candle/standard/opentheory/compilation/proofs
Mar 03 15:28:40 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
Mar 03 15:28:40 Starting candle/overloading/syntax
Mar 03 15:31:35 Finished candle/overloading/syntax                             2m54s   1GB
Mar 03 15:31:35 Starting candle/overloading/semantics
Mar 03 15:38:11 Finished candle/overloading/semantics                          6m36s   3GB
Mar 03 15:38:11 Starting characteristic/examples
Mar 03 15:39:25 Finished characteristic/examples                               1m13s   3GB
Mar 03 15:39:25 Starting tutorial/solutions
Mar 03 15:53:35 Finished tutorial/solutions                                   14m09s   7GB
Mar 03 15:53:35 Starting translator/monadic/examples
Mar 03 15:56:24 Finished translator/monadic/examples                           2m49s   3GB
Mar 03 15:56:24 Starting examples
Mar 03 16:03:40 Finished examples                                              7m15s   3GB
Mar 03 16:03:40 Starting examples/compilation/x64
Mar 03 18:13:42 Finished examples/compilation/x64                           2h10m02s  14GB
Mar 03 18:13:42 Starting examples/compilation/x64/proofs
Mar 03 18:15:16 Finished examples/compilation/x64/proofs                       1m33s   3GB
Mar 03 18:15:16 Starting examples/compilation/ag32
Mar 03 18:45:17 Finished examples/compilation/ag32                            30m00s   5GB
Mar 03 18:45:17 Starting examples/compilation/ag32/proofs
Mar 03 18:45:57 Finished examples/compilation/ag32/proofs                        40s   3GB
Mar 03 18:45:57 Starting examples/cost
Mar 03 19:24:41 Finished examples/cost                                        38m42s   6GB
Mar 03 19:24:41 Starting examples/lpr_checker
Mar 03 19:28:09 Finished examples/lpr_checker                                  3m28s   2GB
Mar 03 19:28:09 Starting examples/lpr_checker/compilation
Mar 03 19:44:12 Finished examples/lpr_checker/compilation                     16m02s   7GB
Mar 03 19:44:12 Starting examples/lpr_checker/compilation/proofs
Mar 03 19:44:48 Finished examples/lpr_checker/compilation/proofs                 35s   2GB
Mar 03 19:44:48 Starting examples/lpr_checker/array
Mar 03 19:52:09 Finished examples/lpr_checker/array                            7m20s   2GB
Mar 03 19:52:09 Starting examples/lpr_checker/array/compilation
Mar 03 20:06:57 Finished examples/lpr_checker/array/compilation               14m48s   8GB
Mar 03 20:06:57 Starting examples/lpr_checker/array/compilation/proofs
Mar 03 20:07:40 Finished examples/lpr_checker/array/compilation/proofs           43s   2GB
Mar 03 20:07:41 Starting translator/okasaki-examples
Mar 03 20:11:40 Finished translator/okasaki-examples                           3m59s   1GB
Mar 03 20:11:40 Starting translator/other-examples
Mar 03 20:13:31 Finished translator/other-examples                             1m51s   1GB
Mar 03 20:13:31 Starting compiler/parsing/tests
Mar 03 20:13:56 Finished compiler/parsing/tests                                  24s 580MB
Mar 03 20:13:56 Starting compiler/inference/tests
Mar 03 20:14:11 FAILED: compiler/inference/tests
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Starting work on README.md
Starting work on basisTypeCheckTheory
README.md                                       real:    0s  user:    0s     OK
basisTypeCheckTheory                            real:   14s  user:   12sFAIL<1>
 /home/cur/sao/cakeml/regression/cakeml-1198/compiler/inference/unifyLib.sml:38: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cur/sao/cakeml/regression/cakeml-1198/compiler/inference/unifyLib.sml:56: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cur/sao/cakeml/regression/cakeml-1198/compiler/inference/unifyLib.sml:62: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cur/sao/cakeml/regression/cakeml-1198/compiler/inference/unifyLib.sml:68: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 <<HOL message: Created theory "basisTypeCheck">>
 error in quse /home/cur/sao/cakeml/regression/cakeml-1198/compiler/inference/tests/basisTypeCheckScript.sml : HOL_ERR {message = "Type inference failed for basis. (Also failed to fully evaluate type inferencer error message)", origin_function = "failwith", origin_structure = "??"}
 error in load /home/cur/sao/cakeml/regression/cakeml-1198/compiler/inference/tests/basisTypeCheckScript : HOL_ERR {message = "Type inference failed for basis. (Also failed to fully evaluate type inferencer error message)", origin_function = "failwith", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "Type inference failed for basis. (Also failed to fully evaluate type inferencer error message)", origin_function = "failwith", origin_structure = "??"}