Job 1117

CakeML:989142823c42cd3f693025fd202a545379a76ed7
  update build sequence [Dec 08 15:35:24]
#708 (lrat)
Merging into:5752e21fdd0a5da28d3bec757206728debc27640
  Merge pull request #702 from CakeML/bufferedio [Dec 03 03:21:05]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 08 23:50:07 Claimed job
Dec 08 23:50:10 Reusing HOL
Dec 08 23:50:58 Starting developers
Dec 08 23:51:02 Finished developers                                               4s  95MB
Dec 08 23:51:02 Starting developers/bin
Dec 08 23:51:09 Finished developers/bin                                           6s 960MB
Dec 08 23:51:09 Starting semantics/ffi
Dec 08 23:51:19 Finished semantics/ffi                                            9s 241MB
Dec 08 23:51:19 Starting semantics
Dec 08 23:52:40 Finished semantics                                             1m20s   1GB
Dec 08 23:52:40 Starting semantics/proofs
Dec 08 23:55:59 Finished semantics/proofs                                      3m18s   1GB
Dec 08 23:55:59 Starting semantics/alt_semantics
Dec 08 23:56:07 Finished semantics/alt_semantics                                  7s 287MB
Dec 08 23:56:07 Starting semantics/alt_semantics/proofs
Dec 08 23:58:04 Finished semantics/alt_semantics/proofs                        1m57s 772MB
Dec 08 23:58:04 Starting basis/pure
Dec 08 23:58:53 Finished basis/pure                                              48s 680MB
Dec 08 23:58:53 Starting translator
Dec 09 00:00:47 Finished translator                                            1m53s   1GB
Dec 09 00:00:47 Starting compiler/parsing
Dec 09 00:01:59 Finished compiler/parsing                                      1m11s   2GB
Dec 09 00:01:59 Starting characteristic
Dec 09 00:07:36 Finished characteristic                                        5m37s   1GB
Dec 09 00:07:36 Starting translator/monadic
Dec 09 00:09:07 Finished translator/monadic                                    1m30s   1GB
Dec 09 00:09:07 Starting basis
Dec 09 00:44:12 Finished basis                                                35m04s  16GB
Dec 09 00:44:12 Starting compiler/inference
Dec 09 00:45:59 Finished compiler/inference                                    1m47s   1GB
Dec 09 00:46:00 Starting compiler/backend/reg_alloc
Dec 09 00:47:02 Finished compiler/backend/reg_alloc                            1m02s   1GB
Dec 09 00:47:02 Starting compiler/backend/gc
Dec 09 00:50:16 Finished compiler/backend/gc                                   3m13s   2GB
Dec 09 00:50:16 Starting compiler/backend
Dec 09 00:54:13 Finished compiler/backend                                      3m56s   2GB
Dec 09 00:54:13 Starting compiler/encoders/asm
Dec 09 00:54:34 Finished compiler/encoders/asm                                   20s 814MB
Dec 09 00:54:34 Starting compiler/encoders/x64
Dec 09 00:54:59 Finished compiler/encoders/x64                                   24s 757MB
Dec 09 00:54:59 Starting compiler/encoders/arm7
Dec 09 00:55:47 Finished compiler/encoders/arm7                                  47s 756MB
Dec 09 00:55:47 Starting compiler/encoders/arm8
Dec 09 00:56:00 Finished compiler/encoders/arm8                                  12s 617MB
Dec 09 00:56:00 Starting compiler/encoders/mips
Dec 09 00:56:17 Finished compiler/encoders/mips                                  16s   1GB
Dec 09 00:56:17 Starting compiler/encoders/riscv
Dec 09 00:56:32 Finished compiler/encoders/riscv                                 15s 803MB
Dec 09 00:56:33 Starting compiler/encoders/ag32
Dec 09 00:56:50 Finished compiler/encoders/ag32                                  17s 538MB
Dec 09 00:56:50 Starting compiler/backend/x64
Dec 09 00:57:08 Finished compiler/backend/x64                                    17s   1GB
Dec 09 00:57:09 Starting compiler/backend/arm7
Dec 09 00:57:28 Finished compiler/backend/arm7                                   19s   1GB
Dec 09 00:57:28 Starting compiler/backend/arm8
Dec 09 00:57:45 Finished compiler/backend/arm8                                   16s   1GB
Dec 09 00:57:45 Starting compiler/backend/mips
Dec 09 00:58:03 Finished compiler/backend/mips                                   18s   1GB
Dec 09 00:58:04 Starting compiler/backend/riscv
Dec 09 00:58:21 Finished compiler/backend/riscv                                  17s 913MB
Dec 09 00:58:21 Starting compiler/backend/ag32
Dec 09 00:59:31 Finished compiler/backend/ag32                                 1m09s 918MB
Dec 09 00:59:31 Starting compiler/parsing/proofs
Dec 09 01:05:13 Finished compiler/parsing/proofs                               5m41s   1GB
Dec 09 01:05:13 Starting compiler/inference/proofs
Dec 09 01:08:13 Finished compiler/inference/proofs                             2m59s   1GB
Dec 09 01:08:13 Starting compiler/backend/semantics
Dec 09 01:30:25 Finished compiler/backend/semantics                           22m11s   1GB
Dec 09 01:30:25 Starting compiler/backend/reg_alloc/proofs
Dec 09 01:34:07 Finished compiler/backend/reg_alloc/proofs                     3m42s 948MB
Dec 09 01:34:07 Starting compiler/backend/proofs
Dec 09 02:35:35 Finished compiler/backend/proofs                            1h01m27s  17GB
Dec 09 02:35:35 Starting compiler/encoders/x64/proofs
Dec 09 02:45:21 Finished compiler/encoders/x64/proofs                          9m45s   5GB
Dec 09 02:45:22 Starting compiler/encoders/arm7/proofs
Dec 09 02:58:32 Finished compiler/encoders/arm7/proofs                        13m09s   5GB
Dec 09 02:58:32 Starting compiler/encoders/arm8/proofs
Dec 09 03:05:09 Finished compiler/encoders/arm8/proofs                         6m37s   1GB
Dec 09 03:05:10 Starting compiler/encoders/mips/proofs
Dec 09 03:15:13 Finished compiler/encoders/mips/proofs                        10m02s   2GB
Dec 09 03:15:13 Starting compiler/encoders/riscv/proofs
Dec 09 03:24:15 Finished compiler/encoders/riscv/proofs                        9m02s   1GB
Dec 09 03:24:15 Starting compiler/encoders/ag32/proofs
Dec 09 03:26:55 Finished compiler/encoders/ag32/proofs                         2m39s 779MB
Dec 09 03:26:55 Starting compiler/backend/x64/proofs
Dec 09 03:27:14 Finished compiler/backend/x64/proofs                             18s   1GB
Dec 09 03:27:14 Starting compiler/backend/arm7/proofs
Dec 09 03:27:34 Finished compiler/backend/arm7/proofs                            19s   1GB
Dec 09 03:27:34 Starting compiler/backend/arm8/proofs
Dec 09 03:27:52 Finished compiler/backend/arm8/proofs                            17s 817MB
Dec 09 03:27:52 Starting compiler/backend/mips/proofs
Dec 09 03:28:12 Finished compiler/backend/mips/proofs                            19s   1GB
Dec 09 03:28:12 Starting compiler/backend/riscv/proofs
Dec 09 03:28:32 Finished compiler/backend/riscv/proofs                           19s   1GB
Dec 09 03:28:32 Starting compiler/backend/ag32/proofs
Dec 09 03:38:21 Finished compiler/backend/ag32/proofs                          9m48s   2GB
Dec 09 03:38:21 Starting compiler/proofs
Dec 09 03:40:01 Finished compiler/proofs                                       1m39s   3GB
Dec 09 03:40:01 Starting candle/set-theory
Dec 09 03:40:30 Finished candle/set-theory                                       28s 833MB
Dec 09 03:40:30 Starting candle/syntax-lib
Dec 09 03:40:40 Finished candle/syntax-lib                                       10s 668MB
Dec 09 03:40:41 Starting candle/standard/syntax
Dec 09 03:42:30 Finished candle/standard/syntax                                1m49s 883MB
Dec 09 03:42:30 Starting candle/standard/semantics
Dec 09 03:44:11 Finished candle/standard/semantics                             1m40s   1GB
Dec 09 03:44:11 Starting candle/standard/monadic
Dec 09 03:45:54 Finished candle/standard/monadic                               1m41s   1GB
Dec 09 03:45:54 Starting candle/standard/ml_kernel
Dec 09 03:50:17 Finished candle/standard/ml_kernel                             4m23s   5GB
Dec 09 03:50:17 Starting candle/standard/opentheory
Dec 09 03:59:51 Finished candle/standard/opentheory                            9m33s   3GB
Dec 09 03:59:51 Starting candle/standard/opentheory/compilation
Dec 09 04:30:29 Finished candle/standard/opentheory/compilation               30m37s  10GB
Dec 09 04:30:29 Starting candle/standard/opentheory/compilation/proofs
Dec 09 04:31:11 Finished candle/standard/opentheory/compilation/proofs           41s   2GB
Dec 09 04:31:11 Starting characteristic/examples
Dec 09 04:32:47 Finished characteristic/examples                               1m35s   2GB
Dec 09 04:32:47 Starting tutorial/solutions
Dec 09 04:46:36 Finished tutorial/solutions                                   13m48s   7GB
Dec 09 04:46:36 Starting translator/monadic/examples
Dec 09 04:49:38 Finished translator/monadic/examples                           3m01s   2GB
Dec 09 04:49:38 Starting examples
Dec 09 04:59:07 Finished examples                                              9m29s   3GB
Dec 09 04:59:08 Starting examples/compilation/x64
Dec 09 07:07:54 Finished examples/compilation/x64                           2h08m46s  12GB
Dec 09 07:07:55 Starting examples/compilation/x64/proofs
Dec 09 07:10:02 Finished examples/compilation/x64/proofs                       2m07s   2GB
Dec 09 07:10:02 Starting examples/compilation/ag32
Dec 09 07:40:16 Finished examples/compilation/ag32                            30m13s   6GB
Dec 09 07:40:16 Starting examples/compilation/ag32/proofs
Dec 09 07:41:08 Finished examples/compilation/ag32/proofs                        52s   2GB
Dec 09 07:41:09 Starting examples/cost
Dec 09 08:03:58 Finished examples/cost                                        22m49s   6GB
Dec 09 08:03:58 Starting examples/lrat_checker
Dec 09 08:07:27 Finished examples/lrat_checker                                 3m28s   3GB
Dec 09 08:07:27 Starting examples/lrat_checker/compilation
Dec 09 08:23:00 Finished examples/lrat_checker/compilation                    15m30s   7GB
Dec 09 08:23:00 Starting examples/lrat_checker/compilation/proofs
Dec 09 08:23:45 Finished examples/lrat_checker/compilation/proofs                44s   3GB
Dec 09 08:23:45 Starting examples/lrat_checker/array
Dec 09 08:30:18 Finished examples/lrat_checker/array                           6m33s   4GB
Dec 09 08:30:18 Starting examples/lrat_checker/array/compilation
Dec 09 08:44:07 Finished examples/lrat_checker/array/compilation              13m47s   6GB
Dec 09 08:44:07 Starting examples/lrat_checker/array/compilation/proofs
Dec 09 08:44:54 Finished examples/lrat_checker/array/compilation/proofs          47s   2GB
Dec 09 08:44:54 Starting translator/okasaki-examples
Dec 09 08:49:14 Finished translator/okasaki-examples                           4m19s   1GB
Dec 09 08:49:14 Starting translator/other-examples
Dec 09 08:49:55 Finished translator/other-examples                               40s   1GB
Dec 09 08:49:55 Starting compiler/parsing/tests
Dec 09 08:50:20 Finished compiler/parsing/tests                                  24s 535MB
Dec 09 08:50:20 Starting compiler/inference/tests
Dec 09 08:54:53 Finished compiler/inference/tests                              4m33s   3GB
Dec 09 08:54:53 Starting compiler/bootstrap/translation
Dec 09 11:45:50 Finished compiler/bootstrap/translation                     2h50m55s  38GB
Dec 09 11:45:50 Starting unverified/sexpr-bootstrap/x64/64
Dec 09 12:00:03 Finished unverified/sexpr-bootstrap/x64/64                    14m13s   2GB
Dec 09 12:00:03 Starting unverified/sexpr-bootstrap/x64/32
Dec 09 12:10:12 Finished unverified/sexpr-bootstrap/x64/32                    10m08s   6GB
Dec 09 12:10:12 Starting compiler/benchmarks
Dec 09 12:10:17 Finished compiler/benchmarks                                      4s  26MB
Dec 09 12:10:18 Starting compiler/bootstrap/compilation/x64/64
Dec 09 22:16:35 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)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
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/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
Starting work on README.md
Starting work on to_dataBootstrapTheory
README.md                                       real:    0s  user:    0s     OK
to_dataBootstrapTheory                          real: 3578s  user: 3551s     OK
Starting work on to_lab_x64BootstrapTheory
to_lab_x64BootstrapTheory                       real:  546m  user: 1320mFAIL<1>
      stack_to_lab (par) eval: runtime: 2h34m51s,    gctime: 14m31s,     systime: 55.4s.
      stack_to_lab (par) real: 39m33s
      stack_to_lab (par) size: 91076993
 Saved theorem _____ "stack_to_lab_thm"
 Saved theorem _____ "to_lab_x64Bootstrap_translator_state_thm"
 Exporting theory "to_lab_x64Bootstrap" ... error in quse /home/cake/oven/regression/cakeml-1117/compiler/bootstrap/compilation/x64/64/to_lab_x64BootstrapScript.sml : Io {cause = SysErr ("No space left on device", SOME ENOSPC), function = "output", name = "./to_lab_x64BootstrapTheory.dat"}
 error in load /home/cake/oven/regression/cakeml-1117/compiler/bootstrap/compilation/x64/64/to_lab_x64BootstrapScript : Io {cause = SysErr ("No space left on device", SOME ENOSPC), function = "output", name = "./to_lab_x64BootstrapTheory.dat"}
 
 Failure while writing theory!
 Uncaught exception: Io {cause = SysErr ("No space left on device", SOME ENOSPC), function = "output", name = "./to_lab_x64BootstrapTheory.dat"}