Job 1200

CakeML:fcce77b65b0ef3e3a17536720597ebf2fc3b88bc
  Refactor assert into RuntimeProg [Mar 03 10:19:02]
#731 (source_assert)
Merging into:cc300b057d3c4870d8abe70a8129375fa3ac9e55
  Merge pull request #732 from CakeML/fix_lem_top [Mar 03 14:11:14]
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 04 07:14:21 Claimed job
Mar 04 07:14:25 Reusing HOL
Mar 04 07:15:16 Starting developers
Mar 04 07:15:20 Finished developers                                               4s 104MB
Mar 04 07:15:20 Starting developers/bin
Mar 04 07:15:27 Finished developers/bin                                           6s   1GB
Mar 04 07:15:27 Starting semantics/ffi
Mar 04 07:15:37 Finished semantics/ffi                                            9s 246MB
Mar 04 07:15:37 Starting semantics
Mar 04 07:16:53 Finished semantics                                             1m15s   1GB
Mar 04 07:16:53 Starting semantics/proofs
Mar 04 07:20:00 Finished semantics/proofs                                      3m06s   1GB
Mar 04 07:20:00 Starting semantics/alt_semantics
Mar 04 07:20:08 Finished semantics/alt_semantics                                  7s 303MB
Mar 04 07:20:08 Starting semantics/alt_semantics/proofs
Mar 04 07:22:07 Finished semantics/alt_semantics/proofs                        1m58s   1GB
Mar 04 07:22:07 Starting basis/pure
Mar 04 07:22:55 Finished basis/pure                                              47s 716MB
Mar 04 07:22:55 Starting translator
Mar 04 07:25:22 Finished translator                                            2m27s   1GB
Mar 04 07:25:23 Starting compiler/parsing
Mar 04 07:26:26 Finished compiler/parsing                                      1m03s   2GB
Mar 04 07:26:26 Starting characteristic
Mar 04 07:32:10 Finished characteristic                                        5m43s   1GB
Mar 04 07:32:10 Starting translator/monadic
Mar 04 07:33:40 Finished translator/monadic                                    1m30s   1GB
Mar 04 07:33:40 Starting basis
Mar 04 08:03:28 Finished basis                                                29m47s  17GB
Mar 04 08:03:28 Starting compiler/inference
Mar 04 08:04:25 Finished compiler/inference                                      56s   1GB
Mar 04 08:04:25 Starting compiler/backend/reg_alloc
Mar 04 08:05:26 Finished compiler/backend/reg_alloc                            1m01s   1GB
Mar 04 08:05:26 Starting compiler/backend/gc
Mar 04 08:08:26 Finished compiler/backend/gc                                   2m59s   2GB
Mar 04 08:08:26 Starting compiler/backend
Mar 04 08:12:38 Finished compiler/backend                                      4m11s   2GB
Mar 04 08:12:38 Starting compiler/encoders/asm
Mar 04 08:12:59 Finished compiler/encoders/asm                                   21s 847MB
Mar 04 08:12:59 Starting compiler/encoders/x64
Mar 04 08:13:23 Finished compiler/encoders/x64                                   23s 983MB
Mar 04 08:13:23 Starting compiler/encoders/arm7
Mar 04 08:14:08 Finished compiler/encoders/arm7                                  45s 749MB
Mar 04 08:14:08 Starting compiler/encoders/arm8
Mar 04 08:14:20 Finished compiler/encoders/arm8                                  12s 932MB
Mar 04 08:14:20 Starting compiler/encoders/mips
Mar 04 08:14:39 Finished compiler/encoders/mips                                  16s   1GB
Mar 04 08:14:39 Starting compiler/encoders/riscv
Mar 04 08:14:54 Finished compiler/encoders/riscv                                 15s 740MB
Mar 04 08:14:54 Starting compiler/encoders/ag32
Mar 04 08:15:11 Finished compiler/encoders/ag32                                  16s 766MB
Mar 04 08:15:11 Starting compiler/backend/x64
Mar 04 08:15:27 Finished compiler/backend/x64                                    16s 926MB
Mar 04 08:15:27 Starting compiler/backend/arm7
Mar 04 08:15:47 Finished compiler/backend/arm7                                   19s   1GB
Mar 04 08:15:47 Starting compiler/backend/arm8
Mar 04 08:16:04 Finished compiler/backend/arm8                                   16s   1GB
Mar 04 08:16:04 Starting compiler/backend/mips
Mar 04 08:16:23 Finished compiler/backend/mips                                   18s   1GB
Mar 04 08:16:23 Starting compiler/backend/riscv
Mar 04 08:16:42 Finished compiler/backend/riscv                                  18s   1GB
Mar 04 08:16:42 Starting compiler/backend/ag32
Mar 04 08:17:48 Finished compiler/backend/ag32                                 1m05s 953MB
Mar 04 08:17:48 Starting compiler/parsing/proofs
Mar 04 08:23:35 Finished compiler/parsing/proofs                               5m46s   1GB
Mar 04 08:23:35 Starting compiler/inference/proofs
Mar 04 08:25:54 Finished compiler/inference/proofs                             2m18s   1GB
Mar 04 08:25:54 Starting compiler/backend/semantics
Mar 04 08:52:05 Finished compiler/backend/semantics                           26m11s   1GB
Mar 04 08:52:05 Starting compiler/backend/reg_alloc/proofs
Mar 04 08:55:18 Finished compiler/backend/reg_alloc/proofs                     3m13s 862MB
Mar 04 08:55:18 Starting compiler/backend/proofs
Mar 04 09:52:39 Finished compiler/backend/proofs                              57m20s  17GB
Mar 04 09:52:39 Starting compiler/encoders/x64/proofs
Mar 04 10:01:27 Finished compiler/encoders/x64/proofs                          8m48s   4GB
Mar 04 10:01:27 Starting compiler/encoders/arm7/proofs
Mar 04 10:13:24 Finished compiler/encoders/arm7/proofs                        11m56s   3GB
Mar 04 10:13:24 Starting compiler/encoders/arm8/proofs
Mar 04 10:19:21 Finished compiler/encoders/arm8/proofs                         5m56s   1GB
Mar 04 10:19:21 Starting compiler/encoders/mips/proofs
Mar 04 10:28:20 Finished compiler/encoders/mips/proofs                         8m58s   3GB
Mar 04 10:28:20 Starting compiler/encoders/riscv/proofs
Mar 04 10:36:29 Finished compiler/encoders/riscv/proofs                        8m08s   1GB
Mar 04 10:36:29 Starting compiler/encoders/ag32/proofs
Mar 04 10:38:47 Finished compiler/encoders/ag32/proofs                         2m18s 734MB
Mar 04 10:38:47 Starting compiler/backend/x64/proofs
Mar 04 10:39:06 Finished compiler/backend/x64/proofs                             19s   1GB
Mar 04 10:39:06 Starting compiler/backend/arm7/proofs
Mar 04 10:39:28 Finished compiler/backend/arm7/proofs                            21s   1GB
Mar 04 10:39:28 Starting compiler/backend/arm8/proofs
Mar 04 10:39:48 Finished compiler/backend/arm8/proofs                            19s   1GB
Mar 04 10:39:48 Starting compiler/backend/mips/proofs
Mar 04 10:40:08 Finished compiler/backend/mips/proofs                            20s   1GB
Mar 04 10:40:08 Starting compiler/backend/riscv/proofs
Mar 04 10:40:29 Finished compiler/backend/riscv/proofs                           20s   1GB
Mar 04 10:40:29 Starting compiler/backend/ag32/proofs
Mar 04 10:52:22 Finished compiler/backend/ag32/proofs                         11m53s   2GB
Mar 04 10:52:23 Starting compiler/proofs
Mar 04 10:53:51 Finished compiler/proofs                                       1m28s   4GB
Mar 04 10:53:51 Starting candle/set-theory
Mar 04 10:54:18 Finished candle/set-theory                                       27s 779MB
Mar 04 10:54:18 Starting candle/syntax-lib
Mar 04 10:54:28 Finished candle/syntax-lib                                       10s 629MB
Mar 04 10:54:29 Starting candle/standard/syntax
Mar 04 10:56:11 Finished candle/standard/syntax                                1m42s   1GB
Mar 04 10:56:12 Starting candle/standard/semantics
Mar 04 10:57:51 Finished candle/standard/semantics                             1m39s 905MB
Mar 04 10:57:51 Starting candle/standard/monadic
Mar 04 10:59:23 Finished candle/standard/monadic                               1m32s   1GB
Mar 04 10:59:23 Starting candle/standard/ml_kernel
Mar 04 11:04:18 Finished candle/standard/ml_kernel                             4m54s   2GB
Mar 04 11:04:18 Starting candle/standard/opentheory
Mar 04 11:12:51 Finished candle/standard/opentheory                            8m33s   4GB
Mar 04 11:12:51 Starting candle/standard/opentheory/compilation
Mar 04 11:42:02 Finished candle/standard/opentheory/compilation               29m10s  17GB
Mar 04 11:42:02 Starting candle/standard/opentheory/compilation/proofs
Mar 04 11:42:39 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
Mar 04 11:42:39 Starting candle/overloading/syntax
Mar 04 11:45:32 Finished candle/overloading/syntax                             2m52s   1GB
Mar 04 11:45:32 Starting candle/overloading/semantics
Mar 04 11:52:10 Finished candle/overloading/semantics                          6m37s   3GB
Mar 04 11:52:10 Starting characteristic/examples
Mar 04 11:53:22 Finished characteristic/examples                               1m10s   1GB
Mar 04 11:53:22 Starting tutorial/solutions
Mar 04 12:07:11 Finished tutorial/solutions                                   13m49s   8GB
Mar 04 12:07:11 Starting translator/monadic/examples
Mar 04 12:10:00 Finished translator/monadic/examples                           2m48s   2GB
Mar 04 12:10:00 Starting examples
Mar 04 12:17:23 Finished examples                                              7m22s   3GB
Mar 04 12:17:23 Starting examples/compilation/x64
Mar 04 14:26:36 Finished examples/compilation/x64                           2h09m13s  11GB
Mar 04 14:26:36 Starting examples/compilation/x64/proofs
Mar 04 14:28:08 Finished examples/compilation/x64/proofs                       1m31s   3GB
Mar 04 14:28:08 Starting examples/compilation/ag32
Mar 04 14:58:04 Finished examples/compilation/ag32                            29m56s   5GB
Mar 04 14:58:05 Starting examples/compilation/ag32/proofs
Mar 04 14:58:44 Finished examples/compilation/ag32/proofs                        39s   2GB
Mar 04 14:58:44 Starting examples/cost
Mar 04 15:37:37 Finished examples/cost                                        38m52s   7GB
Mar 04 15:37:37 Starting examples/lpr_checker
Mar 04 15:41:06 Finished examples/lpr_checker                                  3m28s   2GB
Mar 04 15:41:06 Starting examples/lpr_checker/compilation
Mar 04 15:56:59 Finished examples/lpr_checker/compilation                     15m52s   8GB
Mar 04 15:56:59 Starting examples/lpr_checker/compilation/proofs
Mar 04 15:57:37 Finished examples/lpr_checker/compilation/proofs                 37s   2GB
Mar 04 15:57:37 Starting examples/lpr_checker/array
Mar 04 16:04:56 Finished examples/lpr_checker/array                            7m19s   3GB
Mar 04 16:04:56 Starting examples/lpr_checker/array/compilation
Mar 04 16:19:48 Finished examples/lpr_checker/array/compilation               14m51s   8GB
Mar 04 16:19:48 Starting examples/lpr_checker/array/compilation/proofs
Mar 04 16:20:31 Finished examples/lpr_checker/array/compilation/proofs           42s   3GB
Mar 04 16:20:31 Starting translator/okasaki-examples
Mar 04 16:24:33 Finished translator/okasaki-examples                           4m01s   1GB
Mar 04 16:24:33 Starting translator/other-examples
Mar 04 16:25:11 Finished translator/other-examples                               37s   1GB
Mar 04 16:25:11 Starting compiler/parsing/tests
Mar 04 16:25:36 Finished compiler/parsing/tests                                  24s 566MB
Mar 04 16:25:36 Starting compiler/inference/tests
Mar 04 16:25:53 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:   16s  user:   15sFAIL<1>
 /home/cur/sao/cakeml/regression/cakeml-1200/compiler/inference/unifyLib.sml:38: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cur/sao/cakeml/regression/cakeml-1200/compiler/inference/unifyLib.sml:56: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cur/sao/cakeml/regression/cakeml-1200/compiler/inference/unifyLib.sml:62: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /home/cur/sao/cakeml/regression/cakeml-1200/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-1200/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-1200/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 = "??"}