Job 1881

CakeML:4c966fba47c4550a982b3512dc6a08cc1ee4f7da
  Translate new mlmap functions [Apr 12 08:48:57]
#881 (mlmap-additions)
Merging into:c2be5d64270ec1538eded2eed51612b7708c5d50
  Merge pull request #872 from talsewell/printing-type-check-each-dec [Apr 26 09:47:56]
HOL:a161807cb4e0ea25b8781f3307a590b78703da6f
  Fix some overlong lines [Apr 20 03:46:17]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 29 17:08:33 Claimed job
Apr 29 17:08:38 Reusing HOL
Apr 29 17:09:18 Starting developers
Apr 29 17:09:23 Finished developers                                               4s 113MB
Apr 29 17:09:23 Starting developers/bin
Apr 29 17:09:30 Finished developers/bin                                           6s   1GB
Apr 29 17:09:30 Starting semantics/ffi
Apr 29 17:09:42 Finished semantics/ffi                                           11s 207MB
Apr 29 17:09:42 Starting semantics
Apr 29 17:11:50 Finished semantics                                             2m07s   1GB
Apr 29 17:11:50 Starting semantics/proofs
Apr 29 17:16:16 Finished semantics/proofs                                      4m25s   3GB
Apr 29 17:16:16 Starting semantics/alt_semantics
Apr 29 17:16:42 Finished semantics/alt_semantics                                 25s 561MB
Apr 29 17:16:42 Starting semantics/alt_semantics/proofs
Apr 29 17:19:54 Finished semantics/alt_semantics/proofs                        3m11s   1GB
Apr 29 17:19:55 Starting basis/pure
Apr 29 17:21:03 Finished basis/pure                                            1m08s   1GB
Apr 29 17:21:03 Starting translator
Apr 29 17:24:13 Finished translator                                            3m09s   1GB
Apr 29 17:24:14 Starting compiler/parsing
Apr 29 17:25:35 Finished compiler/parsing                                      1m21s   2GB
Apr 29 17:25:35 Starting characteristic
Apr 29 17:32:20 Finished characteristic                                        6m44s   2GB
Apr 29 17:32:21 Starting translator/monadic
Apr 29 17:34:20 Finished translator/monadic                                    1m59s   1GB
Apr 29 17:34:21 Starting basis
Apr 29 18:24:49 Finished basis                                                50m26s  13GB
Apr 29 18:24:50 Starting compiler/inference
Apr 29 18:26:16 Finished compiler/inference                                    1m25s   1GB
Apr 29 18:26:16 Starting compiler/backend/reg_alloc
Apr 29 18:28:05 Finished compiler/backend/reg_alloc                            1m48s   1GB
Apr 29 18:28:05 Starting compiler/backend/gc
Apr 29 18:32:45 Finished compiler/backend/gc                                   4m39s   1GB
Apr 29 18:32:45 Starting compiler/backend
Apr 29 18:38:49 Finished compiler/backend                                      6m03s   2GB
Apr 29 18:38:49 Starting compiler/encoders/asm
Apr 29 18:39:21 Finished compiler/encoders/asm                                   31s 948MB
Apr 29 18:39:21 Starting compiler/encoders/x64
Apr 29 18:39:53 Finished compiler/encoders/x64                                   31s   1GB
Apr 29 18:39:53 Starting compiler/encoders/arm7
Apr 29 18:40:52 Finished compiler/encoders/arm7                                  58s 788MB
Apr 29 18:40:52 Starting compiler/encoders/arm8
Apr 29 18:41:10 Finished compiler/encoders/arm8                                  17s 593MB
Apr 29 18:41:11 Starting compiler/encoders/arm8_asl
Apr 29 18:44:08 Finished compiler/encoders/arm8_asl                            2m56s   1GB
Apr 29 18:44:08 Starting compiler/encoders/mips
Apr 29 18:44:31 Finished compiler/encoders/mips                                  23s 978MB
Apr 29 18:44:32 Starting compiler/encoders/riscv
Apr 29 18:44:52 Finished compiler/encoders/riscv                                 20s 830MB
Apr 29 18:44:53 Starting compiler/encoders/ag32
Apr 29 18:45:16 Finished compiler/encoders/ag32                                  22s 732MB
Apr 29 18:45:16 Starting compiler/backend/x64
Apr 29 18:45:39 Finished compiler/backend/x64                                    23s   1GB
Apr 29 18:45:39 Starting compiler/backend/arm7
Apr 29 18:46:05 Finished compiler/backend/arm7                                   25s   1GB
Apr 29 18:46:05 Starting compiler/backend/arm8
Apr 29 18:46:28 Finished compiler/backend/arm8                                   22s   1GB
Apr 29 18:46:28 Starting compiler/backend/mips
Apr 29 18:46:51 Finished compiler/backend/mips                                   23s   1GB
Apr 29 18:46:52 Starting compiler/backend/riscv
Apr 29 18:47:15 Finished compiler/backend/riscv                                  23s   1GB
Apr 29 18:47:15 Starting compiler/backend/ag32
Apr 29 18:48:45 Finished compiler/backend/ag32                                 1m29s   1GB
Apr 29 18:48:46 Starting compiler/parsing/proofs
Apr 29 18:52:51 Finished compiler/parsing/proofs                               4m05s   1GB
Apr 29 18:52:51 Starting compiler/inference/proofs
Apr 29 18:55:35 Finished compiler/inference/proofs                             2m43s   1GB
Apr 29 18:55:35 Starting compiler/backend/semantics
Apr 29 19:28:56 Finished compiler/backend/semantics                           33m21s   2GB
Apr 29 19:28:57 Starting compiler/backend/reg_alloc/proofs
Apr 29 19:32:51 Finished compiler/backend/reg_alloc/proofs                     3m54s   1GB
Apr 29 19:32:52 Starting compiler/backend/proofs
Apr 29 20:29:55 Finished compiler/backend/proofs                              57m02s  18GB
Apr 29 20:29:55 Starting compiler/backend/serialiser
Apr 29 20:31:39 Finished compiler/backend/serialiser                           1m43s   1GB
Apr 29 20:31:39 Starting compiler/encoders/x64/proofs
Apr 29 20:41:55 Finished compiler/encoders/x64/proofs                         10m15s   4GB
Apr 29 20:41:55 Starting compiler/encoders/arm7/proofs
Apr 29 20:55:55 Finished compiler/encoders/arm7/proofs                        14m00s   3GB
Apr 29 20:55:56 Starting compiler/encoders/arm8/proofs
Apr 29 21:03:12 Finished compiler/encoders/arm8/proofs                         7m16s   1GB
Apr 29 21:03:13 Starting compiler/encoders/arm8_asl/proofs
Apr 29 21:19:37 Finished compiler/encoders/arm8_asl/proofs                    16m23s   2GB
Apr 29 21:19:37 Starting compiler/encoders/mips/proofs
Apr 29 21:30:15 Finished compiler/encoders/mips/proofs                        10m36s   2GB
Apr 29 21:30:15 Starting compiler/encoders/riscv/proofs
Apr 29 21:39:38 Finished compiler/encoders/riscv/proofs                        9m22s   1GB
Apr 29 21:39:38 Starting compiler/encoders/ag32/proofs
Apr 29 21:42:26 Finished compiler/encoders/ag32/proofs                         2m47s 686MB
Apr 29 21:42:26 Starting compiler/backend/x64/proofs
Apr 29 21:42:55 Finished compiler/backend/x64/proofs                             29s   1GB
Apr 29 21:42:56 Starting compiler/backend/arm7/proofs
Apr 29 21:43:27 Finished compiler/backend/arm7/proofs                            30s   1GB
Apr 29 21:43:27 Starting compiler/backend/arm8/proofs
Apr 29 21:43:57 Finished compiler/backend/arm8/proofs                            30s   1GB
Apr 29 21:43:57 Starting compiler/backend/arm8_asl
Apr 29 21:44:22 Finished compiler/backend/arm8_asl                               24s   1GB
Apr 29 21:44:22 Starting compiler/backend/mips/proofs
Apr 29 21:44:51 Finished compiler/backend/mips/proofs                            28s   1GB
Apr 29 21:44:51 Starting compiler/backend/riscv/proofs
Apr 29 21:45:21 Finished compiler/backend/riscv/proofs                           29s   1GB
Apr 29 21:45:22 Starting compiler/backend/ag32/proofs
Apr 29 21:59:04 Finished compiler/backend/ag32/proofs                         13m42s   2GB
Apr 29 21:59:05 Starting compiler/proofs
Apr 29 22:01:21 Finished compiler/proofs                                       2m15s   3GB
Apr 29 22:01:21 Starting candle/set-theory
Apr 29 22:01:58 Finished candle/set-theory                                       36s 895MB
Apr 29 22:01:58 Starting candle/syntax-lib
Apr 29 22:02:12 Finished candle/syntax-lib                                       13s 657MB
Apr 29 22:02:12 Starting candle/standard/syntax
Apr 29 22:04:21 Finished candle/standard/syntax                                2m09s 998MB
Apr 29 22:04:22 Starting candle/standard/semantics
Apr 29 22:06:16 Finished candle/standard/semantics                             1m54s   1GB
Apr 29 22:06:17 Starting candle/standard/monadic
Apr 29 22:08:17 Finished candle/standard/monadic                               1m59s   1GB
Apr 29 22:08:17 Starting candle/standard/ml_kernel
Apr 29 22:14:56 Finished candle/standard/ml_kernel                             6m38s   3GB
Apr 29 22:14:56 Starting candle/overloading/syntax
Apr 29 22:18:22 Finished candle/overloading/syntax                             3m25s   1GB
Apr 29 22:18:22 Starting candle/overloading/semantics
Apr 29 22:30:37 Finished candle/overloading/semantics                         12m12s   4GB
Apr 29 22:30:37 Starting candle/overloading/monadic
Apr 29 22:33:21 Finished candle/overloading/monadic                            2m43s   2GB
Apr 29 22:33:21 Starting candle/overloading/ml_kernel
Apr 29 22:41:06 Finished candle/overloading/ml_kernel                          7m44s   3GB
Apr 29 22:41:06 Starting candle/overloading/ml_checker
Apr 29 22:43:37 Finished candle/overloading/ml_checker                         2m31s   3GB
Apr 29 22:43:38 Starting candle/prover
Apr 29 22:52:22 Finished candle/prover                                         8m44s   2GB
Apr 29 22:52:22 Starting pancake
Apr 29 22:56:16 Finished pancake                                               3m53s   3GB
Apr 29 22:56:17 Starting pancake/ffi
Apr 29 22:56:18 Finished pancake/ffi                                              0s  19MB
Apr 29 22:56:18 Starting pancake/semantics
Apr 29 22:59:01 Finished pancake/semantics                                     2m42s   1GB
Apr 29 22:59:01 Starting pancake/proofs
Apr 29 23:12:00 Finished pancake/proofs                                       12m58s   5GB
Apr 29 23:12:00 Starting characteristic/examples
Apr 29 23:13:28 Finished characteristic/examples                               1m28s   3GB
Apr 29 23:13:28 Starting tutorial/solutions
Apr 29 23:31:01 Finished tutorial/solutions                                   17m32s   8GB
Apr 29 23:31:01 Starting translator/monadic/examples
Apr 29 23:35:07 Finished translator/monadic/examples                           4m05s   3GB
Apr 29 23:35:07 Starting examples
Apr 29 23:45:35 Finished examples                                             10m27s   3GB
Apr 29 23:45:35 Starting examples/compilation/x64
Apr 30 02:25:24 Finished examples/compilation/x64                           2h39m48s  19GB
Apr 30 02:25:24 Starting examples/compilation/x64/proofs
Apr 30 02:27:57 Finished examples/compilation/x64/proofs                       2m32s   3GB
Apr 30 02:27:57 Starting examples/compilation/ag32
Apr 30 03:04:50 Finished examples/compilation/ag32                            36m53s   8GB
Apr 30 03:04:50 Starting examples/compilation/ag32/proofs
Apr 30 03:05:50 Finished examples/compilation/ag32/proofs                        59s   3GB
Apr 30 03:05:50 Starting examples/cost
Apr 30 04:07:00 Finished examples/cost                                      1h01m08s   8GB
Apr 30 04:07:00 Starting examples/lpr_checker
Apr 30 04:08:04 Finished examples/lpr_checker                                  1m04s 945MB
Apr 30 04:08:04 Starting examples/lpr_checker/array
Apr 30 04:39:29 Finished examples/lpr_checker/array                           31m24s   5GB
Apr 30 04:39:29 Starting examples/lpr_checker/array/compilation
Apr 30 06:10:24 Finished examples/lpr_checker/array/compilation             1h30m54s  45GB
Apr 30 06:10:24 Starting examples/lpr_checker/array/compilation/proofs
Apr 30 06:11:55 Finished examples/lpr_checker/array/compilation/proofs         1m30s   6GB
Apr 30 06:11:55 Starting examples/opentheory
Apr 30 06:22:38 Finished examples/opentheory                                  10m43s   6GB
Apr 30 06:22:38 Starting examples/opentheory
Apr 30 06:22:40 Finished examples/opentheory                                      1s  28MB
Apr 30 06:22:40 Starting examples/opentheory/compilation
Apr 30 07:05:49 Finished examples/opentheory/compilation                      43m08s  26GB
Apr 30 07:05:49 Starting examples/opentheory/compilation/proofs
Apr 30 07:06:49 Finished examples/opentheory/compilation/proofs                  59s   4GB
Apr 30 07:06:50 Starting examples/opentheory/compilation/ag32
Apr 30 07:47:08 Finished examples/opentheory/compilation/ag32                 40m16s  21GB
Apr 30 07:47:08 Starting examples/opentheory/compilation/ag32/proofs
Apr 30 07:49:02 Finished examples/opentheory/compilation/ag32/proofs           1m53s   6GB
Apr 30 07:49:02 Starting examples/sat_encodings
Apr 30 07:51:10 Finished examples/sat_encodings                                2m07s 834MB
Apr 30 07:51:10 Starting examples/sat_encodings/case_studies
Apr 30 07:53:03 Finished examples/sat_encodings/case_studies                   1m52s 766MB
Apr 30 07:53:03 Starting examples/sat_encodings/translation
Apr 30 07:59:10 Finished examples/sat_encodings/translation                    6m06s   5GB
Apr 30 07:59:10 Starting examples/sat_encodings/translation/compilation
Apr 30 08:54:08 Finished examples/sat_encodings/translation/compilation       54m57s  20GB
Apr 30 08:54:08 Starting translator/okasaki-examples
Apr 30 08:59:10 Finished translator/okasaki-examples                           5m01s   2GB
Apr 30 08:59:10 Starting translator/other-examples
Apr 30 09:01:18 Finished translator/other-examples                             2m07s   1GB
Apr 30 09:01:18 Starting compiler/parsing/tests
Apr 30 09:01:50 Finished compiler/parsing/tests                                  32s 590MB
Apr 30 09:01:50 Starting compiler/inference/tests
Apr 30 09:10:30 Finished compiler/inference/tests                              8m39s   5GB
Apr 30 09:10:30 Starting compiler/printing/test
Apr 30 09:14:26 Finished compiler/printing/test                                3m55s   2GB
Apr 30 09:14:26 Starting compiler/repl
Apr 30 09:28:04 Finished compiler/repl                                        13m37s   7GB
Apr 30 09:28:04 Starting compiler/bootstrap/translation
Apr 30 13:41:47 Finished compiler/bootstrap/translation                     4h13m41s  41GB
Apr 30 13:41:47 Starting unverified/sexpr-bootstrap/x64/64
Apr 30 13:52:32 Finished unverified/sexpr-bootstrap/x64/64                    10m44s  12GB
Apr 30 13:52:32 Starting unverified/sexpr-bootstrap/x64/32
Apr 30 14:01:31 Finished unverified/sexpr-bootstrap/x64/32                     8m58s  10GB
Apr 30 14:01:31 Starting compiler/benchmarks
Apr 30 14:01:34 Finished compiler/benchmarks                                      2s  35MB
Apr 30 14:01:34 Starting compiler/bootstrap/compilation/x64/64
May 01 12:54:40 Finished compiler/bootstrap/compilation/x64/64             22h53m06s  64GB
May 01 12:54:41 Starting compiler/bootstrap/compilation/x64/64/proofs
May 01 13:16:59 Finished compiler/bootstrap/compilation/x64/64/proofs         22m18s  28GB
May 01 13:16:59 Starting compiler/bootstrap/compilation/x64/32
May 01 13:18:07 FAILED: compiler/bootstrap/compilation/x64/32
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
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)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
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/algorithms
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
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/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel/lisp
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanned 89 directories
Starting work on README.md
Starting work on to_dataBootstrapTheory
README.md                                                           (0s)     OK
to_dataBootstrapTheory                                             (61s)FAIL<1>
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/explorerProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/decodeProgTheory : 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 /home/cake/oven/regression/cakeml-1881/compiler/bootstrap/compilation/x64/32/to_dataBootstrapScript : Interrupt
 Uncaught exception: Interrupt