Job 799

CakeML:fcc5a94f9d5425e6b678ee610a9226cab8fa20bf
  Fix bug in recursive post-processing of monadic translator [Apr 15 15:51:13]
#627 (monadic-trans-cleanup)
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:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 16 06:49:16 Claimed job
Apr 16 06:50:06 Building HOL
Apr 16 06:58:05 Starting developers
Apr 16 06:58:06 Finished developers                                               0s  22MB
Apr 16 06:58:06 Starting developers/bin
Apr 16 06:58:41 Finished developers/bin                                          34s 204MB
Apr 16 06:58:41 Starting semantics/ffi
Apr 16 06:59:16 Finished semantics/ffi                                           33s 519MB
Apr 16 06:59:16 Starting semantics
Apr 16 07:00:48 Finished semantics                                             1m32s   1GB
Apr 16 07:00:49 Starting semantics/proofs
Apr 16 07:03:46 Finished semantics/proofs                                      2m56s   1GB
Apr 16 07:03:46 Starting basis/pure
Apr 16 07:07:21 Finished basis/pure                                            3m34s 641MB
Apr 16 07:07:22 Starting translator
Apr 16 07:09:00 Finished translator                                            1m37s   1GB
Apr 16 07:09:00 Starting compiler/parsing
Apr 16 07:09:59 Finished compiler/parsing                                        58s   2GB
Apr 16 07:10:00 Starting characteristic
Apr 16 07:15:11 Finished characteristic                                        5m11s   1GB
Apr 16 07:15:12 Starting translator/monadic
Apr 16 07:16:37 Finished translator/monadic                                    1m25s   1GB
Apr 16 07:16:38 Starting basis
Apr 16 07:33:24 Finished basis                                                16m46s   2GB
Apr 16 07:33:24 Starting compiler/inference
Apr 16 07:35:12 Finished compiler/inference                                    1m46s   1GB
Apr 16 07:35:12 Starting compiler/backend/reg_alloc
Apr 16 07:36:11 Finished compiler/backend/reg_alloc                              58s   1GB
Apr 16 07:36:11 Starting compiler/backend/gc
Apr 16 07:45:21 Finished compiler/backend/gc                                   9m09s   2GB
Apr 16 07:45:21 Starting compiler/backend
Apr 16 07:45:23 Finished compiler/backend                                         0s  42MB
Apr 16 07:45:23 Starting compiler/encoders/asm
Apr 16 07:45:23 Finished compiler/encoders/asm                                    0s  32MB
Apr 16 07:45:24 Starting compiler/encoders/x64
Apr 16 07:46:20 Finished compiler/encoders/x64                                   56s 955MB
Apr 16 07:46:21 Starting compiler/encoders/arm6
Apr 16 07:47:56 Finished compiler/encoders/arm6                                1m35s   1GB
Apr 16 07:47:57 Starting compiler/encoders/arm8
Apr 16 07:48:26 Finished compiler/encoders/arm8                                  29s 637MB
Apr 16 07:48:27 Starting compiler/encoders/mips
Apr 16 07:49:33 Finished compiler/encoders/mips                                1m05s 876MB
Apr 16 07:49:33 Starting compiler/encoders/riscv
Apr 16 07:50:51 Finished compiler/encoders/riscv                               1m18s 811MB
Apr 16 07:50:52 Starting compiler/encoders/ag32
Apr 16 07:51:07 Finished compiler/encoders/ag32                                  15s 782MB
Apr 16 07:51:08 Starting compiler/backend/x64
Apr 16 07:51:23 Finished compiler/backend/x64                                    14s 926MB
Apr 16 07:51:23 Starting compiler/backend/arm6
Apr 16 07:51:42 Finished compiler/backend/arm6                                   18s   1GB
Apr 16 07:51:42 Starting compiler/backend/arm8
Apr 16 07:51:59 Finished compiler/backend/arm8                                   16s 888MB
Apr 16 07:51:59 Starting compiler/backend/mips
Apr 16 07:52:16 Finished compiler/backend/mips                                   16s   1GB
Apr 16 07:52:16 Starting compiler/backend/riscv
Apr 16 07:52:33 Finished compiler/backend/riscv                                  16s   1GB
Apr 16 07:52:33 Starting compiler/backend/ag32
Apr 16 07:53:41 Finished compiler/backend/ag32                                 1m07s   1GB
Apr 16 07:53:42 Starting compiler/parsing/proofs
Apr 16 07:59:23 Finished compiler/parsing/proofs                               5m41s 815MB
Apr 16 07:59:23 Starting compiler/inference/proofs
Apr 16 08:02:06 Finished compiler/inference/proofs                             2m41s 971MB
Apr 16 08:02:06 Starting compiler/backend/semantics
Apr 16 08:09:18 Finished compiler/backend/semantics                            7m11s   2GB
Apr 16 08:09:18 Starting compiler/backend/reg_alloc/proofs
Apr 16 08:12:33 Finished compiler/backend/reg_alloc/proofs                     3m14s   1GB
Apr 16 08:12:34 Starting compiler/backend/proofs
Apr 16 08:51:31 Finished compiler/backend/proofs                              38m56s   4GB
Apr 16 08:51:31 Starting compiler/encoders/x64/proofs
Apr 16 09:01:44 Finished compiler/encoders/x64/proofs                         10m13s   4GB
Apr 16 09:01:45 Starting compiler/encoders/arm6/proofs
Apr 16 09:15:39 Finished compiler/encoders/arm6/proofs                        13m53s   3GB
Apr 16 09:15:39 Starting compiler/encoders/arm8/proofs
Apr 16 09:21:27 Finished compiler/encoders/arm8/proofs                         5m47s   1GB
Apr 16 09:21:27 Starting compiler/encoders/mips/proofs
Apr 16 09:31:39 Finished compiler/encoders/mips/proofs                        10m11s   2GB
Apr 16 09:31:39 Starting compiler/encoders/riscv/proofs
Apr 16 09:40:14 Finished compiler/encoders/riscv/proofs                        8m34s   1GB
Apr 16 09:40:15 Starting compiler/encoders/ag32/proofs
Apr 16 09:42:45 Finished compiler/encoders/ag32/proofs                         2m30s 856MB
Apr 16 09:42:46 Starting compiler/backend/x64/proofs
Apr 16 09:43:03 Finished compiler/backend/x64/proofs                             17s   1GB
Apr 16 09:43:03 Starting compiler/backend/arm6/proofs
Apr 16 09:43:22 Finished compiler/backend/arm6/proofs                            18s 852MB
Apr 16 09:43:23 Starting compiler/backend/arm8/proofs
Apr 16 09:43:40 Finished compiler/backend/arm8/proofs                            16s   1GB
Apr 16 09:43:40 Starting compiler/backend/mips/proofs
Apr 16 09:43:58 Finished compiler/backend/mips/proofs                            17s   1GB
Apr 16 09:43:58 Starting compiler/backend/riscv/proofs
Apr 16 09:44:15 Finished compiler/backend/riscv/proofs                           16s   1GB
Apr 16 09:44:15 Starting compiler/backend/ag32/proofs
Apr 16 09:53:26 Finished compiler/backend/ag32/proofs                          9m08s   2GB
Apr 16 09:53:26 Starting compiler/proofs
Apr 16 09:54:44 Finished compiler/proofs                                       1m17s   2GB
Apr 16 09:54:45 Starting candle/set-theory
Apr 16 09:55:10 Finished candle/set-theory                                       25s 817MB
Apr 16 09:55:10 Starting candle/syntax-lib
Apr 16 09:55:20 Finished candle/syntax-lib                                        9s 619MB
Apr 16 09:55:20 Starting candle/standard/syntax
Apr 16 09:56:38 FAILED: candle/standard/syntax
]0;Holmake: ~/regression/cakeml-799/basis/pure]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-799/basis/pure]0;Holmake: ~/regression/cakeml-799/misc]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-799/misc]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-799/misc]0;Holmake: ~/regression/cakeml-799/developers]0;Holmake: ~/regression/cakeml-799/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-799/misc]0;Holmake: ~/regression/cakeml-799/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-799/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-799/misc]0;Holmake: ~/regression/cakeml-799/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-799/basis/pure]0;Holmake: ~/regression/cakeml-799/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-lib[1mWorking in $(CAKEMLDIR)/candle/syntax-lib[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/candle/standard/syntax[0m
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>
 
 codomain (codomain (Fun (Fun Bool Bool) (Fun (Fun Bool Bool) Bool))) = Bool
 
 Failed to prove theorem bool_has_bool_sig.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/myreen/regression/cakeml-799/candle/standard/syntax/holBoolSyntaxScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load holBoolSyntaxScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}