Job 802

CakeML:b2c1007e2e54c223bcc1b1cb29e00c496a52e275
  Find and fix more definition-saves that cause loss of "compute" [Apr 15 05:40:26]
HOL:057a3046e41b50db616e5d385e9b63e940b4957e
  Deal with bad rebindings of theorems under src/ [Apr 15 07:09:08]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 16 10:15:01 Claimed job
Apr 16 10:15:09 Reusing HOL
Apr 16 10:16:01 Starting developers
Apr 16 10:16:04 Finished developers                                               2s  20MB
Apr 16 10:16:04 Starting developers/bin
Apr 16 10:17:14 Finished developers/bin                                        1m09s 918MB
Apr 16 10:17:14 Starting semantics/ffi
Apr 16 10:17:24 Finished semantics/ffi                                           10s 218MB
Apr 16 10:17:25 Starting semantics
Apr 16 10:18:46 Finished semantics                                             1m20s   1GB
Apr 16 10:18:46 Starting semantics/proofs
Apr 16 10:21:41 Finished semantics/proofs                                      2m55s   1GB
Apr 16 10:21:41 Starting basis/pure
Apr 16 10:22:29 Finished basis/pure                                              46s 662MB
Apr 16 10:22:29 Starting translator
Apr 16 10:24:09 Finished translator                                            1m40s   1GB
Apr 16 10:24:10 Starting compiler/parsing
Apr 16 10:25:07 Finished compiler/parsing                                        57s   2GB
Apr 16 10:25:07 Starting characteristic
Apr 16 10:30:16 Finished characteristic                                        5m08s   2GB
Apr 16 10:30:16 Starting translator/monadic
Apr 16 10:31:47 Finished translator/monadic                                    1m30s   1GB
Apr 16 10:31:47 Starting basis
Apr 16 10:48:13 Finished basis                                                16m25s   2GB
Apr 16 10:48:14 Starting compiler/inference
Apr 16 10:49:46 Finished compiler/inference                                    1m31s   1GB
Apr 16 10:49:46 Starting compiler/backend/reg_alloc
Apr 16 10:50:38 Finished compiler/backend/reg_alloc                              51s   1GB
Apr 16 10:50:38 Starting compiler/backend/gc
Apr 16 10:58:39 Finished compiler/backend/gc                                   8m00s   1GB
Apr 16 10:58:40 Starting compiler/backend
Apr 16 10:58:42 Finished compiler/backend                                         2s  15MB
Apr 16 10:58:43 Starting compiler/encoders/asm
Apr 16 10:58:44 Finished compiler/encoders/asm                                    1s  16MB
Apr 16 10:58:44 Starting compiler/encoders/x64
Apr 16 10:59:10 Finished compiler/encoders/x64                                   25s 670MB
Apr 16 10:59:11 Starting compiler/encoders/arm6
Apr 16 10:59:56 Finished compiler/encoders/arm6                                  45s 684MB
Apr 16 10:59:56 Starting compiler/encoders/arm8
Apr 16 11:00:10 Finished compiler/encoders/arm8                                  13s 815MB
Apr 16 11:00:10 Starting compiler/encoders/mips
Apr 16 11:00:28 Finished compiler/encoders/mips                                  17s   1GB
Apr 16 11:00:28 Starting compiler/encoders/riscv
Apr 16 11:00:43 Finished compiler/encoders/riscv                                 14s 776MB
Apr 16 11:00:44 Starting compiler/encoders/ag32
Apr 16 11:01:01 Finished compiler/encoders/ag32                                  17s 744MB
Apr 16 11:01:01 Starting compiler/backend/x64
Apr 16 11:01:19 Finished compiler/backend/x64                                    17s 817MB
Apr 16 11:01:19 Starting compiler/backend/arm6
Apr 16 11:01:39 Finished compiler/backend/arm6                                   19s   1GB
Apr 16 11:01:39 Starting compiler/backend/arm8
Apr 16 11:01:57 Finished compiler/backend/arm8                                   17s   1GB
Apr 16 11:01:58 Starting compiler/backend/mips
Apr 16 11:02:17 Finished compiler/backend/mips                                   19s   1GB
Apr 16 11:02:17 Starting compiler/backend/riscv
Apr 16 11:02:36 Finished compiler/backend/riscv                                  18s   1GB
Apr 16 11:02:37 Starting compiler/backend/ag32
Apr 16 11:03:45 Finished compiler/backend/ag32                                 1m07s   1GB
Apr 16 11:03:45 Starting compiler/parsing/proofs
Apr 16 11:09:19 Finished compiler/parsing/proofs                               5m34s   1GB
Apr 16 11:09:20 Starting compiler/inference/proofs
Apr 16 11:11:57 Finished compiler/inference/proofs                             2m37s   1GB
Apr 16 11:11:58 Starting compiler/backend/semantics
Apr 16 11:18:47 Finished compiler/backend/semantics                            6m49s   2GB
Apr 16 11:18:47 Starting compiler/backend/reg_alloc/proofs
Apr 16 11:21:25 Finished compiler/backend/reg_alloc/proofs                     2m37s   1GB
Apr 16 11:21:25 Starting compiler/backend/proofs
Apr 16 11:58:25 Finished compiler/backend/proofs                              36m59s   3GB
Apr 16 11:58:25 Starting compiler/encoders/x64/proofs
Apr 16 12:07:17 Finished compiler/encoders/x64/proofs                          8m51s   4GB
Apr 16 12:07:17 Starting compiler/encoders/arm6/proofs
Apr 16 12:19:10 Finished compiler/encoders/arm6/proofs                        11m53s   6GB
Apr 16 12:19:10 Starting compiler/encoders/arm8/proofs
Apr 16 12:24:33 Finished compiler/encoders/arm8/proofs                         5m22s   1GB
Apr 16 12:24:33 Starting compiler/encoders/mips/proofs
Apr 16 12:33:55 Finished compiler/encoders/mips/proofs                         9m21s   2GB
Apr 16 12:33:55 Starting compiler/encoders/riscv/proofs
Apr 16 12:42:01 Finished compiler/encoders/riscv/proofs                        8m06s   1GB
Apr 16 12:42:02 Starting compiler/encoders/ag32/proofs
Apr 16 12:44:26 Finished compiler/encoders/ag32/proofs                         2m23s 703MB
Apr 16 12:44:26 Starting compiler/backend/x64/proofs
Apr 16 12:44:46 Finished compiler/backend/x64/proofs                             19s   1GB
Apr 16 12:44:46 Starting compiler/backend/arm6/proofs
Apr 16 12:45:08 Finished compiler/backend/arm6/proofs                            21s   1GB
Apr 16 12:45:09 Starting compiler/backend/arm8/proofs
Apr 16 12:45:29 Finished compiler/backend/arm8/proofs                            19s   1GB
Apr 16 12:45:29 Starting compiler/backend/mips/proofs
Apr 16 12:45:49 Finished compiler/backend/mips/proofs                            19s 956MB
Apr 16 12:45:50 Starting compiler/backend/riscv/proofs
Apr 16 12:46:10 Finished compiler/backend/riscv/proofs                           20s   1GB
Apr 16 12:46:11 Starting compiler/backend/ag32/proofs
Apr 16 12:54:55 Finished compiler/backend/ag32/proofs                          8m43s   2GB
Apr 16 12:54:55 Starting compiler/proofs
Apr 16 12:56:30 Finished compiler/proofs                                       1m34s   3GB
Apr 16 12:56:30 Starting candle/set-theory
Apr 16 12:56:57 Finished candle/set-theory                                       26s 654MB
Apr 16 12:56:58 Starting candle/syntax-lib
Apr 16 12:57:09 Finished candle/syntax-lib                                       11s 568MB
Apr 16 12:57:09 Starting candle/standard/syntax
Apr 16 12:58:30 FAILED: candle/standard/syntax
]0;Holmake: ~/oven/regression/cakeml-802/basis/pure]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-802/basis/pure]0;Holmake: ~/oven/regression/cakeml-802/misc]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-802/misc]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-802/misc]0;Holmake: ~/oven/regression/cakeml-802/developers]0;Holmake: ~/oven/regression/cakeml-802/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-802/misc]0;Holmake: ~/oven/regression/cakeml-802/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-802/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-802/misc]0;Holmake: ~/oven/regression/cakeml-802/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-802/basis/pure]0;Holmake: ~/oven/regression/cakeml-802/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-libWorking in $(CAKEMLDIR)/candle/syntax-lib
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/candle/standard/syntax
Starting work on holSyntaxTheory
Starting work on README.md
README.md                                                                    OK
holSyntaxTheory                                                              OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory                                                         OK
Starting work on holBoolSyntaxTheory
Starting work on holConservativeTheory
holConservativeTheory                                                        OK
holBoolSyntaxTheory                                                 FAILED! <1>
 
 ctxt. is_std_sig (sigof ctxt)  is_bool_sig (sigof (mk_bool_ctxt ctxt))
 
 failed.
 First unsolved sub-goal is
 
 codomain (codomain (Fun (Fun Bool Bool) (Fun (Fun Bool Bool) Bool))) = Bool
 
 Failed to prove theorem bool_has_bool_sig.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}