Job 1502

CakeML:7d3c433f7a6314dbc8bd5a34761102e1180f2b10
  Update ag32 reader proof statement [Mar 27 14:02:36]
#821 (opentheory-improve)
Merging into:9c2de3ee5f524d70e727448b250ce0f8f085ee53
  Merge pull request #820 from CakeML/fix-export-x64-macos [Mar 22 20:43:15]
HOL:ab03cec5200c8b23f9ba60c5cea958cfcd0cd158
  Make all string overloads "inferior" [Mar 23 06:14:09]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Mar 28 21:28:22 Claimed job
Mar 28 21:28:26 Building HOL
Mar 28 21:43:02 Starting developers
Mar 28 21:43:05 Finished developers                                               2s 129MB
Mar 28 21:43:05 Starting developers/bin
Mar 28 21:43:11 Finished developers/bin                                           6s   1GB
Mar 28 21:43:11 Starting semantics/ffi
Mar 28 21:43:21 Finished semantics/ffi                                            9s 296MB
Mar 28 21:43:22 Starting semantics
Mar 28 21:44:54 Finished semantics                                             1m32s   1GB
Mar 28 21:44:54 Starting semantics/proofs
Mar 28 21:48:12 Finished semantics/proofs                                      3m17s   1GB
Mar 28 21:48:12 Starting semantics/alt_semantics
Mar 28 21:48:20 Finished semantics/alt_semantics                                  7s 430MB
Mar 28 21:48:21 Starting semantics/alt_semantics/proofs
Mar 28 21:50:28 Finished semantics/alt_semantics/proofs                        2m06s   1GB
Mar 28 21:50:28 Starting basis/pure
Mar 28 21:53:13 Finished basis/pure                                            2m44s   1GB
Mar 28 21:53:13 Starting translator
Mar 28 21:55:50 Finished translator                                            2m36s   2GB
Mar 28 21:55:51 Starting compiler/parsing
Mar 28 21:56:57 Finished compiler/parsing                                      1m05s   3GB
Mar 28 21:56:57 Starting characteristic
Mar 28 22:02:52 Finished characteristic                                        5m54s   4GB
Mar 28 22:02:52 Starting translator/monadic
Mar 28 22:04:38 Finished translator/monadic                                    1m45s   3GB
Mar 28 22:04:38 Starting basis
Mar 28 22:47:58 Finished basis                                                43m19s  24GB
Mar 28 22:47:58 Starting compiler/inference
Mar 28 22:49:06 Finished compiler/inference                                    1m08s   1GB
Mar 28 22:49:07 Starting compiler/backend/reg_alloc
Mar 28 22:50:13 Finished compiler/backend/reg_alloc                            1m06s   1GB
Mar 28 22:50:14 Starting compiler/backend/gc
Mar 28 22:53:48 Finished compiler/backend/gc                                   3m34s   2GB
Mar 28 22:53:49 Starting compiler/backend
Mar 28 22:58:53 Finished compiler/backend                                      5m04s   5GB
Mar 28 22:58:54 Starting compiler/encoders/asm
Mar 28 22:59:16 Finished compiler/encoders/asm                                   22s   1GB
Mar 28 22:59:16 Starting compiler/encoders/x64
Mar 28 23:00:20 Finished compiler/encoders/x64                                 1m02s   1GB
Mar 28 23:00:20 Starting compiler/encoders/arm7
Mar 28 23:02:23 Finished compiler/encoders/arm7                                2m02s   1GB
Mar 28 23:02:23 Starting compiler/encoders/arm8
Mar 28 23:03:02 Finished compiler/encoders/arm8                                  38s   1GB
Mar 28 23:03:02 Starting compiler/encoders/mips
Mar 28 23:04:27 Finished compiler/encoders/mips                                1m24s   1GB
Mar 28 23:04:27 Starting compiler/encoders/riscv
Mar 28 23:06:03 Finished compiler/encoders/riscv                               1m36s   1GB
Mar 28 23:06:03 Starting compiler/encoders/ag32
Mar 28 23:06:22 Finished compiler/encoders/ag32                                  18s 953MB
Mar 28 23:06:22 Starting compiler/backend/x64
Mar 28 23:06:41 Finished compiler/backend/x64                                    18s   1GB
Mar 28 23:06:41 Starting compiler/backend/arm7
Mar 28 23:07:02 Finished compiler/backend/arm7                                   20s   1GB
Mar 28 23:07:03 Starting compiler/backend/arm8
Mar 28 23:07:23 Finished compiler/backend/arm8                                   19s   1GB
Mar 28 23:07:23 Starting compiler/backend/mips
Mar 28 23:07:43 Finished compiler/backend/mips                                   20s   1GB
Mar 28 23:07:44 Starting compiler/backend/riscv
Mar 28 23:08:05 Finished compiler/backend/riscv                                  20s   1GB
Mar 28 23:08:05 Starting compiler/backend/ag32
Mar 28 23:09:14 Finished compiler/backend/ag32                                 1m08s   2GB
Mar 28 23:09:14 Starting compiler/parsing/proofs
Mar 28 23:14:36 Finished compiler/parsing/proofs                               5m21s   2GB
Mar 28 23:14:36 Starting compiler/inference/proofs
Mar 28 23:17:07 Finished compiler/inference/proofs                             2m30s   2GB
Mar 28 23:17:07 Starting compiler/backend/semantics
Mar 28 23:44:12 Finished compiler/backend/semantics                           27m04s   3GB
Mar 28 23:44:12 Starting compiler/backend/reg_alloc/proofs
Mar 28 23:47:28 Finished compiler/backend/reg_alloc/proofs                     3m15s   1GB
Mar 28 23:47:28 Starting compiler/backend/proofs
Mar 29 00:41:00 Finished compiler/backend/proofs                              53m31s  19GB
Mar 29 00:41:00 Starting compiler/encoders/x64/proofs
Mar 29 00:50:18 Finished compiler/encoders/x64/proofs                          9m17s   7GB
Mar 29 00:50:18 Starting compiler/encoders/arm7/proofs
Mar 29 01:02:55 Finished compiler/encoders/arm7/proofs                        12m37s  10GB
Mar 29 01:02:56 Starting compiler/encoders/arm8/proofs
Mar 29 01:09:08 Finished compiler/encoders/arm8/proofs                         6m12s   2GB
Mar 29 01:09:08 Starting compiler/encoders/mips/proofs
Mar 29 01:18:52 Finished compiler/encoders/mips/proofs                         9m43s   3GB
Mar 29 01:18:52 Starting compiler/encoders/riscv/proofs
Mar 29 01:27:14 Finished compiler/encoders/riscv/proofs                        8m21s   2GB
Mar 29 01:27:14 Starting compiler/encoders/ag32/proofs
Mar 29 01:29:35 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Mar 29 01:29:35 Starting compiler/backend/x64/proofs
Mar 29 01:29:57 Finished compiler/backend/x64/proofs                             21s   2GB
Mar 29 01:29:57 Starting compiler/backend/arm7/proofs
Mar 29 01:30:20 Finished compiler/backend/arm7/proofs                            22s   1GB
Mar 29 01:30:20 Starting compiler/backend/arm8/proofs
Mar 29 01:30:40 Finished compiler/backend/arm8/proofs                            19s   1GB
Mar 29 01:30:40 Starting compiler/backend/mips/proofs
Mar 29 01:31:02 Finished compiler/backend/mips/proofs                            21s   1GB
Mar 29 01:31:02 Starting compiler/backend/riscv/proofs
Mar 29 01:31:24 Finished compiler/backend/riscv/proofs                           22s   2GB
Mar 29 01:31:25 Starting compiler/backend/ag32/proofs
Mar 29 01:43:19 Finished compiler/backend/ag32/proofs                         11m54s   4GB
Mar 29 01:43:19 Starting compiler/proofs
Mar 29 01:45:15 Finished compiler/proofs                                       1m55s   6GB
Mar 29 01:45:16 Starting candle/set-theory
Mar 29 01:45:46 Finished candle/set-theory                                       30s   1GB
Mar 29 01:45:46 Starting candle/syntax-lib
Mar 29 01:45:58 Finished candle/syntax-lib                                       11s 802MB
Mar 29 01:45:58 Starting candle/standard/syntax
Mar 29 01:47:50 Finished candle/standard/syntax                                1m52s   1GB
Mar 29 01:47:50 Starting candle/standard/semantics
Mar 29 01:49:36 Finished candle/standard/semantics                             1m45s   2GB
Mar 29 01:49:36 Starting candle/standard/monadic
Mar 29 01:51:18 Finished candle/standard/monadic                               1m41s   1GB
Mar 29 01:51:18 Starting candle/standard/ml_kernel
Mar 29 01:56:36 Finished candle/standard/ml_kernel                             5m17s   5GB
Mar 29 01:56:36 Starting candle/overloading/syntax
Mar 29 01:59:47 Finished candle/overloading/syntax                             3m10s   1GB
Mar 29 01:59:47 Starting candle/overloading/semantics
Mar 29 02:11:54 Finished candle/overloading/semantics                         12m06s   8GB
Mar 29 02:11:54 Starting characteristic/examples
Mar 29 02:13:12 Finished characteristic/examples                               1m17s   4GB
Mar 29 02:13:12 Starting tutorial/solutions
Mar 29 02:28:28 Finished tutorial/solutions                                   15m16s   9GB
Mar 29 02:28:29 Starting translator/monadic/examples
Mar 29 02:31:50 Finished translator/monadic/examples                           3m21s   4GB
Mar 29 02:31:50 Starting examples
Mar 29 02:40:18 Finished examples                                              8m27s   6GB
Mar 29 02:40:18 Starting examples/compilation/x64
Mar 29 04:59:23 Finished examples/compilation/x64                           2h19m04s  30GB
Mar 29 04:59:23 Starting examples/compilation/x64/proofs
Mar 29 05:01:17 Finished examples/compilation/x64/proofs                       1m53s   3GB
Mar 29 05:01:17 Starting examples/compilation/ag32
Mar 29 05:34:33 Finished examples/compilation/ag32                            33m15s  12GB
Mar 29 05:34:33 Starting examples/compilation/ag32/proofs
Mar 29 05:35:27 Finished examples/compilation/ag32/proofs                        53s   4GB
Mar 29 05:35:27 Starting examples/cost
Mar 29 06:28:34 Finished examples/cost                                        53m06s  12GB
Mar 29 06:28:35 Starting examples/lpr_checker
Mar 29 06:32:24 Finished examples/lpr_checker                                  3m49s   5GB
Mar 29 06:32:24 Starting examples/lpr_checker/compilation
Mar 29 06:50:26 Finished examples/lpr_checker/compilation                     18m01s  12GB
Mar 29 06:50:26 Starting examples/lpr_checker/compilation/proofs
Mar 29 06:51:09 Finished examples/lpr_checker/compilation/proofs                 42s   3GB
Mar 29 06:51:09 Starting examples/lpr_checker/array
Mar 29 07:04:53 Finished examples/lpr_checker/array                           13m44s   5GB
Mar 29 07:04:53 Starting examples/lpr_checker/array/compilation
Mar 29 07:24:40 Finished examples/lpr_checker/array/compilation               19m46s  16GB
Mar 29 07:24:40 Starting examples/lpr_checker/array/compilation/proofs
Mar 29 07:25:32 Finished examples/lpr_checker/array/compilation/proofs           51s   4GB
Mar 29 07:25:32 Starting examples/opentheory
Mar 29 07:34:29 Finished examples/opentheory                                   8m56s   6GB
Mar 29 07:34:29 Starting examples/opentheory
Mar 29 07:34:30 Finished examples/opentheory                                      0s 100MB
Mar 29 07:34:30 Starting examples/opentheory/compilation
Mar 29 08:05:57 Finished examples/opentheory/compilation                      31m26s  23GB
Mar 29 08:05:57 Starting examples/opentheory/compilation/proofs
Mar 29 08:06:40 Finished examples/opentheory/compilation/proofs                  42s   4GB
Mar 29 08:06:40 Starting examples/opentheory/compilation/ag32
Mar 29 08:38:03 Finished examples/opentheory/compilation/ag32                 31m22s  26GB
Mar 29 08:38:03 Starting examples/opentheory/compilation/ag32/proofs
Mar 29 08:39:34 Finished examples/opentheory/compilation/ag32/proofs           1m30s   6GB
Mar 29 08:39:34 Starting translator/okasaki-examples
Mar 29 08:43:40 Finished translator/okasaki-examples                           4m05s   2GB
Mar 29 08:43:41 Starting translator/other-examples
Mar 29 08:45:38 Finished translator/other-examples                             1m56s   2GB
Mar 29 08:45:38 Starting compiler/parsing/tests
Mar 29 08:46:02 Finished compiler/parsing/tests                                  24s 634MB
Mar 29 08:46:03 Starting compiler/inference/tests
Mar 29 08:53:05 Finished compiler/inference/tests                              7m02s   5GB
Mar 29 08:53:06 Starting compiler/bootstrap/translation
Mar 29 11:13:46 Finished compiler/bootstrap/translation                     2h20m40s  49GB
Mar 29 11:13:46 Starting unverified/sexpr-bootstrap/x64/64
Mar 29 11:25:52 Finished unverified/sexpr-bootstrap/x64/64                    12m05s   8GB
Mar 29 11:25:52 Starting unverified/sexpr-bootstrap/x64/32
Mar 29 11:36:27 Finished unverified/sexpr-bootstrap/x64/32                    10m34s   9GB
Mar 29 11:36:27 Starting compiler/benchmarks
Mar 29 12:14:14 Finished compiler/benchmarks                                  37m46s   2GB
Mar 29 12:14:15 Starting compiler/bootstrap/compilation/x64/64
Mar 30 04:54:10 Finished compiler/bootstrap/compilation/x64/64             16h39m55s  64GB
Mar 30 04:54:11 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 30 04:56:33 Finished compiler/bootstrap/compilation/x64/64/proofs          2m22s  20GB
Mar 30 04:56:33 Starting compiler/bootstrap/compilation/x64/32
Mar 30 19:08:36 Finished compiler/bootstrap/compilation/x64/32             14h12m01s  64GB
Mar 30 19:08:36 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 30 19:10:56 Finished compiler/bootstrap/compilation/x64/32/proofs          2m20s  18GB
Mar 30 19:10:56 Starting compiler/bootstrap/compilation/ag32/32
Mar 31 04:31:18 FAILED: compiler/bootstrap/compilation/ag32/32
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)/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/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[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)/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)/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/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Starting work on README.md
Starting work on to_dataBootstrapTheory
README.md                                                                        real:    0s  user:    0s     OK
to_dataBootstrapTheory                                                           real: 3692s  user: 3670s     OK
Starting work on to_lab_ag32BootstrapTheory
to_lab_ag32BootstrapTheory                                                       real:  498m  user:  996mFAIL<1>
       stack_names (par) size: 49297745
      stack_to_lab (par) eval: runtime: 1h35m13s,    gctime: 8m26s,     systime: 39.1s.
      stack_to_lab (par) real: 25m38s
      stack_to_lab (par) size: 62808910
 Saved theorem _____ "stack_to_lab_thm"
 Exporting theory "to_lab_ag32Bootstrap" ... 
 Failure while writing theory!
 error in quse /home/myreen/regression/cakeml-1502/compiler/bootstrap/compilation/ag32/32/to_lab_ag32BootstrapScript.sml : Io {cause = SysErr ("No space left on device", SOME ENOSPC), function = "output", name = "./to_lab_ag32BootstrapTheory.dat"}
 error in load /home/myreen/regression/cakeml-1502/compiler/bootstrap/compilation/ag32/32/to_lab_ag32BootstrapScript : Io {cause = SysErr ("No space left on device", SOME ENOSPC), function = "output", name = "./to_lab_ag32BootstrapTheory.dat"}
 Uncaught exception: Io {cause = SysErr ("No space left on device", SOME ENOSPC), function = "output", name = "./to_lab_ag32BootstrapTheory.dat"}