Job 1939

CakeML:4a0c2518b33324bc0725249fe551d431e60fc858
  Fix DoubleProof [Jun 22 07:35:15]
#892 (double-type-new)
Merging into:3edf3dfb5230ae6668e0082093cc00b303838e59
  Merge pull request #884 from CakeML/let-lift [Jun 22 20:28:35]
HOL:3810cf53c6050c5b2748cb042415145bd842957f
  Make parsing in RealField properly independent of context [Jun 21 00:55:21]
Machine:oven3

Jun 22 20:41:40 Claimed job
Jun 22 20:41:54 Building HOL
Jun 22 21:05:16 Starting developers
Jun 22 21:05:26 Finished developers                                               9s 130MB
Jun 22 21:05:26 Starting developers/bin
Jun 22 21:05:39 Finished developers/bin                                          12s   1GB
Jun 22 21:05:39 Starting semantics/ffi
Jun 22 21:06:04 Finished semantics/ffi                                           25s 260MB
Jun 22 21:06:05 Starting semantics
Jun 22 21:11:27 Finished semantics                                             5m21s   1GB
Jun 22 21:11:27 Starting semantics/proofs
Jun 22 21:26:43 Finished semantics/proofs                                     15m15s   1GB
Jun 22 21:26:43 Starting semantics/alt_semantics
Jun 22 21:27:44 Finished semantics/alt_semantics                               1m00s 582MB
Jun 22 21:27:45 Starting semantics/alt_semantics/proofs
Jun 22 21:53:04 Finished semantics/alt_semantics/proofs                       25m19s   1GB
Jun 22 21:53:05 Starting basis/pure
Jun 22 22:00:38 Finished basis/pure                                            7m33s   1GB
Jun 22 22:00:38 Starting translator
Jun 22 22:08:29 Finished translator                                            7m50s   1GB
Jun 22 22:08:29 Starting compiler/parsing
Jun 22 22:11:32 Finished compiler/parsing                                      3m03s   5GB
Jun 22 22:11:33 Starting characteristic
Jun 22 22:26:16 Finished characteristic                                       14m43s   2GB
Jun 22 22:26:16 Starting translator/monadic
Jun 22 22:30:30 Finished translator/monadic                                    4m13s   1GB
Jun 22 22:30:31 Starting basis
Jun 23 00:26:54 Finished basis                                              1h56m23s  11GB
Jun 23 00:26:55 Starting compiler/inference
Jun 23 00:30:18 Finished compiler/inference                                    3m23s   1GB
Jun 23 00:30:19 Starting compiler/backend/reg_alloc
Jun 23 00:33:35 Finished compiler/backend/reg_alloc                            3m15s   1GB
Jun 23 00:33:35 Starting compiler/backend/gc
Jun 23 00:42:11 Finished compiler/backend/gc                                   8m36s   3GB
Jun 23 00:42:12 Starting compiler/backend
Jun 23 00:54:23 Finished compiler/backend                                     12m11s   3GB
Jun 23 00:54:24 Starting compiler/encoders/asm
Jun 23 00:55:31 Finished compiler/encoders/asm                                 1m06s 778MB
Jun 23 00:55:31 Starting compiler/encoders/x64
Jun 23 00:58:04 Finished compiler/encoders/x64                                 2m32s 965MB
Jun 23 00:58:04 Starting compiler/encoders/arm7
Jun 23 01:02:50 Finished compiler/encoders/arm7                                4m46s   1GB
Jun 23 01:02:50 Starting compiler/encoders/arm8
Jun 23 01:04:27 Finished compiler/encoders/arm8                                1m36s   1GB
Jun 23 01:04:27 Starting compiler/encoders/arm8_asl
Jun 23 05:23:06 Finished compiler/encoders/arm8_asl                         4h18m37s  32GB
Jun 23 05:23:06 Starting compiler/encoders/mips
Jun 23 05:26:30 Finished compiler/encoders/mips                                3m23s   1GB
Jun 23 05:26:31 Starting compiler/encoders/riscv
Jun 23 05:30:25 Finished compiler/encoders/riscv                               3m54s 888MB
Jun 23 05:30:25 Starting compiler/encoders/ag32
Jun 23 05:31:15 Finished compiler/encoders/ag32                                  49s 708MB
Jun 23 05:31:15 Starting compiler/backend/x64
Jun 23 05:32:06 Finished compiler/backend/x64                                    50s   1GB
Jun 23 05:32:06 Starting compiler/backend/arm7
Jun 23 05:32:59 Finished compiler/backend/arm7                                   53s   1GB
Jun 23 05:33:00 Starting compiler/backend/arm8
Jun 23 05:33:47 Finished compiler/backend/arm8                                   47s   1GB
Jun 23 05:33:48 Starting compiler/backend/mips
Jun 23 05:34:42 Finished compiler/backend/mips                                   53s   1GB
Jun 23 05:34:42 Starting compiler/backend/riscv
Jun 23 05:35:30 Finished compiler/backend/riscv                                  47s   1GB
Jun 23 05:35:30 Starting compiler/backend/ag32
Jun 23 05:38:23 Finished compiler/backend/ag32                                 2m52s   1GB
Jun 23 05:38:23 Starting compiler/parsing/proofs
Jun 23 05:46:48 Finished compiler/parsing/proofs                               8m24s   1GB
Jun 23 05:46:48 Starting compiler/inference/proofs
Jun 23 05:52:46 Finished compiler/inference/proofs                             5m58s   1GB
Jun 23 05:52:47 Starting compiler/backend/semantics
Jun 23 06:50:11 Finished compiler/backend/semantics                           57m24s   2GB
Jun 23 06:50:12 Starting compiler/backend/reg_alloc/proofs
Jun 23 06:58:09 Finished compiler/backend/reg_alloc/proofs                     7m56s   1GB
Jun 23 06:58:09 Starting compiler/backend/proofs
Jun 23 08:49:32 Finished compiler/backend/proofs                            1h51m22s  20GB
Jun 23 08:49:32 Starting compiler/backend/serialiser
Jun 23 08:52:59 Finished compiler/backend/serialiser                           3m26s   1GB
Jun 23 08:52:59 Starting compiler/encoders/x64/proofs
Jun 23 09:14:07 Finished compiler/encoders/x64/proofs                         21m07s   5GB
Jun 23 09:14:07 Starting compiler/encoders/arm7/proofs
Jun 23 09:43:21 Finished compiler/encoders/arm7/proofs                        29m12s   3GB
Jun 23 09:43:21 Starting compiler/encoders/arm8/proofs
Jun 23 09:58:43 Finished compiler/encoders/arm8/proofs                        15m21s   1GB
Jun 23 09:58:43 Starting compiler/encoders/arm8_asl/proofs
Jun 23 11:51:04 Finished compiler/encoders/arm8_asl/proofs                  1h52m21s   9GB
Jun 23 11:51:05 Starting compiler/encoders/mips/proofs
Jun 23 12:14:25 Finished compiler/encoders/mips/proofs                        23m20s   2GB
Jun 23 12:14:26 Starting compiler/encoders/riscv/proofs
Jun 23 12:34:30 Finished compiler/encoders/riscv/proofs                       20m04s   1GB
Jun 23 12:34:30 Starting compiler/encoders/ag32/proofs
Jun 23 12:40:11 Finished compiler/encoders/ag32/proofs                         5m40s 940MB
Jun 23 12:40:11 Starting compiler/backend/x64/proofs
Jun 23 12:41:13 Finished compiler/backend/x64/proofs                           1m01s   1GB
Jun 23 12:41:14 Starting compiler/backend/arm7/proofs
Jun 23 12:42:20 Finished compiler/backend/arm7/proofs                          1m05s   1GB
Jun 23 12:42:20 Starting compiler/backend/arm8/proofs
Jun 23 12:43:25 Finished compiler/backend/arm8/proofs                          1m04s   1GB
Jun 23 12:43:25 Starting compiler/backend/arm8_asl
Jun 23 12:44:19 Finished compiler/backend/arm8_asl                               53s   1GB
Jun 23 12:44:20 Starting compiler/backend/mips/proofs
Jun 23 12:45:20 Finished compiler/backend/mips/proofs                          1m00s   1GB
Jun 23 12:45:20 Starting compiler/backend/riscv/proofs
Jun 23 12:46:19 Finished compiler/backend/riscv/proofs                           58s   1GB
Jun 23 12:46:19 Starting compiler/backend/ag32/proofs
Jun 23 13:16:42 Finished compiler/backend/ag32/proofs                         30m22s   2GB
Jun 23 13:16:42 Starting compiler/proofs
Jun 23 13:21:52 Finished compiler/proofs                                       5m09s   3GB
Jun 23 13:21:53 Starting candle/set-theory
Jun 23 13:23:02 Finished candle/set-theory                                     1m09s   1GB
Jun 23 13:23:03 Starting candle/syntax-lib
Jun 23 13:23:32 Finished candle/syntax-lib                                       29s 533MB
Jun 23 13:23:33 Starting candle/standard/syntax
Jun 23 13:27:57 Finished candle/standard/syntax                                4m23s   1GB
Jun 23 13:27:57 Starting candle/standard/semantics
Jun 23 13:32:04 Finished candle/standard/semantics                             4m06s   1GB
Jun 23 13:32:04 Starting candle/standard/monadic
Jun 23 13:36:06 Finished candle/standard/monadic                               4m01s   1GB
Jun 23 13:36:06 Starting candle/standard/ml_kernel
Jun 23 13:49:51 Finished candle/standard/ml_kernel                            13m45s   3GB
Jun 23 13:49:52 Starting candle/overloading/syntax
Jun 23 13:56:38 Finished candle/overloading/syntax                             6m46s   1GB
Jun 23 13:56:38 Starting candle/overloading/semantics
Jun 23 14:22:27 Finished candle/overloading/semantics                         25m47s   2GB
Jun 23 14:22:27 Starting candle/overloading/monadic
Jun 23 14:27:59 Finished candle/overloading/monadic                            5m32s   1GB
Jun 23 14:27:59 Starting candle/overloading/ml_kernel
Jun 23 14:43:37 Finished candle/overloading/ml_kernel                         15m37s   3GB
Jun 23 14:43:38 Starting candle/overloading/ml_checker
Jun 23 14:49:08 Finished candle/overloading/ml_checker                         5m30s   3GB
Jun 23 14:49:08 Starting candle/prover
Jun 23 14:53:57 FAILED: candle/prover
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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)/src/coalgebras[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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[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$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanned 36 directories
Starting work on README.md
Starting work on ast_extrasTheory
README.md                                                                                                                                                                                             (0s)     OK
ast_extrasTheory                                                                                                                                                                                     (25s)     OK
Starting work on permsTheory
permsTheory                                                                                                                                                                                         (206s)     OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory                                                                                                                                                                             (42s)FAIL<1>
 <<HOL message: Created theory "candle_kernel_vals">>
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn:
 between line 20, character 2 and line 86, character 2:
 at Defn.prim_mk_defn:
 Free variables (abs_1_v) on RHS of nullary definition
 error in quse /root/regression/cakeml-1939/candle/prover/candle_kernel_valsScript.sml : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 20, character 2 and line 86, character 2:\nat Defn.prim_mk_defn:\nFree variables (abs_1_v) on RHS of nullary definition", origin_function = "xDefine", origin_structure = "TotalDefn"}
 error in load /root/regression/cakeml-1939/candle/prover/candle_kernel_valsScript : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 20, character 2 and line 86, character 2:\nat Defn.prim_mk_defn:\nFree variables (abs_1_v) on RHS of nullary definition", origin_function = "xDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 20, character 2 and line 86, character 2:\nat Defn.prim_mk_defn:\nFree variables (abs_1_v) on RHS of nullary definition", origin_function = "xDefine", origin_structure = "TotalDefn"}