Job 631

CakeML:59adcb7ec4a72ccf8e448687cf3a4af8e4577e30
  Clean more Holmakefiles [Dec 14 14:13:38]
#583 (heapfree)
Merging into:9b366aa092a1e2c8100d95bbe3fa77b5fe513dc9
  Merge pull request #582 from CakeML/cleanup [Dec 14 06:05:52]
HOL:2300978321a15932fdaf49ff5e1365d09a9a1c3b
  Fix typo [Dec 13 15:46:26]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 15 06:45:02 Claimed job
Dec 15 06:45:22 Building HOL
Dec 15 06:54:41 Starting developers
Dec 15 06:54:44 Finished developers                                               2s  21MB
Dec 15 06:54:45 Starting developers/bin
Dec 15 06:55:57 Finished developers/bin                                        1m11s 916MB
Dec 15 06:55:57 Starting semantics/ffi
Dec 15 06:56:36 Finished semantics/ffi                                           38s 305MB
Dec 15 06:56:37 Starting semantics
Dec 15 06:58:17 Finished semantics                                             1m39s   1GB
Dec 15 06:58:18 Starting semantics/proofs
Dec 15 07:01:36 Finished semantics/proofs                                      3m17s   1GB
Dec 15 07:01:37 Starting basis/pure
Dec 15 07:05:16 Finished basis/pure                                            3m38s 655MB
Dec 15 07:05:17 Starting translator
Dec 15 07:06:57 Finished translator                                            1m39s   1GB
Dec 15 07:06:57 Starting compiler/parsing
Dec 15 07:08:05 Finished compiler/parsing                                      1m06s   1GB
Dec 15 07:08:05 Starting characteristic
Dec 15 07:11:29 Finished characteristic                                        3m23s   1GB
Dec 15 07:11:30 Starting translator/monadic
Dec 15 07:13:00 Finished translator/monadic                                    1m29s   1GB
Dec 15 07:13:01 Starting basis
Dec 15 07:29:22 Finished basis                                                16m20s   2GB
Dec 15 07:29:23 Starting compiler/inference
Dec 15 07:31:21 Finished compiler/inference                                    1m57s   1GB
Dec 15 07:31:21 Starting compiler/backend/reg_alloc
Dec 15 07:32:16 Finished compiler/backend/reg_alloc                              53s   1GB
Dec 15 07:32:17 Starting compiler/backend/gc
Dec 15 07:41:24 Finished compiler/backend/gc                                   9m06s   1GB
Dec 15 07:41:25 Starting compiler/backend
Dec 15 07:41:28 Finished compiler/backend                                         2s  25MB
Dec 15 07:41:29 Starting compiler/encoders/asm
Dec 15 07:41:31 Finished compiler/encoders/asm                                    1s  15MB
Dec 15 07:41:31 Starting compiler/encoders/x64
Dec 15 07:42:33 Finished compiler/encoders/x64                                 1m01s 593MB
Dec 15 07:42:34 Starting compiler/encoders/arm6
Dec 15 07:44:27 Finished compiler/encoders/arm6                                1m52s   1GB
Dec 15 07:44:28 Starting compiler/encoders/arm8
Dec 15 07:45:00 Finished compiler/encoders/arm8                                  31s 875MB
Dec 15 07:45:01 Starting compiler/encoders/mips
Dec 15 07:46:08 Finished compiler/encoders/mips                                1m06s 794MB
Dec 15 07:46:09 Starting compiler/encoders/riscv
Dec 15 07:47:17 Finished compiler/encoders/riscv                               1m07s 825MB
Dec 15 07:47:17 Starting compiler/encoders/ag32
Dec 15 07:47:35 Finished compiler/encoders/ag32                                  17s 823MB
Dec 15 07:47:36 Starting compiler/backend/x64
Dec 15 07:47:55 Finished compiler/backend/x64                                    18s 923MB
Dec 15 07:47:56 Starting compiler/backend/arm6
Dec 15 07:48:16 Finished compiler/backend/arm6                                   18s   1GB
Dec 15 07:48:16 Starting compiler/backend/arm8
Dec 15 07:48:36 Finished compiler/backend/arm8                                   19s 956MB
Dec 15 07:48:37 Starting compiler/backend/mips
Dec 15 07:48:56 Finished compiler/backend/mips                                   18s   1GB
Dec 15 07:48:57 Starting compiler/backend/riscv
Dec 15 07:49:18 Finished compiler/backend/riscv                                  20s   1GB
Dec 15 07:49:18 Starting compiler/backend/ag32
Dec 15 07:50:33 Finished compiler/backend/ag32                                 1m14s   1GB
Dec 15 07:50:34 Starting compiler/parsing/proofs
Dec 15 07:56:49 Finished compiler/parsing/proofs                               6m14s 927MB
Dec 15 07:56:50 Starting compiler/inference/proofs
Dec 15 07:59:47 Finished compiler/inference/proofs                             2m55s   1GB
Dec 15 07:59:47 Starting compiler/backend/semantics
Dec 15 08:07:13 Finished compiler/backend/semantics                            7m24s   2GB
Dec 15 08:07:13 Starting compiler/backend/reg_alloc/proofs
Dec 15 08:10:00 Finished compiler/backend/reg_alloc/proofs                     2m45s 758MB
Dec 15 08:10:00 Starting compiler/backend/proofs
Dec 15 08:48:26 Finished compiler/backend/proofs                              38m24s   3GB
Dec 15 08:48:27 Starting compiler/encoders/x64/proofs
Dec 15 08:59:27 Finished compiler/encoders/x64/proofs                         10m59s   4GB
Dec 15 08:59:28 Starting compiler/encoders/arm6/proofs
Dec 15 09:14:26 Finished compiler/encoders/arm6/proofs                        14m57s   3GB
Dec 15 09:14:27 Starting compiler/encoders/arm8/proofs
Dec 15 09:20:34 Finished compiler/encoders/arm8/proofs                         6m06s   1GB
Dec 15 09:20:35 Starting compiler/encoders/mips/proofs
Dec 15 09:31:43 Finished compiler/encoders/mips/proofs                        11m07s   3GB
Dec 15 09:31:44 Starting compiler/encoders/riscv/proofs
Dec 15 09:39:40 Finished compiler/encoders/riscv/proofs                        7m55s   1GB
Dec 15 09:39:40 Starting compiler/encoders/ag32/proofs
Dec 15 09:42:26 Finished compiler/encoders/ag32/proofs                         2m44s 646MB
Dec 15 09:42:26 Starting compiler/backend/x64/proofs
Dec 15 09:42:47 Finished compiler/backend/x64/proofs                             19s   1GB
Dec 15 09:42:47 Starting compiler/backend/arm6/proofs
Dec 15 09:43:11 Finished compiler/backend/arm6/proofs                            22s   1GB
Dec 15 09:43:12 Starting compiler/backend/arm8/proofs
Dec 15 09:43:32 Finished compiler/backend/arm8/proofs                            19s   1GB
Dec 15 09:43:33 Starting compiler/backend/mips/proofs
Dec 15 09:43:55 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 15 09:43:55 Starting compiler/backend/riscv/proofs
Dec 15 09:44:16 Finished compiler/backend/riscv/proofs                           20s   1GB
Dec 15 09:44:17 Starting compiler/backend/ag32/proofs
Dec 15 09:53:36 Finished compiler/backend/ag32/proofs                          9m17s   2GB
Dec 15 09:53:37 Starting compiler/proofs
Dec 15 09:55:03 Finished compiler/proofs                                       1m25s   4GB
Dec 15 09:55:04 Starting candle/set-theory
Dec 15 09:55:37 Finished candle/set-theory                                       32s 689MB
Dec 15 09:55:38 Starting candle/syntax-lib
Dec 15 09:55:49 Finished candle/syntax-lib                                       10s 664MB
Dec 15 09:55:50 Starting candle/standard/syntax
Dec 15 09:57:43 Finished candle/standard/syntax                                1m53s 947MB
Dec 15 09:57:44 Starting candle/standard/semantics
Dec 15 09:59:28 Finished candle/standard/semantics                             1m43s   1GB
Dec 15 09:59:28 Starting candle/standard/monadic
Dec 15 10:01:12 Finished candle/standard/monadic                               1m43s   1GB
Dec 15 10:01:13 Starting candle/standard/ml_kernel
Dec 15 10:16:32 Finished candle/standard/ml_kernel                            15m18s   4GB
Dec 15 10:16:33 Starting candle/standard/opentheory
Dec 15 10:16:50 FAILED: candle/standard/opentheory
]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-631/basis/pure]0;Holmake: ~/oven/regression/cakeml-631/misc]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-631/misc]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-631/misc]0;Holmake: ~/oven/regression/cakeml-631/developers]0;Holmake: ~/oven/regression/cakeml-631/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-631/misc]0;Holmake: ~/oven/regression/cakeml-631/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-631/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-631/misc]0;Holmake: ~/oven/regression/cakeml-631/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-631/basis/pure]0;Holmake: ~/oven/regression/cakeml-631/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-631/basis]0;Holmake: ~/oven/regression/cakeml-631/characteristic]0;Holmake: ~/oven/regression/cakeml-631/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-631/semantics]0;Holmake: ~/oven/regression/cakeml-631/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-631/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-631/semantics]0;Holmake: ~/oven/regression/cakeml-631/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-631/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-631/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-631/characteristic]0;Holmake: ~/oven/regression/cakeml-631/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-631/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-631/characteristic]0;Holmake: ~/oven/regression/cakeml-631/translator]0;Holmake: ~/oven/regression/cakeml-631/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-631/characteristic]0;Holmake: ~/oven/regression/cakeml-631/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-631/basis]0;Holmake: ~/oven/regression/cakeml-631/translator/monadic]0;Holmake: ~/oven/regression/cakeml-631/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-631/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-631/translator/monadic]0;Holmake: ~/oven/regression/cakeml-631/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-631/basis]0;Holmake: ~/oven/regression/cakeml-631/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ../ml_kernel]0;Holmake: ../monadic]0;Holmake: ../syntax]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-libWorking in $(CAKEMLDIR)/candle/syntax-lib
]0;Holmake: ../syntax]0;Holmake: ../syntaxWorking in $(CAKEMLDIR)/candle/standard/syntax
]0;Holmake: ../monadic]0;Holmake: ../monadicWorking in $(CAKEMLDIR)/candle/standard/monadic
]0;Holmake: ../ml_kernel]0;Holmake: ../ml_kernelWorking in $(CAKEMLDIR)/candle/standard/ml_kernel
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../../set-theory]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/src/pred_set/src/more_theories]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/src/emit/ML]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/src/emit]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/src/emitWorking in $(HOLDIR)/src/emit
]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/src/emit/ML]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/src/emit/MLWorking in $(HOLDIR)/src/emit/ML
]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/src/pred_set/src/more_theories]0;Holmake: ~/oven/regression/HOL-2300978321a15932fdaf49ff5e1365d09a9a1c3b/src/pred_set/src/more_theoriesWorking in $(HOLDIR)/src/pred_set/src/more_theories
]0;Holmake: ../../set-theory]0;Holmake: ../../set-theoryWorking in $(CAKEMLDIR)/candle/set-theory
]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/candle/standard/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/candle/standard/opentheory
Starting work on prettyTheory
Starting work on README.md
README.md                                                                    OK
prettyTheory                                                        FAILED! <1>
 Saved induction ___ "pp_term_ind"
 
 Exception raised at TotalDefn.Define:
 between line 387, character 2 and line 391, character 68:
 at Defn.prim_mk_defn:
 at Pmatch.mk_case0_heu:
 Term Sequent asl c is a bad pattern (of var type?)
 error in quse /home/cake/oven/regression/cakeml-631/candle/standard/opentheory/prettyScript.sml : HOL_ERR {message = "between line 387, character 2 and line 391, character 68:\nat Defn.prim_mk_defn:\nat Pmatch.mk_case0_heu:\nTerm Sequent asl c is a bad pattern (of var type?)", origin_function = "Define", origin_structure = "TotalDefn"}
 error in load prettyScript : HOL_ERR {message = "between line 387, character 2 and line 391, character 68:\nat Defn.prim_mk_defn:\nat Pmatch.mk_case0_heu:\nTerm Sequent asl c is a bad pattern (of var type?)", origin_function = "Define", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "between line 387, character 2 and line 391, character 68:\nat Defn.prim_mk_defn:\nat Pmatch.mk_case0_heu:\nTerm Sequent asl c is a bad pattern (of var type?)", origin_function = "Define", origin_structure = "TotalDefn"}