Job 868

CakeML:5a9eb41285f88f2a0ee430bbab15d5dfffc8ee76
  More fixes to make armV7 backend compile [May 14 11:51:14]
#633 (FMA_support)
Merging into:d12bf8c081357963887ad183f2f09e395105cdf6
  renaming for Isabelle (resurrect 7fbd3c0) [May 13 08:52:17]
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again [May 09 11:06:43]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 14 12:16:14 Claimed job
May 14 12:16:18 Reusing HOL
May 14 12:16:27 Starting developers
May 14 12:16:27 Finished developers                                               0s  21MB
May 14 12:16:28 Starting developers/bin
May 14 12:16:31 Finished developers/bin                                           3s 144MB
May 14 12:16:32 Starting semantics/ffi
May 14 12:16:40 Finished semantics/ffi                                            7s 221MB
May 14 12:16:40 Starting semantics
May 14 12:17:56 Finished semantics                                             1m16s   1GB
May 14 12:17:57 Starting semantics/proofs
May 14 12:20:55 Finished semantics/proofs                                      2m57s   1GB
May 14 12:20:55 Starting basis/pure
May 14 12:21:38 Finished basis/pure                                              43s 724MB
May 14 12:21:38 Starting translator
May 14 12:23:17 Finished translator                                            1m38s   1GB
May 14 12:23:18 Starting compiler/parsing
May 14 12:24:15 Finished compiler/parsing                                        56s   2GB
May 14 12:24:15 Starting characteristic
May 14 12:29:23 Finished characteristic                                        5m07s   1GB
May 14 12:29:23 Starting translator/monadic
May 14 12:30:46 Finished translator/monadic                                    1m22s   1GB
May 14 12:30:47 Starting basis
May 14 12:47:16 Finished basis                                                16m28s   2GB
May 14 12:47:16 Starting compiler/inference
May 14 12:48:49 Finished compiler/inference                                    1m32s   1GB
May 14 12:48:49 Starting compiler/backend/reg_alloc
May 14 12:49:47 Finished compiler/backend/reg_alloc                              57s   1GB
May 14 12:49:47 Starting compiler/backend/gc
May 14 12:57:45 Finished compiler/backend/gc                                   7m58s   1GB
May 14 12:57:46 Starting compiler/backend
May 14 12:57:47 Finished compiler/backend                                         0s  42MB
May 14 12:57:47 Starting compiler/encoders/asm
May 14 12:57:47 Finished compiler/encoders/asm                                    0s  32MB
May 14 12:57:48 Starting compiler/encoders/x64
May 14 12:58:10 Finished compiler/encoders/x64                                   22s 943MB
May 14 12:58:11 Starting compiler/encoders/arm7
May 14 12:58:55 Finished compiler/encoders/arm7                                  44s 809MB
May 14 12:58:55 Starting compiler/encoders/arm8
May 14 12:59:07 Finished compiler/encoders/arm8                                  11s 562MB
May 14 12:59:07 Starting compiler/encoders/mips
May 14 12:59:23 Finished compiler/encoders/mips                                  15s   1GB
May 14 12:59:23 Starting compiler/encoders/riscv
May 14 12:59:37 Finished compiler/encoders/riscv                                 13s 948MB
May 14 12:59:37 Starting compiler/encoders/ag32
May 14 12:59:52 Finished compiler/encoders/ag32                                  14s 776MB
May 14 12:59:52 Starting compiler/backend/x64
May 14 13:00:07 Finished compiler/backend/x64                                    14s 829MB
May 14 13:00:08 Starting compiler/backend/arm7
May 14 13:00:25 Finished compiler/backend/arm7                                   17s   1GB
May 14 13:00:25 Starting compiler/backend/arm8
May 14 13:00:42 Finished compiler/backend/arm8                                   15s   1GB
May 14 13:00:42 Starting compiler/backend/mips
May 14 13:00:58 Finished compiler/backend/mips                                   15s   1GB
May 14 13:00:58 Starting compiler/backend/riscv
May 14 13:01:15 Finished compiler/backend/riscv                                  16s   1GB
May 14 13:01:15 Starting compiler/backend/ag32
May 14 13:02:24 Finished compiler/backend/ag32                                 1m07s   1GB
May 14 13:02:24 Starting compiler/parsing/proofs
May 14 13:07:58 Finished compiler/parsing/proofs                               5m34s   1GB
May 14 13:07:58 Starting compiler/inference/proofs
May 14 13:10:37 Finished compiler/inference/proofs                             2m37s   1GB
May 14 13:10:37 Starting compiler/backend/semantics
May 14 13:17:39 Finished compiler/backend/semantics                            7m02s   2GB
May 14 13:17:39 Starting compiler/backend/reg_alloc/proofs
May 14 13:21:02 Finished compiler/backend/reg_alloc/proofs                     3m22s 742MB
May 14 13:21:02 Starting compiler/backend/proofs
May 14 13:59:37 Finished compiler/backend/proofs                              38m34s   3GB
May 14 13:59:37 Starting compiler/encoders/x64/proofs
May 14 14:08:43 Finished compiler/encoders/x64/proofs                          9m05s   4GB
May 14 14:08:43 Starting compiler/encoders/arm7/proofs
May 14 14:17:45 FAILED: compiler/encoders/arm7/proofs
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/prog]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/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-868/misc]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-868/misc]0;Holmake: ~/regression/cakeml-868/developers]0;Holmake: ~/regression/cakeml-868/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-868/misc]0;Holmake: ~/regression/cakeml-868/misc/lem_lib_stub]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/cakeml-868/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-868/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-868/misc]0;Holmake: ~/regression/cakeml-868/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-868/semantics]0;Holmake: ~/regression/cakeml-868/semantics/ffi]0;Holmake: ~/regression/cakeml-868/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-868/semantics]0;Holmake: ~/regression/cakeml-868/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/arm7[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm7/proofs[0m
Starting work on arm7_targetProofTheory
arm7_targetProofTheory                                                                                                   FAILED! <1>
 encoder_correct arm7_target
 
 failed.
 Failed to prove theorem arm7_encoder_correct.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 1129) (THEN1 on line 1130) (THEN1 on line 1131) (THEN1 on line 1132) (THEN1 on line 1133) (THEN1 on line 1148) (THEN1 on line 992) (THEN1 on line 1158) (THEN1 on line 1165) (THEN1 on line 1177) (THEN1 on line 1186) (THEN1 on line 1193)
 error in quse /home/myreen/regression/cakeml-868/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1129) (THEN1 on line 1130) (THEN1 on line 1131) (THEN1 on line 1132) (THEN1 on line 1133) (THEN1 on line 1148) (THEN1 on line 992) (THEN1 on line 1158) (THEN1 on line 1165) (THEN1 on line 1177) (THEN1 on line 1186) (THEN1 on line 1193)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load arm7_targetProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1129) (THEN1 on line 1130) (THEN1 on line 1131) (THEN1 on line 1132) (THEN1 on line 1133) (THEN1 on line 1148) (THEN1 on line 992) (THEN1 on line 1158) (THEN1 on line 1165) (THEN1 on line 1177) (THEN1 on line 1186) (THEN1 on line 1193)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1129) (THEN1 on line 1130) (THEN1 on line 1131) (THEN1 on line 1132) (THEN1 on line 1133) (THEN1 on line 1148) (THEN1 on line 992) (THEN1 on line 1158) (THEN1 on line 1165) (THEN1 on line 1177) (THEN1 on line 1186) (THEN1 on line 1193)", origin_function = "THEN1", origin_structure = "Tactical"}