Job 823

CakeML:4f52c414a947ee02c325243a742e35334d42d847
  Fix typos in comments, replace ARMv6 with ARMv7 [Apr 29 11:14:04]
#633 (FMA_support)
Merging into:62c51fa831d455390795c47c53f56b050a23f7ad
  Merge pull request #627 from CakeML/monadic-trans-cleanup [Apr 27 07:20:55]
HOL:8e183cc626814e8bfbee46abcbf51798ee1c69b6
  Emacs mode: fix dumb bug in M-h H [Apr 29 06:05:42]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 29 15:33:41 Claimed job
Apr 29 15:33:45 Reusing HOL
Apr 29 15:33:50 Starting developers
Apr 29 15:33:51 Finished developers                                               0s  22MB
Apr 29 15:33:51 Starting developers/bin
Apr 29 15:34:23 Finished developers/bin                                          31s 207MB
Apr 29 15:34:24 Starting semantics/ffi
Apr 29 15:34:32 Finished semantics/ffi                                            7s 221MB
Apr 29 15:34:32 Starting semantics
Apr 29 15:35:50 Finished semantics                                             1m17s   1GB
Apr 29 15:35:50 Starting semantics/proofs
Apr 29 15:38:46 Finished semantics/proofs                                      2m55s   1GB
Apr 29 15:38:46 Starting basis/pure
Apr 29 15:39:31 Finished basis/pure                                              44s 670MB
Apr 29 15:39:31 Starting translator
Apr 29 15:41:11 Finished translator                                            1m39s   1GB
Apr 29 15:41:12 Starting compiler/parsing
Apr 29 15:42:13 Finished compiler/parsing                                      1m01s   2GB
Apr 29 15:42:13 Starting characteristic
Apr 29 15:47:31 Finished characteristic                                        5m17s   1GB
Apr 29 15:47:32 Starting translator/monadic
Apr 29 15:49:14 Finished translator/monadic                                    1m42s   1GB
Apr 29 15:49:15 Starting basis
Apr 29 16:07:02 Finished basis                                                17m46s   2GB
Apr 29 16:07:02 Starting compiler/inference
Apr 29 16:08:44 Finished compiler/inference                                    1m41s   1GB
Apr 29 16:08:44 Starting compiler/backend/reg_alloc
Apr 29 16:09:48 Finished compiler/backend/reg_alloc                            1m03s   1GB
Apr 29 16:09:49 Starting compiler/backend/gc
Apr 29 16:18:44 Finished compiler/backend/gc                                   8m55s   2GB
Apr 29 16:18:45 Starting compiler/backend
Apr 29 16:18:46 Finished compiler/backend                                         0s  42MB
Apr 29 16:18:46 Starting compiler/encoders/asm
Apr 29 16:18:47 Finished compiler/encoders/asm                                    0s  32MB
Apr 29 16:18:47 Starting compiler/encoders/x64
Apr 29 16:19:17 Finished compiler/encoders/x64                                   30s 924MB
Apr 29 16:19:18 Starting compiler/encoders/arm6
Apr 29 16:20:19 Finished compiler/encoders/arm6                                1m00s 767MB
Apr 29 16:20:20 Starting compiler/encoders/arm8
Apr 29 16:20:35 Finished compiler/encoders/arm8                                  15s 532MB
Apr 29 16:20:36 Starting compiler/encoders/mips
Apr 29 16:21:00 Finished compiler/encoders/mips                                  23s 758MB
Apr 29 16:21:00 Starting compiler/encoders/riscv
Apr 29 16:21:19 Finished compiler/encoders/riscv                                 18s 742MB
Apr 29 16:21:19 Starting compiler/encoders/ag32
Apr 29 16:21:42 Finished compiler/encoders/ag32                                  22s 483MB
Apr 29 16:21:43 Starting compiler/backend/x64
Apr 29 16:22:05 Finished compiler/backend/x64                                    22s 842MB
Apr 29 16:22:06 Starting compiler/backend/arm6
Apr 29 16:22:32 Finished compiler/backend/arm6                                   26s   1GB
Apr 29 16:22:33 Starting compiler/backend/arm8
Apr 29 16:22:59 Finished compiler/backend/arm8                                   26s 944MB
Apr 29 16:22:59 Starting compiler/backend/mips
Apr 29 16:23:25 Finished compiler/backend/mips                                   24s   1GB
Apr 29 16:23:25 Starting compiler/backend/riscv
Apr 29 16:23:49 Finished compiler/backend/riscv                                  23s   1GB
Apr 29 16:23:49 Starting compiler/backend/ag32
Apr 29 16:25:28 Finished compiler/backend/ag32                                 1m38s 951MB
Apr 29 16:25:29 Starting compiler/parsing/proofs
Apr 29 16:31:33 Finished compiler/parsing/proofs                               6m04s 796MB
Apr 29 16:31:34 Starting compiler/inference/proofs
Apr 29 16:34:11 Finished compiler/inference/proofs                             2m36s   1GB
Apr 29 16:34:12 Starting compiler/backend/semantics
Apr 29 16:41:11 Finished compiler/backend/semantics                            6m59s   1GB
Apr 29 16:41:12 Starting compiler/backend/reg_alloc/proofs
Apr 29 16:44:22 Finished compiler/backend/reg_alloc/proofs                     3m09s 919MB
Apr 29 16:44:22 Starting compiler/backend/proofs
Apr 29 17:22:44 Finished compiler/backend/proofs                              38m21s   3GB
Apr 29 17:22:45 Starting compiler/encoders/x64/proofs
Apr 29 17:31:43 Finished compiler/encoders/x64/proofs                          8m57s   4GB
Apr 29 17:31:43 Starting compiler/encoders/arm6/proofs
Apr 29 17:40:40 FAILED: compiler/encoders/arm6/proofs
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/prog]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/prog[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-823/misc]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-823/misc]0;Holmake: ~/regression/cakeml-823/developers]0;Holmake: ~/regression/cakeml-823/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-823/misc]0;Holmake: ~/regression/cakeml-823/misc/lem_lib_stub]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/cakeml-823/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-823/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-823/misc]0;Holmake: ~/regression/cakeml-823/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-823/semantics]0;Holmake: ~/regression/cakeml-823/semantics/ffi]0;Holmake: ~/regression/cakeml-823/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-823/semantics]0;Holmake: ~/regression/cakeml-823/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../asm]0;Holmake: ../../asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6/proofs[0m
Starting work on arm6_targetProofTheory
Starting work on README.md
README.md                                                                                                  OK
arm6_targetProofTheory                                                                            FAILED! <1>
 encoder_correct arm6_target
 
 failed.
 Failed to prove theorem arm6_encoder_correct.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 1146) (THEN1 on line 991) (THEN1 on line 1156) (THEN1 on line 1163) (THEN1 on line 1175) (THEN1 on line 1184) (THEN1 on line 1191)
 error in quse /home/myreen/regression/cakeml-823/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1146) (THEN1 on line 991) (THEN1 on line 1156) (THEN1 on line 1163) (THEN1 on line 1175) (THEN1 on line 1184) (THEN1 on line 1191)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load arm6_targetProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1146) (THEN1 on line 991) (THEN1 on line 1156) (THEN1 on line 1163) (THEN1 on line 1175) (THEN1 on line 1184) (THEN1 on line 1191)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1146) (THEN1 on line 991) (THEN1 on line 1156) (THEN1 on line 1163) (THEN1 on line 1175) (THEN1 on line 1184) (THEN1 on line 1191)", origin_function = "THEN1", origin_structure = "Tactical"}