Job 800

CakeML:399b058e56b33256cbf0ee55326d01009bccbe21
  Fix ag32_basis_ffi [Apr 15 18:44:38]
#629 (vstte18)
Merging into: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 06:55:20 Claimed job
Apr 16 06:58:35 Building HOL
Apr 16 07:07:56 Starting developers
Apr 16 07:07:58 Finished developers                                               2s  21MB
Apr 16 07:07:58 Starting developers/bin
Apr 16 07:09:04 Finished developers/bin                                        1m05s 918MB
Apr 16 07:09:04 Starting semantics/ffi
Apr 16 07:09:43 Finished semantics/ffi                                           38s 483MB
Apr 16 07:09:43 Starting semantics
Apr 16 07:11:19 Finished semantics                                             1m36s   1GB
Apr 16 07:11:20 Starting semantics/proofs
Apr 16 07:14:14 Finished semantics/proofs                                      2m54s   1GB
Apr 16 07:14:15 Starting basis/pure
Apr 16 07:17:52 Finished basis/pure                                            3m37s 715MB
Apr 16 07:17:53 Starting translator
Apr 16 07:19:35 Finished translator                                            1m42s   1GB
Apr 16 07:19:35 Starting compiler/parsing
Apr 16 07:20:33 Finished compiler/parsing                                        57s   1GB
Apr 16 07:20:33 Starting characteristic
Apr 16 07:25:45 Finished characteristic                                        5m12s   1GB
Apr 16 07:25:45 Starting translator/monadic
Apr 16 07:27:12 Finished translator/monadic                                    1m26s   1GB
Apr 16 07:27:12 Starting basis
Apr 16 07:44:00 Finished basis                                                16m47s   3GB
Apr 16 07:44:01 Starting compiler/inference
Apr 16 07:45:51 Finished compiler/inference                                    1m50s   1GB
Apr 16 07:45:51 Starting compiler/backend/reg_alloc
Apr 16 07:46:44 Finished compiler/backend/reg_alloc                              52s   1GB
Apr 16 07:46:44 Starting compiler/backend/gc
Apr 16 07:55:46 Finished compiler/backend/gc                                   9m01s   2GB
Apr 16 07:55:46 Starting compiler/backend
Apr 16 07:55:49 Finished compiler/backend                                         2s  22MB
Apr 16 07:55:49 Starting compiler/encoders/asm
Apr 16 07:55:51 Finished compiler/encoders/asm                                    1s  14MB
Apr 16 07:55:51 Starting compiler/encoders/x64
Apr 16 07:56:51 Finished compiler/encoders/x64                                 1m00s 763MB
Apr 16 07:56:52 Starting compiler/encoders/arm6
Apr 16 07:58:31 Finished compiler/encoders/arm6                                1m39s   1GB
Apr 16 07:58:31 Starting compiler/encoders/arm8
Apr 16 07:59:04 Finished compiler/encoders/arm8                                  32s 618MB
Apr 16 07:59:04 Starting compiler/encoders/mips
Apr 16 08:00:12 Finished compiler/encoders/mips                                1m07s 848MB
Apr 16 08:00:12 Starting compiler/encoders/riscv
Apr 16 08:01:33 Finished compiler/encoders/riscv                               1m20s   1GB
Apr 16 08:01:33 Starting compiler/encoders/ag32
Apr 16 08:01:51 Finished compiler/encoders/ag32                                  17s 744MB
Apr 16 08:01:51 Starting compiler/backend/x64
Apr 16 08:02:10 Finished compiler/backend/x64                                    18s   1GB
Apr 16 08:02:10 Starting compiler/backend/arm6
Apr 16 08:02:31 Finished compiler/backend/arm6                                   20s   1GB
Apr 16 08:02:31 Starting compiler/backend/arm8
Apr 16 08:02:50 Finished compiler/backend/arm8                                   19s   1GB
Apr 16 08:02:51 Starting compiler/backend/mips
Apr 16 08:03:10 Finished compiler/backend/mips                                   19s   1GB
Apr 16 08:03:10 Starting compiler/backend/riscv
Apr 16 08:03:30 Finished compiler/backend/riscv                                  19s   1GB
Apr 16 08:03:30 Starting compiler/backend/ag32
Apr 16 08:04:38 Finished compiler/backend/ag32                                 1m07s 925MB
Apr 16 08:04:38 Starting compiler/parsing/proofs
Apr 16 08:10:13 Finished compiler/parsing/proofs                               5m34s 900MB
Apr 16 08:10:13 Starting compiler/inference/proofs
Apr 16 08:12:52 Finished compiler/inference/proofs                             2m38s   1GB
Apr 16 08:12:52 Starting compiler/backend/semantics
Apr 16 08:19:44 Finished compiler/backend/semantics                            6m51s   2GB
Apr 16 08:19:44 Starting compiler/backend/reg_alloc/proofs
Apr 16 08:22:22 Finished compiler/backend/reg_alloc/proofs                     2m37s   1GB
Apr 16 08:22:22 Starting compiler/backend/proofs
Apr 16 08:59:33 Finished compiler/backend/proofs                              37m10s   4GB
Apr 16 08:59:33 Starting compiler/encoders/x64/proofs
Apr 16 09:09:25 Finished compiler/encoders/x64/proofs                          9m52s   5GB
Apr 16 09:09:25 Starting compiler/encoders/arm6/proofs
Apr 16 09:22:49 Finished compiler/encoders/arm6/proofs                        13m23s   3GB
Apr 16 09:22:49 Starting compiler/encoders/arm8/proofs
Apr 16 09:28:27 Finished compiler/encoders/arm8/proofs                         5m37s   1GB
Apr 16 09:28:27 Starting compiler/encoders/mips/proofs
Apr 16 09:38:13 Finished compiler/encoders/mips/proofs                         9m45s   2GB
Apr 16 09:38:13 Starting compiler/encoders/riscv/proofs
Apr 16 09:46:29 Finished compiler/encoders/riscv/proofs                        8m15s   1GB
Apr 16 09:46:29 Starting compiler/encoders/ag32/proofs
Apr 16 09:48:55 Finished compiler/encoders/ag32/proofs                         2m25s 642MB
Apr 16 09:48:56 Starting compiler/backend/x64/proofs
Apr 16 09:49:16 Finished compiler/backend/x64/proofs                             19s 792MB
Apr 16 09:49:16 Starting compiler/backend/arm6/proofs
Apr 16 09:49:38 Finished compiler/backend/arm6/proofs                            22s   1GB
Apr 16 09:49:38 Starting compiler/backend/arm8/proofs
Apr 16 09:49:58 Finished compiler/backend/arm8/proofs                            19s   1GB
Apr 16 09:49:59 Starting compiler/backend/mips/proofs
Apr 16 09:50:19 Finished compiler/backend/mips/proofs                            19s 899MB
Apr 16 09:50:19 Starting compiler/backend/riscv/proofs
Apr 16 09:50:40 Finished compiler/backend/riscv/proofs                           20s   1GB
Apr 16 09:50:40 Starting compiler/backend/ag32/proofs
Apr 16 09:59:16 Finished compiler/backend/ag32/proofs                          8m35s   2GB
Apr 16 09:59:16 Starting compiler/proofs
Apr 16 10:00:41 Finished compiler/proofs                                       1m24s   2GB
Apr 16 10:00:41 Starting candle/set-theory
Apr 16 10:01:08 Finished candle/set-theory                                       26s 676MB
Apr 16 10:01:08 Starting candle/syntax-lib
Apr 16 10:01:19 Finished candle/syntax-lib                                       10s 646MB
Apr 16 10:01:19 Starting candle/standard/syntax
Apr 16 10:02:39 FAILED: candle/standard/syntax
]0;Holmake: ~/oven/regression/cakeml-800/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-800/basis/pure]0;Holmake: ~/oven/regression/cakeml-800/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-800/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-800/misc]0;Holmake: ~/oven/regression/cakeml-800/developers]0;Holmake: ~/oven/regression/cakeml-800/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-800/misc]0;Holmake: ~/oven/regression/cakeml-800/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-800/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-800/misc]0;Holmake: ~/oven/regression/cakeml-800/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-800/basis/pure]0;Holmake: ~/oven/regression/cakeml-800/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"}