Job 1132

CakeML:ead003649d6dc901f4d31ecb7b95e38cd1e203ad
  Fix up ml_monad_translator for new packLib implementation [Jan 06 05:58:40]
#714 (nopacklib)
Merging into:07bca965721baed53cea03de48b0e523ff1af007
  Merge pull request #711 from CakeML/refs-unchanged [Dec 22 21:35:58]
HOL:76d78d3b69ca8b114cb7d8ebf345c8ac28d0f83f
  Provide plausible default (not []) for POLY_LDFLAGS on all platforms [Jan 03 23:23:48]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Jan 06 10:08:02 Claimed job
Jan 06 10:08:08 Building HOL
Jan 06 10:18:38 Starting developers
Jan 06 10:18:42 Finished developers                                               3s 122MB
Jan 06 10:18:42 Starting developers/bin
Jan 06 10:18:48 Finished developers/bin                                           6s 964MB
Jan 06 10:18:48 Starting semantics/ffi
Jan 06 10:18:58 Finished semantics/ffi                                            9s 249MB
Jan 06 10:18:58 Starting semantics
Jan 06 10:20:23 Finished semantics                                             1m24s   1GB
Jan 06 10:20:23 Starting semantics/proofs
Jan 06 10:23:24 Finished semantics/proofs                                      3m01s   1GB
Jan 06 10:23:24 Starting semantics/alt_semantics
Jan 06 10:23:32 Finished semantics/alt_semantics                                  7s 327MB
Jan 06 10:23:32 Starting semantics/alt_semantics/proofs
Jan 06 10:25:28 Finished semantics/alt_semantics/proofs                        1m56s 748MB
Jan 06 10:25:28 Starting basis/pure
Jan 06 10:28:07 Finished basis/pure                                            2m38s 717MB
Jan 06 10:28:07 Starting translator
Jan 06 10:30:31 Finished translator                                            2m23s   1GB
Jan 06 10:30:31 Starting compiler/parsing
Jan 06 10:31:34 Finished compiler/parsing                                      1m02s   2GB
Jan 06 10:31:34 Starting characteristic
Jan 06 10:37:01 Finished characteristic                                        5m27s   2GB
Jan 06 10:37:01 Starting translator/monadic
Jan 06 10:38:35 Finished translator/monadic                                    1m33s   1GB
Jan 06 10:38:35 Starting basis
Jan 06 11:10:27 Finished basis                                                31m51s  19GB
Jan 06 11:10:27 Starting compiler/inference
Jan 06 11:12:12 Finished compiler/inference                                    1m45s   1GB
Jan 06 11:12:12 Starting compiler/backend/reg_alloc
Jan 06 11:13:11 Finished compiler/backend/reg_alloc                              58s   1GB
Jan 06 11:13:11 Starting compiler/backend/gc
Jan 06 11:16:18 Finished compiler/backend/gc                                   3m06s   2GB
Jan 06 11:16:18 Starting compiler/backend
Jan 06 11:19:52 Finished compiler/backend                                      3m34s   2GB
Jan 06 11:19:53 Starting compiler/encoders/asm
Jan 06 11:20:13 Finished compiler/encoders/asm                                   20s 857MB
Jan 06 11:20:13 Starting compiler/encoders/x64
Jan 06 11:21:06 Finished compiler/encoders/x64                                   53s 948MB
Jan 06 11:21:06 Starting compiler/encoders/arm7
Jan 06 11:22:43 Finished compiler/encoders/arm7                                1m36s   1GB
Jan 06 11:22:43 Starting compiler/encoders/arm8
Jan 06 11:23:14 Finished compiler/encoders/arm8                                  30s 651MB
Jan 06 11:23:14 Starting compiler/encoders/mips
Jan 06 11:24:21 Finished compiler/encoders/mips                                1m06s   1GB
Jan 06 11:24:21 Starting compiler/encoders/riscv
Jan 06 11:25:40 Finished compiler/encoders/riscv                               1m18s   1GB
Jan 06 11:25:40 Starting compiler/encoders/ag32
Jan 06 11:25:56 Finished compiler/encoders/ag32                                  16s 774MB
Jan 06 11:25:56 Starting compiler/backend/x64
Jan 06 11:26:13 Finished compiler/backend/x64                                    16s   1GB
Jan 06 11:26:13 Starting compiler/backend/arm7
Jan 06 11:26:31 Finished compiler/backend/arm7                                   18s   1GB
Jan 06 11:26:32 Starting compiler/backend/arm8
Jan 06 11:26:48 Finished compiler/backend/arm8                                   16s   1GB
Jan 06 11:26:48 Starting compiler/backend/mips
Jan 06 11:27:06 Finished compiler/backend/mips                                   17s   1GB
Jan 06 11:27:06 Starting compiler/backend/riscv
Jan 06 11:27:23 Finished compiler/backend/riscv                                  17s   1GB
Jan 06 11:27:23 Starting compiler/backend/ag32
Jan 06 11:28:28 Finished compiler/backend/ag32                                 1m04s   1GB
Jan 06 11:28:28 Starting compiler/parsing/proofs
Jan 06 11:34:14 Finished compiler/parsing/proofs                               5m45s   1GB
Jan 06 11:34:14 Starting compiler/inference/proofs
Jan 06 11:36:57 Finished compiler/inference/proofs                             2m43s   1GB
Jan 06 11:36:57 Starting compiler/backend/semantics
Jan 06 12:02:48 Finished compiler/backend/semantics                           25m50s   2GB
Jan 06 12:02:48 Starting compiler/backend/reg_alloc/proofs
Jan 06 12:06:05 Finished compiler/backend/reg_alloc/proofs                     3m16s 810MB
Jan 06 12:06:05 Starting compiler/backend/proofs
Jan 06 13:02:39 Finished compiler/backend/proofs                              56m33s  15GB
Jan 06 13:02:39 Starting compiler/encoders/x64/proofs
Jan 06 13:11:37 Finished compiler/encoders/x64/proofs                          8m58s   4GB
Jan 06 13:11:37 Starting compiler/encoders/arm7/proofs
Jan 06 13:23:32 Finished compiler/encoders/arm7/proofs                        11m53s   3GB
Jan 06 13:23:32 Starting compiler/encoders/arm8/proofs
Jan 06 13:29:38 Finished compiler/encoders/arm8/proofs                         6m05s   1GB
Jan 06 13:29:38 Starting compiler/encoders/mips/proofs
Jan 06 13:38:48 Finished compiler/encoders/mips/proofs                         9m10s   2GB
Jan 06 13:38:48 Starting compiler/encoders/riscv/proofs
Jan 06 13:47:00 Finished compiler/encoders/riscv/proofs                        8m11s   1GB
Jan 06 13:47:00 Starting compiler/encoders/ag32/proofs
Jan 06 13:49:20 Finished compiler/encoders/ag32/proofs                         2m19s 874MB
Jan 06 13:49:20 Starting compiler/backend/x64/proofs
Jan 06 13:49:37 Finished compiler/backend/x64/proofs                             17s 838MB
Jan 06 13:49:37 Starting compiler/backend/arm7/proofs
Jan 06 13:49:56 Finished compiler/backend/arm7/proofs                            19s   1GB
Jan 06 13:49:56 Starting compiler/backend/arm8/proofs
Jan 06 13:50:14 Finished compiler/backend/arm8/proofs                            17s   1GB
Jan 06 13:50:14 Starting compiler/backend/mips/proofs
Jan 06 13:50:32 Finished compiler/backend/mips/proofs                            17s   1GB
Jan 06 13:50:32 Starting compiler/backend/riscv/proofs
Jan 06 13:50:50 Finished compiler/backend/riscv/proofs                           18s   1GB
Jan 06 13:50:50 Starting compiler/backend/ag32/proofs
Jan 06 13:59:42 Finished compiler/backend/ag32/proofs                          8m51s   2GB
Jan 06 13:59:42 Starting compiler/proofs
Jan 06 14:01:10 Finished compiler/proofs                                       1m27s   3GB
Jan 06 14:01:10 Starting candle/set-theory
Jan 06 14:01:36 Finished candle/set-theory                                       26s 919MB
Jan 06 14:01:36 Starting candle/syntax-lib
Jan 06 14:01:47 Finished candle/syntax-lib                                       10s 660MB
Jan 06 14:01:47 Starting candle/standard/syntax
Jan 06 14:03:29 Finished candle/standard/syntax                                1m41s   1GB
Jan 06 14:03:29 Starting candle/standard/semantics
Jan 06 14:05:05 Finished candle/standard/semantics                             1m36s   1GB
Jan 06 14:05:05 Starting candle/standard/monadic
Jan 06 14:06:38 Finished candle/standard/monadic                               1m32s   1GB
Jan 06 14:06:38 Starting candle/standard/ml_kernel
Jan 06 14:12:52 Finished candle/standard/ml_kernel                             6m13s   4GB
Jan 06 14:12:52 Starting candle/standard/opentheory
Jan 06 14:27:41 Finished candle/standard/opentheory                           14m49s   4GB
Jan 06 14:27:41 Starting candle/standard/opentheory/compilation
Jan 06 14:56:45 Finished candle/standard/opentheory/compilation               29m03s  17GB
Jan 06 14:56:45 Starting candle/standard/opentheory/compilation/proofs
Jan 06 14:57:19 Finished candle/standard/opentheory/compilation/proofs           33s   2GB
Jan 06 14:57:19 Starting characteristic/examples
Jan 06 14:57:51 FAILED: characteristic/examples
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
Starting work on README.md
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
README.md                                       real:    0s  user:    0s     OK
cf_examplesTheory                               real:   30s  user:   28sFAIL<1>
 Adding nsLookup representation thms for [cf_examples_env_2]
 Adding nsLookup representation thms for [init_env]
 error in quse /home/cur/sao/cakeml/regression/cakeml-1132/characteristic/examples/cf_examplesScript.sml : HOL_ERR {message = "Unbound function (THEN1 on line 67) (THEN1 on line 69)", origin_function = "xapp", origin_structure = "cfTacticsLib"}
 error in load /home/cur/sao/cakeml/regression/cakeml-1132/characteristic/examples/cf_examplesScript : HOL_ERR {message = "Unbound function (THEN1 on line 67) (THEN1 on line 69)", origin_function = "xapp", origin_structure = "cfTacticsLib"}
 Proof of 
 
 n nv. INT n nv  app p example_let_v [nv] emp (POSTv v. &INT (2 * n) v)
 
 failed.
 Uncaught exception: HOL_ERR {message = "Unbound function (THEN1 on line 67) (THEN1 on line 69)", origin_function = "xapp", origin_structure = "cfTacticsLib"}
cf_tutorialTheory                                                       M-KILLED