Job 1868

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: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 20 07:20:49 Claimed job
Apr 20 07:20:59 Building HOL
Apr 20 07:33:01 Starting developers
Apr 20 07:33:07 Finished developers                                               5s  96MB
Apr 20 07:33:07 Starting developers/bin
Apr 20 07:33:16 Finished developers/bin                                           9s   1GB
Apr 20 07:33:16 Starting semantics/ffi
Apr 20 07:33:29 Finished semantics/ffi                                           12s 209MB
Apr 20 07:33:29 Starting semantics
Apr 20 07:36:08 Finished semantics                                             2m38s   1GB
Apr 20 07:36:08 Starting semantics/proofs
Apr 20 07:42:26 Finished semantics/proofs                                      6m16s   1GB
Apr 20 07:42:27 Starting semantics/alt_semantics
Apr 20 07:42:58 Finished semantics/alt_semantics                                 30s 514MB
Apr 20 07:42:58 Starting semantics/alt_semantics/proofs
Apr 20 07:46:41 Finished semantics/alt_semantics/proofs                        3m42s 832MB
Apr 20 07:46:41 Starting basis/pure
Apr 20 07:50:34 Finished basis/pure                                            3m53s 693MB
Apr 20 07:50:34 Starting translator
Apr 20 07:54:34 Finished translator                                            3m59s 929MB
Apr 20 07:54:34 Starting compiler/parsing
Apr 20 07:56:33 Finished compiler/parsing                                      1m59s   1GB
Apr 20 07:56:34 Starting characteristic
Apr 20 08:04:27 Finished characteristic                                        7m53s   1GB
Apr 20 08:04:27 Starting translator/monadic
Apr 20 08:07:06 Finished translator/monadic                                    2m38s 642MB
Apr 20 08:07:06 Starting basis
Apr 20 09:08:51 Finished basis                                              1h01m44s   2GB
Apr 20 09:08:51 Starting compiler/inference
Apr 20 09:10:34 Finished compiler/inference                                    1m43s 817MB
Apr 20 09:10:34 Starting compiler/backend/reg_alloc
Apr 20 09:12:44 Finished compiler/backend/reg_alloc                            2m09s   1GB
Apr 20 09:12:44 Starting compiler/backend/gc
Apr 20 09:18:41 Finished compiler/backend/gc                                   5m56s   1GB
Apr 20 09:18:41 Starting compiler/backend
Apr 20 09:27:05 Finished compiler/backend                                      8m23s   1GB
Apr 20 09:27:05 Starting compiler/encoders/asm
Apr 20 09:27:40 Finished compiler/encoders/asm                                   34s 721MB
Apr 20 09:27:41 Starting compiler/encoders/x64
Apr 20 09:29:02 Finished compiler/encoders/x64                                 1m21s   1GB
Apr 20 09:29:02 Starting compiler/encoders/arm7
Apr 20 09:31:43 Finished compiler/encoders/arm7                                2m40s   1GB
Apr 20 09:31:43 Starting compiler/encoders/arm8
Apr 20 09:32:35 Finished compiler/encoders/arm8                                  51s   1GB
Apr 20 09:32:35 Starting compiler/encoders/arm8_asl
Apr 20 12:38:20 Finished compiler/encoders/arm8_asl                         3h05m44s   7GB
Apr 20 12:38:20 Starting compiler/encoders/mips
Apr 20 12:40:27 Finished compiler/encoders/mips                                2m05s 536MB
Apr 20 12:40:27 Starting compiler/encoders/riscv
Apr 20 12:42:34 Finished compiler/encoders/riscv                               2m07s 883MB
Apr 20 12:42:34 Starting compiler/encoders/ag32
Apr 20 12:43:02 Finished compiler/encoders/ag32                                  27s 611MB
Apr 20 12:43:03 Starting compiler/backend/x64
Apr 20 12:43:34 Finished compiler/backend/x64                                    31s 674MB
Apr 20 12:43:34 Starting compiler/backend/arm7
Apr 20 12:44:21 Finished compiler/backend/arm7                                   46s 755MB
Apr 20 12:44:21 Starting compiler/backend/arm8
Apr 20 12:45:00 Finished compiler/backend/arm8                                   38s 498MB
Apr 20 12:45:01 Starting compiler/backend/mips
Apr 20 12:45:41 Finished compiler/backend/mips                                   40s 634MB
Apr 20 12:45:42 Starting compiler/backend/riscv
Apr 20 12:46:24 Finished compiler/backend/riscv                                  42s 672MB
Apr 20 12:46:25 Starting compiler/backend/ag32
Apr 20 12:48:32 Finished compiler/backend/ag32                                 2m07s 614MB
Apr 20 12:48:32 Starting compiler/parsing/proofs
Apr 20 12:53:40 Finished compiler/parsing/proofs                               5m07s 676MB
Apr 20 12:53:40 Starting compiler/inference/proofs
Apr 20 12:57:18 Finished compiler/inference/proofs                             3m37s 425MB
Apr 20 12:57:18 Starting compiler/backend/semantics
Apr 20 13:37:06 Finished compiler/backend/semantics                           39m48s 840MB
Apr 20 13:37:07 Starting compiler/backend/reg_alloc/proofs
Apr 20 13:41:53 Finished compiler/backend/reg_alloc/proofs                     4m45s 367MB
Apr 20 13:41:53 Starting compiler/backend/proofs
Apr 20 15:00:08 Finished compiler/backend/proofs                            1h18m13s   6GB
Apr 20 15:00:08 Starting compiler/backend/serialiser
Apr 20 15:02:23 Finished compiler/backend/serialiser                           2m14s 649MB
Apr 20 15:02:23 Starting compiler/encoders/x64/proofs
Apr 20 15:15:22 Finished compiler/encoders/x64/proofs                         12m58s   1GB
Apr 20 15:15:22 Starting compiler/encoders/arm7/proofs
Apr 20 15:32:24 Finished compiler/encoders/arm7/proofs                        17m01s   1GB
Apr 20 15:32:24 Starting compiler/encoders/arm8/proofs
Apr 20 15:40:46 Finished compiler/encoders/arm8/proofs                         8m21s 838MB
Apr 20 15:40:46 Starting compiler/encoders/arm8_asl/proofs
Apr 20 16:45:02 Finished compiler/encoders/arm8_asl/proofs                  1h04m15s   3GB
Apr 20 16:45:03 Starting compiler/encoders/mips/proofs
Apr 20 16:57:25 Finished compiler/encoders/mips/proofs                        12m19s   1GB
Apr 20 16:57:25 Starting compiler/encoders/riscv/proofs
Apr 20 17:08:20 Finished compiler/encoders/riscv/proofs                       10m54s 456MB
Apr 20 17:08:20 Starting compiler/encoders/ag32/proofs
Apr 20 17:11:28 Finished compiler/encoders/ag32/proofs                         3m07s 532MB
Apr 20 17:11:28 Starting compiler/backend/x64/proofs
Apr 20 17:12:08 Finished compiler/backend/x64/proofs                             40s 947MB
Apr 20 17:12:09 Starting compiler/backend/arm7/proofs
Apr 20 17:12:44 Finished compiler/backend/arm7/proofs                            35s   1GB
Apr 20 17:12:44 Starting compiler/backend/arm8/proofs
Apr 20 17:13:37 Finished compiler/backend/arm8/proofs                            52s 828MB
Apr 20 17:13:37 Starting compiler/backend/arm8_asl
Apr 20 17:14:31 Finished compiler/backend/arm8_asl                               53s 747MB
Apr 20 17:14:31 Starting compiler/backend/mips/proofs
Apr 20 17:15:41 Finished compiler/backend/mips/proofs                          1m09s 691MB
Apr 20 17:15:41 Starting compiler/backend/riscv/proofs
Apr 20 17:16:37 Finished compiler/backend/riscv/proofs                           55s 978MB
Apr 20 17:16:37 Starting compiler/backend/ag32/proofs
Apr 20 17:34:10 Finished compiler/backend/ag32/proofs                         17m33s   1GB
Apr 20 17:34:11 Starting compiler/proofs
Apr 20 17:38:49 Finished compiler/proofs                                       4m38s   1GB
Apr 20 17:38:49 Starting candle/set-theory
Apr 20 17:39:37 Finished candle/set-theory                                       47s 260MB
Apr 20 17:39:37 Starting candle/syntax-lib
Apr 20 17:39:53 Finished candle/syntax-lib                                       15s 748MB
Apr 20 17:39:53 Starting candle/standard/syntax
Apr 20 17:42:24 Finished candle/standard/syntax                                2m30s 870MB
Apr 20 17:42:24 Starting candle/standard/semantics
Apr 20 17:44:43 Finished candle/standard/semantics                             2m18s 689MB
Apr 20 17:44:44 Starting candle/standard/monadic
Apr 20 17:47:07 Finished candle/standard/monadic                               2m21s   1GB
Apr 20 17:47:08 Starting candle/standard/ml_kernel
Apr 20 17:55:44 Finished candle/standard/ml_kernel                             8m35s   1GB
Apr 20 17:55:45 Starting candle/overloading/syntax
Apr 20 18:00:21 Finished candle/overloading/syntax                             4m36s 317MB
Apr 20 18:00:21 Starting candle/overloading/semantics
Apr 20 18:15:44 Finished candle/overloading/semantics                         15m22s   1GB
Apr 20 18:15:44 Starting candle/overloading/monadic
Apr 20 18:18:58 Finished candle/overloading/monadic                            3m13s 897MB
Apr 20 18:18:58 Starting candle/overloading/ml_kernel
Apr 20 18:28:53 Finished candle/overloading/ml_kernel                          9m54s   1GB
Apr 20 18:28:53 Starting candle/overloading/ml_checker
Apr 20 18:32:10 Finished candle/overloading/ml_checker                         3m16s   1GB
Apr 20 18:32:10 Starting candle/prover
Apr 20 18:43:33 Finished candle/prover                                        11m22s   1GB
Apr 20 18:43:33 Starting pancake
Apr 20 18:48:47 Finished pancake                                               5m12s   1GB
Apr 20 18:48:47 Starting pancake/ffi
Apr 20 18:48:48 Finished pancake/ffi                                              0s  12MB
Apr 20 18:48:48 Starting pancake/semantics
Apr 20 18:52:00 Finished pancake/semantics                                     3m10s 810MB
Apr 20 18:52:00 Starting pancake/proofs
Apr 20 19:08:28 Finished pancake/proofs                                       16m28s   2GB
Apr 20 19:08:29 Starting characteristic/examples
Apr 20 19:10:25 Finished characteristic/examples                               1m55s 832MB
Apr 20 19:10:25 Starting tutorial/solutions
Apr 20 19:35:43 Finished tutorial/solutions                                   25m17s   2GB
Apr 20 19:35:43 Starting translator/monadic/examples
Apr 20 19:41:15 Finished translator/monadic/examples                           5m31s 829MB
Apr 20 19:41:15 Starting examples
Apr 20 19:57:04 Finished examples                                             15m48s   1GB
Apr 20 19:57:04 Starting examples/compilation/x64
Apr 20 23:56:21 Finished examples/compilation/x64                           3h59m14s   3GB
Apr 20 23:56:21 Starting examples/compilation/x64/proofs
Apr 21 00:01:29 Finished examples/compilation/x64/proofs                       5m07s   2GB
Apr 21 00:01:29 Starting examples/compilation/ag32
Apr 21 00:49:56 Finished examples/compilation/ag32                            48m27s   4GB
Apr 21 00:49:56 Starting examples/compilation/ag32/proofs
Apr 21 00:51:52 Finished examples/compilation/ag32/proofs                      1m55s   1GB
Apr 21 00:51:52 Starting examples/cost
Apr 21 02:16:48 Finished examples/cost                                      1h24m55s   2GB
Apr 21 02:16:49 Starting examples/lpr_checker
Apr 21 02:18:04 Finished examples/lpr_checker                                  1m15s   1GB
Apr 21 02:18:04 Starting examples/lpr_checker/array
Apr 21 02:57:16 Finished examples/lpr_checker/array                           39m11s   1GB
Apr 21 02:57:16 Starting examples/lpr_checker/array/compilation
Apr 21 05:17:06 Finished examples/lpr_checker/array/compilation             2h19m48s   7GB
Apr 21 05:17:06 Starting examples/lpr_checker/array/compilation/proofs
Apr 21 05:20:01 Finished examples/lpr_checker/array/compilation/proofs         2m55s   3GB
Apr 21 05:20:01 Starting examples/opentheory
Apr 21 05:33:54 Finished examples/opentheory                                  13m52s   1GB
Apr 21 05:33:55 Starting examples/opentheory
Apr 21 05:33:57 Finished examples/opentheory                                      1s  18MB
Apr 21 05:33:57 Starting examples/opentheory/compilation
Apr 21 06:42:02 Finished examples/opentheory/compilation                    1h08m05s   4GB
Apr 21 06:42:03 Starting examples/opentheory/compilation/proofs
Apr 21 06:44:25 Finished examples/opentheory/compilation/proofs                2m22s   1GB
Apr 21 06:44:25 Starting examples/opentheory/compilation/ag32
Apr 21 07:47:48 Finished examples/opentheory/compilation/ag32               1h03m22s   4GB
Apr 21 07:47:49 Starting examples/opentheory/compilation/ag32/proofs
Apr 21 07:51:03 Finished examples/opentheory/compilation/ag32/proofs           3m14s   1GB
Apr 21 07:51:04 Starting examples/sat_encodings
Apr 21 07:53:43 Finished examples/sat_encodings                                2m39s 633MB
Apr 21 07:53:44 Starting examples/sat_encodings/case_studies
Apr 21 07:56:20 Finished examples/sat_encodings/case_studies                   2m36s 684MB
Apr 21 07:56:20 Starting examples/sat_encodings/translation
Apr 21 08:04:58 Finished examples/sat_encodings/translation                    8m37s   1GB
Apr 21 08:04:58 Starting examples/sat_encodings/translation/compilation
Apr 21 09:17:05 Finished examples/sat_encodings/translation/compilation     1h12m05s   5GB
Apr 21 09:17:05 Starting translator/okasaki-examples
Apr 21 09:23:34 Finished translator/okasaki-examples                           6m28s   1GB
Apr 21 09:23:34 Starting translator/other-examples
Apr 21 09:26:24 Finished translator/other-examples                             2m49s 526MB
Apr 21 09:26:24 Starting compiler/parsing/tests
Apr 21 09:27:05 Finished compiler/parsing/tests                                  40s 222MB
Apr 21 09:27:05 Starting compiler/inference/tests
Apr 21 09:37:54 Finished compiler/inference/tests                             10m48s   1GB
Apr 21 09:37:54 Starting compiler/printing/test
Apr 21 09:42:59 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  (7s)     OK
Finished $(CAKEMLDIR)/compiler/printing [#theories: 3]                (22.797s) 
Starting work on printingTestTheory
printingTestTheory                          compiler/printing/test(253s)FAIL<1>
               Bind
                 [("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|>))
 Uncaught exception: HOL_ERR {message = "test printing/inference assembly failed", origin_function = "failwith", origin_structure = "??"}