Job 1943

CakeML:099c12cd5cc72f05c5be3d73a4a72a8c7f076e54
  Fixes for name change abs_1_v --> abs_v [Jun 22 21:13:52]
#892 (double-type-new)
Merging into:fbd56dc0d32e0e8b24d8ea10dd77112eee529460
  Fix a bunch of real$abs --> realax$abs (also for min, max) [Jun 23 20:53:47]
HOL:3810cf53c6050c5b2748cb042415145bd842957f
  Make parsing in RealField properly independent of context [Jun 21 00:55:21]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jun 23 21:00:28 Claimed job
Jun 23 21:01:46 Reusing HOL
Jun 23 21:02:29 Starting developers
Jun 23 21:02:35 Finished developers                                               5s  96MB
Jun 23 21:02:35 Starting developers/bin
Jun 23 21:04:15 Finished developers/bin                                        1m39s   1GB
Jun 23 21:04:15 Starting semantics/ffi
Jun 23 21:04:26 Finished semantics/ffi                                           10s 213MB
Jun 23 21:04:27 Starting semantics
Jun 23 21:07:09 Finished semantics                                             2m42s   1GB
Jun 23 21:07:10 Starting semantics/proofs
Jun 23 21:14:38 Finished semantics/proofs                                      7m28s   1GB
Jun 23 21:14:38 Starting semantics/alt_semantics
Jun 23 21:15:09 Finished semantics/alt_semantics                                 30s 535MB
Jun 23 21:15:09 Starting semantics/alt_semantics/proofs
Jun 23 21:27:46 Finished semantics/alt_semantics/proofs                       12m36s   1GB
Jun 23 21:27:47 Starting basis/pure
Jun 23 21:28:58 Finished basis/pure                                            1m11s 881MB
Jun 23 21:28:59 Starting translator
Jun 23 21:32:59 Finished translator                                            3m59s   1GB
Jun 23 21:32:59 Starting compiler/parsing
Jun 23 21:34:28 Finished compiler/parsing                                      1m29s   3GB
Jun 23 21:34:29 Starting characteristic
Jun 23 21:41:51 Finished characteristic                                        7m20s   1GB
Jun 23 21:41:51 Starting translator/monadic
Jun 23 21:43:58 Finished translator/monadic                                    2m06s   1GB
Jun 23 21:43:59 Starting basis
Jun 23 22:39:26 Finished basis                                                55m26s  13GB
Jun 23 22:39:26 Starting compiler/inference
Jun 23 22:41:03 Finished compiler/inference                                    1m36s   2GB
Jun 23 22:41:03 Starting compiler/backend/reg_alloc
Jun 23 22:42:56 Finished compiler/backend/reg_alloc                            1m50s   1GB
Jun 23 22:42:56 Starting compiler/backend/gc
Jun 23 22:47:48 Finished compiler/backend/gc                                   4m52s   1GB
Jun 23 22:47:49 Starting compiler/backend
Jun 23 22:54:34 Finished compiler/backend                                      6m45s   3GB
Jun 23 22:54:34 Starting compiler/encoders/asm
Jun 23 22:55:07 Finished compiler/encoders/asm                                   32s 751MB
Jun 23 22:55:07 Starting compiler/encoders/x64
Jun 23 22:55:39 Finished compiler/encoders/x64                                   31s   1GB
Jun 23 22:55:39 Starting compiler/encoders/arm7
Jun 23 22:56:40 Finished compiler/encoders/arm7                                1m00s 809MB
Jun 23 22:56:41 Starting compiler/encoders/arm8
Jun 23 22:56:59 Finished compiler/encoders/arm8                                  18s   1GB
Jun 23 22:56:59 Starting compiler/encoders/arm8_asl
Jun 23 22:59:59 Finished compiler/encoders/arm8_asl                            2m59s   1GB
Jun 23 22:59:59 Starting compiler/encoders/mips
Jun 23 23:00:22 Finished compiler/encoders/mips                                  22s   1GB
Jun 23 23:00:22 Starting compiler/encoders/riscv
Jun 23 23:00:44 Finished compiler/encoders/riscv                                 21s 861MB
Jun 23 23:00:44 Starting compiler/encoders/ag32
Jun 23 23:01:08 Finished compiler/encoders/ag32                                  23s 838MB
Jun 23 23:01:08 Starting compiler/backend/x64
Jun 23 23:01:33 Finished compiler/backend/x64                                    24s   1GB
Jun 23 23:01:33 Starting compiler/backend/arm7
Jun 23 23:01:59 Finished compiler/backend/arm7                                   25s   1GB
Jun 23 23:01:59 Starting compiler/backend/arm8
Jun 23 23:02:24 Finished compiler/backend/arm8                                   24s   1GB
Jun 23 23:02:24 Starting compiler/backend/mips
Jun 23 23:02:48 Finished compiler/backend/mips                                   23s   1GB
Jun 23 23:02:48 Starting compiler/backend/riscv
Jun 23 23:03:13 Finished compiler/backend/riscv                                  24s   1GB
Jun 23 23:03:13 Starting compiler/backend/ag32
Jun 23 23:04:46 Finished compiler/backend/ag32                                 1m32s   1GB
Jun 23 23:04:47 Starting compiler/parsing/proofs
Jun 23 23:08:51 Finished compiler/parsing/proofs                               4m04s   1GB
Jun 23 23:08:51 Starting compiler/inference/proofs
Jun 23 23:11:48 Finished compiler/inference/proofs                             2m56s   1GB
Jun 23 23:11:48 Starting compiler/backend/semantics
Jun 23 23:42:12 Finished compiler/backend/semantics                           30m23s   2GB
Jun 23 23:42:12 Starting compiler/backend/reg_alloc/proofs
Jun 23 23:46:10 Finished compiler/backend/reg_alloc/proofs                     3m57s   1GB
Jun 23 23:46:10 Starting compiler/backend/proofs
Jun 24 00:48:41 Finished compiler/backend/proofs                            1h02m30s  16GB
Jun 24 00:48:41 Starting compiler/backend/serialiser
Jun 24 00:50:31 Finished compiler/backend/serialiser                           1m49s   1GB
Jun 24 00:50:31 Starting compiler/encoders/x64/proofs
Jun 24 01:00:52 Finished compiler/encoders/x64/proofs                         10m20s   5GB
Jun 24 01:00:52 Starting compiler/encoders/arm7/proofs
Jun 24 01:15:16 Finished compiler/encoders/arm7/proofs                        14m24s   3GB
Jun 24 01:15:17 Starting compiler/encoders/arm8/proofs
Jun 24 01:22:41 Finished compiler/encoders/arm8/proofs                         7m24s   1GB
Jun 24 01:22:41 Starting compiler/encoders/arm8_asl/proofs
Jun 24 01:39:18 Finished compiler/encoders/arm8_asl/proofs                    16m36s   1GB
Jun 24 01:39:18 Starting compiler/encoders/mips/proofs
Jun 24 01:50:30 Finished compiler/encoders/mips/proofs                        11m11s   1GB
Jun 24 01:50:30 Starting compiler/encoders/riscv/proofs
Jun 24 01:59:57 Finished compiler/encoders/riscv/proofs                        9m26s   1GB
Jun 24 01:59:57 Starting compiler/encoders/ag32/proofs
Jun 24 02:02:49 Finished compiler/encoders/ag32/proofs                         2m51s 651MB
Jun 24 02:02:50 Starting compiler/backend/x64/proofs
Jun 24 02:03:20 Finished compiler/backend/x64/proofs                             30s   1GB
Jun 24 02:03:20 Starting compiler/backend/arm7/proofs
Jun 24 02:03:52 Finished compiler/backend/arm7/proofs                            31s   1GB
Jun 24 02:03:52 Starting compiler/backend/arm8/proofs
Jun 24 02:04:23 Finished compiler/backend/arm8/proofs                            30s   1GB
Jun 24 02:04:24 Starting compiler/backend/arm8_asl
Jun 24 02:04:50 Finished compiler/backend/arm8_asl                               25s   1GB
Jun 24 02:04:50 Starting compiler/backend/mips/proofs
Jun 24 02:05:21 Finished compiler/backend/mips/proofs                            30s   1GB
Jun 24 02:05:21 Starting compiler/backend/riscv/proofs
Jun 24 02:05:51 Finished compiler/backend/riscv/proofs                           29s   1GB
Jun 24 02:05:51 Starting compiler/backend/ag32/proofs
Jun 24 02:20:30 Finished compiler/backend/ag32/proofs                         14m38s   2GB
Jun 24 02:20:30 Starting compiler/proofs
Jun 24 02:22:51 Finished compiler/proofs                                       2m21s   3GB
Jun 24 02:22:52 Starting candle/set-theory
Jun 24 02:23:28 Finished candle/set-theory                                       36s   1GB
Jun 24 02:23:29 Starting candle/syntax-lib
Jun 24 02:23:43 Finished candle/syntax-lib                                       13s 802MB
Jun 24 02:23:43 Starting candle/standard/syntax
Jun 24 02:25:53 Finished candle/standard/syntax                                2m09s   1GB
Jun 24 02:25:53 Starting candle/standard/semantics
Jun 24 02:27:50 Finished candle/standard/semantics                             1m56s   1GB
Jun 24 02:27:50 Starting candle/standard/monadic
Jun 24 02:29:55 Finished candle/standard/monadic                               2m04s   1GB
Jun 24 02:29:55 Starting candle/standard/ml_kernel
Jun 24 02:37:00 Finished candle/standard/ml_kernel                             7m04s   2GB
Jun 24 02:37:00 Starting candle/overloading/syntax
Jun 24 02:40:30 Finished candle/overloading/syntax                             3m29s   1GB
Jun 24 02:40:30 Starting candle/overloading/semantics
Jun 24 02:52:42 Finished candle/overloading/semantics                         12m11s   4GB
Jun 24 02:52:42 Starting candle/overloading/monadic
Jun 24 02:55:29 Finished candle/overloading/monadic                            2m46s   1GB
Jun 24 02:55:29 Starting candle/overloading/ml_kernel
Jun 24 03:03:36 Finished candle/overloading/ml_kernel                          8m06s   3GB
Jun 24 03:03:36 Starting candle/overloading/ml_checker
Jun 24 03:06:08 Finished candle/overloading/ml_checker                         2m31s   2GB
Jun 24 03:06:08 Starting candle/prover
Jun 24 03:17:33 Finished candle/prover                                        11m25s   2GB
Jun 24 03:17:34 Starting pancake
Jun 24 03:21:41 Finished pancake                                               4m06s   3GB
Jun 24 03:21:41 Starting pancake/ffi
Jun 24 03:21:42 Finished pancake/ffi                                              0s  16MB
Jun 24 03:21:42 Starting pancake/semantics
Jun 24 03:24:32 Finished pancake/semantics                                     2m49s   1GB
Jun 24 03:24:32 Starting pancake/proofs
Jun 24 03:37:36 Finished pancake/proofs                                       13m03s   6GB
Jun 24 03:37:36 Starting characteristic/examples
Jun 24 03:39:05 Finished characteristic/examples                               1m29s   2GB
Jun 24 03:39:06 Starting tutorial/solutions
Jun 24 03:56:08 Finished tutorial/solutions                                   17m02s   8GB
Jun 24 03:56:09 Starting translator/monadic/examples
Jun 24 04:00:22 Finished translator/monadic/examples                           4m13s   2GB
Jun 24 04:00:23 Starting examples
Jun 24 04:11:32 Finished examples                                             11m08s   3GB
Jun 24 04:11:32 Starting examples/compilation/x64
Jun 24 06:20:49 Finished examples/compilation/x64                           2h09m16s  13GB
Jun 24 06:20:49 Starting examples/compilation/x64/proofs
Jun 24 06:23:22 Finished examples/compilation/x64/proofs                       2m32s   3GB
Jun 24 06:23:23 Starting examples/compilation/ag32
Jun 24 06:58:10 Finished examples/compilation/ag32                            34m47s   6GB
Jun 24 06:58:10 Starting examples/compilation/ag32/proofs
Jun 24 06:59:10 Finished examples/compilation/ag32/proofs                        59s   3GB
Jun 24 06:59:10 Starting examples/lpr_checker
Jun 24 07:00:15 Finished examples/lpr_checker                                  1m04s 966MB
Jun 24 07:00:15 Starting examples/lpr_checker/array
Jun 24 07:36:07 Finished examples/lpr_checker/array                           35m51s   5GB
Jun 24 07:36:07 Starting examples/lpr_checker/array/compilation
Jun 24 08:18:06 Finished examples/lpr_checker/array/compilation               41m58s  24GB
Jun 24 08:18:06 Starting examples/lpr_checker/array/compilation/proofs
Jun 24 08:19:33 Finished examples/lpr_checker/array/compilation/proofs         1m27s   5GB
Jun 24 08:19:34 Starting examples/opentheory
Jun 27 08:15:36 Resuming examples/opentheory
Jun 27 08:25:08 Finished examples/opentheory                                   9m30s   5GB
Jun 27 08:25:08 Starting examples/opentheory
Jun 27 08:25:10 Finished examples/opentheory                                      1s  24MB
Jun 27 08:25:10 Starting examples/opentheory/compilation
Jun 27 09:04:55 Finished examples/opentheory/compilation                      39m45s  23GB
Jun 27 09:04:55 Starting examples/opentheory/compilation/proofs
Jun 27 09:06:10 Finished examples/opentheory/compilation/proofs                1m14s   3GB
Jun 27 09:06:10 Starting examples/opentheory/compilation/ag32
Jun 27 09:41:35 Finished examples/opentheory/compilation/ag32                 35m23s  25GB
Jun 27 09:41:35 Starting examples/opentheory/compilation/ag32/proofs
Jun 27 09:43:27 Finished examples/opentheory/compilation/ag32/proofs           1m51s   5GB
Jun 27 09:43:27 Starting examples/sat_encodings
Jun 27 09:45:34 Finished examples/sat_encodings                                2m06s 873MB
Jun 27 09:45:34 Starting examples/sat_encodings/case_studies
Jun 27 09:47:26 Finished examples/sat_encodings/case_studies                   1m52s 721MB
Jun 27 09:47:27 Starting examples/sat_encodings/translation
Jun 27 09:53:38 Finished examples/sat_encodings/translation                    6m11s   3GB
Jun 27 09:53:39 Starting examples/sat_encodings/translation/compilation
Jun 27 10:45:54 Finished examples/sat_encodings/translation/compilation       52m14s  20GB
Jun 27 10:45:54 Starting examples/deflate
Jun 27 10:46:55 Finished examples/deflate                                      1m01s 965MB
Jun 27 10:46:55 Starting examples/deflate/translation
Jun 27 10:48:37 Finished examples/deflate/translation                          1m40s   3GB
Jun 27 10:48:37 Starting examples/deflate/translation/compilation
Jun 27 11:12:08 Finished examples/deflate/translation/compilation             23m30s  15GB
Jun 27 11:12:08 Starting translator/okasaki-examples
Jun 27 11:17:36 Finished translator/okasaki-examples                           5m27s   1GB
Jun 27 11:17:36 Starting translator/other-examples
Jun 27 11:18:32 Finished translator/other-examples                               55s   1GB
Jun 27 11:18:32 Starting compiler/parsing/tests
Jun 27 11:19:03 Finished compiler/parsing/tests                                  31s 619MB
Jun 27 11:19:03 Starting compiler/inference/tests
Jun 27 11:27:54 Finished compiler/inference/tests                              8m49s   5GB
Jun 27 11:27:54 Starting compiler/printing/test
Jun 27 11:31:53 Finished compiler/printing/test                                3m58s   3GB
Jun 27 11:31:53 Starting icing/flover
Jun 27 12:22:38 Finished icing/flover                                         50m43s   1GB
Jun 27 12:22:38 Starting icing/
Jun 27 13:39:55 Finished icing/                                             1h17m15s   6GB
Jun 27 13:39:55 Starting icing/examples
Jun 27 13:41:39 Finished icing/examples                                        1m43s   5GB
Jun 27 13:41:39 Starting compiler/repl
Jun 27 13:55:34 Finished compiler/repl                                        13m54s   6GB
Jun 27 13:55:34 Starting compiler/bootstrap/translation
Jun 27 18:29:35 Finished compiler/bootstrap/translation                     4h34m00s  39GB
Jun 27 18:29:36 Starting unverified/sexpr-bootstrap/x64/64
Jun 27 18:40:27 Finished unverified/sexpr-bootstrap/x64/64                    10m50s  11GB
Jun 27 18:40:27 Starting unverified/sexpr-bootstrap/x64/32
Jun 27 18:49:25 Finished unverified/sexpr-bootstrap/x64/32                     8m57s  10GB
Jun 27 18:49:25 Starting compiler/benchmarks
Jun 27 18:49:28 Finished compiler/benchmarks                                      2s  32MB
Jun 27 18:49:29 Starting compiler/bootstrap/compilation/x64/64
Jun 27 18:50:44 FAILED: compiler/bootstrap/compilation/x64/64
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/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
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
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanned 90 directories
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                                           (0s)     OK
cake-sexpr-32                                                      (67s)FAIL<1>
 Run out of store - interrupting threads
 error in quse /home/cake/oven/regression/cakeml-1943/compiler/bootstrap/translation/sexp_parserProgTheory.sml : 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-1943/compiler/bootstrap/compilation/x64/64/sexprBootstrap32Script : Interrupt
 Uncaught exception: Interrupt
cake-sexpr-64                                                      (67s)MKILLED
to_dataBootstrapTheory                                             (68s)MKILLED