Job 564

CakeML:c3c3dd155b4a7f634b8e3ef9894c88b32e99d29e
  Fix up x64 version of wordcountProof [Nov 20 09:45:54]
#554 (tiny)
Merging into:8ee5d433f5e6a93e9a41ea5e46b961c65130c2ef
  Merge pull request #551 from CakeML/translator-alist-tree [Nov 17 12:09:47]
HOL:57ef4df497757f622a7fe2bfeda16116585da6d4
  Update experimental kernel for world free of Globals.priming [Nov 20 05:59:15]
Machine:demi

Nov 20 13:14:30 Claimed job
Nov 20 13:14:34 Reusing HOL
Nov 20 13:15:34 Starting developers/bin
Nov 20 13:15:40 Finished developers/bin                                           6s 929MB
Nov 20 13:15:41 Starting semantics/ffi
Nov 20 13:15:58 Finished semantics/ffi                                           16s 304MB
Nov 20 13:15:58 Starting semantics
Nov 20 13:17:41 Finished semantics                                             1m42s 856MB
Nov 20 13:17:42 Starting semantics/proofs
Nov 20 13:21:41 Finished semantics/proofs                                      3m58s   1GB
Nov 20 13:21:42 Starting basis/pure
Nov 20 13:22:56 Finished basis/pure                                            1m13s 710MB
Nov 20 13:22:56 Starting translator
Nov 20 13:27:11 Finished translator                                            4m14s   1GB
Nov 20 13:27:11 Starting compiler/parsing
Nov 20 13:28:56 Finished compiler/parsing                                      1m44s   1GB
Nov 20 13:28:57 Starting characteristic
Nov 20 13:32:30 Finished characteristic                                        3m32s   1GB
Nov 20 13:32:31 Starting translator/monadic
Nov 20 13:34:30 Finished translator/monadic                                    1m58s   1GB
Nov 20 13:34:31 Starting basis
Nov 20 13:57:14 Finished basis                                                22m43s   3GB
Nov 20 13:57:15 Starting compiler/inference
Nov 20 13:59:07 Finished compiler/inference                                    1m51s   1GB
Nov 20 13:59:07 Starting compiler/backend/reg_alloc
Nov 20 14:00:13 Finished compiler/backend/reg_alloc                            1m04s   1GB
Nov 20 14:00:13 Starting compiler/backend/gc
Nov 20 14:08:50 Finished compiler/backend/gc                                   8m36s   1GB
Nov 20 14:08:51 Starting compiler/backend
Nov 20 14:08:54 Finished compiler/backend                                         3s  33MB
Nov 20 14:08:55 Starting compiler/encoders/asm
Nov 20 14:08:57 Finished compiler/encoders/asm                                    1s  33MB
Nov 20 14:08:57 Starting compiler/encoders/x64
Nov 20 14:09:23 Finished compiler/encoders/x64                                   25s 443MB
Nov 20 14:09:23 Starting compiler/encoders/arm6
Nov 20 14:10:24 Finished compiler/encoders/arm6                                1m00s 428MB
Nov 20 14:10:25 Starting compiler/encoders/arm8
Nov 20 14:10:36 Finished compiler/encoders/arm8                                  11s 393MB
Nov 20 14:10:37 Starting compiler/encoders/mips
Nov 20 14:10:51 Finished compiler/encoders/mips                                  13s 544MB
Nov 20 14:10:51 Starting compiler/encoders/riscv
Nov 20 14:11:03 Finished compiler/encoders/riscv                                 11s 434MB
Nov 20 14:11:04 Starting compiler/encoders/ag32
Nov 20 14:11:30 Finished compiler/encoders/ag32                                  25s 605MB
Nov 20 14:11:30 Starting compiler/backend/x64
Nov 20 14:11:54 Finished compiler/backend/x64                                    23s   1GB
Nov 20 14:11:55 Starting compiler/backend/arm6
Nov 20 14:12:21 Finished compiler/backend/arm6                                   25s   1GB
Nov 20 14:12:21 Starting compiler/backend/arm8
Nov 20 14:12:47 Finished compiler/backend/arm8                                   25s   1GB
Nov 20 14:12:48 Starting compiler/backend/mips
Nov 20 14:13:14 Finished compiler/backend/mips                                   25s   1GB
Nov 20 14:13:14 Starting compiler/backend/riscv
Nov 20 14:13:40 Finished compiler/backend/riscv                                  25s   1GB
Nov 20 14:13:41 Starting compiler/backend/ag32
Nov 20 14:15:19 Finished compiler/backend/ag32                                 1m37s   1GB
Nov 20 14:15:19 Starting compiler/parsing/proofs
Nov 20 14:24:40 Finished compiler/parsing/proofs                               9m19s 930MB
Nov 20 14:24:40 Starting compiler/inference/proofs
Nov 20 14:28:45 Finished compiler/inference/proofs                             4m04s   1GB
Nov 20 14:28:46 Starting compiler/backend/semantics
Nov 20 14:40:43 Finished compiler/backend/semantics                           11m56s   2GB
Nov 20 14:40:43 Starting compiler/backend/reg_alloc/proofs
Nov 20 14:44:28 Finished compiler/backend/reg_alloc/proofs                     3m44s 914MB
Nov 20 14:44:29 Starting compiler/backend/proofs
Nov 20 15:41:54 Finished compiler/backend/proofs                              57m24s   3GB
Nov 20 15:41:54 Starting compiler/encoders/x64/proofs
Nov 20 15:54:16 Finished compiler/encoders/x64/proofs                         12m20s   1GB
Nov 20 15:54:16 Starting compiler/encoders/arm6/proofs
Nov 20 16:13:04 Finished compiler/encoders/arm6/proofs                        18m47s   1GB
Nov 20 16:13:04 Starting compiler/encoders/arm8/proofs
Nov 20 16:20:57 Finished compiler/encoders/arm8/proofs                         7m52s   1GB
Nov 20 16:20:58 Starting compiler/encoders/mips/proofs
Nov 20 16:34:52 Finished compiler/encoders/mips/proofs                        13m53s   2GB
Nov 20 16:34:52 Starting compiler/encoders/riscv/proofs
Nov 20 16:35:00 FAILED: compiler/encoders/riscv/proofs
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/common]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/prog]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/decompiler]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/lib]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/prog]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/prog[0m
]0;Holmake: .]0;Holmake: ../../asm]0;Holmake: ../../../../misc]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../../misc]0;Holmake: ../../../../developers]0;Holmake: ../../../../developers[1mWorking in ../../../../developers[0m
]0;Holmake: ../../../../misc]0;Holmake: ../../../../misc/lem_lib_stub]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/context-free]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ../../../../misc/lem_lib_stub]0;Holmake: ../../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../../misc]0;Holmake: ../../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ../../../../semantics]0;Holmake: ../../../../semantics/ffi]0;Holmake: ../../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../../semantics]0;Holmake: ../../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../asm]0;Holmake: ../../asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv/proofs[0m
Starting work on riscv_targetProofTheory
riscv_targetProofTheory                                                                                                                                                                                                                                                       FAILED! <1>
 error in quse /usr/local/google/home/ramanakumar/cakeml/regression-worker/cakeml-564/compiler/encoders/riscv/proofs/riscv_targetProofScript.sml : Fail "Static Errors"
 error in load riscv_targetProofScript : Fail "Static Errors"
 /usr/local/google/home/ramanakumar/cakeml/regression-worker/cakeml-564/compiler/encoders/riscv/proofs/riscv_targetProofScript.sml:188: error: Value or constructor (priming) has not been declared in structure Globals
 Found near
   Lib.with_flag (Globals.priming, ... ...)
   (Term.variant (List.concat (... ... l))) ms
 Uncaught exception: Fail "Static Errors"