Job 454

CakeML:16f69c4c7da2be267278da648ae0162f32a8ceec
  Make basisTypeCheck fail on failed type check [Aug 24 17:36:13]
HOL:65213190ea2f7198c593aefc0f515c9ecc771ab8
  Merge pull request #574 from binghe/rich_topology [Aug 24 05:56:37]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Aug 24 17:44:56 Claimed job
Aug 24 17:45:08 Building HOL
Aug 24 17:58:41 Starting developers/bin
Aug 24 17:58:50 Finished developers/bin                                           7s 143MB
Aug 24 17:58:52 Starting semantics/ffi
Aug 24 17:59:53 Finished semantics/ffi                                           59s 507MB
Aug 24 17:59:55 Starting semantics
Aug 24 18:02:20 Finished semantics                                             2m22s 756MB
Aug 24 18:02:22 Starting semantics/proofs
Aug 24 18:07:37 Finished semantics/proofs                                      5m12s   1GB
Aug 24 18:07:39 Starting basis/pure
Aug 24 18:13:24 Finished basis/pure                                            5m42s 785MB
Aug 24 18:13:26 Starting translator
Aug 24 18:15:21 Finished translator                                            1m53s 963MB
Aug 24 18:15:23 Starting compiler/parsing
Aug 24 18:17:45 Finished compiler/parsing                                      2m19s   1GB
Aug 24 18:17:47 Starting characteristic
Aug 24 18:22:23 Finished characteristic                                        4m34s   1GB
Aug 24 18:22:25 Starting translator/monadic
Aug 24 18:25:12 Finished translator/monadic                                    2m45s   1GB
Aug 24 18:25:14 Starting basis
Aug 24 18:53:02 Finished basis                                                27m45s   2GB
Aug 24 18:53:04 Starting compiler/inference
Aug 24 18:55:53 Finished compiler/inference                                    2m46s   1GB
Aug 24 18:55:55 Starting compiler/backend/reg_alloc
Aug 24 18:57:17 Finished compiler/backend/reg_alloc                            1m20s   1GB
Aug 24 18:57:19 Starting compiler/backend/gc
Aug 24 19:12:18 Finished compiler/backend/gc                                  14m56s   3GB
Aug 24 19:12:20 Starting compiler/backend
Aug 24 19:12:25 Finished compiler/backend                                         3s  14MB
Aug 24 19:12:27 Starting compiler/encoders/asm
Aug 24 19:12:30 Finished compiler/encoders/asm                                    0s  13MB
Aug 24 19:12:32 Starting compiler/encoders/x64
Aug 24 19:13:59 Finished compiler/encoders/x64                                 1m24s 510MB
Aug 24 19:14:01 Starting compiler/encoders/arm6
Aug 24 19:17:01 Finished compiler/encoders/arm6                                2m57s   1GB
Aug 24 19:17:02 Starting compiler/encoders/arm8
Aug 24 19:17:47 Finished compiler/encoders/arm8                                  42s 373MB
Aug 24 19:17:49 Starting compiler/encoders/mips
Aug 24 19:19:26 Finished compiler/encoders/mips                                1m35s 676MB
Aug 24 19:19:28 Starting compiler/encoders/riscv
Aug 24 19:21:02 Finished compiler/encoders/riscv                               1m31s 477MB
Aug 24 19:21:04 Starting compiler/backend/x64
Aug 24 19:21:37 Finished compiler/backend/x64                                    30s   1GB
Aug 24 19:21:39 Starting compiler/backend/arm6
Aug 24 19:22:13 Finished compiler/backend/arm6                                   32s   1GB
Aug 24 19:22:15 Starting compiler/backend/arm8
Aug 24 19:22:46 Finished compiler/backend/arm8                                   28s 911MB
Aug 24 19:22:48 Starting compiler/backend/mips
Aug 24 19:23:23 Finished compiler/backend/mips                                   32s   1GB
Aug 24 19:23:25 Starting compiler/backend/riscv
Aug 24 19:23:59 Finished compiler/backend/riscv                                  31s   1GB
Aug 24 19:24:01 Starting compiler/parsing/proofs
Aug 24 19:27:59 Finished compiler/parsing/proofs                               3m56s 945MB
Aug 24 19:28:01 Starting compiler/inference/proofs
Aug 24 19:32:51 Finished compiler/inference/proofs                             4m48s   1GB
Aug 24 19:32:53 Starting compiler/backend/semantics
Aug 24 19:47:35 Finished compiler/backend/semantics                           14m39s   2GB
Aug 24 19:47:37 Starting compiler/backend/reg_alloc/proofs
Aug 24 19:59:26 Finished compiler/backend/reg_alloc/proofs                    11m47s 418MB
Aug 24 19:59:28 Starting compiler/backend/proofs
Aug 24 20:54:08 Finished compiler/backend/proofs                              54m37s   3GB
Aug 24 20:54:10 Starting compiler/encoders/x64/proofs
Aug 24 21:05:53 Finished compiler/encoders/x64/proofs                         11m41s   1GB
Aug 24 21:05:55 Starting compiler/encoders/arm6/proofs
Aug 24 21:18:02 Finished compiler/encoders/arm6/proofs                        12m04s   3GB
Aug 24 21:18:04 Starting compiler/encoders/arm8/proofs
Aug 24 21:26:20 Finished compiler/encoders/arm8/proofs                         8m12s   1GB
Aug 24 21:26:21 Starting compiler/encoders/mips/proofs
Aug 24 21:37:54 Finished compiler/encoders/mips/proofs                        11m30s   2GB
Aug 24 21:37:56 Starting compiler/encoders/riscv/proofs
Aug 24 21:50:36 Finished compiler/encoders/riscv/proofs                       12m38s   1GB
Aug 24 21:50:38 Starting compiler/backend/x64/proofs
Aug 24 21:51:13 Finished compiler/backend/x64/proofs                             32s   1GB
Aug 24 21:51:15 Starting compiler/backend/arm6/proofs
Aug 24 21:51:55 Finished compiler/backend/arm6/proofs                            38s   1GB
Aug 24 21:51:57 Starting compiler/backend/arm8/proofs
Aug 24 21:52:31 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 24 21:52:33 Starting compiler/backend/mips/proofs
Aug 24 21:53:10 Finished compiler/backend/mips/proofs                            35s   1GB
Aug 24 21:53:12 Starting compiler/backend/riscv/proofs
Aug 24 21:53:48 Finished compiler/backend/riscv/proofs                           33s   1GB
Aug 24 21:53:50 Starting compiler/proofs
Aug 24 21:56:14 Finished compiler/proofs                                       2m22s   2GB
Aug 24 21:56:16 Starting candle/set-theory
Aug 24 21:57:12 Finished candle/set-theory                                       53s 560MB
Aug 24 21:57:14 Starting candle/syntax-lib
Aug 24 21:57:33 Finished candle/syntax-lib                                       17s 575MB
Aug 24 21:57:35 Starting candle/standard/syntax
Aug 24 22:00:18 Finished candle/standard/syntax                                2m41s 684MB
Aug 24 22:00:20 Starting candle/standard/semantics
Aug 24 22:02:37 Finished candle/standard/semantics                             2m14s 954MB
Aug 24 22:02:39 Starting candle/standard/monadic
Aug 24 22:05:06 Finished candle/standard/monadic                               2m25s 950MB
Aug 24 22:05:08 Starting candle/standard/ml_kernel
Aug 24 22:10:50 Finished candle/standard/ml_kernel                             5m39s   2GB
Aug 24 22:10:52 Starting candle/standard/opentheory
Aug 24 22:11:18 Finished candle/standard/opentheory                              24s 622MB
Aug 24 22:11:20 Starting characteristic/examples
Aug 24 22:13:59 Finished characteristic/examples                               2m37s   1GB
Aug 24 22:14:01 Starting tutorial/solutions
Aug 24 22:35:05 Finished tutorial/solutions                                   21m01s   5GB
Aug 24 22:35:07 Starting translator/monadic/examples
Aug 24 22:37:54 Finished translator/monadic/examples                           2m45s   2GB
Aug 24 22:37:56 Starting examples
Aug 24 22:46:07 Finished examples                                              8m08s   4GB
Aug 24 22:46:09 Starting examples/compilation
Aug 25 01:41:34 Finished examples/compilation                               2h55m23s  15GB
Aug 25 01:41:36 Starting examples/compilation/proofs
Aug 25 01:45:07 Finished examples/compilation/proofs                           3m28s   3GB
Aug 25 01:45:09 Starting compiler/benchmarks
Aug 25 01:45:11 Finished compiler/benchmarks                                      0s   4MB
Aug 25 01:45:13 Starting translator/okasaki-examples
Aug 25 01:51:40 Finished translator/okasaki-examples                           6m24s   1GB
Aug 25 01:51:42 Starting translator/other-examples
Aug 25 01:58:19 Finished translator/other-examples                             6m34s 919MB
Aug 25 01:58:21 Starting compiler/parsing/tests
Aug 25 01:59:03 Finished compiler/parsing/tests                                  40s 339MB
Aug 25 01:59:05 Starting compiler/inference/tests
Aug 25 02:00:32 FAILED: compiler/inference/tests
]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in ../../../developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-65213190ea2f7198c593aefc0f515c9ecc771ab8/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/inference/tests[0m
Starting work on basisTypeCheckTheory
basisTypeCheckTheory                                                                                                                              FAILED! <1>
 
 s. infertype_prog init_config basis = Success s
 
 failed.
 First unsolved sub-goal is
 
 F
 
 Failed to prove theorem infertype_prog_succeeds.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}