Job 681

CakeML:cdee9fccff46dda0f505e20a5bd1fbaf8a3c56c3
  Update CF examples for True, False, Ref [Jan 15 07:31:12]
#591 (better-names)
Merging into:901708feeaa4cd0a8263ec24d39144eeb1f6d15d
  Merge pull request #599 from CakeML/lem-readme [Jan 14 09:15:32]
HOL:9884befd7ef626e7a20cde7aedb6f358330d8ba4
  Merge remote-tracking branch 'origin/pr/637' into develop [Jan 11 23:27:51]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 15 07:31:33 Claimed job
Jan 15 07:31:37 Reusing HOL
Jan 15 07:31:45 Starting developers
Jan 15 07:31:46 Finished developers                                               0s  30MB
Jan 15 07:31:46 Starting developers/bin
Jan 15 07:32:22 Finished developers/bin                                          34s 140MB
Jan 15 07:32:23 Starting semantics/ffi
Jan 15 07:32:32 Finished semantics/ffi                                            8s 225MB
Jan 15 07:32:33 Starting semantics
Jan 15 07:34:02 Finished semantics                                             1m28s   1GB
Jan 15 07:34:03 Starting semantics/proofs
Jan 15 07:37:29 Finished semantics/proofs                                      3m25s   1GB
Jan 15 07:37:30 Starting basis/pure
Jan 15 07:38:23 Finished basis/pure                                              52s 909MB
Jan 15 07:38:24 Starting translator
Jan 15 07:40:11 Finished translator                                            1m45s   1GB
Jan 15 07:40:12 Starting compiler/parsing
Jan 15 07:41:23 Finished compiler/parsing                                      1m10s   2GB
Jan 15 07:41:24 Starting characteristic
Jan 15 07:44:43 Finished characteristic                                        3m18s   1GB
Jan 15 07:44:43 Starting translator/monadic
Jan 15 07:46:12 Finished translator/monadic                                    1m27s   1GB
Jan 15 07:46:13 Starting basis
Jan 15 08:02:53 Finished basis                                                16m39s   3GB
Jan 15 08:02:54 Starting compiler/inference
Jan 15 08:04:37 Finished compiler/inference                                    1m42s   1GB
Jan 15 08:04:38 Starting compiler/backend/reg_alloc
Jan 15 08:05:32 Finished compiler/backend/reg_alloc                              52s   1GB
Jan 15 08:05:32 Starting compiler/backend/gc
Jan 15 08:14:17 Finished compiler/backend/gc                                   8m44s   2GB
Jan 15 08:14:18 Starting compiler/backend
Jan 15 08:14:20 Finished compiler/backend                                         1s  17MB
Jan 15 08:14:21 Starting compiler/encoders/asm
Jan 15 08:14:22 Finished compiler/encoders/asm                                    0s  16MB
Jan 15 08:14:23 Starting compiler/encoders/x64
Jan 15 08:14:48 Finished compiler/encoders/x64                                   24s 823MB
Jan 15 08:14:49 Starting compiler/encoders/arm6
Jan 15 08:15:42 Finished compiler/encoders/arm6                                  52s 699MB
Jan 15 08:15:42 Starting compiler/encoders/arm8
Jan 15 08:15:56 Finished compiler/encoders/arm8                                  12s 815MB
Jan 15 08:15:56 Starting compiler/encoders/mips
Jan 15 08:16:14 Finished compiler/encoders/mips                                  16s   1GB
Jan 15 08:16:14 Starting compiler/encoders/riscv
Jan 15 08:16:29 Finished compiler/encoders/riscv                                 13s 845MB
Jan 15 08:16:30 Starting compiler/encoders/ag32
Jan 15 08:16:46 Finished compiler/encoders/ag32                                  16s 790MB
Jan 15 08:16:47 Starting compiler/backend/x64
Jan 15 08:17:05 Finished compiler/backend/x64                                    17s 817MB
Jan 15 08:17:06 Starting compiler/backend/arm6
Jan 15 08:17:26 Finished compiler/backend/arm6                                   19s   1GB
Jan 15 08:17:27 Starting compiler/backend/arm8
Jan 15 08:17:44 Finished compiler/backend/arm8                                   16s   1GB
Jan 15 08:17:45 Starting compiler/backend/mips
Jan 15 08:18:02 Finished compiler/backend/mips                                   16s 806MB
Jan 15 08:18:03 Starting compiler/backend/riscv
Jan 15 08:18:22 Finished compiler/backend/riscv                                  18s   1GB
Jan 15 08:18:23 Starting compiler/backend/ag32
Jan 15 08:19:41 Finished compiler/backend/ag32                                 1m17s   1GB
Jan 15 08:19:42 Starting compiler/parsing/proofs
Jan 15 08:25:46 Finished compiler/parsing/proofs                               6m03s 958MB
Jan 15 08:25:47 Starting compiler/inference/proofs
Jan 15 08:28:48 Finished compiler/inference/proofs                             3m00s   1GB
Jan 15 08:28:49 Starting compiler/backend/semantics
Jan 15 10:40:09 Resuming compiler/backend/semantics
Jan 15 10:40:55 Finished compiler/backend/semantics                              45s 758MB
Jan 15 10:40:56 Starting compiler/backend/reg_alloc/proofs
Jan 15 10:43:42 Finished compiler/backend/reg_alloc/proofs                     2m44s 727MB
Jan 15 10:43:42 Starting compiler/backend/proofs
Jan 15 11:22:50 Finished compiler/backend/proofs                              39m06s   3GB
Jan 15 11:22:51 Starting compiler/encoders/x64/proofs
Jan 15 11:32:44 Finished compiler/encoders/x64/proofs                          9m52s   5GB
Jan 15 11:32:44 Starting compiler/encoders/arm6/proofs
Jan 15 11:46:55 Finished compiler/encoders/arm6/proofs                        14m10s   3GB
Jan 15 11:46:56 Starting compiler/encoders/arm8/proofs
Jan 15 11:53:02 Finished compiler/encoders/arm8/proofs                         6m05s   1GB
Jan 15 11:53:03 Starting compiler/encoders/mips/proofs
Jan 15 12:03:35 Finished compiler/encoders/mips/proofs                        10m31s   2GB
Jan 15 12:03:36 Starting compiler/encoders/riscv/proofs
Jan 15 12:11:36 Finished compiler/encoders/riscv/proofs                        7m58s   1GB
Jan 15 12:11:37 Starting compiler/encoders/ag32/proofs
Jan 15 12:14:20 Finished compiler/encoders/ag32/proofs                         2m43s 797MB
Jan 15 12:14:21 Starting compiler/backend/x64/proofs
Jan 15 12:14:40 Finished compiler/backend/x64/proofs                             18s   1GB
Jan 15 12:14:41 Starting compiler/backend/arm6/proofs
Jan 15 12:15:02 Finished compiler/backend/arm6/proofs                            20s   1GB
Jan 15 12:15:03 Starting compiler/backend/arm8/proofs
Jan 15 12:15:22 Finished compiler/backend/arm8/proofs                            18s   1GB
Jan 15 12:15:23 Starting compiler/backend/mips/proofs
Jan 15 12:15:43 Finished compiler/backend/mips/proofs                            19s   1GB
Jan 15 12:15:44 Starting compiler/backend/riscv/proofs
Jan 15 12:16:03 Finished compiler/backend/riscv/proofs                           18s   1GB
Jan 15 12:16:04 Starting compiler/backend/ag32/proofs
Jan 15 12:25:26 Finished compiler/backend/ag32/proofs                          9m21s   2GB
Jan 15 12:25:27 Starting compiler/proofs
Jan 15 12:26:48 Finished compiler/proofs                                       1m20s   3GB
Jan 15 12:26:49 Starting candle/set-theory
Jan 15 12:27:15 Finished candle/set-theory                                       25s 723MB
Jan 15 12:27:16 Starting candle/syntax-lib
Jan 15 12:27:27 Finished candle/syntax-lib                                        9s 640MB
Jan 15 12:27:27 Starting candle/standard/syntax
Jan 15 12:29:15 Finished candle/standard/syntax                                1m46s   1GB
Jan 15 12:29:15 Starting candle/standard/semantics
Jan 15 12:30:54 Finished candle/standard/semantics                             1m37s   1GB
Jan 15 12:30:55 Starting candle/standard/monadic
Jan 15 12:32:37 Finished candle/standard/monadic                               1m41s   1GB
Jan 15 12:32:37 Starting candle/standard/ml_kernel
Jan 15 12:36:26 Finished candle/standard/ml_kernel                             3m47s   3GB
Jan 15 12:36:27 Starting candle/standard/opentheory
Jan 15 12:45:05 Finished candle/standard/opentheory                            8m36s   3GB
Jan 15 12:45:05 Starting candle/standard/opentheory/compilation
Jan 15 13:14:30 Finished candle/standard/opentheory/compilation               29m23s  21GB
Jan 15 13:14:31 Starting candle/standard/opentheory/compilation/proofs
Jan 15 13:15:12 Finished candle/standard/opentheory/compilation/proofs           40s   5GB
Jan 15 13:15:12 Starting characteristic/examples
Jan 15 13:16:37 Finished characteristic/examples                               1m23s   2GB
Jan 15 13:16:37 Starting tutorial/solutions
Jan 15 13:29:34 Finished tutorial/solutions                                   12m55s   6GB
Jan 15 13:29:34 Starting translator/monadic/examples
Jan 15 13:31:42 Finished translator/monadic/examples                           2m07s   2GB
Jan 15 13:31:43 Starting examples
Jan 15 13:32:53 FAILED: examples
]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-681/basis]0;Holmake: ~/regression/cakeml-681/basis/pure]0;Holmake: ~/regression/cakeml-681/misc]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-681/misc]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-681/misc]0;Holmake: ~/regression/cakeml-681/developers]0;Holmake: ~/regression/cakeml-681/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-681/misc]0;Holmake: ~/regression/cakeml-681/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-681/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-681/misc]0;Holmake: ~/regression/cakeml-681/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-681/basis/pure]0;Holmake: ~/regression/cakeml-681/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-681/basis]0;Holmake: ~/regression/cakeml-681/characteristic]0;Holmake: ~/regression/cakeml-681/compiler/parsing]0;Holmake: ~/regression/cakeml-681/semantics]0;Holmake: ~/regression/cakeml-681/semantics/ffi]0;Holmake: ~/regression/cakeml-681/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-681/semantics]0;Holmake: ~/regression/cakeml-681/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-681/compiler/parsing]0;Holmake: ~/regression/cakeml-681/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-681/characteristic]0;Holmake: ~/regression/cakeml-681/semantics/proofs]0;Holmake: ~/regression/cakeml-681/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-681/characteristic]0;Holmake: ~/regression/cakeml-681/translator]0;Holmake: ~/regression/cakeml-681/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-681/characteristic]0;Holmake: ~/regression/cakeml-681/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-681/basis]0;Holmake: ~/regression/cakeml-681/translator/monadic]0;Holmake: ~/regression/cakeml-681/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-681/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-681/translator/monadic]0;Holmake: ~/regression/cakeml-681/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-681/basis]0;Holmake: ~/regression/cakeml-681/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on doubleProgTheory
lcsTheory                                                                                                  OK
Starting work on diffTheory
diffTheory                                                                                                 OK
Starting work on diffProgTheory
doubleProgTheory                                                                                  FAILED! <1>
 inp inp_v inp_ref ffi_p.
     NUM inp inp_v 
     app ffi_p double_ref_v [inp_ref] (inp_ref ~~> inp_v)
       (POSTv ret_ref.
            (SEP_EXISTS inp0_v. inp_ref ~~> inp0_v * &NUM 0 inp0_v) *
            SEP_EXISTS ret_v. ret_ref ~~> ret_v * &NUM (2 * inp) ret_v)
 
 failed.
 Failed to prove theorem double_ref_spec.
 Uncaught exception: HOL_ERR {message = "REWR_CONV: lhs of thm doesn't match term (THEN1 on line 131) (THEN1 on line 151) (THEN1 on line 153) (THEN1 on line 155) (THEN1 on line 157) (THEN1 on line 159) (THEN1 on line 162) (THEN1 on line 164) (THEN1 on line 166) (THEN1 on line 168)", origin_function = "RATOR_CONV", origin_structure = "Conv"}
quicksortProgTheory                                                                                  M-KILLED
catProgTheory                                                                                        M-KILLED
diffProgTheory                                                                                       M-KILLED