Job 432

CakeML:4adad68356d8434850ba430123340df226d03fab
  Fix another ERR [Aug 18 20:08:16]
HOL:f59f1264f77465a8321b6b7c9115f007db7d2bc1
  Fix a missing ERR definition [Aug 18 19:10:45]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Aug 18 22:57:48 Claimed job
Aug 18 22:57:59 Building HOL
Aug 18 23:10:22 Starting developers/bin
Aug 18 23:10:31 Finished developers/bin                                           7s 142MB
Aug 18 23:10:33 Starting semantics/ffi
Aug 18 23:11:34 Finished semantics/ffi                                           58s 584MB
Aug 18 23:11:36 Starting semantics
Aug 18 23:13:55 Finished semantics                                             2m17s 853MB
Aug 18 23:13:57 Starting semantics/proofs
Aug 18 23:19:10 Finished semantics/proofs                                      5m11s   1GB
Aug 18 23:19:12 Starting basis/pure
Aug 18 23:25:05 Finished basis/pure                                            5m50s 673MB
Aug 18 23:25:07 Starting translator
Aug 18 23:27:51 Finished translator                                            2m42s   1GB
Aug 18 23:27:53 Starting compiler/parsing
Aug 18 23:30:14 Finished compiler/parsing                                      2m19s   3GB
Aug 18 23:30:16 Starting characteristic
Aug 18 23:34:37 Finished characteristic                                        4m18s   1GB
Aug 18 23:34:39 Starting translator/monadic
Aug 18 23:37:17 Finished translator/monadic                                    2m36s   1GB
Aug 18 23:37:19 Starting basis
Aug 19 00:03:52 Finished basis                                                26m31s   3GB
Aug 19 00:03:54 Starting compiler/inference
Aug 19 00:06:42 Finished compiler/inference                                    2m45s   1GB
Aug 19 00:06:44 Starting compiler/backend/reg_alloc
Aug 19 00:07:40 Finished compiler/backend/reg_alloc                              54s   1GB
Aug 19 00:07:42 Starting compiler/backend/gc
Aug 19 00:22:30 Finished compiler/backend/gc                                  14m45s   3GB
Aug 19 00:22:32 Starting compiler/backend
Aug 19 00:22:37 Finished compiler/backend                                         2s  23MB
Aug 19 00:22:39 Starting compiler/encoders/asm
Aug 19 00:22:42 Finished compiler/encoders/asm                                    0s  14MB
Aug 19 00:22:44 Starting compiler/encoders/x64
Aug 19 00:24:12 Finished compiler/encoders/x64                                 1m25s 521MB
Aug 19 00:24:14 Starting compiler/encoders/arm6
Aug 19 00:27:11 Finished compiler/encoders/arm6                                2m54s   1GB
Aug 19 00:27:13 Starting compiler/encoders/arm8
Aug 19 00:28:00 Finished compiler/encoders/arm8                                  44s 396MB
Aug 19 00:28:02 Starting compiler/encoders/mips
Aug 19 00:29:36 Finished compiler/encoders/mips                                1m32s   1GB
Aug 19 00:29:38 Starting compiler/encoders/riscv
Aug 19 00:31:14 Finished compiler/encoders/riscv                               1m34s 558MB
Aug 19 00:31:16 Starting compiler/backend/x64
Aug 19 00:31:47 Finished compiler/backend/x64                                    29s   1GB
Aug 19 00:31:49 Starting compiler/backend/arm6
Aug 19 00:32:24 Finished compiler/backend/arm6                                   32s   1GB
Aug 19 00:32:26 Starting compiler/backend/arm8
Aug 19 00:32:59 Finished compiler/backend/arm8                                   31s   1GB
Aug 19 00:33:01 Starting compiler/backend/mips
Aug 19 00:33:32 Finished compiler/backend/mips                                   28s 854MB
Aug 19 00:33:34 Starting compiler/backend/riscv
Aug 19 00:34:06 Finished compiler/backend/riscv                                  30s   1GB
Aug 19 00:34:08 Starting compiler/parsing/proofs
Aug 19 00:38:17 Finished compiler/parsing/proofs                               4m07s 792MB
Aug 19 00:38:19 Starting compiler/inference/proofs
Aug 19 00:43:06 Finished compiler/inference/proofs                             4m45s   1GB
Aug 19 00:43:08 Starting compiler/backend/semantics
Aug 19 00:57:24 Finished compiler/backend/semantics                           14m14s   2GB
Aug 19 00:57:26 Starting compiler/backend/reg_alloc/proofs
Aug 19 00:58:50 Finished compiler/backend/reg_alloc/proofs                     1m21s 404MB
Aug 19 00:58:52 Starting compiler/backend/proofs
Aug 19 01:53:25 Finished compiler/backend/proofs                              54m30s   3GB
Aug 19 01:53:27 Starting compiler/encoders/x64/proofs
Aug 19 02:04:58 Finished compiler/encoders/x64/proofs                         11m28s   1GB
Aug 19 02:05:00 Starting compiler/encoders/arm6/proofs
Aug 19 02:07:32 FAILED: compiler/encoders/arm6/proofs
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/prog]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/prog[0m
Starting work on arm-step-heap
arm-step-heap                                                                OK
Starting work on arm_progTheory
arm_progTheory                                                               OK
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../asm]0;Holmake: ../../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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: ..[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6/proofs[0m
Starting work on arm6_targetProofTheory
arm6_targetProofTheory                                              FAILED! <1>
 /scratch/cakeml/regression/cakeml-432/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml:802: error: Value or constructor (ERR) has not been declared
 Found near raise ERR "number_of_instructions" ""
 error in quse /scratch/cakeml/regression/cakeml-432/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml : Fail "Static Errors"
 error in load arm6_targetProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"