Job 1866

CakeML:ce7d2a18407525c943e5d48a2e9f60ee752d6f8e
  Fix translation for printing changes [Apr 08 09:54:26]
#872 (printing-type-check-each-dec)
Merging into:37af395434ed1290ae673bd6e3b3e07f8b5c03c4
  Fix some broken pancake proofs [Apr 18 10:13:33]
HOL:3b1931c130fcab243da332adb2c1413c42c59cf9
  Escape # in TeX output [Apr 12 23:45:24]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 18 10:53:05 Claimed job
Apr 18 10:53:07 Reusing HOL
Apr 18 10:54:01 Starting developers
Apr 18 10:54:10 Finished developers                                               8s  59MB
Apr 18 10:54:10 Starting developers/bin
Apr 18 10:54:35 Finished developers/bin                                          24s   1GB
Apr 18 10:54:35 Starting semantics/ffi
Apr 18 10:54:48 Finished semantics/ffi                                           12s 181MB
Apr 18 10:54:48 Starting semantics
Apr 18 10:57:50 Finished semantics                                             3m00s 473MB
Apr 18 10:57:50 Starting semantics/proofs
Apr 18 11:04:39 Finished semantics/proofs                                      6m48s   1GB
Apr 18 11:04:39 Starting semantics/alt_semantics
Apr 18 11:05:16 Finished semantics/alt_semantics                                 36s 222MB
Apr 18 11:05:16 Starting semantics/alt_semantics/proofs
Apr 18 11:09:33 Finished semantics/alt_semantics/proofs                        4m16s 532MB
Apr 18 11:09:34 Starting basis/pure
Apr 18 11:11:12 Finished basis/pure                                            1m38s 262MB
Apr 18 11:11:12 Starting translator
Apr 18 11:15:53 Finished translator                                            4m40s 685MB
Apr 18 11:15:53 Starting compiler/parsing
Apr 18 11:17:42 Finished compiler/parsing                                      1m48s 749MB
Apr 18 11:17:42 Starting characteristic
Apr 18 11:26:57 Finished characteristic                                        9m14s 888MB
Apr 18 11:26:57 Starting translator/monadic
Apr 18 11:29:51 Finished translator/monadic                                    2m53s 646MB
Apr 18 11:29:51 Starting basis
Apr 18 12:32:31 Finished basis                                              1h02m37s   2GB
Apr 18 12:32:31 Starting compiler/inference
Apr 18 12:34:02 Finished compiler/inference                                    1m30s   1GB
Apr 18 12:34:02 Starting compiler/backend/reg_alloc
Apr 18 12:36:08 Finished compiler/backend/reg_alloc                            2m06s 598MB
Apr 18 12:36:09 Starting compiler/backend/gc
Apr 18 12:41:48 Finished compiler/backend/gc                                   5m39s   1GB
Apr 18 12:41:48 Starting compiler/backend
Apr 18 12:49:26 Finished compiler/backend                                      7m37s   1GB
Apr 18 12:49:26 Starting compiler/encoders/asm
Apr 18 12:50:03 Finished compiler/encoders/asm                                   36s 724MB
Apr 18 12:50:03 Starting compiler/encoders/x64
Apr 18 12:50:41 Finished compiler/encoders/x64                                   37s 476MB
Apr 18 12:50:41 Starting compiler/encoders/arm7
Apr 18 12:51:42 Finished compiler/encoders/arm7                                1m00s 775MB
Apr 18 12:51:42 Starting compiler/encoders/arm8
Apr 18 12:52:02 Finished compiler/encoders/arm8                                  19s 804MB
Apr 18 12:52:02 Starting compiler/encoders/arm8_asl
Apr 18 12:59:27 Finished compiler/encoders/arm8_asl                            7m23s   3GB
Apr 18 12:59:27 Starting compiler/encoders/mips
Apr 18 13:01:26 Finished compiler/encoders/mips                                1m58s 744MB
Apr 18 13:01:27 Starting compiler/encoders/riscv
Apr 18 13:03:45 Finished compiler/encoders/riscv                               2m18s 743MB
Apr 18 13:03:46 Starting compiler/encoders/ag32
Apr 18 13:04:11 Finished compiler/encoders/ag32                                  25s 843MB
Apr 18 13:04:12 Starting compiler/backend/x64
Apr 18 13:04:37 Finished compiler/backend/x64                                    25s 874MB
Apr 18 13:04:37 Starting compiler/backend/arm7
Apr 18 13:05:11 Finished compiler/backend/arm7                                   33s 786MB
Apr 18 13:05:11 Starting compiler/backend/arm8
Apr 18 13:05:38 Finished compiler/backend/arm8                                   26s   1GB
Apr 18 13:05:39 Starting compiler/backend/mips
Apr 18 13:06:14 Finished compiler/backend/mips                                   34s 557MB
Apr 18 13:06:14 Starting compiler/backend/riscv
Apr 18 13:06:40 Finished compiler/backend/riscv                                  26s   1GB
Apr 18 13:06:40 Starting compiler/backend/ag32
Apr 18 13:08:26 Finished compiler/backend/ag32                                 1m44s   1GB
Apr 18 13:08:26 Starting compiler/parsing/proofs
Apr 18 13:13:37 Finished compiler/parsing/proofs                               5m10s 641MB
Apr 18 13:13:37 Starting compiler/inference/proofs
Apr 18 13:16:49 Finished compiler/inference/proofs                             3m12s   1GB
Apr 18 13:16:50 Starting compiler/backend/semantics
Apr 18 13:58:08 Finished compiler/backend/semantics                           41m17s 907MB
Apr 18 13:58:08 Starting compiler/backend/reg_alloc/proofs
Apr 18 14:02:45 Finished compiler/backend/reg_alloc/proofs                     4m37s 423MB
Apr 18 14:02:45 Starting compiler/backend/proofs
Apr 18 15:19:42 Finished compiler/backend/proofs                            1h16m55s   7GB
Apr 18 15:19:42 Starting compiler/backend/serialiser
Apr 18 15:21:50 Finished compiler/backend/serialiser                           2m07s 762MB
Apr 18 15:21:50 Starting compiler/encoders/x64/proofs
Apr 18 15:34:25 Finished compiler/encoders/x64/proofs                         12m34s   1GB
Apr 18 15:34:25 Starting compiler/encoders/arm7/proofs
Apr 18 15:50:59 Finished compiler/encoders/arm7/proofs                        16m34s   1GB
Apr 18 15:51:00 Starting compiler/encoders/arm8/proofs
Apr 18 15:59:20 Finished compiler/encoders/arm8/proofs                         8m19s 861MB
Apr 18 15:59:20 Starting compiler/encoders/arm8_asl/proofs
Apr 18 17:02:25 Finished compiler/encoders/arm8_asl/proofs                  1h03m05s   2GB
Apr 18 17:02:26 Starting compiler/encoders/mips/proofs
Apr 18 17:16:08 Finished compiler/encoders/mips/proofs                        13m42s   1GB
Apr 18 17:16:08 Starting compiler/encoders/riscv/proofs
Apr 18 17:27:36 Finished compiler/encoders/riscv/proofs                       11m27s 571MB
Apr 18 17:27:36 Starting compiler/encoders/ag32/proofs
Apr 18 17:30:44 Finished compiler/encoders/ag32/proofs                         3m07s 505MB
Apr 18 17:30:44 Starting compiler/backend/x64/proofs
Apr 18 17:31:26 Finished compiler/backend/x64/proofs                             41s 924MB
Apr 18 17:31:26 Starting compiler/backend/arm7/proofs
Apr 18 17:31:58 Finished compiler/backend/arm7/proofs                            32s   1GB
Apr 18 17:31:58 Starting compiler/backend/arm8/proofs
Apr 18 17:32:30 Finished compiler/backend/arm8/proofs                            31s   1GB
Apr 18 17:32:30 Starting compiler/backend/arm8_asl
Apr 18 17:32:56 Finished compiler/backend/arm8_asl                               25s   1GB
Apr 18 17:32:56 Starting compiler/backend/mips/proofs
Apr 18 17:33:36 Finished compiler/backend/mips/proofs                            40s   1GB
Apr 18 17:33:36 Starting compiler/backend/riscv/proofs
Apr 18 17:34:22 Finished compiler/backend/riscv/proofs                           45s   1GB
Apr 18 17:34:22 Starting compiler/backend/ag32/proofs
Apr 18 17:50:47 Finished compiler/backend/ag32/proofs                         16m25s   1GB
Apr 18 17:50:48 Starting compiler/proofs
Apr 18 17:54:42 Finished compiler/proofs                                       3m52s   1GB
Apr 18 17:54:42 Starting candle/set-theory
Apr 18 17:55:29 Finished candle/set-theory                                       46s 289MB
Apr 18 17:55:29 Starting candle/syntax-lib
Apr 18 17:55:55 Finished candle/syntax-lib                                       25s 198MB
Apr 18 17:55:55 Starting candle/standard/syntax
Apr 18 17:58:51 Finished candle/standard/syntax                                2m56s 348MB
Apr 18 17:58:52 Starting candle/standard/semantics
Apr 18 18:01:27 Finished candle/standard/semantics                             2m34s 494MB
Apr 18 18:01:27 Starting candle/standard/monadic
Apr 18 18:03:55 Finished candle/standard/monadic                               2m27s 430MB
Apr 18 18:03:55 Starting candle/standard/ml_kernel
Apr 18 18:12:02 Finished candle/standard/ml_kernel                             8m06s   1GB
Apr 18 18:12:02 Starting candle/overloading/syntax
Apr 18 18:16:00 Finished candle/overloading/syntax                             3m57s   1GB
Apr 18 18:16:00 Starting candle/overloading/semantics
Apr 18 18:30:46 Finished candle/overloading/semantics                         14m45s   1GB
Apr 18 18:30:46 Starting candle/overloading/monadic
Apr 18 18:34:18 Finished candle/overloading/monadic                            3m31s 414MB
Apr 18 18:34:19 Starting candle/overloading/ml_kernel
Apr 18 18:44:19 Finished candle/overloading/ml_kernel                         10m00s   1GB
Apr 18 18:44:20 Starting candle/overloading/ml_checker
Apr 18 18:46:59 Finished candle/overloading/ml_checker                         2m39s   2GB
Apr 18 18:46:59 Starting candle/prover
Apr 18 18:58:01 Finished candle/prover                                        11m01s   1GB
Apr 18 18:58:02 Starting pancake
Apr 18 19:03:05 Finished pancake                                               5m02s   1GB
Apr 18 19:03:05 Starting pancake/ffi
Apr 18 19:03:06 Finished pancake/ffi                                              0s  12MB
Apr 18 19:03:06 Starting pancake/semantics
Apr 18 19:06:39 Finished pancake/semantics                                     3m32s 821MB
Apr 18 19:06:39 Starting pancake/proofs
Apr 18 19:22:59 Finished pancake/proofs                                       16m19s   2GB
Apr 18 19:22:59 Starting characteristic/examples
Apr 18 19:25:06 Finished characteristic/examples                               2m06s 946MB
Apr 18 19:25:06 Starting tutorial/solutions
Apr 18 19:49:41 Finished tutorial/solutions                                   24m34s   2GB
Apr 18 19:49:41 Starting translator/monadic/examples
Apr 18 19:55:23 Finished translator/monadic/examples                           5m41s 924MB
Apr 18 19:55:23 Starting examples
Apr 18 20:11:22 Finished examples                                             15m58s   1GB
Apr 18 20:11:22 Starting examples/compilation/x64
Apr 18 23:55:39 Finished examples/compilation/x64                           3h44m16s   3GB
Apr 18 23:55:39 Starting examples/compilation/x64/proofs
Apr 19 00:00:45 Finished examples/compilation/x64/proofs                       5m05s   2GB
Apr 19 00:00:45 Starting examples/compilation/ag32
Apr 19 00:50:28 Finished examples/compilation/ag32                            49m42s   2GB
Apr 19 00:50:28 Starting examples/compilation/ag32/proofs
Apr 19 00:52:24 Finished examples/compilation/ag32/proofs                      1m55s   2GB
Apr 19 00:52:24 Starting examples/cost
Apr 19 02:13:27 Finished examples/cost                                      1h21m01s   2GB
Apr 19 02:13:27 Starting examples/lpr_checker
Apr 19 02:14:42 Finished examples/lpr_checker                                  1m14s 966MB
Apr 19 02:14:42 Starting examples/lpr_checker/array
Apr 19 02:52:22 Finished examples/lpr_checker/array                           37m39s   2GB
Apr 19 02:52:22 Starting examples/lpr_checker/array/compilation
Apr 19 05:06:45 Finished examples/lpr_checker/array/compilation             2h14m20s   5GB
Apr 19 05:06:45 Starting examples/lpr_checker/array/compilation/proofs
Apr 19 05:09:46 Finished examples/lpr_checker/array/compilation/proofs         3m00s   2GB
Apr 19 05:09:46 Starting examples/opentheory
Apr 19 05:23:16 Finished examples/opentheory                                  13m29s   1GB
Apr 19 05:23:16 Starting examples/opentheory
Apr 19 05:23:18 Finished examples/opentheory                                      1s  18MB
Apr 19 05:23:19 Starting examples/opentheory/compilation
Apr 19 06:32:33 Finished examples/opentheory/compilation                    1h09m14s   3GB
Apr 19 06:32:34 Starting examples/opentheory/compilation/proofs
Apr 19 06:34:37 Finished examples/opentheory/compilation/proofs                2m03s   2GB
Apr 19 06:34:37 Starting examples/opentheory/compilation/ag32
Apr 19 07:52:43 Finished examples/opentheory/compilation/ag32               1h18m04s   4GB
Apr 19 07:52:43 Starting examples/opentheory/compilation/ag32/proofs
Apr 19 07:55:32 Finished examples/opentheory/compilation/ag32/proofs           2m48s   3GB
Apr 19 07:55:32 Starting examples/sat_encodings
Apr 19 07:57:58 Finished examples/sat_encodings                                2m25s 882MB
Apr 19 07:57:58 Starting examples/sat_encodings/case_studies
Apr 19 08:00:10 Finished examples/sat_encodings/case_studies                   2m12s 660MB
Apr 19 08:00:11 Starting examples/sat_encodings/translation
Apr 19 08:08:21 Finished examples/sat_encodings/translation                    8m09s   1GB
Apr 19 08:08:21 Starting examples/sat_encodings/translation/compilation
Apr 19 09:20:38 Finished examples/sat_encodings/translation/compilation     1h12m14s   4GB
Apr 19 09:20:39 Starting translator/okasaki-examples
Apr 19 09:27:21 Finished translator/okasaki-examples                           6m42s   1GB
Apr 19 09:27:21 Starting translator/other-examples
Apr 19 09:30:05 Finished translator/other-examples                             2m43s 968MB
Apr 19 09:30:05 Starting compiler/parsing/tests
Apr 19 09:30:45 Finished compiler/parsing/tests                                  40s 265MB
Apr 19 09:30:45 Starting compiler/inference/tests
Apr 19 09:40:37 Finished compiler/inference/tests                              9m51s   1GB
Apr 19 09:40:37 Starting compiler/printing/test
Apr 19 09:45:26 FAILED: compiler/printing/test
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/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanned 35 directories
Starting work on addPrintValsTheory
Starting work on addTypePPTheory
Starting work on README.md
README.md                                   compiler/printing/test  (0s)     OK
addTypePPTheory                                  compiler/printing  (4s)     OK
addPrintValsTheory                               compiler/printing (10s)     OK
Starting work on printTweaksTheory
printTweaksTheory                                compiler/printing  (6s)     OK
Finished $(CAKEMLDIR)/compiler/printing [#theories: 3]                (22.128s) 
Starting work on printingTestTheory
printingTestTheory                          compiler/printing/test(244s)FAIL<1>
                 [("binary_ieee_rounding",[],... ... 24);
                  ("double",[],... ... )] []); ("CommandLine",Bind [] []);
              ("Hashtable",Bind [("hashtable",... ,... )] []);
              ("Map",Bind [(... ,... )] []); ("Array",Bind [... ] []);
              ("Word8Array",... ... []); ("Word8",... ... ); (... ,... );
              ... ; ... ]|>,
       <|next_uvar := 2; subst := FEMPTY |+ (1,Infer_Tapp [Infer_Tuvar 0] 17);
         next_id := 29|>))
 error in load /home/cake/oven/regression/cakeml-1866/compiler/printing/test/printingTestScript : HOL_ERR {message = "test printing/inference assembly failed", origin_function = "failwith", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "test printing/inference assembly failed", origin_function = "failwith", origin_structure = "??"}