Job 1898

CakeML:ba560f509fe5ce7923a0ec94fe3cf0826ca23fcc
  Change how the caml parser deals with guards [May 12 09:44:15]
#885 (caml-pattern-guards)
Merging into:b22ea8e8ba7e6a7474e33f8273f526a9360cc788
  Merge pull request #883 from CakeML/pan-lemma [May 09 03:44:38]
HOL:db0c48a4df81300b8f4ab65af329cee860f6d921
  Fix a l3_equivalence_misc proof [May 10 01:22:03]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

May 14 01:43:40 Claimed job
May 14 01:43:43 Reusing HOL
May 14 01:43:57 Starting developers
May 14 01:44:01 Finished developers                                               4s 112MB
May 14 01:44:01 Starting developers/bin
May 14 01:44:08 Finished developers/bin                                           6s   1GB
May 14 01:44:08 Starting semantics/ffi
May 14 01:44:18 Finished semantics/ffi                                            9s 216MB
May 14 01:44:18 Starting semantics
May 14 01:46:16 Finished semantics                                             1m57s   1GB
May 14 01:46:16 Starting semantics/proofs
May 14 01:50:18 Finished semantics/proofs                                      4m01s   2GB
May 14 01:50:18 Starting semantics/alt_semantics
May 14 01:50:41 Finished semantics/alt_semantics                                 23s 504MB
May 14 01:50:41 Starting semantics/alt_semantics/proofs
May 14 01:53:41 Finished semantics/alt_semantics/proofs                        2m59s   1GB
May 14 01:53:41 Starting basis/pure
May 14 01:54:46 Finished basis/pure                                            1m05s   1GB
May 14 01:54:46 Starting translator
May 14 01:57:46 Finished translator                                            2m59s   2GB
May 14 01:57:46 Starting compiler/parsing
May 14 01:59:01 Finished compiler/parsing                                      1m15s   2GB
May 14 01:59:01 Starting characteristic
May 14 02:05:27 Finished characteristic                                        6m25s   2GB
May 14 02:05:27 Starting translator/monadic
May 14 02:07:25 Finished translator/monadic                                    1m57s   1GB
May 14 02:07:25 Starting basis
May 14 02:54:18 Finished basis                                                46m49s  18GB
May 14 02:54:18 Starting compiler/inference
May 14 02:55:40 Finished compiler/inference                                    1m21s   1GB
May 14 02:55:41 Starting compiler/backend/reg_alloc
May 14 02:57:26 Finished compiler/backend/reg_alloc                            1m44s   1GB
May 14 02:57:26 Starting compiler/backend/gc
May 14 03:01:47 Finished compiler/backend/gc                                   4m20s   1GB
May 14 03:01:48 Starting compiler/backend
May 14 03:07:29 Finished compiler/backend                                      5m41s   2GB
May 14 03:07:30 Starting compiler/encoders/asm
May 14 03:08:00 Finished compiler/encoders/asm                                   30s 723MB
May 14 03:08:00 Starting compiler/encoders/x64
May 14 03:08:30 Finished compiler/encoders/x64                                   30s   1GB
May 14 03:08:31 Starting compiler/encoders/arm7
May 14 03:09:24 Finished compiler/encoders/arm7                                  52s 758MB
May 14 03:09:24 Starting compiler/encoders/arm8
May 14 03:09:42 Finished compiler/encoders/arm8                                  16s 782MB
May 14 03:09:42 Starting compiler/encoders/arm8_asl
May 14 03:12:14 Finished compiler/encoders/arm8_asl                            2m31s   1GB
May 14 03:12:14 Starting compiler/encoders/mips
May 14 03:12:36 Finished compiler/encoders/mips                                  21s   1GB
May 14 03:12:37 Starting compiler/encoders/riscv
May 14 03:12:56 Finished compiler/encoders/riscv                                 18s 905MB
May 14 03:12:56 Starting compiler/encoders/ag32
May 14 03:13:17 Finished compiler/encoders/ag32                                  21s 871MB
May 14 03:13:17 Starting compiler/backend/x64
May 14 03:13:40 Finished compiler/backend/x64                                    21s   1GB
May 14 03:13:40 Starting compiler/backend/arm7
May 14 03:14:03 Finished compiler/backend/arm7                                   22s   1GB
May 14 03:14:03 Starting compiler/backend/arm8
May 14 03:14:26 Finished compiler/backend/arm8                                   22s   1GB
May 14 03:14:26 Starting compiler/backend/mips
May 14 03:14:49 Finished compiler/backend/mips                                   23s   1GB
May 14 03:14:49 Starting compiler/backend/riscv
May 14 03:15:12 Finished compiler/backend/riscv                                  22s   1GB
May 14 03:15:12 Starting compiler/backend/ag32
May 14 03:16:40 Finished compiler/backend/ag32                                 1m27s   1GB
May 14 03:16:40 Starting compiler/parsing/proofs
May 14 03:20:23 Finished compiler/parsing/proofs                               3m43s   1GB
May 14 03:20:23 Starting compiler/inference/proofs
May 14 03:22:57 Finished compiler/inference/proofs                             2m32s   1GB
May 14 03:22:57 Starting compiler/backend/semantics
May 14 03:52:16 Finished compiler/backend/semantics                           29m19s   2GB
May 14 03:52:16 Starting compiler/backend/reg_alloc/proofs
May 14 03:55:46 Finished compiler/backend/reg_alloc/proofs                     3m28s 986MB
May 14 03:55:47 Starting compiler/backend/proofs
May 14 04:46:41 Finished compiler/backend/proofs                              50m54s  17GB
May 14 04:46:41 Starting compiler/backend/serialiser
May 14 04:48:20 Finished compiler/backend/serialiser                           1m38s   1GB
May 14 04:48:20 Starting compiler/encoders/x64/proofs
May 14 04:57:59 Finished compiler/encoders/x64/proofs                          9m38s   3GB
May 14 04:57:59 Starting compiler/encoders/arm7/proofs
May 14 05:11:08 Finished compiler/encoders/arm7/proofs                        13m08s   4GB
May 14 05:11:09 Starting compiler/encoders/arm8/proofs
May 14 05:17:55 Finished compiler/encoders/arm8/proofs                         6m46s   1GB
May 14 05:17:55 Starting compiler/encoders/arm8_asl/proofs
May 14 05:32:57 Finished compiler/encoders/arm8_asl/proofs                    15m01s   2GB
May 14 05:32:57 Starting compiler/encoders/mips/proofs
May 14 05:43:03 Finished compiler/encoders/mips/proofs                        10m06s   2GB
May 14 05:43:03 Starting compiler/encoders/riscv/proofs
May 14 05:52:02 Finished compiler/encoders/riscv/proofs                        8m58s   1GB
May 14 05:52:02 Starting compiler/encoders/ag32/proofs
May 14 05:54:36 Finished compiler/encoders/ag32/proofs                         2m34s 689MB
May 14 05:54:36 Starting compiler/backend/x64/proofs
May 14 05:55:04 Finished compiler/backend/x64/proofs                             27s   1GB
May 14 05:55:04 Starting compiler/backend/arm7/proofs
May 14 05:55:32 Finished compiler/backend/arm7/proofs                            28s   1GB
May 14 05:55:33 Starting compiler/backend/arm8/proofs
May 14 05:56:01 Finished compiler/backend/arm8/proofs                            27s   1GB
May 14 05:56:01 Starting compiler/backend/arm8_asl
May 14 05:56:24 Finished compiler/backend/arm8_asl                               23s   1GB
May 14 05:56:27 Starting compiler/backend/mips/proofs
May 14 05:56:55 Finished compiler/backend/mips/proofs                            27s   1GB
May 14 05:56:56 Starting compiler/backend/riscv/proofs
May 14 05:57:24 Finished compiler/backend/riscv/proofs                           28s   1GB
May 14 05:57:24 Starting compiler/backend/ag32/proofs
May 14 06:10:27 Finished compiler/backend/ag32/proofs                         13m02s   2GB
May 14 06:10:27 Starting compiler/proofs
May 14 06:12:34 Finished compiler/proofs                                       2m06s   3GB
May 14 06:12:34 Starting candle/set-theory
May 14 06:13:08 Finished candle/set-theory                                       34s   1GB
May 14 06:13:08 Starting candle/syntax-lib
May 14 06:13:22 Finished candle/syntax-lib                                       13s 615MB
May 14 06:13:22 Starting candle/standard/syntax
May 14 06:15:24 Finished candle/standard/syntax                                2m02s   1GB
May 14 06:15:24 Starting candle/standard/semantics
May 14 06:17:16 Finished candle/standard/semantics                             1m51s   1GB
May 14 06:17:16 Starting candle/standard/monadic
May 14 06:19:08 Finished candle/standard/monadic                               1m52s   1GB
May 14 06:19:08 Starting candle/standard/ml_kernel
May 14 06:25:13 Finished candle/standard/ml_kernel                             6m04s   3GB
May 14 06:25:13 Starting candle/overloading/syntax
May 14 06:28:26 Finished candle/overloading/syntax                             3m12s   1GB
May 14 06:28:26 Starting candle/overloading/semantics
May 14 06:40:13 Finished candle/overloading/semantics                         11m46s   2GB
May 14 06:40:13 Starting candle/overloading/monadic
May 14 06:42:43 Finished candle/overloading/monadic                            2m29s   1GB
May 14 06:42:43 Starting candle/overloading/ml_kernel
May 14 06:49:51 Finished candle/overloading/ml_kernel                          7m07s   3GB
May 14 06:49:51 Starting candle/overloading/ml_checker
May 14 06:52:19 Finished candle/overloading/ml_checker                         2m27s   3GB
May 14 06:52:19 Starting candle/prover
May 14 07:00:25 Finished candle/prover                                         8m04s   3GB
May 14 07:00:25 Starting pancake
May 14 07:04:06 Finished pancake                                               3m41s   3GB
May 14 07:04:06 Starting pancake/ffi
May 14 07:04:07 Finished pancake/ffi                                              0s  35MB
May 14 07:04:07 Starting pancake/semantics
May 14 07:06:36 Finished pancake/semantics                                     2m28s   1GB
May 14 07:06:36 Starting pancake/proofs
May 14 07:18:41 Finished pancake/proofs                                       12m04s   6GB
May 14 07:18:41 Starting characteristic/examples
May 14 07:20:02 Finished characteristic/examples                               1m21s   3GB
May 14 07:20:02 Starting tutorial/solutions
May 14 07:36:55 Finished tutorial/solutions                                   16m52s   9GB
May 14 07:36:55 Starting translator/monadic/examples
May 14 07:40:47 Finished translator/monadic/examples                           3m51s   3GB
May 14 07:40:47 Starting examples
May 14 07:50:05 Finished examples                                              9m18s   6GB
May 14 07:50:05 Starting examples/compilation/x64
May 14 10:22:17 Finished examples/compilation/x64                           2h32m08s  20GB
May 14 10:22:17 Starting examples/compilation/x64/proofs
May 14 10:24:49 Finished examples/compilation/x64/proofs                       2m32s   3GB
May 14 10:24:49 Starting examples/compilation/ag32
May 14 10:59:32 Finished examples/compilation/ag32                            34m42s   9GB
May 14 10:59:32 Starting examples/compilation/ag32/proofs
May 14 11:00:28 Finished examples/compilation/ag32/proofs                        55s   3GB
May 14 11:00:28 Starting examples/cost
May 14 11:56:06 Finished examples/cost                                        55m36s   9GB
May 14 11:56:06 Starting examples/lpr_checker
May 14 11:57:11 Finished examples/lpr_checker                                  1m05s 984MB
May 14 11:57:11 Starting examples/lpr_checker/array
May 14 12:25:20 Finished examples/lpr_checker/array                           28m08s   7GB
May 14 12:25:20 Starting examples/lpr_checker/array/compilation
May 14 13:48:23 Finished examples/lpr_checker/array/compilation             1h23m01s  31GB
May 14 13:48:23 Starting examples/lpr_checker/array/compilation/proofs
May 14 13:49:47 Finished examples/lpr_checker/array/compilation/proofs         1m23s   6GB
May 14 13:49:47 Starting examples/opentheory
May 14 13:59:46 Finished examples/opentheory                                   9m58s   4GB
May 14 13:59:46 Starting examples/opentheory
May 14 13:59:47 Finished examples/opentheory                                      1s 138MB
May 14 13:59:47 Starting examples/opentheory/compilation
May 14 14:40:36 Finished examples/opentheory/compilation                      40m48s  27GB
May 14 14:40:36 Starting examples/opentheory/compilation/proofs
May 14 14:41:32 Finished examples/opentheory/compilation/proofs                  56s   4GB
May 14 14:41:32 Starting examples/opentheory/compilation/ag32
May 14 15:20:24 Finished examples/opentheory/compilation/ag32                 38m48s  42GB
May 14 15:20:24 Starting examples/opentheory/compilation/ag32/proofs
May 14 15:22:09 Finished examples/opentheory/compilation/ag32/proofs           1m44s   4GB
May 14 15:22:09 Starting examples/sat_encodings
May 14 15:24:10 Finished examples/sat_encodings                                2m01s 894MB
May 14 15:24:11 Starting examples/sat_encodings/case_studies
May 14 15:25:53 Finished examples/sat_encodings/case_studies                   1m42s 930MB
May 14 15:25:53 Starting examples/sat_encodings/translation
May 14 15:31:37 Finished examples/sat_encodings/translation                    5m43s   3GB
May 14 15:31:37 Starting examples/sat_encodings/translation/compilation
May 14 16:20:43 Finished examples/sat_encodings/translation/compilation       49m04s  20GB
May 14 16:20:43 Starting translator/okasaki-examples
May 14 16:25:27 Finished translator/okasaki-examples                           4m44s   1GB
May 14 16:25:27 Starting translator/other-examples
May 14 16:26:15 Finished translator/other-examples                               47s   1GB
May 14 16:26:15 Starting compiler/parsing/tests
May 14 16:26:45 Finished compiler/parsing/tests                                  29s 614MB
May 14 16:26:45 Starting compiler/inference/tests
May 14 16:35:05 Finished compiler/inference/tests                              8m20s   5GB
May 14 16:35:05 Starting compiler/printing/test
May 14 16:38:43 Finished compiler/printing/test                                3m37s   3GB
May 14 16:38:43 Starting compiler/repl
May 14 16:51:40 Finished compiler/repl                                        12m56s   8GB
May 14 16:51:40 Starting compiler/bootstrap/translation
May 14 20:46:53 Finished compiler/bootstrap/translation                     3h55m11s  40GB
May 14 20:46:55 Starting unverified/sexpr-bootstrap/x64/64
May 14 20:58:40 Finished unverified/sexpr-bootstrap/x64/64                    11m44s  12GB
May 14 20:58:40 Starting unverified/sexpr-bootstrap/x64/32
May 14 21:08:12 Finished unverified/sexpr-bootstrap/x64/32                     9m31s  10GB
May 14 21:08:12 Starting compiler/benchmarks
May 14 21:09:08 Finished compiler/benchmarks                                     56s 673MB
May 14 21:09:08 Starting compiler/bootstrap/compilation/x64/64
May 15 14:06:28 FAILED: compiler/bootstrap/compilation/x64/64
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/ocaml[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/candle/prover[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanned 90 directories
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                                                                                                                                                       (0s)     OK
cake-sexpr-32                                                                                                                                                                 (100s)     OK
cake-sexpr-64                                                                                                                                                                 (109s)     OK
to_dataBootstrapTheory                                                                                                                                                        (123m)     OK
Starting work on to_lab_x64BootstrapTheory
to_lab_x64BootstrapTheory                                                                                                                                                      (23h)     OK
Starting work on cake.S
cake.S                                                                                                                                                                        (230m)FAIL<Signal 9>
   val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL message: Created theory "x64Bootstrap">>
           lab_to_target eval: runtime: 3h41m57s,    gctime: 52m21s,     systime: 1m12s.
           lab_to_target real: 3h43m06s
           lab_to_target size: 146543936