Job 1452

CakeML:92d134e96e54a9b869fa52f8aec44e3738f30ffb
  More adjustments [Jan 25 12:39:05]
HOL:5f5ada572b9ae917397a3ffa4cee0d84b511b402
  Document BIGINTER_SUBSET change [Jan 22 10:51:29]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 25 13:00:24 Claimed job
Jan 25 13:00:27 Reusing HOL
Jan 25 13:00:34 Starting developers
Jan 25 13:00:35 Finished developers                                               0s  35MB
Jan 25 13:00:35 Starting developers/bin
Jan 25 13:00:43 Finished developers/bin                                           7s   1GB
Jan 25 13:00:43 Starting semantics/ffi
Jan 25 13:00:55 Finished semantics/ffi                                           11s 269MB
Jan 25 13:00:55 Starting semantics
Jan 25 13:02:45 Finished semantics                                             1m49s   1GB
Jan 25 13:02:45 Starting semantics/proofs
Jan 25 13:06:35 Finished semantics/proofs                                      3m49s   1GB
Jan 25 13:06:35 Starting semantics/alt_semantics
Jan 25 13:06:44 Finished semantics/alt_semantics                                  8s 409MB
Jan 25 13:06:44 Starting semantics/alt_semantics/proofs
Jan 25 13:09:08 Finished semantics/alt_semantics/proofs                        2m23s   1GB
Jan 25 13:09:08 Starting basis/pure
Jan 25 13:10:35 Finished basis/pure                                            1m26s   1GB
Jan 25 13:10:35 Starting translator
Jan 25 13:14:51 Finished translator                                            4m14s   2GB
Jan 25 13:14:51 Starting compiler/parsing
Jan 25 13:16:24 Finished compiler/parsing                                      1m32s   2GB
Jan 25 13:16:24 Starting characteristic
Jan 25 13:23:01 Finished characteristic                                        6m36s   4GB
Jan 25 13:23:01 Starting translator/monadic
Jan 25 13:24:52 Finished translator/monadic                                    1m50s   2GB
Jan 25 13:24:52 Starting basis
Jan 25 14:08:09 Finished basis                                                43m16s  23GB
Jan 25 14:08:09 Starting compiler/inference
Jan 25 14:09:12 Finished compiler/inference                                    1m02s   1GB
Jan 25 14:09:12 Starting compiler/backend/reg_alloc
Jan 25 14:10:16 Finished compiler/backend/reg_alloc                            1m04s   1GB
Jan 25 14:10:17 Starting compiler/backend/gc
Jan 25 14:13:38 Finished compiler/backend/gc                                   3m21s   3GB
Jan 25 14:13:38 Starting compiler/backend
Jan 25 14:18:38 Finished compiler/backend                                      5m00s   5GB
Jan 25 14:18:39 Starting compiler/encoders/asm
Jan 25 14:19:01 Finished compiler/encoders/asm                                   22s   1GB
Jan 25 14:19:02 Starting compiler/encoders/x64
Jan 25 14:19:28 Finished compiler/encoders/x64                                   26s   1GB
Jan 25 14:19:28 Starting compiler/encoders/arm7
Jan 25 14:20:19 Finished compiler/encoders/arm7                                  50s   1GB
Jan 25 14:20:19 Starting compiler/encoders/arm8
Jan 25 14:20:33 Finished compiler/encoders/arm8                                  13s   1GB
Jan 25 14:20:33 Starting compiler/encoders/mips
Jan 25 14:20:51 Finished compiler/encoders/mips                                  17s   1GB
Jan 25 14:20:51 Starting compiler/encoders/riscv
Jan 25 14:21:07 Finished compiler/encoders/riscv                                 16s   1GB
Jan 25 14:21:08 Starting compiler/encoders/ag32
Jan 25 14:21:26 Finished compiler/encoders/ag32                                  18s 924MB
Jan 25 14:21:27 Starting compiler/backend/x64
Jan 25 14:21:46 Finished compiler/backend/x64                                    19s   1GB
Jan 25 14:21:47 Starting compiler/backend/arm7
Jan 25 14:22:09 Finished compiler/backend/arm7                                   21s   1GB
Jan 25 14:22:09 Starting compiler/backend/arm8
Jan 25 14:22:29 Finished compiler/backend/arm8                                   19s   1GB
Jan 25 14:22:29 Starting compiler/backend/mips
Jan 25 14:22:50 Finished compiler/backend/mips                                   20s   1GB
Jan 25 14:22:50 Starting compiler/backend/riscv
Jan 25 14:23:11 Finished compiler/backend/riscv                                  20s   1GB
Jan 25 14:23:11 Starting compiler/backend/ag32
Jan 25 14:24:20 Finished compiler/backend/ag32                                 1m09s   2GB
Jan 25 14:24:20 Starting compiler/parsing/proofs
Jan 25 14:29:47 Finished compiler/parsing/proofs                               5m26s   2GB
Jan 25 14:29:47 Starting compiler/inference/proofs
Jan 25 14:32:18 Finished compiler/inference/proofs                             2m31s   2GB
Jan 25 14:32:18 Starting compiler/backend/semantics
Jan 25 14:59:09 Finished compiler/backend/semantics                           26m50s   3GB
Jan 25 14:59:09 Starting compiler/backend/reg_alloc/proofs
Jan 25 15:02:24 Finished compiler/backend/reg_alloc/proofs                     3m14s   1GB
Jan 25 15:02:24 Starting compiler/backend/proofs
Jan 25 15:55:43 Finished compiler/backend/proofs                              53m18s  16GB
Jan 25 15:55:43 Starting compiler/encoders/x64/proofs
Jan 25 15:57:11 FAILED: compiler/encoders/x64/proofs
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Starting work on x64_targetProofTheory
x64_targetProofTheory                                                         real:   87s  user:   82sFAIL<1>
   num2Zreg (w2n r)  RDI
 
 failed.
 First unsolved sub-goal is
 
 F
 
 error in quse /home/myreen/regression/cakeml-1452/compiler/encoders/x64/proofs/x64_targetProofScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1452/compiler/encoders/x64/proofs/x64_targetProofScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}