Job 711

CakeML:01444fe36cb917d1f0d64a94cf521fd86435a181
  Also update mlton-derived CakeML benchmarks for new datatype syntax [Jan 31 10:28:34]
#613 (gh611)
Merging into:2d7c75fa02a5b1347dd76fa2b7150e0af74d940b
  Fix some uses of Theorem syntax [Jan 31 16:15:24]
HOL:e53c040a60b6ad258c99b0887434bda862eb81a8
  Build sequences must have src/finite_maps before src/integer [Jan 31 01:43:52]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 31 16:56:20 Claimed job
Jan 31 16:56:24 Reusing HOL
Jan 31 16:57:17 Starting developers
Jan 31 16:57:20 Finished developers                                               2s  21MB
Jan 31 16:57:20 Starting developers/bin
Jan 31 16:58:29 Finished developers/bin                                        1m07s 918MB
Jan 31 16:58:29 Starting semantics/ffi
Jan 31 16:58:40 Finished semantics/ffi                                           10s 241MB
Jan 31 16:58:41 Starting semantics
Jan 31 17:00:02 Finished semantics                                             1m20s   1GB
Jan 31 17:00:02 Starting semantics/proofs
Jan 31 17:03:09 Finished semantics/proofs                                      3m06s   1GB
Jan 31 17:03:10 Starting basis/pure
Jan 31 17:03:57 Finished basis/pure                                              46s 696MB
Jan 31 17:03:58 Starting translator
Jan 31 17:05:37 Finished translator                                            1m38s   1GB
Jan 31 17:05:37 Starting compiler/parsing
Jan 31 17:06:36 Finished compiler/parsing                                        58s   1GB
Jan 31 17:06:37 Starting characteristic
Jan 31 17:10:58 Finished characteristic                                        4m20s   1GB
Jan 31 17:10:59 Starting translator/monadic
Jan 31 17:12:26 Finished translator/monadic                                    1m26s   1GB
Jan 31 17:12:26 Starting basis
Jan 31 17:28:45 Finished basis                                                16m17s   2GB
Jan 31 17:28:45 Starting compiler/inference
Jan 31 17:30:18 Finished compiler/inference                                    1m32s   1GB
Jan 31 17:30:19 Starting compiler/backend/reg_alloc
Jan 31 17:31:12 Finished compiler/backend/reg_alloc                              52s   1GB
Jan 31 17:31:13 Starting compiler/backend/gc
Jan 31 17:40:07 Finished compiler/backend/gc                                   8m53s   2GB
Jan 31 17:40:08 Starting compiler/backend
Jan 31 17:40:11 Finished compiler/backend                                         2s  21MB
Jan 31 17:40:12 Starting compiler/encoders/asm
Jan 31 17:40:13 Finished compiler/encoders/asm                                    1s  20MB
Jan 31 17:40:14 Starting compiler/encoders/x64
Jan 31 17:41:15 Finished compiler/encoders/x64                                   59s 750MB
Jan 31 17:41:16 Starting compiler/encoders/arm6
Jan 31 17:43:00 Finished compiler/encoders/arm6                                1m43s   1GB
Jan 31 17:43:01 Starting compiler/encoders/arm8
Jan 31 17:43:33 Finished compiler/encoders/arm8                                  31s 548MB
Jan 31 17:43:34 Starting compiler/encoders/mips
Jan 31 17:44:40 Finished compiler/encoders/mips                                1m05s   1GB
Jan 31 17:44:40 Starting compiler/encoders/riscv
Jan 31 17:45:49 Finished compiler/encoders/riscv                               1m07s 760MB
Jan 31 17:45:49 Starting compiler/encoders/ag32
Jan 31 17:46:07 Finished compiler/encoders/ag32                                  16s 762MB
Jan 31 17:46:07 Starting compiler/backend/x64
Jan 31 17:46:26 Finished compiler/backend/x64                                    17s   1GB
Jan 31 17:46:27 Starting compiler/backend/arm6
Jan 31 17:46:46 Finished compiler/backend/arm6                                   18s   1GB
Jan 31 17:46:47 Starting compiler/backend/arm8
Jan 31 17:47:05 Finished compiler/backend/arm8                                   17s 913MB
Jan 31 17:47:05 Starting compiler/backend/mips
Jan 31 17:47:25 Finished compiler/backend/mips                                   19s   1GB
Jan 31 17:47:26 Starting compiler/backend/riscv
Jan 31 17:47:45 Finished compiler/backend/riscv                                  17s 879MB
Jan 31 17:47:45 Starting compiler/backend/ag32
Jan 31 17:48:53 Finished compiler/backend/ag32                                 1m06s 943MB
Jan 31 17:48:53 Starting compiler/parsing/proofs
Jan 31 17:54:23 Finished compiler/parsing/proofs                               5m29s   1GB
Jan 31 17:54:24 Starting compiler/inference/proofs
Jan 31 17:57:04 Finished compiler/inference/proofs                             2m40s   1GB
Jan 31 17:57:05 Starting compiler/backend/semantics
Jan 31 18:03:53 Finished compiler/backend/semantics                            6m46s   3GB
Jan 31 18:03:53 Starting compiler/backend/reg_alloc/proofs
Jan 31 18:06:31 Finished compiler/backend/reg_alloc/proofs                     2m37s   1GB
Jan 31 18:06:31 Starting compiler/backend/proofs
Jan 31 18:42:26 Finished compiler/backend/proofs                              35m53s   3GB
Jan 31 18:42:27 Starting compiler/encoders/x64/proofs
Jan 31 18:52:21 Finished compiler/encoders/x64/proofs                          9m53s   4GB
Jan 31 18:52:21 Starting compiler/encoders/arm6/proofs
Jan 31 19:05:25 Finished compiler/encoders/arm6/proofs                        13m02s   6GB
Jan 31 19:05:26 Starting compiler/encoders/arm8/proofs
Jan 31 19:11:08 Finished compiler/encoders/arm8/proofs                         5m41s   1GB
Jan 31 19:11:08 Starting compiler/encoders/mips/proofs
Jan 31 19:20:51 Finished compiler/encoders/mips/proofs                         9m41s   2GB
Jan 31 19:20:51 Starting compiler/encoders/riscv/proofs
Jan 31 19:28:30 Finished compiler/encoders/riscv/proofs                        7m37s   1GB
Jan 31 19:28:30 Starting compiler/encoders/ag32/proofs
Jan 31 19:30:56 Finished compiler/encoders/ag32/proofs                         2m25s 653MB
Jan 31 19:30:57 Starting compiler/backend/x64/proofs
Jan 31 19:31:18 Finished compiler/backend/x64/proofs                             20s   1GB
Jan 31 19:31:19 Starting compiler/backend/arm6/proofs
Jan 31 19:31:42 Finished compiler/backend/arm6/proofs                            22s   1GB
Jan 31 19:31:42 Starting compiler/backend/arm8/proofs
Jan 31 19:32:02 Finished compiler/backend/arm8/proofs                            18s 822MB
Jan 31 19:32:02 Starting compiler/backend/mips/proofs
Jan 31 19:32:23 Finished compiler/backend/mips/proofs                            20s 947MB
Jan 31 19:32:24 Starting compiler/backend/riscv/proofs
Jan 31 19:32:45 Finished compiler/backend/riscv/proofs                           20s   1GB
Jan 31 19:32:46 Starting compiler/backend/ag32/proofs
Jan 31 19:41:31 Finished compiler/backend/ag32/proofs                          8m45s   2GB
Jan 31 19:41:32 Starting compiler/proofs
Jan 31 19:42:54 Finished compiler/proofs                                       1m21s   2GB
Jan 31 19:42:55 Starting candle/set-theory
Jan 31 19:43:22 Finished candle/set-theory                                       25s 752MB
Jan 31 19:43:22 Starting candle/syntax-lib
Jan 31 19:43:34 Finished candle/syntax-lib                                       10s 548MB
Jan 31 19:43:35 Starting candle/standard/syntax
Jan 31 19:45:18 Finished candle/standard/syntax                                1m43s   1GB
Jan 31 19:45:19 Starting candle/standard/semantics
Jan 31 19:46:57 Finished candle/standard/semantics                             1m36s   1GB
Jan 31 19:46:57 Starting candle/standard/monadic
Jan 31 19:48:30 Finished candle/standard/monadic                               1m31s   1GB
Jan 31 19:48:30 Starting candle/standard/ml_kernel
Jan 31 19:52:14 Finished candle/standard/ml_kernel                             3m42s   3GB
Jan 31 19:52:14 Starting candle/standard/opentheory
Jan 31 20:00:44 Finished candle/standard/opentheory                            8m29s   3GB
Jan 31 20:00:45 Starting candle/standard/opentheory/compilation
Jan 31 20:29:40 Finished candle/standard/opentheory/compilation               28m53s  21GB
Jan 31 20:29:40 Starting candle/standard/opentheory/compilation/proofs
Jan 31 20:30:24 Finished candle/standard/opentheory/compilation/proofs           43s   4GB
Jan 31 20:30:25 Starting characteristic/examples
Jan 31 20:31:26 FAILED: characteristic/examples
]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-711/basis]0;Holmake: ~/oven/regression/cakeml-711/basis/pure]0;Holmake: ~/oven/regression/cakeml-711/misc]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/oven/regression/cakeml-711/misc]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/oven/regression/cakeml-711/misc]0;Holmake: ~/oven/regression/cakeml-711/developers]0;Holmake: ~/oven/regression/cakeml-711/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/oven/regression/cakeml-711/misc]0;Holmake: ~/oven/regression/cakeml-711/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-711/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/oven/regression/cakeml-711/misc]0;Holmake: ~/oven/regression/cakeml-711/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/oven/regression/cakeml-711/basis/pure]0;Holmake: ~/oven/regression/cakeml-711/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/oven/regression/cakeml-711/basis]0;Holmake: ~/oven/regression/cakeml-711/characteristic]0;Holmake: ~/oven/regression/cakeml-711/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-711/semantics]0;Holmake: ~/oven/regression/cakeml-711/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-711/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/oven/regression/cakeml-711/semantics]0;Holmake: ~/oven/regression/cakeml-711/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/oven/regression/cakeml-711/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-711/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/oven/regression/cakeml-711/characteristic]0;Holmake: ~/oven/regression/cakeml-711/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-711/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/oven/regression/cakeml-711/characteristic]0;Holmake: ~/oven/regression/cakeml-711/translator]0;Holmake: ~/oven/regression/cakeml-711/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/oven/regression/cakeml-711/characteristic]0;Holmake: ~/oven/regression/cakeml-711/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/oven/regression/cakeml-711/basis]0;Holmake: ~/oven/regression/cakeml-711/translator/monadic]0;Holmake: ~/oven/regression/cakeml-711/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-711/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/oven/regression/cakeml-711/translator/monadic]0;Holmake: ~/oven/regression/cakeml-711/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/oven/regression/cakeml-711/basis]0;Holmake: ~/oven/regression/cakeml-711/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/characteristic/examples[0m
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
Starting work on README.md
README.md                                                                    OK
cf_tutorialTheory                                                            OK
cf_examplesTheory                                                   FAILED! <1>
 Adding nsLookup representation thms for [cf_examples_env_8]
 Using translator specification eq_v_thm from theory mlbasicsProg
 Saved theorem _____ "nsLookup_cf_examples_env_9_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_9]
 Saved theorem _____ "nsLookup_cf_examples_env_10_pfun_eqs"
 Saved theorem _____ "nsLookup_cf_examples_env_11_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_11, cf_examples_env_10]
 error in quse /home/cake/oven/regression/cakeml-711/characteristic/examples/cf_examplesScript.sml : HOL_ERR {message = "not terminated with nil", origin_function = "dest_list", origin_structure = "listSyntax"}
 error in load cf_examplesScript : HOL_ERR {message = "not terminated with nil", origin_function = "dest_list", origin_structure = "listSyntax"}
 Uncaught exception: HOL_ERR {message = "not terminated with nil", origin_function = "dest_list", origin_structure = "listSyntax"}