Job 1233

CakeML:4bc2df653478adec779906cf1820673fb1751a31
  Merge pull request #736 from CakeML/data-cost [May 20 05:27:48]
HOL:d0b4f135f9d0ca34127c775ce90771ace76482e8
  Fix a MULRELNORM instance: 2 * x = inv 2 * y should canonicalise [May 15 07:11:51]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

May 21 06:00:02 Claimed job
May 21 06:00:09 Reusing HOL
May 21 06:00:56 Starting developers
May 21 06:01:01 Finished developers                                               4s  86MB
May 21 06:01:01 Starting developers/bin
May 21 06:01:09 Finished developers/bin                                           7s   1GB
May 21 06:01:09 Starting semantics/ffi
May 21 06:01:19 Finished semantics/ffi                                           10s 230MB
May 21 06:01:20 Starting semantics
May 21 06:02:42 Finished semantics                                             1m22s 831MB
May 21 06:02:42 Starting semantics/proofs
May 21 06:06:15 Finished semantics/proofs                                      3m32s 970MB
May 21 06:06:15 Starting semantics/alt_semantics
May 21 06:06:23 Finished semantics/alt_semantics                                  8s 297MB
May 21 06:06:24 Starting semantics/alt_semantics/proofs
May 21 06:08:36 Finished semantics/alt_semantics/proofs                        2m12s 858MB
May 21 06:08:36 Starting basis/pure
May 21 06:09:27 Finished basis/pure                                              50s 667MB
May 21 06:09:27 Starting translator
May 21 06:12:08 Finished translator                                            2m40s   1GB
May 21 06:12:08 Starting compiler/parsing
May 21 06:13:21 Finished compiler/parsing                                      1m13s   1GB
May 21 06:13:21 Starting characteristic
May 21 06:19:29 Finished characteristic                                        6m06s   1GB
May 21 06:19:29 Starting translator/monadic
May 21 06:21:07 Finished translator/monadic                                    1m38s   1GB
May 21 06:21:07 Starting basis
May 21 06:54:50 Finished basis                                                33m42s  21GB
May 21 06:54:50 Starting compiler/inference
May 21 06:55:51 Finished compiler/inference                                    1m01s   1GB
May 21 06:55:52 Starting compiler/backend/reg_alloc
May 21 06:56:54 Finished compiler/backend/reg_alloc                            1m02s   1GB
May 21 06:56:55 Starting compiler/backend/gc
May 21 07:00:13 Finished compiler/backend/gc                                   3m18s   2GB
May 21 07:00:13 Starting compiler/backend
May 21 07:04:54 Finished compiler/backend                                      4m40s   3GB
May 21 07:04:54 Starting compiler/encoders/asm
May 21 07:05:16 Finished compiler/encoders/asm                                   22s 897MB
May 21 07:05:16 Starting compiler/encoders/x64
May 21 07:05:43 Finished compiler/encoders/x64                                   26s   1GB
May 21 07:05:43 Starting compiler/encoders/arm7
May 21 07:06:34 Finished compiler/encoders/arm7                                  50s 733MB
May 21 07:06:34 Starting compiler/encoders/arm8
May 21 07:06:48 Finished compiler/encoders/arm8                                  13s 849MB
May 21 07:06:48 Starting compiler/encoders/mips
May 21 07:07:06 Finished compiler/encoders/mips                                  17s   1GB
May 21 07:07:06 Starting compiler/encoders/riscv
May 21 07:07:21 Finished compiler/encoders/riscv                                 14s 854MB
May 21 07:07:21 Starting compiler/encoders/ag32
May 21 07:07:39 Finished compiler/encoders/ag32                                  17s 822MB
May 21 07:07:39 Starting compiler/backend/x64
May 21 07:07:57 Finished compiler/backend/x64                                    18s   1GB
May 21 07:07:58 Starting compiler/backend/arm7
May 21 07:08:18 Finished compiler/backend/arm7                                   20s   1GB
May 21 07:08:19 Starting compiler/backend/arm8
May 21 07:08:37 Finished compiler/backend/arm8                                   18s   1GB
May 21 07:08:37 Starting compiler/backend/mips
May 21 07:08:57 Finished compiler/backend/mips                                   19s   1GB
May 21 07:08:57 Starting compiler/backend/riscv
May 21 07:09:17 Finished compiler/backend/riscv                                  19s   1GB
May 21 07:09:17 Starting compiler/backend/ag32
May 21 07:10:29 Finished compiler/backend/ag32                                 1m12s   1GB
May 21 07:10:30 Starting compiler/parsing/proofs
May 21 07:16:30 Finished compiler/parsing/proofs                               5m59s 814MB
May 21 07:16:30 Starting compiler/inference/proofs
May 21 07:19:04 Finished compiler/inference/proofs                             2m34s   1GB
May 21 07:19:05 Starting compiler/backend/semantics
May 21 07:50:48 Finished compiler/backend/semantics                           31m42s   2GB
May 21 07:50:48 Starting compiler/backend/reg_alloc/proofs
May 21 07:54:32 Finished compiler/backend/reg_alloc/proofs                     3m44s 932MB
May 21 07:54:32 Starting compiler/backend/proofs
May 21 09:03:03 Finished compiler/backend/proofs                            1h08m30s  13GB
May 21 09:03:03 Starting compiler/encoders/x64/proofs
May 21 09:13:05 Finished compiler/encoders/x64/proofs                         10m01s   4GB
May 21 09:13:05 Starting compiler/encoders/arm7/proofs
May 21 09:26:46 Finished compiler/encoders/arm7/proofs                        13m40s   3GB
May 21 09:26:46 Starting compiler/encoders/arm8/proofs
May 21 09:33:36 Finished compiler/encoders/arm8/proofs                         6m50s   1GB
May 21 09:33:37 Starting compiler/encoders/mips/proofs
May 21 09:44:04 Finished compiler/encoders/mips/proofs                        10m27s   2GB
May 21 09:44:04 Starting compiler/encoders/riscv/proofs
May 21 09:53:11 Finished compiler/encoders/riscv/proofs                        9m07s   1GB
May 21 09:53:12 Starting compiler/encoders/ag32/proofs
May 21 09:55:55 Finished compiler/encoders/ag32/proofs                         2m42s 773MB
May 21 09:55:55 Starting compiler/backend/x64/proofs
May 21 09:56:14 Finished compiler/backend/x64/proofs                             19s 864MB
May 21 09:56:15 Starting compiler/backend/arm7/proofs
May 21 09:56:36 Finished compiler/backend/arm7/proofs                            20s   1GB
May 21 09:56:36 Starting compiler/backend/arm8/proofs
May 21 09:56:55 Finished compiler/backend/arm8/proofs                            18s 828MB
May 21 09:56:55 Starting compiler/backend/mips/proofs
May 21 09:57:16 Finished compiler/backend/mips/proofs                            20s   1GB
May 21 09:57:16 Starting compiler/backend/riscv/proofs
May 21 09:57:37 Finished compiler/backend/riscv/proofs                           21s   1GB
May 21 09:57:37 Starting compiler/backend/ag32/proofs
May 21 10:11:19 Finished compiler/backend/ag32/proofs                         13m40s   1GB
May 21 10:11:19 Starting compiler/proofs
May 21 10:12:50 Finished compiler/proofs                                       1m30s   3GB
May 21 10:12:50 Starting candle/set-theory
May 21 10:13:18 Finished candle/set-theory                                       28s   1GB
May 21 10:13:19 Starting candle/syntax-lib
May 21 10:13:30 Finished candle/syntax-lib                                       10s 690MB
May 21 10:13:30 Starting candle/standard/syntax
May 21 10:15:23 Finished candle/standard/syntax                                1m53s   1GB
May 21 10:15:23 Starting candle/standard/semantics
May 21 10:17:09 Finished candle/standard/semantics                             1m45s   1GB
May 21 10:17:09 Starting candle/standard/monadic
May 21 10:18:56 Finished candle/standard/monadic                               1m46s   1GB
May 21 10:18:56 Starting candle/standard/ml_kernel
May 21 10:24:33 Finished candle/standard/ml_kernel                             5m36s   4GB
May 21 10:24:33 Starting candle/standard/opentheory
May 21 10:33:54 Finished candle/standard/opentheory                            9m20s   4GB
May 21 10:33:54 Starting candle/standard/opentheory/compilation
May 21 11:05:24 Finished candle/standard/opentheory/compilation               31m29s  13GB
May 21 11:05:24 Starting candle/standard/opentheory/compilation/proofs
May 21 11:06:02 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
May 21 11:06:02 Starting candle/overloading/syntax
May 21 11:09:15 Finished candle/overloading/syntax                             3m12s   1GB
May 21 11:09:15 Starting candle/overloading/semantics
May 21 11:16:32 Finished candle/overloading/semantics                          7m16s   3GB
May 21 11:16:33 Starting characteristic/examples
May 21 11:17:49 Finished characteristic/examples                               1m15s   3GB
May 21 11:17:49 Starting tutorial/solutions
May 21 11:32:31 Finished tutorial/solutions                                   14m42s   6GB
May 21 11:32:31 Starting translator/monadic/examples
May 21 11:35:37 Finished translator/monadic/examples                           3m05s   2GB
May 21 11:35:37 Starting examples
May 21 11:44:04 Finished examples                                              8m26s   3GB
May 21 11:44:04 Starting examples/compilation/x64
May 21 14:00:22 Finished examples/compilation/x64                           2h16m18s  13GB
May 21 14:00:23 Starting examples/compilation/x64/proofs
May 21 14:01:57 Finished examples/compilation/x64/proofs                       1m33s   3GB
May 21 14:01:57 Starting examples/compilation/ag32
May 21 14:32:48 Finished examples/compilation/ag32                            30m51s   6GB
May 21 14:32:49 Starting examples/compilation/ag32/proofs
May 21 14:33:31 Finished examples/compilation/ag32/proofs                        42s   2GB
May 21 14:33:31 Starting examples/cost
May 21 15:23:10 Finished examples/cost                                        49m38s   5GB
May 21 15:23:10 Starting examples/lpr_checker
May 21 15:27:04 Finished examples/lpr_checker                                  3m53s   4GB
May 21 15:27:04 Starting examples/lpr_checker/compilation
May 21 15:44:27 Finished examples/lpr_checker/compilation                     17m22s   8GB
May 21 15:44:27 Starting examples/lpr_checker/compilation/proofs
May 21 15:45:04 Finished examples/lpr_checker/compilation/proofs                 37s   2GB
May 21 15:45:04 Starting examples/lpr_checker/array
May 21 15:55:40 Finished examples/lpr_checker/array                           10m35s   2GB
May 21 15:55:40 Starting examples/lpr_checker/array/compilation
May 21 16:14:34 Finished examples/lpr_checker/array/compilation               18m53s  10GB
May 21 16:14:34 Starting examples/lpr_checker/array/compilation/proofs
May 21 16:15:22 Finished examples/lpr_checker/array/compilation/proofs           47s   4GB
May 21 16:15:22 Starting translator/okasaki-examples
May 21 16:19:48 Finished translator/okasaki-examples                           4m25s   1GB
May 21 16:19:48 Starting translator/other-examples
May 21 16:20:30 Finished translator/other-examples                               41s   1GB
May 21 16:20:30 Starting compiler/parsing/tests
May 21 16:20:56 Finished compiler/parsing/tests                                  25s 659MB
May 21 16:20:56 Starting compiler/inference/tests
May 21 16:25:33 Finished compiler/inference/tests                              4m36s   5GB
May 21 16:25:33 Starting compiler/bootstrap/translation
May 21 19:14:07 Finished compiler/bootstrap/translation                     2h48m33s  44GB
May 21 19:14:07 Starting unverified/sexpr-bootstrap/x64/64
May 21 19:28:08 Finished unverified/sexpr-bootstrap/x64/64                    13m59s   5GB
May 21 19:28:08 Starting unverified/sexpr-bootstrap/x64/32
May 21 19:38:10 Finished unverified/sexpr-bootstrap/x64/32                    10m01s   7GB
May 21 19:38:10 Starting compiler/benchmarks
May 21 19:38:12 Finished compiler/benchmarks                                      1s  27MB
May 21 19:38:12 Starting compiler/bootstrap/compilation/x64/64
May 22 10:18:50 Finished compiler/bootstrap/compilation/x64/64             14h40m36s  64GB
May 22 10:18:50 Starting compiler/bootstrap/compilation/x64/64/proofs
May 22 10:22:01 Finished compiler/bootstrap/compilation/x64/64/proofs          3m10s  13GB
May 22 10:22:01 Starting compiler/bootstrap/compilation/x64/32
May 22 23:40:33 Finished compiler/bootstrap/compilation/x64/32             13h18m31s  64GB
May 22 23:40:33 Starting compiler/bootstrap/compilation/x64/32/proofs
May 22 23:43:40 Finished compiler/bootstrap/compilation/x64/32/proofs          3m06s  13GB
May 22 23:43:40 Starting compiler/bootstrap/compilation/ag32/32
May 23 00:41:14 FAILED: compiler/bootstrap/compilation/ag32/32
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/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
Starting work on README.md
Starting work on to_dataBootstrapTheory
README.md                                       real:    0s  user:    0s     OK
to_dataBootstrapTheory                          real: 3406s  user: 3388s     OK
Starting work on to_lab_ag32BootstrapTheory
to_lab_ag32BootstrapTheory                      real:   45s  user:   43sFAIL<1>
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/explorerProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/sexp_parserProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/to_word32ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/to_target32ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/arm7ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/ag32ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/compiler32ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/to_dataBootstrapTheory : Interrupt
 error in load /home/cake/oven/regression/cakeml-1233/compiler/bootstrap/compilation/ag32/32/to_lab_ag32BootstrapScript : Interrupt
 Uncaught exception: Interrupt