Job 1363

CakeML:9a0180ee6a0bbcf4cc2d2aee6efc20caa0f62e95
  Add sexpr files to cake-x64-64.tar.gz artefact [Sep 24 05:41:42]
#788 (symbols)
Merging into:411c80da717a8e99b5a8e7f6519e95637ecb7225
  Merge pull request #752 from sorear/rv_fixes [Sep 24 08:22:45]
HOL:841cced433cd0e9e4913c6e9c05c9b7542e38a6b
  Handle change to Slavonic asterisk (25dec53e17) in Manual production [Sep 23 11:12:05]
Machine:oven5s2 5.7.19 x86_64 GNU/Linux

Sep 25 00:56:09 Claimed job
Sep 25 00:56:13 Building HOL
Sep 25 01:08:44 Starting developers
Sep 25 01:08:47 Finished developers                                               1s 158MB
Sep 25 01:08:47 Starting developers/bin
Sep 25 01:08:56 Finished developers/bin                                           8s   1GB
Sep 25 01:08:56 Starting semantics/ffi
Sep 25 01:09:06 Finished semantics/ffi                                            9s   2GB
Sep 25 01:09:06 Starting semantics
Sep 25 01:10:27 Finished semantics                                             1m20s   4GB
Sep 25 01:10:27 Starting semantics/proofs
Sep 25 01:13:29 Finished semantics/proofs                                      3m02s   4GB
Sep 25 01:13:30 Starting semantics/alt_semantics
Sep 25 01:13:38 Finished semantics/alt_semantics                                  8s   4GB
Sep 25 01:13:39 Starting semantics/alt_semantics/proofs
Sep 25 01:15:40 Finished semantics/alt_semantics/proofs                        2m01s   4GB
Sep 25 01:15:41 Starting basis/pure
Sep 25 01:18:04 Finished basis/pure                                            2m22s   4GB
Sep 25 01:18:05 Starting translator
Sep 25 01:20:28 Finished translator                                            2m23s   8GB
Sep 25 01:20:29 Starting compiler/parsing
Sep 25 01:21:30 Finished compiler/parsing                                      1m01s   6GB
Sep 25 01:21:31 Starting characteristic
Sep 25 01:27:06 Finished characteristic                                        5m34s   5GB
Sep 25 01:27:06 Starting translator/monadic
Sep 25 01:28:33 Finished translator/monadic                                    1m26s   4GB
Sep 25 01:28:34 Starting basis
Sep 25 02:01:13 Finished basis                                                32m37s  31GB
Sep 25 02:01:14 Starting compiler/inference
Sep 25 02:02:19 Finished compiler/inference                                    1m03s   4GB
Sep 25 02:02:19 Starting compiler/backend/reg_alloc
Sep 25 02:03:09 Finished compiler/backend/reg_alloc                              49s   4GB
Sep 25 02:03:10 Starting compiler/backend/gc
Sep 25 02:06:11 Finished compiler/backend/gc                                   3m00s   6GB
Sep 25 02:06:11 Starting compiler/backend
Sep 25 02:11:01 Finished compiler/backend                                      4m49s   7GB
Sep 25 02:11:02 Starting compiler/encoders/asm
Sep 25 02:11:24 Finished compiler/encoders/asm                                   22s   4GB
Sep 25 02:11:24 Starting compiler/encoders/x64
Sep 25 02:12:28 Finished compiler/encoders/x64                                 1m03s   4GB
Sep 25 02:12:29 Starting compiler/encoders/arm7
Sep 25 02:14:40 Finished compiler/encoders/arm7                                2m11s   4GB
Sep 25 02:14:41 Starting compiler/encoders/arm8
Sep 25 02:15:20 Finished compiler/encoders/arm8                                  39s   4GB
Sep 25 02:15:21 Starting compiler/encoders/mips
Sep 25 02:16:47 Finished compiler/encoders/mips                                1m26s   4GB
Sep 25 02:16:48 Starting compiler/encoders/riscv
Sep 25 02:18:15 Finished compiler/encoders/riscv                               1m26s   4GB
Sep 25 02:18:15 Starting compiler/encoders/ag32
Sep 25 02:18:31 Finished compiler/encoders/ag32                                  15s   4GB
Sep 25 02:18:31 Starting compiler/backend/x64
Sep 25 02:18:49 Finished compiler/backend/x64                                    17s   4GB
Sep 25 02:18:50 Starting compiler/backend/arm7
Sep 25 02:19:11 Finished compiler/backend/arm7                                   20s   4GB
Sep 25 02:19:11 Starting compiler/backend/arm8
Sep 25 02:19:32 Finished compiler/backend/arm8                                   20s   4GB
Sep 25 02:19:32 Starting compiler/backend/mips
Sep 25 02:19:54 Finished compiler/backend/mips                                   21s   4GB
Sep 25 02:19:54 Starting compiler/backend/riscv
Sep 25 02:20:16 Finished compiler/backend/riscv                                  21s   4GB
Sep 25 02:20:16 Starting compiler/backend/ag32
Sep 25 02:21:22 Finished compiler/backend/ag32                                 1m05s   6GB
Sep 25 02:21:22 Starting compiler/parsing/proofs
Sep 25 02:26:00 Finished compiler/parsing/proofs                               4m37s   4GB
Sep 25 02:26:00 Starting compiler/inference/proofs
Sep 25 02:28:15 Finished compiler/inference/proofs                             2m14s   4GB
Sep 25 02:28:15 Starting compiler/backend/semantics
Sep 25 02:55:03 Finished compiler/backend/semantics                           26m47s   8GB
Sep 25 02:55:04 Starting compiler/backend/reg_alloc/proofs
Sep 25 02:58:23 Finished compiler/backend/reg_alloc/proofs                     3m19s   4GB
Sep 25 02:58:23 Starting compiler/backend/proofs
Sep 25 03:48:14 Finished compiler/backend/proofs                              49m49s  28GB
Sep 25 03:48:14 Starting compiler/encoders/x64/proofs
Sep 25 03:57:17 Finished compiler/encoders/x64/proofs                          9m02s  10GB
Sep 25 03:57:17 Starting compiler/encoders/arm7/proofs
Sep 25 04:09:30 Finished compiler/encoders/arm7/proofs                        12m12s   6GB
Sep 25 04:09:31 Starting compiler/encoders/arm8/proofs
Sep 25 04:16:27 Finished compiler/encoders/arm8/proofs                         6m56s   5GB
Sep 25 04:16:28 Starting compiler/encoders/mips/proofs
Sep 25 04:26:39 Finished compiler/encoders/mips/proofs                        10m11s   7GB
Sep 25 04:26:39 Starting compiler/encoders/riscv/proofs
Sep 25 04:35:07 Finished compiler/encoders/riscv/proofs                        8m26s   8GB
Sep 25 04:35:07 Starting compiler/encoders/ag32/proofs
Sep 25 04:37:30 Finished compiler/encoders/ag32/proofs                         2m23s   4GB
Sep 25 04:37:31 Starting compiler/backend/x64/proofs
Sep 25 04:37:53 Finished compiler/backend/x64/proofs                             21s   4GB
Sep 25 04:37:53 Starting compiler/backend/arm7/proofs
Sep 25 04:38:17 Finished compiler/backend/arm7/proofs                            23s   4GB
Sep 25 04:38:17 Starting compiler/backend/arm8/proofs
Sep 25 04:38:38 Finished compiler/backend/arm8/proofs                            21s   4GB
Sep 25 04:38:39 Starting compiler/backend/mips/proofs
Sep 25 04:39:01 Finished compiler/backend/mips/proofs                            21s   4GB
Sep 25 04:39:01 Starting compiler/backend/riscv/proofs
Sep 25 04:39:23 Finished compiler/backend/riscv/proofs                           21s   4GB
Sep 25 04:39:24 Starting compiler/backend/ag32/proofs
Sep 25 04:51:45 Finished compiler/backend/ag32/proofs                         12m20s  11GB
Sep 25 04:51:45 Starting compiler/proofs
Sep 25 04:53:33 Finished compiler/proofs                                       1m46s   7GB
Sep 25 04:53:33 Starting candle/set-theory
Sep 25 04:53:58 Finished candle/set-theory                                       24s   4GB
Sep 25 04:53:59 Starting candle/syntax-lib
Sep 25 04:54:08 Finished candle/syntax-lib                                        9s   4GB
Sep 25 04:54:09 Starting candle/standard/syntax
Sep 25 04:55:46 Finished candle/standard/syntax                                1m37s   4GB
Sep 25 04:55:47 Starting candle/standard/semantics
Sep 25 04:57:30 Finished candle/standard/semantics                             1m43s   6GB
Sep 25 04:57:30 Starting candle/standard/monadic
Sep 25 04:59:04 Finished candle/standard/monadic                               1m32s   4GB
Sep 25 04:59:04 Starting candle/standard/ml_kernel
Sep 25 05:04:07 Finished candle/standard/ml_kernel                             5m02s  10GB
Sep 25 05:04:07 Starting candle/overloading/syntax
Sep 25 05:06:48 Finished candle/overloading/syntax                             2m40s   4GB
Sep 25 05:06:48 Starting candle/overloading/semantics
Sep 25 05:18:29 Finished candle/overloading/semantics                         11m40s   6GB
Sep 25 05:18:30 Starting characteristic/examples
Sep 25 05:19:44 Finished characteristic/examples                               1m14s  10GB
Sep 25 05:19:45 Starting tutorial/solutions
Sep 25 05:33:03 Finished tutorial/solutions                                   13m17s  22GB
Sep 25 05:33:03 Starting translator/monadic/examples
Sep 25 05:35:43 Finished translator/monadic/examples                           2m39s   9GB
Sep 25 05:35:43 Starting examples
Sep 25 05:42:41 Finished examples                                              6m57s  11GB
Sep 25 05:42:41 Starting examples/compilation/x64
Sep 25 07:47:18 Finished examples/compilation/x64                           2h04m36s  36GB
Sep 25 07:47:18 Starting examples/compilation/x64/proofs
Sep 25 07:48:51 Finished examples/compilation/x64/proofs                       1m32s   5GB
Sep 25 07:48:52 Starting examples/compilation/ag32
Sep 25 08:18:14 Finished examples/compilation/ag32                            29m22s  12GB
Sep 25 08:18:15 Starting examples/compilation/ag32/proofs
Sep 25 08:18:57 Finished examples/compilation/ag32/proofs                        41s   6GB
Sep 25 08:18:57 Starting examples/cost
Sep 25 09:00:27 Finished examples/cost                                        41m29s  17GB
Sep 25 09:00:28 Starting examples/lpr_checker
Sep 25 09:04:01 Finished examples/lpr_checker                                  3m33s  11GB
Sep 25 09:04:02 Starting examples/lpr_checker/compilation
Sep 25 09:18:43 Finished examples/lpr_checker/compilation                     14m40s  45GB
Sep 25 09:18:43 Starting examples/lpr_checker/compilation/proofs
Sep 25 09:19:20 Finished examples/lpr_checker/compilation/proofs                 36s   5GB
Sep 25 09:19:21 Starting examples/lpr_checker/array
Sep 25 09:31:27 Finished examples/lpr_checker/array                           12m05s  10GB
Sep 25 09:31:27 Starting examples/lpr_checker/array/compilation
Sep 25 09:47:31 Finished examples/lpr_checker/array/compilation               16m03s  12GB
Sep 25 09:47:32 Starting examples/lpr_checker/array/compilation/proofs
Sep 25 09:48:15 Finished examples/lpr_checker/array/compilation/proofs           42s   6GB
Sep 25 09:48:15 Starting examples/opentheory
Sep 25 09:56:49 Finished examples/opentheory                                   8m33s  11GB
Sep 25 09:56:50 Starting examples/opentheory
Sep 25 09:56:51 Finished examples/opentheory                                      0s  56MB
Sep 25 09:56:51 Starting examples/opentheory/compilation
Sep 25 10:26:27 Finished examples/opentheory/compilation                      29m36s  50GB
Sep 25 10:26:28 Starting examples/opentheory/compilation/proofs
Sep 25 10:27:06 Finished examples/opentheory/compilation/proofs                  37s   5GB
Sep 25 10:27:07 Starting examples/opentheory/compilation/ag32
Sep 25 10:59:03 Finished examples/opentheory/compilation/ag32                 31m55s  37GB
Sep 25 10:59:03 Starting examples/opentheory/compilation/ag32/proofs
Sep 25 11:00:38 Finished examples/opentheory/compilation/ag32/proofs           1m34s  10GB
Sep 25 11:00:39 Starting translator/okasaki-examples
Sep 25 11:04:48 Finished translator/okasaki-examples                           4m08s   8GB
Sep 25 11:04:48 Starting translator/other-examples
Sep 25 11:06:31 Finished translator/other-examples                             1m41s   5GB
Sep 25 11:06:31 Starting compiler/parsing/tests
Sep 25 11:06:55 Finished compiler/parsing/tests                                  23s   4GB
Sep 25 11:06:55 Starting compiler/inference/tests
Sep 25 11:11:04 Finished compiler/inference/tests                              4m09s   8GB
Sep 25 11:11:05 Starting compiler/bootstrap/translation
Sep 25 13:39:59 Finished compiler/bootstrap/translation                     2h28m51s  81GB
Sep 25 13:39:59 Starting unverified/sexpr-bootstrap/x64/64
Sep 25 13:49:01 Finished unverified/sexpr-bootstrap/x64/64                     9m01s   8GB
Sep 25 13:49:01 Starting unverified/sexpr-bootstrap/x64/32
Sep 25 13:56:27 Finished unverified/sexpr-bootstrap/x64/32                     7m25s   8GB
Sep 25 13:56:27 Starting compiler/benchmarks
Sep 25 13:56:29 Finished compiler/benchmarks                                      1s  79MB
Sep 25 13:56:29 Starting compiler/bootstrap/compilation/x64/64
Sep 25 13:57:25 FAILED: compiler/bootstrap/compilation/x64/64
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 $(HOLDIR)/examples/machine-code/hoare-triple
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)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
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)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
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/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/unification/triangular
Scanning $(HOLDIR)/examples/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                       real:    0s  user:    0s     OK
cake-sexpr-32                                   real:   53s  user:   49sFAIL<1>
 Heap: Full GC (after) Major heap used 2.11G of 2.11G (100%). Alloc space used 237.72M of 2.87G (8%). Total space 11.36G 21% full.
 Heap: Local spaces 4772, permanent spaces 30, code spaces 73, stack spaces 2
 Heap: Code area: total 572.00K occupied: 230.72K
 Heap: Stack area: total 1.00M
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/compiler32ProgTheory : Interrupt
 error in load /oven/cakeml-1363/compiler/bootstrap/compilation/x64/64/sexprBootstrap32Script : Interrupt
 Uncaught exception: Interrupt
 GC (Total): Non-GC time: CPU user: 24.520 system: 2.973 real: 27.487
 GC (Total): GC time: CPU user: 25.108 system: 1.055 real: 26.164
 Heap: Total CPU GC time 26.163secs,  Non-GC 27.493secs, ratio 0.952
cake-sexpr-64                                                           M-KILLED
to_dataBootstrapTheory                                                  M-KILLED