Job 431

CakeML:42c919452dd418e7f3f60eec74e38fb6a9cc9d41
  Rename `flag` configuration type to `flagConf` [Aug 17 12:24:35]
#511 (argparse)
Merging into:4adad68356d8434850ba430123340df226d03fab
  Fix another ERR [Aug 18 20:08:16]
HOL:f59f1264f77465a8321b6b7c9115f007db7d2bc1
  Fix a missing ERR definition [Aug 18 19:10:45]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Aug 18 21:32:42 Claimed job
Aug 18 21:32:52 Building HOL
Aug 18 21:45:10 Starting developers/bin
Aug 18 21:45:20 Finished developers/bin                                           8s 143MB
Aug 18 21:45:22 Starting semantics/ffi
Aug 18 21:46:23 Finished semantics/ffi                                           59s 539MB
Aug 18 21:46:25 Starting semantics
Aug 18 21:48:44 Finished semantics                                             2m17s 925MB
Aug 18 21:48:46 Starting semantics/proofs
Aug 18 21:54:02 Finished semantics/proofs                                      5m13s   1GB
Aug 18 21:54:03 Starting basis/pure
Aug 18 21:59:52 Finished basis/pure                                            5m45s 699MB
Aug 18 21:59:54 Starting translator
Aug 18 22:02:42 Finished translator                                            2m45s 926MB
Aug 18 22:02:44 Starting compiler/parsing
Aug 18 22:05:03 Finished compiler/parsing                                      2m17s   1GB
Aug 18 22:05:05 Starting characteristic
Aug 18 22:09:40 Finished characteristic                                        4m33s   1GB
Aug 18 22:09:42 Starting translator/monadic
Aug 18 22:12:23 Finished translator/monadic                                    2m38s   1GB
Aug 18 22:12:25 Starting basis
Aug 18 22:42:55 Finished basis                                                30m27s   4GB
Aug 18 22:42:57 Starting compiler/inference
Aug 18 22:45:44 Finished compiler/inference                                    2m45s   1GB
Aug 18 22:45:46 Starting compiler/backend/reg_alloc
Aug 18 22:46:41 Finished compiler/backend/reg_alloc                              53s   1GB
Aug 18 22:46:43 Starting compiler/backend/gc
Aug 18 23:01:35 Finished compiler/backend/gc                                  14m49s   3GB
Aug 18 23:01:37 Starting compiler/backend
Aug 18 23:01:42 Finished compiler/backend                                         2s  20MB
Aug 18 23:01:43 Starting compiler/encoders/asm
Aug 18 23:01:46 Finished compiler/encoders/asm                                    0s  11MB
Aug 18 23:01:48 Starting compiler/encoders/x64
Aug 18 23:03:18 Finished compiler/encoders/x64                                 1m27s 557MB
Aug 18 23:03:19 Starting compiler/encoders/arm6
Aug 18 23:06:23 Finished compiler/encoders/arm6                                3m01s   1GB
Aug 18 23:06:24 Starting compiler/encoders/arm8
Aug 18 23:07:10 Finished compiler/encoders/arm8                                  43s 372MB
Aug 18 23:07:12 Starting compiler/encoders/mips
Aug 18 23:08:47 Finished compiler/encoders/mips                                1m33s 733MB
Aug 18 23:08:49 Starting compiler/encoders/riscv
Aug 18 23:10:24 Finished compiler/encoders/riscv                               1m33s 500MB
Aug 18 23:10:26 Starting compiler/backend/x64
Aug 18 23:10:57 Finished compiler/backend/x64                                    29s   1GB
Aug 18 23:10:59 Starting compiler/backend/arm6
Aug 18 23:11:35 Finished compiler/backend/arm6                                   33s   1GB
Aug 18 23:11:37 Starting compiler/backend/arm8
Aug 18 23:12:11 Finished compiler/backend/arm8                                   31s   1GB
Aug 18 23:12:12 Starting compiler/backend/mips
Aug 18 23:12:46 Finished compiler/backend/mips                                   31s   1GB
Aug 18 23:12:48 Starting compiler/backend/riscv
Aug 18 23:13:20 Finished compiler/backend/riscv                                  30s   1GB
Aug 18 23:13:22 Starting compiler/parsing/proofs
Aug 18 23:17:27 Finished compiler/parsing/proofs                               4m03s 865MB
Aug 18 23:17:29 Starting compiler/inference/proofs
Aug 18 23:22:15 Finished compiler/inference/proofs                             4m44s   1GB
Aug 18 23:22:17 Starting compiler/backend/semantics
Aug 18 23:36:39 Finished compiler/backend/semantics                           14m20s   2GB
Aug 18 23:36:41 Starting compiler/backend/reg_alloc/proofs
Aug 18 23:38:06 Finished compiler/backend/reg_alloc/proofs                     1m22s 627MB
Aug 18 23:38:08 Starting compiler/backend/proofs
Aug 19 00:32:34 Finished compiler/backend/proofs                              54m23s   2GB
Aug 19 00:32:36 Starting compiler/encoders/x64/proofs
Aug 19 00:44:23 Finished compiler/encoders/x64/proofs                         11m45s   1GB
Aug 19 00:44:25 Starting compiler/encoders/arm6/proofs
Aug 19 00:46:56 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>
 error in quse /scratch/cakeml/regression/cakeml-431/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml : Fail "Static Errors"
 error in load arm6_targetProofScript : Fail "Static Errors"
 /scratch/cakeml/regression/cakeml-431/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml:802: error: Value or constructor (ERR) has not been declared
 Found near raise ERR "number_of_instructions" ""
 Uncaught exception: Fail "Static Errors"