Job 517

CakeML:761b55f0e38306602e2f95abef7f8a49fc0bb25b
  Add clos_fvs and clos_labels to backendCompute [Oct 07 10:54:39]
#533 (remove-cheats)
Merging into:675c1da06454efcef70f62574de96a524820287f
  Merge pull request #532 from CakeML/trans-msg [Oct 03 07:58:05]
HOL:c99b7420019e4deae768b219d3c8e926b43af0b7
  Make buildheap preserve temporary files when --dbg flag is set [Oct 05 01:50:41]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Oct 07 13:44:12 Claimed job
Oct 07 13:46:07 Building HOL
Oct 07 13:54:00 Starting developers/bin
Oct 07 13:54:33 Finished developers/bin                                          32s 136MB
Oct 07 13:54:34 Starting semantics/ffi
Oct 07 13:55:11 Finished semantics/ffi                                           35s 398MB
Oct 07 13:55:11 Starting semantics
Oct 07 13:56:39 Finished semantics                                             1m26s   1GB
Oct 07 13:56:39 Starting semantics/proofs
Oct 07 13:59:27 Finished semantics/proofs                                      2m46s   1GB
Oct 07 13:59:27 Starting basis/pure
Oct 07 14:03:05 Finished basis/pure                                            3m36s 613MB
Oct 07 14:03:06 Starting translator
Oct 07 14:06:11 Finished translator                                            3m04s   1GB
Oct 07 14:06:12 Starting compiler/parsing
Oct 07 14:07:26 Finished compiler/parsing                                      1m13s   1GB
Oct 07 14:07:26 Starting characteristic
Oct 07 14:09:50 Finished characteristic                                        2m22s   1GB
Oct 07 14:09:51 Starting translator/monadic
Oct 07 14:11:16 Finished translator/monadic                                    1m24s   1GB
Oct 07 14:11:17 Starting basis
Oct 07 14:27:52 Finished basis                                                16m33s   2GB
Oct 07 14:27:53 Starting compiler/inference
Oct 07 14:29:31 Finished compiler/inference                                    1m37s   1GB
Oct 07 14:29:32 Starting compiler/backend/reg_alloc
Oct 07 14:30:18 Finished compiler/backend/reg_alloc                              45s 952MB
Oct 07 14:30:19 Starting compiler/backend/gc
Oct 07 14:39:05 Finished compiler/backend/gc                                   8m45s   3GB
Oct 07 14:39:06 Starting compiler/backend
Oct 07 14:39:10 Finished compiler/backend                                         2s  18MB
Oct 07 14:39:11 Starting compiler/encoders/asm
Oct 07 14:39:12 Finished compiler/encoders/asm                                    0s  21MB
Oct 07 14:39:13 Starting compiler/encoders/x64
Oct 07 14:40:02 Finished compiler/encoders/x64                                   47s 596MB
Oct 07 14:40:03 Starting compiler/encoders/arm6
Oct 07 14:41:46 Finished compiler/encoders/arm6                                1m42s   1GB
Oct 07 14:41:47 Starting compiler/encoders/arm8
Oct 07 14:42:11 Finished compiler/encoders/arm8                                  23s 414MB
Oct 07 14:42:12 Starting compiler/encoders/mips
Oct 07 14:43:07 Finished compiler/encoders/mips                                  54s 822MB
Oct 07 14:43:08 Starting compiler/encoders/riscv
Oct 07 14:44:07 Finished compiler/encoders/riscv                                 58s 651MB
Oct 07 14:44:08 Starting compiler/backend/x64
Oct 07 14:44:26 Finished compiler/backend/x64                                    16s 844MB
Oct 07 14:44:27 Starting compiler/backend/arm6
Oct 07 14:44:46 Finished compiler/backend/arm6                                   18s 984MB
Oct 07 14:44:47 Starting compiler/backend/arm8
Oct 07 14:45:06 Finished compiler/backend/arm8                                   18s   1GB
Oct 07 14:45:07 Starting compiler/backend/mips
Oct 07 14:45:26 Finished compiler/backend/mips                                   18s 948MB
Oct 07 14:45:27 Starting compiler/backend/riscv
Oct 07 14:45:45 Finished compiler/backend/riscv                                  17s   1GB
Oct 07 14:45:46 Starting compiler/parsing/proofs
Oct 07 14:51:55 Finished compiler/parsing/proofs                               6m08s 852MB
Oct 07 14:51:56 Starting compiler/inference/proofs
Oct 07 14:54:56 Finished compiler/inference/proofs                             2m59s   1GB
Oct 07 14:54:57 Starting compiler/backend/semantics
Oct 07 15:04:55 Finished compiler/backend/semantics                            9m58s   2GB
Oct 07 15:04:56 Starting compiler/backend/reg_alloc/proofs
Oct 07 15:12:17 Finished compiler/backend/reg_alloc/proofs                     7m20s 541MB
Oct 07 15:12:18 Starting compiler/backend/proofs
Oct 07 15:59:34 Finished compiler/backend/proofs                              47m15s   3GB
Oct 07 15:59:35 Starting compiler/encoders/x64/proofs
Oct 07 16:07:09 Finished compiler/encoders/x64/proofs                          7m33s   4GB
Oct 07 16:07:10 Starting compiler/encoders/arm6/proofs
Oct 07 16:14:49 Finished compiler/encoders/arm6/proofs                         7m38s   3GB
Oct 07 16:14:50 Starting compiler/encoders/arm8/proofs
Oct 07 16:20:16 Finished compiler/encoders/arm8/proofs                         5m25s 951MB
Oct 07 16:20:17 Starting compiler/encoders/mips/proofs
Oct 07 16:27:46 Finished compiler/encoders/mips/proofs                         7m28s   1GB
Oct 07 16:27:47 Starting compiler/encoders/riscv/proofs
Oct 07 16:35:43 Finished compiler/encoders/riscv/proofs                        7m55s 779MB
Oct 07 16:35:44 Starting compiler/backend/x64/proofs
Oct 07 16:36:05 Finished compiler/backend/x64/proofs                             19s   1GB
Oct 07 16:36:05 Starting compiler/backend/arm6/proofs
Oct 07 16:36:27 Finished compiler/backend/arm6/proofs                            21s 977MB
Oct 07 16:36:28 Starting compiler/backend/arm8/proofs
Oct 07 16:36:48 Finished compiler/backend/arm8/proofs                            18s 990MB
Oct 07 16:36:48 Starting compiler/backend/mips/proofs
Oct 07 16:37:10 Finished compiler/backend/mips/proofs                            20s   1GB
Oct 07 16:37:10 Starting compiler/backend/riscv/proofs
Oct 07 16:37:32 Finished compiler/backend/riscv/proofs                           20s   1GB
Oct 07 16:37:33 Starting compiler/proofs
Oct 07 16:38:50 Finished compiler/proofs                                       1m16s   2GB
Oct 07 16:38:51 Starting candle/set-theory
Oct 07 16:39:20 Finished candle/set-theory                                       28s 627MB
Oct 07 16:39:21 Starting candle/syntax-lib
Oct 07 16:39:30 Finished candle/syntax-lib                                        8s 574MB
Oct 07 16:39:31 Starting candle/standard/syntax
Oct 07 16:41:04 Finished candle/standard/syntax                                1m31s 992MB
Oct 07 16:41:05 Starting candle/standard/semantics
Oct 07 16:42:24 Finished candle/standard/semantics                             1m18s   1GB
Oct 07 16:42:25 Starting candle/standard/monadic
Oct 07 16:43:58 Finished candle/standard/monadic                               1m32s 821MB
Oct 07 16:43:59 Starting candle/standard/ml_kernel
Oct 07 17:00:11 Finished candle/standard/ml_kernel                            16m11s   7GB
Oct 07 17:00:12 Starting candle/standard/opentheory
Oct 07 17:09:22 Finished candle/standard/opentheory                            9m09s   7GB
Oct 07 17:09:23 Starting candle/standard/opentheory/compilation
Oct 07 17:46:45 Finished candle/standard/opentheory/compilation               37m21s  16GB
Oct 07 17:46:46 Starting characteristic/examples
Oct 07 17:48:20 Finished characteristic/examples                               1m33s   2GB
Oct 07 17:48:21 Starting tutorial/solutions
Oct 07 18:02:07 Finished tutorial/solutions                                   13m44s   5GB
Oct 07 18:02:07 Starting translator/monadic/examples
Oct 07 18:03:51 Finished translator/monadic/examples                           1m43s   2GB
Oct 07 18:03:52 Starting examples
Oct 07 18:05:02 FAILED: examples
]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ../basis]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[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: ../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: ../basis/pure]0;Holmake: ../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../basis]0;Holmake: ../characteristic]0;Holmake: ../compiler/parsing]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: ../compiler/parsing]0;Holmake: ../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../characteristic]0;Holmake: ../translator]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semantics[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
]0;Holmake: ../translator]0;Holmake: ../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../characteristic]0;Holmake: ../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../basis]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../basis]0;Holmake: ../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on heap
Starting work on README.md
README.md                                                                                                                                                                       OK
heap                                                                                                                                                                            OK
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on echoProgTheory
Starting work on grepProgTheory
lcsTheory                                                                                                                                                                       OK
Starting work on diffTheory
echoProgTheory                                                                                                                                                                  OK
Starting work on helloErrProgTheory
diffTheory                                                                                                                                                             FAILED! <1>
 Proof of 
 
 l' l.
     headers_within (n + LENGTH l') m p1  m  n + LENGTH l' 
     patch_alg_offs n p1 (l'  l) =
     OPTION_MAP ($++ l') (patch_alg_offs (n + LENGTH l') p1 l)
 
 failed.
 Failed to prove theorem headers_within_append1.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 1002", origin_function = "by", origin_structure = "BasicProvers"}
catProgTheory                                                                                                                                                             M-KILLED
grepProgTheory                                                                                                                                                            M-KILLED
helloErrProgTheory                                                                                                                                                        M-KILLED