Job 1255

CakeML:39062399ce376be1cd397e25bf6c9f2cdbdc9af6
  Get some files to build [Jun 07 20:16:15]
HOL:ac7497223d5845f2709250fa8fdcb566cbc2e1ae
  emacs-mode: make regexp searching case-sensitive; SOME not a q'fier [Jun 03 04:25:22]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 07 20:16:29 Claimed job
Jun 07 20:16:31 Reusing HOL
Jun 07 20:16:36 Starting developers
Jun 07 20:16:36 Finished developers                                               0s  29MB
Jun 07 20:16:37 Starting developers/bin
Jun 07 20:16:43 Finished developers/bin                                           6s   1GB
Jun 07 20:16:43 Starting semantics/ffi
Jun 07 20:16:54 Finished semantics/ffi                                           10s 242MB
Jun 07 20:16:54 Starting semantics
Jun 07 20:18:36 Finished semantics                                             1m41s 944MB
Jun 07 20:18:36 Starting semantics/proofs
Jun 07 20:22:23 Finished semantics/proofs                                      3m47s   1GB
Jun 07 20:22:23 Starting semantics/alt_semantics
Jun 07 20:22:32 Finished semantics/alt_semantics                                  8s 310MB
Jun 07 20:22:33 Starting semantics/alt_semantics/proofs
Jun 07 20:24:51 Finished semantics/alt_semantics/proofs                        2m18s 822MB
Jun 07 20:24:51 Starting basis/pure
Jun 07 20:25:45 Finished basis/pure                                              54s 792MB
Jun 07 20:25:45 Starting translator
Jun 07 20:28:44 Finished translator                                            2m58s   1GB
Jun 07 20:28:44 Starting compiler/parsing
Jun 07 20:30:13 Finished compiler/parsing                                      1m29s   2GB
Jun 07 20:30:13 Starting characteristic
Jun 07 20:36:30 Finished characteristic                                        6m17s   2GB
Jun 07 20:36:31 Starting translator/monadic
Jun 07 20:38:15 Finished translator/monadic                                    1m43s   1GB
Jun 07 20:38:15 Starting basis
Jun 07 21:13:13 Finished basis                                                34m58s  16GB
Jun 07 21:13:13 Starting compiler/inference
Jun 07 21:14:14 Finished compiler/inference                                    1m00s 911MB
Jun 07 21:14:14 Starting compiler/backend/reg_alloc
Jun 07 21:15:17 Finished compiler/backend/reg_alloc                            1m02s   1GB
Jun 07 21:15:17 Starting compiler/backend/gc
Jun 07 21:18:29 Finished compiler/backend/gc                                   3m11s   2GB
Jun 07 21:18:29 Starting compiler/backend
Jun 07 21:23:02 Finished compiler/backend                                      4m33s   2GB
Jun 07 21:23:02 Starting compiler/encoders/asm
Jun 07 21:23:24 Finished compiler/encoders/asm                                   21s 780MB
Jun 07 21:23:24 Starting compiler/encoders/x64
Jun 07 21:23:48 Finished compiler/encoders/x64                                   24s   1GB
Jun 07 21:23:48 Starting compiler/encoders/arm7
Jun 07 21:24:35 Finished compiler/encoders/arm7                                  47s 701MB
Jun 07 21:24:36 Starting compiler/encoders/arm8
Jun 07 21:24:48 Finished compiler/encoders/arm8                                  11s 933MB
Jun 07 21:24:48 Starting compiler/encoders/mips
Jun 07 21:25:05 Finished compiler/encoders/mips                                  16s   1GB
Jun 07 21:25:05 Starting compiler/encoders/riscv
Jun 07 21:25:20 Finished compiler/encoders/riscv                                 15s 767MB
Jun 07 21:25:20 Starting compiler/encoders/ag32
Jun 07 21:25:37 Finished compiler/encoders/ag32                                  16s 864MB
Jun 07 21:25:37 Starting compiler/backend/x64
Jun 07 21:25:54 Finished compiler/backend/x64                                    16s   1GB
Jun 07 21:25:54 Starting compiler/backend/arm7
Jun 07 21:26:14 Finished compiler/backend/arm7                                   20s   1GB
Jun 07 21:26:14 Starting compiler/backend/arm8
Jun 07 21:26:33 Finished compiler/backend/arm8                                   18s   1GB
Jun 07 21:26:33 Starting compiler/backend/mips
Jun 07 21:26:52 Finished compiler/backend/mips                                   18s   1GB
Jun 07 21:26:52 Starting compiler/backend/riscv
Jun 07 21:27:08 Finished compiler/backend/riscv                                  16s 978MB
Jun 07 21:27:09 Starting compiler/backend/ag32
Jun 07 21:28:17 Finished compiler/backend/ag32                                 1m08s   1GB
Jun 07 21:28:18 Starting compiler/parsing/proofs
Jun 07 21:33:51 Finished compiler/parsing/proofs                               5m33s   1GB
Jun 07 21:33:51 Starting compiler/inference/proofs
Jun 07 21:36:17 Finished compiler/inference/proofs                             2m25s   1GB
Jun 07 21:36:17 Starting compiler/backend/semantics
Jun 07 22:03:50 Finished compiler/backend/semantics                           27m32s   2GB
Jun 07 22:03:50 Starting compiler/backend/reg_alloc/proofs
Jun 07 22:07:07 Finished compiler/backend/reg_alloc/proofs                     3m17s 775MB
Jun 07 22:07:07 Starting compiler/backend/proofs
Jun 07 22:59:29 Finished compiler/backend/proofs                              52m21s  16GB
Jun 07 22:59:29 Starting compiler/encoders/x64/proofs
Jun 07 23:08:45 Finished compiler/encoders/x64/proofs                          9m15s   5GB
Jun 07 23:08:45 Starting compiler/encoders/arm7/proofs
Jun 07 23:21:07 Finished compiler/encoders/arm7/proofs                        12m21s   6GB
Jun 07 23:21:07 Starting compiler/encoders/arm8/proofs
Jun 07 23:27:27 Finished compiler/encoders/arm8/proofs                         6m19s   1GB
Jun 07 23:27:27 Starting compiler/encoders/mips/proofs
Jun 07 23:37:05 Finished compiler/encoders/mips/proofs                         9m37s   3GB
Jun 07 23:37:06 Starting compiler/encoders/riscv/proofs
Jun 07 23:45:42 Finished compiler/encoders/riscv/proofs                        8m36s   1GB
Jun 07 23:45:42 Starting compiler/encoders/ag32/proofs
Jun 07 23:48:12 Finished compiler/encoders/ag32/proofs                         2m29s 683MB
Jun 07 23:48:12 Starting compiler/backend/x64/proofs
Jun 07 23:48:32 Finished compiler/backend/x64/proofs                             19s   1GB
Jun 07 23:48:32 Starting compiler/backend/arm7/proofs
Jun 07 23:48:53 Finished compiler/backend/arm7/proofs                            20s   1GB
Jun 07 23:48:53 Starting compiler/backend/arm8/proofs
Jun 07 23:49:12 Finished compiler/backend/arm8/proofs                            18s   1GB
Jun 07 23:49:12 Starting compiler/backend/mips/proofs
Jun 07 23:49:32 Finished compiler/backend/mips/proofs                            20s   1GB
Jun 07 23:49:33 Starting compiler/backend/riscv/proofs
Jun 07 23:49:52 Finished compiler/backend/riscv/proofs                           19s   1GB
Jun 07 23:49:52 Starting compiler/backend/ag32/proofs
Jun 08 00:02:16 Finished compiler/backend/ag32/proofs                         12m23s   2GB
Jun 08 00:02:16 Starting compiler/proofs
Jun 08 00:04:02 Finished compiler/proofs                                       1m45s   4GB
Jun 08 00:04:02 Starting candle/set-theory
Jun 08 00:04:31 Finished candle/set-theory                                       27s 811MB
Jun 08 00:04:31 Starting candle/syntax-lib
Jun 08 00:04:41 Finished candle/syntax-lib                                        9s 701MB
Jun 08 00:04:41 Starting candle/standard/syntax
Jun 08 00:06:27 Finished candle/standard/syntax                                1m46s 881MB
Jun 08 00:06:28 Starting candle/standard/semantics
Jun 08 00:07:04 FAILED: candle/standard/semantics
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)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Starting work on holSemanticsTheory
holSemanticsTheory                                                                                                                                   real:    9s  user:    9s     OK
Starting work on holSemanticsExtraTheory
holSemanticsExtraTheory                                                                                                                              real:    9s  user:    9s     OK
Starting work on holBoolTheory
Starting work on holSoundnessTheory
holSoundnessTheory                                                                                                                                   real:   10s  user:    9s     OK
Starting work on holExtensionTheory
holBoolTheory                                                                                                                                        real:   16s  user:   15sFAIL<1>
     is_bool_interpretation i
 
 failed.
 Failed to prove theorem bool_has_bool_interpretation.
 
 Exception raised at BasicProvers.by:
 by's tactic failed to prove subgoal on line 131 (THEN1 on line 219) (THEN1 on line 232) (THEN1 on line 212) (THEN1 on line 287) (THEN1 on line 336) (THEN1 on line 373) (THEN1 on line 432) (THEN1 on line 471)
 error in quse /home/myreen/regression/cakeml-1255/candle/standard/semantics/holBoolScript.sml : HOL_ERR {message = "by's tactic failed to prove subgoal on line 131 (THEN1 on line 219) (THEN1 on line 232) (THEN1 on line 212) (THEN1 on line 287) (THEN1 on line 336) (THEN1 on line 373) (THEN1 on line 432) (THEN1 on line 471)", origin_function = "by", origin_structure = "BasicProvers"}
 error in load /home/myreen/regression/cakeml-1255/candle/standard/semantics/holBoolScript : HOL_ERR {message = "by's tactic failed to prove subgoal on line 131 (THEN1 on line 219) (THEN1 on line 232) (THEN1 on line 212) (THEN1 on line 287) (THEN1 on line 336) (THEN1 on line 373) (THEN1 on line 432) (THEN1 on line 471)", origin_function = "by", origin_structure = "BasicProvers"}
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 131 (THEN1 on line 219) (THEN1 on line 232) (THEN1 on line 212) (THEN1 on line 287) (THEN1 on line 336) (THEN1 on line 373) (THEN1 on line 432) (THEN1 on line 471)", origin_function = "by", origin_structure = "BasicProvers"}
holExtensionTheory                                                                                                                                                           M-KILLED