Job 1358

CakeML:cab8296f3531716a7090e22761c1f5456b37770b
  Use config to pass symbols out of backend.  Update all proofs [Sep 20 23:19:57]
#788 (symbols)
Merging into:aced251f056eb8714178746a7df203a936cc6991
  Fix compiler/parsing/Holmakefile to make parsingComputeLib build [Sep 18 08:05:26]
HOL:412fb6454a8fa37864443db29a5d354d425a0a78
  emacs-mode: add indentation after Unicode iff symbol [Sep 18 07:22:36]
Machine:oven4s 5.7.19 x86_64 GNU/Linux

Sep 21 22:16:41 Claimed job
Sep 21 22:16:45 Building HOL
Sep 21 22:28:54 Starting developers
Sep 21 22:28:56 Finished developers                                               1s 158MB
Sep 21 22:28:56 Starting developers/bin
Sep 21 22:29:04 Finished developers/bin                                           7s   1GB
Sep 21 22:29:05 Starting semantics/ffi
Sep 21 22:29:14 Finished semantics/ffi                                            9s   2GB
Sep 21 22:29:15 Starting semantics
Sep 21 22:30:35 Finished semantics                                             1m19s   4GB
Sep 21 22:30:35 Starting semantics/proofs
Sep 21 22:33:30 Finished semantics/proofs                                      2m54s   4GB
Sep 21 22:33:31 Starting semantics/alt_semantics
Sep 21 22:33:39 Finished semantics/alt_semantics                                  8s   4GB
Sep 21 22:33:40 Starting semantics/alt_semantics/proofs
Sep 21 22:35:36 Finished semantics/alt_semantics/proofs                        1m55s   4GB
Sep 21 22:35:36 Starting basis/pure
Sep 21 22:37:55 Finished basis/pure                                            2m18s   4GB
Sep 21 22:37:55 Starting translator
Sep 21 22:40:18 Finished translator                                            2m22s   7GB
Sep 21 22:40:18 Starting compiler/parsing
Sep 21 22:41:22 Finished compiler/parsing                                      1m03s   6GB
Sep 21 22:41:23 Starting characteristic
Sep 21 22:46:46 Finished characteristic                                        5m23s   5GB
Sep 21 22:46:47 Starting translator/monadic
Sep 21 22:48:10 Finished translator/monadic                                    1m23s   4GB
Sep 21 22:48:11 Starting basis
Sep 21 23:19:34 Finished basis                                                31m23s  27GB
Sep 21 23:19:35 Starting compiler/inference
Sep 21 23:20:35 Finished compiler/inference                                    1m00s   4GB
Sep 21 23:20:36 Starting compiler/backend/reg_alloc
Sep 21 23:21:23 Finished compiler/backend/reg_alloc                              47s   4GB
Sep 21 23:21:24 Starting compiler/backend/gc
Sep 21 23:24:29 Finished compiler/backend/gc                                   3m04s   6GB
Sep 21 23:24:29 Starting compiler/backend
Sep 21 23:28:44 Finished compiler/backend                                      4m15s   7GB
Sep 21 23:28:45 Starting compiler/encoders/asm
Sep 21 23:29:04 Finished compiler/encoders/asm                                   19s   4GB
Sep 21 23:29:05 Starting compiler/encoders/x64
Sep 21 23:30:01 Finished compiler/encoders/x64                                   55s   4GB
Sep 21 23:30:01 Starting compiler/encoders/arm7
Sep 21 23:31:55 Finished compiler/encoders/arm7                                1m53s   4GB
Sep 21 23:31:55 Starting compiler/encoders/arm8
Sep 21 23:32:30 Finished compiler/encoders/arm8                                  34s   4GB
Sep 21 23:32:30 Starting compiler/encoders/mips
Sep 21 23:33:48 Finished compiler/encoders/mips                                1m16s   4GB
Sep 21 23:33:48 Starting compiler/encoders/riscv
Sep 21 23:35:12 Finished compiler/encoders/riscv                               1m23s   4GB
Sep 21 23:35:12 Starting compiler/encoders/ag32
Sep 21 23:35:28 Finished compiler/encoders/ag32                                  15s   4GB
Sep 21 23:35:28 Starting compiler/backend/x64
Sep 21 23:35:45 Finished compiler/backend/x64                                    17s   4GB
Sep 21 23:35:46 Starting compiler/backend/arm7
Sep 21 23:36:02 Finished compiler/backend/arm7                                   15s   4GB
Sep 21 23:36:02 Starting compiler/backend/arm8
Sep 21 23:36:20 Finished compiler/backend/arm8                                   17s   4GB
Sep 21 23:36:20 Starting compiler/backend/mips
Sep 21 23:36:39 Finished compiler/backend/mips                                   18s   4GB
Sep 21 23:36:39 Starting compiler/backend/riscv
Sep 21 23:36:57 Finished compiler/backend/riscv                                  18s   4GB
Sep 21 23:36:58 Starting compiler/backend/ag32
Sep 21 23:37:57 Finished compiler/backend/ag32                                   59s   4GB
Sep 21 23:37:58 Starting compiler/parsing/proofs
Sep 21 23:42:20 Finished compiler/parsing/proofs                               4m22s   4GB
Sep 21 23:42:21 Starting compiler/inference/proofs
Sep 21 23:44:32 Finished compiler/inference/proofs                             2m10s   4GB
Sep 21 23:44:32 Starting compiler/backend/semantics
Sep 22 00:07:48 Finished compiler/backend/semantics                           23m15s   8GB
Sep 22 00:07:49 Starting compiler/backend/reg_alloc/proofs
Sep 22 00:10:40 Finished compiler/backend/reg_alloc/proofs                     2m50s   4GB
Sep 22 00:10:40 Starting compiler/backend/proofs
Sep 22 00:58:26 Finished compiler/backend/proofs                              47m45s  30GB
Sep 22 00:58:26 Starting compiler/encoders/x64/proofs
Sep 22 01:07:20 Finished compiler/encoders/x64/proofs                          8m53s  10GB
Sep 22 01:07:20 Starting compiler/encoders/arm7/proofs
Sep 22 01:19:18 Finished compiler/encoders/arm7/proofs                        11m57s  14GB
Sep 22 01:19:19 Starting compiler/encoders/arm8/proofs
Sep 22 01:25:14 Finished compiler/encoders/arm8/proofs                         5m54s   4GB
Sep 22 01:25:14 Starting compiler/encoders/mips/proofs
Sep 22 01:34:41 Finished compiler/encoders/mips/proofs                         9m26s  10GB
Sep 22 01:34:42 Starting compiler/encoders/riscv/proofs
Sep 22 01:42:09 Finished compiler/encoders/riscv/proofs                        7m26s   8GB
Sep 22 01:42:09 Starting compiler/encoders/ag32/proofs
Sep 22 01:44:19 Finished compiler/encoders/ag32/proofs                         2m09s   4GB
Sep 22 01:44:19 Starting compiler/backend/x64/proofs
Sep 22 01:44:39 Finished compiler/backend/x64/proofs                             19s   4GB
Sep 22 01:44:40 Starting compiler/backend/arm7/proofs
Sep 22 01:45:02 Finished compiler/backend/arm7/proofs                            21s   4GB
Sep 22 01:45:02 Starting compiler/backend/arm8/proofs
Sep 22 01:45:22 Finished compiler/backend/arm8/proofs                            19s   4GB
Sep 22 01:45:22 Starting compiler/backend/mips/proofs
Sep 22 01:45:43 Finished compiler/backend/mips/proofs                            20s   4GB
Sep 22 01:45:44 Starting compiler/backend/riscv/proofs
Sep 22 01:46:04 Finished compiler/backend/riscv/proofs                           19s   4GB
Sep 22 01:46:04 Starting compiler/backend/ag32/proofs
Sep 22 01:57:24 Finished compiler/backend/ag32/proofs                         11m19s  11GB
Sep 22 01:57:24 Starting compiler/proofs
Sep 22 01:59:08 Finished compiler/proofs                                       1m43s   7GB
Sep 22 01:59:08 Starting candle/set-theory
Sep 22 01:59:32 Finished candle/set-theory                                       23s   4GB
Sep 22 01:59:32 Starting candle/syntax-lib
Sep 22 01:59:42 Finished candle/syntax-lib                                        9s   4GB
Sep 22 01:59:42 Starting candle/standard/syntax
Sep 22 02:01:16 Finished candle/standard/syntax                                1m33s   4GB
Sep 22 02:01:16 Starting candle/standard/semantics
Sep 22 02:02:52 Finished candle/standard/semantics                             1m35s   5GB
Sep 22 02:02:53 Starting candle/standard/monadic
Sep 22 02:04:21 Finished candle/standard/monadic                               1m28s   4GB
Sep 22 02:04:22 Starting candle/standard/ml_kernel
Sep 22 02:09:06 Finished candle/standard/ml_kernel                             4m43s  10GB
Sep 22 02:09:06 Starting candle/overloading/syntax
Sep 22 02:11:41 Finished candle/overloading/syntax                             2m34s   4GB
Sep 22 02:11:42 Starting candle/overloading/semantics
Sep 22 02:22:51 Finished candle/overloading/semantics                         11m08s   6GB
Sep 22 02:22:52 Starting characteristic/examples
Sep 22 02:24:05 Finished characteristic/examples                               1m12s  10GB
Sep 22 02:24:05 Starting tutorial/solutions
Sep 22 02:37:00 Finished tutorial/solutions                                   12m54s  12GB
Sep 22 02:37:01 Starting translator/monadic/examples
Sep 22 02:39:44 Finished translator/monadic/examples                           2m42s   9GB
Sep 22 02:39:44 Starting examples
Sep 22 02:47:17 Finished examples                                              7m32s  11GB
Sep 22 02:47:17 Starting examples/compilation/x64
Sep 22 04:47:58 Finished examples/compilation/x64                           2h00m40s  18GB
Sep 22 04:47:59 Starting examples/compilation/x64/proofs
Sep 22 04:49:31 Finished examples/compilation/x64/proofs                       1m32s   5GB
Sep 22 04:49:32 Starting examples/compilation/ag32
Sep 22 05:18:16 Finished examples/compilation/ag32                            28m43s  12GB
Sep 22 05:18:21 Starting examples/compilation/ag32/proofs
Sep 22 05:19:03 Finished examples/compilation/ag32/proofs                        41s   6GB
Sep 22 05:19:03 Starting examples/cost
Sep 22 06:02:04 Finished examples/cost                                        43m00s  17GB
Sep 22 06:02:04 Starting examples/lpr_checker
Sep 22 06:05:34 Finished examples/lpr_checker                                  3m29s  11GB
Sep 22 06:05:34 Starting examples/lpr_checker/compilation
Sep 22 06:20:55 Finished examples/lpr_checker/compilation                     15m20s  38GB
Sep 22 06:20:55 Starting examples/lpr_checker/compilation/proofs
Sep 22 06:21:32 Finished examples/lpr_checker/compilation/proofs                 36s   5GB
Sep 22 06:21:32 Starting examples/lpr_checker/array
Sep 22 06:33:23 Finished examples/lpr_checker/array                           11m50s  10GB
Sep 22 06:33:24 Starting examples/lpr_checker/array/compilation
Sep 22 06:49:35 Finished examples/lpr_checker/array/compilation               16m11s  13GB
Sep 22 06:49:36 Starting examples/lpr_checker/array/compilation/proofs
Sep 22 06:50:18 Finished examples/lpr_checker/array/compilation/proofs           42s   6GB
Sep 22 06:50:18 Starting examples/opentheory
Sep 22 06:58:37 Finished examples/opentheory                                   8m17s  11GB
Sep 22 06:58:37 Starting examples/opentheory
Sep 22 06:58:38 Finished examples/opentheory                                      0s  19MB
Sep 22 06:58:38 Starting examples/opentheory/compilation
Sep 22 07:29:39 Finished examples/opentheory/compilation                      30m59s  47GB
Sep 22 07:29:39 Starting examples/opentheory/compilation/proofs
Sep 22 07:30:17 Finished examples/opentheory/compilation/proofs                  36s   5GB
Sep 22 07:30:17 Starting examples/opentheory/compilation/ag32
Sep 22 08:01:31 Finished examples/opentheory/compilation/ag32                 31m13s  57GB
Sep 22 08:01:31 Starting examples/opentheory/compilation/ag32/proofs
Sep 22 08:02:58 Finished examples/opentheory/compilation/ag32/proofs           1m26s  10GB
Sep 22 08:02:59 Starting translator/okasaki-examples
Sep 22 08:06:45 Finished translator/okasaki-examples                           3m46s   8GB
Sep 22 08:06:46 Starting translator/other-examples
Sep 22 08:08:33 Finished translator/other-examples                             1m47s   5GB
Sep 22 08:08:33 Starting compiler/parsing/tests
Sep 22 08:08:55 Finished compiler/parsing/tests                                  20s   4GB
Sep 22 08:08:55 Starting compiler/inference/tests
Sep 22 08:12:45 Finished compiler/inference/tests                              3m49s   8GB
Sep 22 08:12:45 Starting compiler/bootstrap/translation
Sep 22 10:41:24 Finished compiler/bootstrap/translation                     2h28m38s  75GB
Sep 22 10:41:24 Starting unverified/sexpr-bootstrap/x64/64
Sep 22 10:50:22 Finished unverified/sexpr-bootstrap/x64/64                     8m57s   8GB
Sep 22 10:50:23 Starting unverified/sexpr-bootstrap/x64/32
Sep 22 10:57:44 Finished unverified/sexpr-bootstrap/x64/32                     7m21s   8GB
Sep 22 10:57:45 Starting compiler/benchmarks
Sep 22 10:57:46 Finished compiler/benchmarks                                      1s  79MB
Sep 22 10:57:47 Starting compiler/bootstrap/compilation/x64/64
Sep 22 22:39:03 Finished compiler/bootstrap/compilation/x64/64             11h41m15s  88GB
Sep 22 22:39:03 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 22 22:41:12 FAILED: compiler/bootstrap/compilation/x64/64/proofs
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/unification/triangular
Scanning $(HOLDIR)/examples/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Starting work on README.md
Starting work on x64BootstrapProofTheory
README.md                                       real:    0s  user:    0s     OK
x64BootstrapProofTheory                         real:  127s  user:  116sFAIL<1>
 Heap: Local spaces 16907, permanent spaces 29, code spaces 335, stack spaces 2
 Heap: Code area: total 2.27M occupied: 2.26M
 Heap: Stack area: total 4.00M
 GC: Completed successfully
 error in quse /oven/cakeml-1358/compiler/bootstrap/compilation/x64/64/proofs/x64BootstrapProofScript.sml : HOL_ERR {message = "different constructors", origin_function = "raw_match_term", origin_structure = "Term"}
 error in load /oven/cakeml-1358/compiler/bootstrap/compilation/x64/64/proofs/x64BootstrapProofScript : HOL_ERR {message = "different constructors", origin_function = "raw_match_term", origin_structure = "Term"}
 Uncaught exception: HOL_ERR {message = "different constructors", origin_function = "raw_match_term", origin_structure = "Term"}
 GC (Total): Non-GC time: CPU user: 52.530 system: 6.365 real: 59.006
 GC (Total): GC time: CPU user: 63.638 system: 3.908 real: 67.550
 Heap: Total CPU GC time 67.546secs,  Non-GC 58.896secs, ratio 1.147