Job 1872

CakeML:7b46a34107e23323ef446bba5a66643c003b87bf
  Fix test for translation-themed changes [Apr 21 11:56:54]
#872 (printing-type-check-each-dec)
Merging into:915403669818aaaea2c42cd400fad0542de3fa99
  Merge pull request #878 from CakeML/array-appi-fix [Apr 20 08:36:39]
HOL:cb44cc2412d08a2baf1dd127ba6dc5f565e2834b
  "orthogonal edge routing" style of core theory hierarchy graph [Apr 14 03:45:39]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 22 03:00:05 Claimed job
Apr 22 03:00:07 Reusing HOL
Apr 22 03:01:00 Starting developers
Apr 22 03:01:05 Finished developers                                               5s  95MB
Apr 22 03:01:05 Starting developers/bin
Apr 22 03:01:15 Finished developers/bin                                           9s   1GB
Apr 22 03:01:16 Starting semantics/ffi
Apr 22 03:01:31 Finished semantics/ffi                                           15s 181MB
Apr 22 03:01:31 Starting semantics
Apr 22 03:03:59 Finished semantics                                             2m27s   1GB
Apr 22 03:03:59 Starting semantics/proofs
Apr 22 03:10:35 Finished semantics/proofs                                      6m35s   1GB
Apr 22 03:10:35 Starting semantics/alt_semantics
Apr 22 03:11:06 Finished semantics/alt_semantics                                 30s 490MB
Apr 22 03:11:06 Starting semantics/alt_semantics/proofs
Apr 22 03:15:02 Finished semantics/alt_semantics/proofs                        3m55s 728MB
Apr 22 03:15:02 Starting basis/pure
Apr 22 03:16:27 Finished basis/pure                                            1m25s 754MB
Apr 22 03:16:28 Starting translator
Apr 22 03:20:39 Finished translator                                            4m11s 755MB
Apr 22 03:20:40 Starting compiler/parsing
Apr 22 03:22:43 Finished compiler/parsing                                      2m02s 678MB
Apr 22 03:22:43 Starting characteristic
Apr 22 03:31:18 Finished characteristic                                        8m34s 884MB
Apr 22 03:31:18 Starting translator/monadic
Apr 22 03:34:09 Finished translator/monadic                                    2m50s 628MB
Apr 22 03:34:09 Starting basis
Apr 22 04:39:46 Finished basis                                              1h05m33s   1GB
Apr 22 04:39:46 Starting compiler/inference
Apr 22 04:41:38 Finished compiler/inference                                    1m51s 908MB
Apr 22 04:41:38 Starting compiler/backend/reg_alloc
Apr 22 04:43:43 Finished compiler/backend/reg_alloc                            2m04s   1GB
Apr 22 04:43:44 Starting compiler/backend/gc
Apr 22 04:49:51 Finished compiler/backend/gc                                   6m06s   1GB
Apr 22 04:49:51 Starting compiler/backend
Apr 22 04:58:35 Finished compiler/backend                                      8m43s   1GB
Apr 22 04:58:35 Starting compiler/encoders/asm
Apr 22 04:59:19 Finished compiler/encoders/asm                                   43s 877MB
Apr 22 04:59:19 Starting compiler/encoders/x64
Apr 22 05:00:00 Finished compiler/encoders/x64                                   38s 867MB
Apr 22 05:00:00 Starting compiler/encoders/arm7
Apr 22 05:01:09 Finished compiler/encoders/arm7                                1m09s 720MB
Apr 22 05:01:10 Starting compiler/encoders/arm8
Apr 22 05:01:33 Finished compiler/encoders/arm8                                  23s 328MB
Apr 22 05:01:34 Starting compiler/encoders/arm8_asl
Apr 22 05:04:58 Finished compiler/encoders/arm8_asl                            3m24s 542MB
Apr 22 05:04:58 Starting compiler/encoders/mips
Apr 22 05:05:24 Finished compiler/encoders/mips                                  25s 948MB
Apr 22 05:05:24 Starting compiler/encoders/riscv
Apr 22 05:05:55 Finished compiler/encoders/riscv                                 30s 415MB
Apr 22 05:05:55 Starting compiler/encoders/ag32
Apr 22 05:06:19 Finished compiler/encoders/ag32                                  24s 696MB
Apr 22 05:06:20 Starting compiler/backend/x64
Apr 22 05:06:51 Finished compiler/backend/x64                                    30s 541MB
Apr 22 05:06:51 Starting compiler/backend/arm7
Apr 22 05:07:27 Finished compiler/backend/arm7                                   36s 749MB
Apr 22 05:07:28 Starting compiler/backend/arm8
Apr 22 05:08:03 Finished compiler/backend/arm8                                   34s 675MB
Apr 22 05:08:03 Starting compiler/backend/mips
Apr 22 05:08:37 Finished compiler/backend/mips                                   33s 699MB
Apr 22 05:08:37 Starting compiler/backend/riscv
Apr 22 05:09:06 Finished compiler/backend/riscv                                  28s 710MB
Apr 22 05:09:06 Starting compiler/backend/ag32
Apr 22 05:10:51 Finished compiler/backend/ag32                                 1m44s 636MB
Apr 22 05:10:51 Starting compiler/parsing/proofs
Apr 22 05:15:51 Finished compiler/parsing/proofs                               5m00s 683MB
Apr 22 05:15:52 Starting compiler/inference/proofs
Apr 22 05:19:19 Finished compiler/inference/proofs                             3m27s 718MB
Apr 22 05:19:20 Starting compiler/backend/semantics
Apr 22 05:59:26 Finished compiler/backend/semantics                           40m06s 921MB
Apr 22 05:59:26 Starting compiler/backend/reg_alloc/proofs
Apr 22 06:04:04 Finished compiler/backend/reg_alloc/proofs                     4m35s 600MB
Apr 22 06:04:05 Starting compiler/backend/proofs
Apr 22 07:21:29 Finished compiler/backend/proofs                            1h17m23s   5GB
Apr 22 07:21:29 Starting compiler/backend/serialiser
Apr 22 07:23:55 Finished compiler/backend/serialiser                           2m25s 823MB
Apr 22 07:23:56 Starting compiler/encoders/x64/proofs
Apr 22 07:36:42 Finished compiler/encoders/x64/proofs                         12m46s   1GB
Apr 22 07:36:42 Starting compiler/encoders/arm7/proofs
Apr 22 07:53:54 Finished compiler/encoders/arm7/proofs                        17m11s   1GB
Apr 22 07:53:54 Starting compiler/encoders/arm8/proofs
Apr 22 08:02:20 Finished compiler/encoders/arm8/proofs                         8m25s 815MB
Apr 22 08:02:20 Starting compiler/encoders/arm8_asl/proofs
Apr 22 08:21:49 Finished compiler/encoders/arm8_asl/proofs                    19m28s   1GB
Apr 22 08:21:50 Starting compiler/encoders/mips/proofs
Apr 22 08:34:23 Finished compiler/encoders/mips/proofs                        12m32s   1GB
Apr 22 08:34:23 Starting compiler/encoders/riscv/proofs
Apr 22 08:45:12 Finished compiler/encoders/riscv/proofs                       10m49s 452MB
Apr 22 08:45:13 Starting compiler/encoders/ag32/proofs
Apr 22 08:48:20 Finished compiler/encoders/ag32/proofs                         3m07s 457MB
Apr 22 08:48:21 Starting compiler/backend/x64/proofs
Apr 22 08:49:06 Finished compiler/backend/x64/proofs                             45s 838MB
Apr 22 08:49:06 Starting compiler/backend/arm7/proofs
Apr 22 08:50:00 Finished compiler/backend/arm7/proofs                            53s 935MB
Apr 22 08:50:00 Starting compiler/backend/arm8/proofs
Apr 22 08:50:40 Finished compiler/backend/arm8/proofs                            40s 911MB
Apr 22 08:50:41 Starting compiler/backend/arm8_asl
Apr 22 08:51:14 Finished compiler/backend/arm8_asl                               33s   1GB
Apr 22 08:51:14 Starting compiler/backend/mips/proofs
Apr 22 08:52:06 Finished compiler/backend/mips/proofs                            52s 943MB
Apr 22 08:52:07 Starting compiler/backend/riscv/proofs
Apr 22 08:53:00 Finished compiler/backend/riscv/proofs                           53s 871MB
Apr 22 08:53:00 Starting compiler/backend/ag32/proofs
Apr 22 09:10:48 Finished compiler/backend/ag32/proofs                         17m47s   1GB
Apr 22 09:10:49 Starting compiler/proofs
Apr 22 09:14:44 Finished compiler/proofs                                       3m55s   1GB
Apr 22 09:14:45 Starting candle/set-theory
Apr 22 09:15:27 Finished candle/set-theory                                       41s 669MB
Apr 22 09:15:27 Starting candle/syntax-lib
Apr 22 09:15:45 Finished candle/syntax-lib                                       17s 623MB
Apr 22 09:15:45 Starting candle/standard/syntax
Apr 22 09:18:36 Finished candle/standard/syntax                                2m51s 932MB
Apr 22 09:18:37 Starting candle/standard/semantics
Apr 22 09:20:55 Finished candle/standard/semantics                             2m18s 873MB
Apr 22 09:20:56 Starting candle/standard/monadic
Apr 22 09:23:18 Finished candle/standard/monadic                               2m21s 503MB
Apr 22 09:23:18 Starting candle/standard/ml_kernel
Apr 22 09:32:42 Finished candle/standard/ml_kernel                             9m23s   1GB
Apr 22 09:32:42 Starting candle/overloading/syntax
Apr 22 09:36:57 Finished candle/overloading/syntax                             4m14s 542MB
Apr 22 09:36:57 Starting candle/overloading/semantics
Apr 22 09:52:06 Finished candle/overloading/semantics                         15m08s 951MB
Apr 22 09:52:06 Starting candle/overloading/monadic
Apr 22 09:55:21 Finished candle/overloading/monadic                            3m14s 528MB
Apr 22 09:55:22 Starting candle/overloading/ml_kernel
Apr 22 10:06:07 Finished candle/overloading/ml_kernel                         10m45s   1GB
Apr 22 10:06:07 Starting candle/overloading/ml_checker
Apr 22 10:09:34 Finished candle/overloading/ml_checker                         3m26s   1GB
Apr 22 10:09:34 Starting candle/prover
Apr 22 10:21:21 Finished candle/prover                                        11m46s   1GB
Apr 22 10:21:21 Starting pancake
Apr 22 10:26:40 Finished pancake                                               5m18s 954MB
Apr 22 10:26:40 Starting pancake/ffi
Apr 22 10:26:41 Finished pancake/ffi                                              0s  12MB
Apr 22 10:26:41 Starting pancake/semantics
Apr 22 10:30:05 Finished pancake/semantics                                     3m23s 526MB
Apr 22 10:30:05 Starting pancake/proofs
Apr 22 10:47:15 Finished pancake/proofs                                       17m08s   2GB
Apr 22 10:47:15 Starting characteristic/examples
Apr 22 10:49:19 Finished characteristic/examples                               2m03s 742MB
Apr 22 10:49:19 Starting tutorial/solutions
Apr 22 11:25:42 Finished tutorial/solutions                                   36m22s   2GB
Apr 22 11:25:42 Starting translator/monadic/examples
Apr 22 11:31:35 Finished translator/monadic/examples                           5m52s   1GB
Apr 22 11:31:36 Starting examples
Apr 22 11:47:19 Finished examples                                             15m40s   2GB
Apr 22 11:47:19 Starting examples/compilation/x64
Apr 22 15:47:15 Finished examples/compilation/x64                           3h59m54s   3GB
Apr 22 15:47:15 Starting examples/compilation/x64/proofs
Apr 22 15:51:32 Finished examples/compilation/x64/proofs                       4m17s   2GB
Apr 22 15:51:32 Starting examples/compilation/ag32
Apr 22 16:36:58 Finished examples/compilation/ag32                            45m25s   2GB
Apr 22 16:36:58 Starting examples/compilation/ag32/proofs
Apr 22 16:39:01 Finished examples/compilation/ag32/proofs                      2m02s   2GB
Apr 22 16:39:01 Starting examples/cost
Apr 22 18:02:40 Finished examples/cost                                      1h23m38s   2GB
Apr 22 18:02:40 Starting examples/lpr_checker
Apr 22 18:03:59 Finished examples/lpr_checker                                  1m17s 902MB
Apr 22 18:03:59 Starting examples/lpr_checker/array
Apr 22 18:40:29 Finished examples/lpr_checker/array                           36m30s   1GB
Apr 22 18:40:30 Starting examples/lpr_checker/array/compilation
Apr 22 20:53:34 Finished examples/lpr_checker/array/compilation             2h13m04s   5GB
Apr 22 20:53:35 Starting examples/lpr_checker/array/compilation/proofs
Apr 22 20:56:19 Finished examples/lpr_checker/array/compilation/proofs         2m43s   2GB
Apr 22 20:56:19 Starting examples/opentheory
Apr 22 21:09:15 Finished examples/opentheory                                  12m55s   2GB
Apr 22 21:09:15 Starting examples/opentheory
Apr 22 21:09:17 Finished examples/opentheory                                      1s  20MB
Apr 22 21:09:17 Starting examples/opentheory/compilation
Apr 22 22:18:09 Finished examples/opentheory/compilation                    1h08m50s   3GB
Apr 22 22:18:10 Starting examples/opentheory/compilation/proofs
Apr 22 22:20:12 Finished examples/opentheory/compilation/proofs                2m02s   2GB
Apr 22 22:20:12 Starting examples/opentheory/compilation/ag32
Apr 22 23:15:57 Finished examples/opentheory/compilation/ag32                 55m44s   3GB
Apr 22 23:15:57 Starting examples/opentheory/compilation/ag32/proofs
Apr 22 23:18:57 Finished examples/opentheory/compilation/ag32/proofs           2m59s   3GB
Apr 22 23:18:57 Starting examples/sat_encodings
Apr 22 23:21:15 Finished examples/sat_encodings                                2m18s 970MB
Apr 22 23:21:16 Starting examples/sat_encodings/case_studies
Apr 22 23:23:36 Finished examples/sat_encodings/case_studies                   2m19s 595MB
Apr 22 23:23:36 Starting examples/sat_encodings/translation
Apr 22 23:31:27 Finished examples/sat_encodings/translation                    7m50s   1GB
Apr 22 23:31:27 Starting examples/sat_encodings/translation/compilation
Apr 23 00:42:19 Finished examples/sat_encodings/translation/compilation     1h10m49s   5GB
Apr 23 00:42:19 Starting translator/okasaki-examples
Apr 23 00:48:58 Finished translator/okasaki-examples                           6m38s   1GB
Apr 23 00:48:58 Starting translator/other-examples
Apr 23 00:50:16 Finished translator/other-examples                             1m17s 535MB
Apr 23 00:50:16 Starting compiler/parsing/tests
Apr 23 00:50:57 Finished compiler/parsing/tests                                  40s 226MB
Apr 23 00:50:57 Starting compiler/inference/tests
Apr 23 01:01:21 Finished compiler/inference/tests                             10m23s   1GB
Apr 23 01:01:22 Starting compiler/printing/test
Apr 23 01:06:30 Finished compiler/printing/test                                5m07s   1GB
Apr 23 01:06:31 Starting compiler/repl
Apr 23 01:26:53 Finished compiler/repl                                        20m21s   1GB
Apr 23 01:26:53 Starting compiler/bootstrap/translation
Apr 23 07:36:27 Finished compiler/bootstrap/translation                     6h09m33s   9GB
Apr 23 07:36:27 Starting unverified/sexpr-bootstrap/x64/64
Apr 23 07:49:59 Finished unverified/sexpr-bootstrap/x64/64                    13m31s   8GB
Apr 23 07:49:59 Starting unverified/sexpr-bootstrap/x64/32
Apr 23 08:03:08 Finished unverified/sexpr-bootstrap/x64/32                    13m08s   8GB
Apr 23 08:03:08 Starting compiler/benchmarks
Apr 23 08:03:15 Finished compiler/benchmarks                                      6s  28MB
Apr 23 08:03:15 Starting compiler/bootstrap/compilation/x64/64
Apr 26 09:22:39 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                                                     (199s)     OK
cake-sexpr-64                                                     (195s)     OK
to_dataBootstrapTheory                                            (175m)     OK
Starting work on to_lab_x64BootstrapTheory
to_lab_x64BootstrapTheory                                          (49h)     OK
Starting work on cake.S
cake.S                                                            (990m)FAIL<1>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL message: Created theory "x64Bootstrap">>
           lab_to_target eval: runtime: 15h59m05s,    gctime: 13h12m30s,     systime: 12m14s.
           lab_to_target real: 19h25m13s
           lab_to_target size: 144080079
 Warning - Unable to increase stack - interrupting thread
 error in quse /home/cake/oven/regression/cakeml-1872/compiler/bootstrap/compilation/x64/64/x64BootstrapScript.sml : Interrupt
 error in load /home/cake/oven/regression/cakeml-1872/compiler/bootstrap/compilation/x64/64/x64BootstrapScript : Interrupt
 Uncaught exception: Interrupt