Job 957

CakeML:840ccb3c0c6ecc230ad05d07d0e2bb7649a4977a
  Merge branch 'master' into fp_basis [Jul 24 12:10:18]
#671 (fp_basis)
Merging into:771865c05a96606969aac5f75811602d8c061768
  Fix proof broken by HOL's removal of relationTheory.RTC_DEF [Jul 24 12:06:35]
HOL:e736cb4999577a492e6abd84f789113b9a4c80c3
  Use new Inductive syntax in PEG theory [Jul 23 03:51:48]
Machine:brain09 4.14.127.1.amd64-smp

Jul 24 12:18:01 Claimed job
Jul 24 12:18:05 Building HOL
Jul 24 12:34:05 Starting developers
Jul 24 12:34:06 Finished developers                                               0s  30MB
Jul 24 12:34:06 Starting developers/bin
Jul 24 12:34:16 Finished developers/bin                                           9s 970MB
Jul 24 12:34:16 Starting semantics/ffi
Jul 24 12:35:28 Finished semantics/ffi                                         1m11s 613MB
Jul 24 12:35:28 Starting semantics
Jul 24 12:38:26 Finished semantics                                             2m57s   1GB
Jul 24 12:38:26 Starting semantics/proofs
Jul 24 12:44:05 Finished semantics/proofs                                      5m38s   1GB
Jul 24 12:44:05 Starting semantics/alt_semantics
Jul 24 12:44:21 Finished semantics/alt_semantics                                 15s 348MB
Jul 24 12:44:21 Starting semantics/alt_semantics/proofs
Jul 24 12:47:43 Finished semantics/alt_semantics/proofs                        3m21s 982MB
Jul 24 12:47:43 Starting basis/pure
Jul 24 12:54:25 Finished basis/pure                                            6m42s   1GB
Jul 24 12:54:26 Starting translator
Jul 24 12:57:36 Finished translator                                            3m10s   1GB
Jul 24 12:57:36 Starting compiler/parsing
Jul 24 12:59:16 Finished compiler/parsing                                      1m39s   2GB
Jul 24 12:59:16 Starting characteristic
Jul 24 13:09:16 Finished characteristic                                        9m59s   2GB
Jul 24 13:09:16 Starting translator/monadic
Jul 24 13:12:08 Finished translator/monadic                                    2m52s   1GB
Jul 24 13:12:09 Starting basis
Jul 24 13:48:23 Finished basis                                                36m13s   7GB
Jul 24 13:48:23 Starting compiler/inference
Jul 24 13:51:57 Finished compiler/inference                                    3m34s   2GB
Jul 24 13:51:58 Starting compiler/backend/reg_alloc
Jul 24 13:53:39 Finished compiler/backend/reg_alloc                            1m40s   1GB
Jul 24 13:53:39 Starting compiler/backend/gc
Jul 24 14:09:55 Finished compiler/backend/gc                                  16m16s   2GB
Jul 24 14:09:56 Starting compiler/backend
Jul 24 14:09:58 Finished compiler/backend                                         2s  49MB
Jul 24 14:09:58 Starting compiler/encoders/asm
Jul 24 14:09:59 Finished compiler/encoders/asm                                    0s  30MB
Jul 24 14:09:59 Starting compiler/encoders/x64
Jul 24 14:12:04 Finished compiler/encoders/x64                                 2m04s 981MB
Jul 24 14:12:04 Starting compiler/encoders/arm7
Jul 24 14:15:53 Finished compiler/encoders/arm7                                3m48s   2GB
Jul 24 14:15:53 Starting compiler/encoders/arm8
Jul 24 14:16:56 Finished compiler/encoders/arm8                                1m03s 742MB
Jul 24 14:16:56 Starting compiler/encoders/mips
Jul 24 14:19:11 Finished compiler/encoders/mips                                2m14s   1GB
Jul 24 14:19:11 Starting compiler/encoders/riscv
Jul 24 14:21:40 Finished compiler/encoders/riscv                               2m28s   1GB
Jul 24 14:21:40 Starting compiler/encoders/ag32
Jul 24 14:22:15 Finished compiler/encoders/ag32                                  34s 547MB
Jul 24 14:22:15 Starting compiler/backend/x64
Jul 24 14:22:49 Finished compiler/backend/x64                                    33s   1GB
Jul 24 14:22:49 Starting compiler/backend/arm7
Jul 24 14:23:27 Finished compiler/backend/arm7                                   37s   1GB
Jul 24 14:23:27 Starting compiler/backend/arm8
Jul 24 14:24:00 Finished compiler/backend/arm8                                   33s   1GB
Jul 24 14:24:01 Starting compiler/backend/mips
Jul 24 14:24:37 Finished compiler/backend/mips                                   36s   1GB
Jul 24 14:24:37 Starting compiler/backend/riscv
Jul 24 14:25:13 Finished compiler/backend/riscv                                  35s   1GB
Jul 24 14:25:14 Starting compiler/backend/ag32
Jul 24 14:27:19 Finished compiler/backend/ag32                                 2m05s   1GB
Jul 24 14:27:19 Starting compiler/parsing/proofs
Jul 24 14:37:26 Finished compiler/parsing/proofs                              10m06s   1GB
Jul 24 14:37:26 Starting compiler/inference/proofs
Jul 24 14:42:40 Finished compiler/inference/proofs                             5m13s   1GB
Jul 24 14:42:40 Starting compiler/backend/semantics
Jul 24 14:55:11 Finished compiler/backend/semantics                           12m30s   1GB
Jul 24 14:55:11 Starting compiler/backend/reg_alloc/proofs
Jul 24 15:01:18 Finished compiler/backend/reg_alloc/proofs                     6m06s   1GB
Jul 24 15:01:18 Starting compiler/backend/proofs
Jul 24 16:06:42 Finished compiler/backend/proofs                            1h05m23s  10GB
Jul 24 16:06:42 Starting compiler/encoders/x64/proofs
Jul 24 16:25:20 Finished compiler/encoders/x64/proofs                         18m37s   6GB
Jul 24 16:25:20 Starting compiler/encoders/arm7/proofs
Jul 24 16:50:36 Finished compiler/encoders/arm7/proofs                        25m15s   8GB
Jul 24 16:50:36 Starting compiler/encoders/arm8/proofs
Jul 24 17:03:01 Finished compiler/encoders/arm8/proofs                        12m25s   1GB
Jul 24 17:03:01 Starting compiler/encoders/mips/proofs
Jul 24 17:21:33 Finished compiler/encoders/mips/proofs                        18m31s   2GB
Jul 24 17:21:33 Starting compiler/encoders/riscv/proofs
Jul 24 17:36:59 Finished compiler/encoders/riscv/proofs                       15m25s   1GB
Jul 24 17:36:59 Starting compiler/encoders/ag32/proofs
Jul 24 17:41:29 Finished compiler/encoders/ag32/proofs                         4m30s 900MB
Jul 24 17:41:30 Starting compiler/backend/x64/proofs
Jul 24 17:42:07 Finished compiler/backend/x64/proofs                             37s   1GB
Jul 24 17:42:08 Starting compiler/backend/arm7/proofs
Jul 24 17:42:46 Finished compiler/backend/arm7/proofs                            38s   1GB
Jul 24 17:42:46 Starting compiler/backend/arm8/proofs
Jul 24 17:43:22 Finished compiler/backend/arm8/proofs                            34s   1GB
Jul 24 17:43:22 Starting compiler/backend/mips/proofs
Jul 24 17:44:01 Finished compiler/backend/mips/proofs                            38s   1GB
Jul 24 17:44:01 Starting compiler/backend/riscv/proofs
Jul 24 17:44:39 Finished compiler/backend/riscv/proofs                           37s   1GB
Jul 24 17:44:39 Starting compiler/backend/ag32/proofs
Jul 24 18:01:15 Finished compiler/backend/ag32/proofs                         16m35s   9GB
Jul 24 18:01:15 Starting compiler/proofs
Jul 24 18:03:44 Finished compiler/proofs                                       2m28s   4GB
Jul 24 18:03:44 Starting candle/set-theory
Jul 24 18:04:31 Finished candle/set-theory                                       47s   1GB
Jul 24 18:04:32 Starting candle/syntax-lib
Jul 24 18:04:52 Finished candle/syntax-lib                                       20s 694MB
Jul 24 18:04:52 Starting candle/standard/syntax
Jul 24 18:08:04 Finished candle/standard/syntax                                3m11s   1GB
Jul 24 18:08:04 Starting candle/standard/semantics
Jul 24 18:11:24 Finished candle/standard/semantics                             3m19s   1GB
Jul 24 18:11:24 Starting candle/standard/monadic
Jul 24 18:14:18 Finished candle/standard/monadic                               2m53s   1GB
Jul 24 18:14:18 Starting candle/standard/ml_kernel
Jul 24 18:21:21 Finished candle/standard/ml_kernel                             7m02s   3GB
Jul 24 18:21:21 Starting candle/standard/opentheory
Jul 24 18:37:46 Finished candle/standard/opentheory                           16m25s   5GB
Jul 24 18:37:46 Starting candle/standard/opentheory/compilation
Jul 25 08:05:09 Finished candle/standard/opentheory/compilation            13h27m21s 598GB
Jul 25 08:05:09 Starting candle/standard/opentheory/compilation/proofs
Jul 25 08:07:02 Finished candle/standard/opentheory/compilation/proofs         1m52s   2GB
Jul 25 08:07:02 Starting characteristic/examples
Jul 25 08:10:02 Finished characteristic/examples                               2m59s   5GB
Jul 25 08:10:02 Starting tutorial/solutions
Jul 25 10:01:41 Finished tutorial/solutions                                 1h51m37s 210GB
Jul 25 10:01:41 Starting translator/monadic/examples
Jul 25 10:06:08 Finished translator/monadic/examples                           4m27s   2GB
Jul 25 10:06:09 Starting examples
Jul 25 10:20:45 Finished examples                                             14m36s  20GB
Jul 25 10:20:45 Starting examples/compilation/x64
Jul 26 07:08:50 Finished examples/compilation/x64                          20h48m04s 490GB
Jul 26 07:08:51 Starting examples/compilation/x64/proofs
Jul 26 07:11:27 Finished examples/compilation/x64/proofs                       2m36s   2GB
Jul 26 07:11:28 Starting examples/compilation/ag32
Jul 26 09:48:56 Finished examples/compilation/ag32                          2h37m28s 151GB
Jul 26 09:48:57 Starting examples/compilation/ag32/proofs
Jul 26 09:50:59 Finished examples/compilation/ag32/proofs                      2m02s   5GB
Jul 26 09:51:00 Starting translator/okasaki-examples
Jul 26 09:58:06 Finished translator/okasaki-examples                           7m05s   1GB
Jul 26 09:58:06 Starting translator/other-examples
Jul 26 10:04:41 Finished translator/other-examples                             6m35s   1GB
Jul 26 10:04:41 Starting compiler/parsing/tests
Jul 26 10:05:40 Finished compiler/parsing/tests                                  58s   2GB
Jul 26 10:05:40 Starting compiler/inference/tests
Jul 26 10:24:21 FAILED: compiler/inference/tests
]0;Holmake: /local/hbecker/regression/cakeml-957/basis/pure]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/formal-languages]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/formal-languages/context-free]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: /local/hbecker/regression/cakeml-957/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-957/misc]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/fun-op-sem/lprefix_lub]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: /local/hbecker/regression/cakeml-957/misc]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/machine-code/hoare-triple]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: /local/hbecker/regression/cakeml-957/misc]0;Holmake: /local/hbecker/regression/cakeml-957/developers]0;Holmake: /local/hbecker/regression/cakeml-957/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: /local/hbecker/regression/cakeml-957/misc]0;Holmake: /local/hbecker/regression/cakeml-957/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/cakeml-957/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: /local/hbecker/regression/cakeml-957/misc]0;Holmake: /local/hbecker/regression/cakeml-957/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: /local/hbecker/regression/cakeml-957/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-957/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: /local/hbecker/regression/cakeml-957/basis]0;Holmake: /local/hbecker/regression/cakeml-957/characteristic]0;Holmake: /local/hbecker/regression/cakeml-957/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-957/semantics]0;Holmake: /local/hbecker/regression/cakeml-957/semantics/ffi]0;Holmake: /local/hbecker/regression/cakeml-957/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: /local/hbecker/regression/cakeml-957/semantics]0;Holmake: /local/hbecker/regression/cakeml-957/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: /local/hbecker/regression/cakeml-957/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-957/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: /local/hbecker/regression/cakeml-957/characteristic]0;Holmake: /local/hbecker/regression/cakeml-957/semantics/proofs]0;Holmake: /local/hbecker/regression/cakeml-957/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: /local/hbecker/regression/cakeml-957/characteristic]0;Holmake: /local/hbecker/regression/cakeml-957/translator]0;Holmake: /local/hbecker/regression/cakeml-957/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: /local/hbecker/regression/cakeml-957/characteristic]0;Holmake: /local/hbecker/regression/cakeml-957/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: /local/hbecker/regression/cakeml-957/basis]0;Holmake: /local/hbecker/regression/cakeml-957/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-957/translator/monadic/monad_base]0;Holmake: /local/hbecker/regression/cakeml-957/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: /local/hbecker/regression/cakeml-957/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-957/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: /local/hbecker/regression/cakeml-957/basis]0;Holmake: /local/hbecker/regression/cakeml-957/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ..]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/unification/triangular/first-order]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/unification/triangular]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/unification/triangular/first-order]0;Holmake: /local/hbecker/regression/HOL-e736cb4999577a492e6abd84f789113b9a4c80c3/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/inference
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/inference/tests
Starting work on basisTypeCheckTheory
Starting work on README.md
README.md                                                                                                                        OK
basisTypeCheckTheory                                                                                                    FAILED! <1>
 /local/hbecker/regression/cakeml-957/compiler/inference/unifyLib.sml:38: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /local/hbecker/regression/cakeml-957/compiler/inference/unifyLib.sml:56: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /local/hbecker/regression/cakeml-957/compiler/inference/unifyLib.sml:62: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 /local/hbecker/regression/cakeml-957/compiler/inference/unifyLib.sml:68: warning: Pattern is not exhaustive. Found near val (_, [s, ...]) = strip_comb tm
 <<HOL message: Created theory "basisTypeCheck">>
 error in quse /local/hbecker/regression/cakeml-957/compiler/inference/tests/basisTypeCheckScript.sml : HOL_ERR {message = "not terminated by EMPTYSTRING", origin_function = "dest_string_lit", origin_structure = "Literal"}
 error in load basisTypeCheckScript : HOL_ERR {message = "not terminated by EMPTYSTRING", origin_function = "dest_string_lit", origin_structure = "Literal"}
 Uncaught exception: HOL_ERR {message = "not terminated by EMPTYSTRING", origin_function = "dest_string_lit", origin_structure = "Literal"}