Job 1531

CakeML:01a1321ec6df3fc0b121a4a6a1ee4a3759b24aa8
  Fix another broken proof [May 18 14:27:17]
HOL:fe4634b86ea93f927bb796c73b7f77e15362962e
  Universally quantify statements [May 17 23:32:35]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 19 08:15:17 Claimed job
May 19 08:15:20 Building HOL
May 19 08:29:46 Starting developers
May 19 08:29:49 Finished developers                                               2s 138MB
May 19 08:29:49 Starting developers/bin
May 19 08:29:56 Finished developers/bin                                           6s   1GB
May 19 08:29:56 Starting semantics/ffi
May 19 08:30:06 Finished semantics/ffi                                           10s 297MB
May 19 08:30:07 Starting semantics
May 19 08:31:41 Finished semantics                                             1m33s   1GB
May 19 08:31:41 Starting semantics/proofs
May 19 08:35:12 Finished semantics/proofs                                      3m30s   1GB
May 19 08:35:12 Starting semantics/alt_semantics
May 19 08:35:21 Finished semantics/alt_semantics                                  8s 391MB
May 19 08:35:21 Starting semantics/alt_semantics/proofs
May 19 08:37:34 Finished semantics/alt_semantics/proofs                        2m12s   1GB
May 19 08:37:35 Starting basis/pure
May 19 08:40:21 Finished basis/pure                                            2m45s   1GB
May 19 08:40:21 Starting translator
May 19 08:43:38 Finished translator                                            3m17s   2GB
May 19 08:43:38 Starting compiler/parsing
May 19 08:44:48 Finished compiler/parsing                                      1m09s   4GB
May 19 08:44:48 Starting characteristic
May 19 08:50:32 Finished characteristic                                        5m43s   3GB
May 19 08:50:32 Starting translator/monadic
May 19 08:52:21 Finished translator/monadic                                    1m48s   3GB
May 19 08:52:21 Starting basis
May 19 09:36:14 Finished basis                                                43m52s  40GB
May 19 09:36:14 Starting compiler/inference
May 19 09:37:26 Finished compiler/inference                                    1m12s   2GB
May 19 09:37:27 Starting compiler/backend/reg_alloc
May 19 09:38:33 Finished compiler/backend/reg_alloc                            1m06s   1GB
May 19 09:38:34 Starting compiler/backend/gc
May 19 09:42:14 Finished compiler/backend/gc                                   3m40s   3GB
May 19 09:42:14 Starting compiler/backend
May 19 09:47:26 Finished compiler/backend                                      5m10s   5GB
May 19 09:47:26 Starting compiler/encoders/asm
May 19 09:47:49 Finished compiler/encoders/asm                                   22s   1GB
May 19 09:47:49 Starting compiler/encoders/x64
May 19 09:48:53 Finished compiler/encoders/x64                                 1m03s   1GB
May 19 09:48:53 Starting compiler/encoders/arm7
May 19 09:50:56 Finished compiler/encoders/arm7                                2m02s   1GB
May 19 09:50:56 Starting compiler/encoders/arm8
May 19 09:51:36 Finished compiler/encoders/arm8                                  39s   1GB
May 19 09:51:36 Starting compiler/encoders/mips
May 19 09:53:03 Finished compiler/encoders/mips                                1m26s   1GB
May 19 09:53:03 Starting compiler/encoders/riscv
May 19 09:54:44 Finished compiler/encoders/riscv                               1m40s   1GB
May 19 09:54:44 Starting compiler/encoders/ag32
May 19 09:55:02 Finished compiler/encoders/ag32                                  18s 951MB
May 19 09:55:02 Starting compiler/backend/x64
May 19 09:55:21 Finished compiler/backend/x64                                    18s   1GB
May 19 09:55:21 Starting compiler/backend/arm7
May 19 09:55:43 Finished compiler/backend/arm7                                   21s   1GB
May 19 09:55:44 Starting compiler/backend/arm8
May 19 09:56:04 Finished compiler/backend/arm8                                   20s   1GB
May 19 09:56:04 Starting compiler/backend/mips
May 19 09:56:25 Finished compiler/backend/mips                                   20s   1GB
May 19 09:56:25 Starting compiler/backend/riscv
May 19 09:56:46 Finished compiler/backend/riscv                                  21s   1GB
May 19 09:56:47 Starting compiler/backend/ag32
May 19 09:57:56 Finished compiler/backend/ag32                                 1m09s   2GB
May 19 09:57:57 Starting compiler/parsing/proofs
May 19 10:03:49 Finished compiler/parsing/proofs                               5m52s   2GB
May 19 10:03:49 Starting compiler/inference/proofs
May 19 10:06:22 Finished compiler/inference/proofs                             2m32s   2GB
May 19 10:06:22 Starting compiler/backend/semantics
May 19 10:33:18 Finished compiler/backend/semantics                           26m55s   3GB
May 19 10:33:19 Starting compiler/backend/reg_alloc/proofs
May 19 10:36:36 Finished compiler/backend/reg_alloc/proofs                     3m17s   1GB
May 19 10:36:37 Starting compiler/backend/proofs
May 19 11:30:30 Finished compiler/backend/proofs                              53m53s  16GB
May 19 11:30:30 Starting compiler/encoders/x64/proofs
May 19 11:32:21 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 README.md
Starting work on x64_targetProofTheory
README.md                                                                                                                                            real:    0s  user:    0s     OK
x64_targetProofTheory                                                                                                                                real:  110s  user:  105sFAIL<1>
      (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
      (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
      (... ..., ...) => Zfull_inst (...) |
      (...) => ... ... |
      ... => ... |
      ...
 <<HOL message: Created theory "x64_targetProof">>
 error in quse /home/myreen/regression/cakeml-1531/compiler/encoders/x64/proofs/x64_targetProofScript.sml : HOL_ERR {message = "\"asm_state_failed\" not found in theory \"asmSem\"", origin_function = "prim_mk_const", origin_structure = "Term"}
 error in load /home/myreen/regression/cakeml-1531/compiler/encoders/x64/proofs/x64_targetProofScript : HOL_ERR {message = "\"asm_state_failed\" not found in theory \"asmSem\"", origin_function = "prim_mk_const", origin_structure = "Term"}
 Uncaught exception: HOL_ERR {message = "\"asm_state_failed\" not found in theory \"asmSem\"", origin_function = "prim_mk_const", origin_structure = "Term"}