Job 1228

CakeML:126109fde48f06518350d201ec6e93771b1adecc
  Add tight bounds for data_safe_lcgLoop [May 16 13:08:53]
#736 (data-cost)
Merging into:5ada84258acfe6d2ac5c4badb919b738fc22fb03
  Various minor fixes following changes in listTheory [May 18 11:07:52]
HOL:d0b4f135f9d0ca34127c775ce90771ace76482e8
  Fix a MULRELNORM instance: 2 * x = inv 2 * y should canonicalise [May 15 07:11:51]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 18 11:34:42 Claimed job
May 18 11:34:52 Building HOL
May 18 11:46:06 Starting developers
May 18 11:46:09 Finished developers                                               2s  86MB
May 18 11:46:09 Starting developers/bin
May 18 11:46:16 Finished developers/bin                                           6s   1GB
May 18 11:46:16 Starting semantics/ffi
May 18 11:46:24 Finished semantics/ffi                                            8s 248MB
May 18 11:46:24 Starting semantics
May 18 11:47:50 Finished semantics                                             1m25s   1GB
May 18 11:47:50 Starting semantics/proofs
May 18 11:51:04 Finished semantics/proofs                                      3m13s   1GB
May 18 11:51:04 Starting semantics/alt_semantics
May 18 11:51:11 Finished semantics/alt_semantics                                  6s 351MB
May 18 11:51:11 Starting semantics/alt_semantics/proofs
May 18 11:53:12 Finished semantics/alt_semantics/proofs                        2m00s 911MB
May 18 11:53:12 Starting basis/pure
May 18 11:55:58 Finished basis/pure                                            2m45s 839MB
May 18 11:55:58 Starting translator
May 18 11:58:28 Finished translator                                            2m29s   1GB
May 18 11:58:28 Starting compiler/parsing
May 18 11:59:36 Finished compiler/parsing                                      1m07s   3GB
May 18 11:59:36 Starting characteristic
May 18 12:05:18 Finished characteristic                                        5m41s   1GB
May 18 12:05:18 Starting translator/monadic
May 18 12:06:51 Finished translator/monadic                                    1m33s   1GB
May 18 12:06:51 Starting basis
May 18 12:37:12 Finished basis                                                30m19s  17GB
May 18 12:37:12 Starting compiler/inference
May 18 12:38:15 Finished compiler/inference                                    1m02s   1GB
May 18 12:38:15 Starting compiler/backend/reg_alloc
May 18 12:39:16 Finished compiler/backend/reg_alloc                            1m00s   1GB
May 18 12:39:16 Starting compiler/backend/gc
May 18 12:42:32 Finished compiler/backend/gc                                   3m16s   2GB
May 18 12:42:32 Starting compiler/backend
May 18 12:46:59 Finished compiler/backend                                      4m26s   3GB
May 18 12:46:59 Starting compiler/encoders/asm
May 18 12:47:20 Finished compiler/encoders/asm                                   20s 900MB
May 18 12:47:20 Starting compiler/encoders/x64
May 18 12:48:14 Finished compiler/encoders/x64                                   53s 835MB
May 18 12:48:14 Starting compiler/encoders/arm7
May 18 12:50:02 Finished compiler/encoders/arm7                                1m47s   1GB
May 18 12:50:02 Starting compiler/encoders/arm8
May 18 12:50:34 Finished compiler/encoders/arm8                                  31s 626MB
May 18 12:50:34 Starting compiler/encoders/mips
May 18 12:51:38 Finished compiler/encoders/mips                                1m04s   1GB
May 18 12:51:39 Starting compiler/encoders/riscv
May 18 12:52:59 Finished compiler/encoders/riscv                               1m20s   1GB
May 18 12:52:59 Starting compiler/encoders/ag32
May 18 12:53:15 Finished compiler/encoders/ag32                                  16s 752MB
May 18 12:53:15 Starting compiler/backend/x64
May 18 12:53:33 Finished compiler/backend/x64                                    17s   1GB
May 18 12:53:33 Starting compiler/backend/arm7
May 18 12:53:53 Finished compiler/backend/arm7                                   19s   1GB
May 18 12:53:53 Starting compiler/backend/arm8
May 18 12:54:11 Finished compiler/backend/arm8                                   17s   1GB
May 18 12:54:11 Starting compiler/backend/mips
May 18 12:54:29 Finished compiler/backend/mips                                   17s   1GB
May 18 12:54:29 Starting compiler/backend/riscv
May 18 12:54:48 Finished compiler/backend/riscv                                  18s   1GB
May 18 12:54:48 Starting compiler/backend/ag32
May 18 12:55:56 Finished compiler/backend/ag32                                 1m08s   1GB
May 18 12:55:56 Starting compiler/parsing/proofs
May 18 13:01:38 Finished compiler/parsing/proofs                               5m41s   1GB
May 18 13:01:38 Starting compiler/inference/proofs
May 18 13:04:01 Finished compiler/inference/proofs                             2m22s   1GB
May 18 13:04:01 Starting compiler/backend/semantics
May 18 13:31:07 Finished compiler/backend/semantics                           27m05s   2GB
May 18 13:31:07 Starting compiler/backend/reg_alloc/proofs
May 18 13:34:32 Finished compiler/backend/reg_alloc/proofs                     3m25s 790MB
May 18 13:34:32 Starting compiler/backend/proofs
May 18 14:36:27 Finished compiler/backend/proofs                            1h01m54s  17GB
May 18 14:36:27 Starting compiler/encoders/x64/proofs
May 18 14:45:40 Finished compiler/encoders/x64/proofs                          9m12s   5GB
May 18 14:45:40 Starting compiler/encoders/arm7/proofs
May 18 14:58:02 Finished compiler/encoders/arm7/proofs                        12m21s   4GB
May 18 14:58:02 Starting compiler/encoders/arm8/proofs
May 18 15:04:22 Finished compiler/encoders/arm8/proofs                         6m20s   1GB
May 18 15:04:22 Starting compiler/encoders/mips/proofs
May 18 15:14:12 Finished compiler/encoders/mips/proofs                         9m49s   2GB
May 18 15:14:12 Starting compiler/encoders/riscv/proofs
May 18 15:22:36 Finished compiler/encoders/riscv/proofs                        8m24s   1GB
May 18 15:22:36 Starting compiler/encoders/ag32/proofs
May 18 15:25:04 Finished compiler/encoders/ag32/proofs                         2m27s 702MB
May 18 15:25:04 Starting compiler/backend/x64/proofs
May 18 15:25:23 Finished compiler/backend/x64/proofs                             19s   1GB
May 18 15:25:23 Starting compiler/backend/arm7/proofs
May 18 15:25:45 Finished compiler/backend/arm7/proofs                            21s 883MB
May 18 15:25:45 Starting compiler/backend/arm8/proofs
May 18 15:26:03 Finished compiler/backend/arm8/proofs                            18s 841MB
May 18 15:26:03 Starting compiler/backend/mips/proofs
May 18 15:26:23 Finished compiler/backend/mips/proofs                            19s   1GB
May 18 15:26:23 Starting compiler/backend/riscv/proofs
May 18 15:26:42 Finished compiler/backend/riscv/proofs                           19s   1GB
May 18 15:26:43 Starting compiler/backend/ag32/proofs
May 18 15:39:12 Finished compiler/backend/ag32/proofs                         12m29s   2GB
May 18 15:39:12 Starting compiler/proofs
May 18 15:40:54 Finished compiler/proofs                                       1m41s   2GB
May 18 15:40:54 Starting candle/set-theory
May 18 15:41:20 Finished candle/set-theory                                       26s 860MB
May 18 15:41:21 Starting candle/syntax-lib
May 18 15:41:30 Finished candle/syntax-lib                                        9s 716MB
May 18 15:41:31 Starting candle/standard/syntax
May 18 15:43:16 Finished candle/standard/syntax                                1m44s   1GB
May 18 15:43:16 Starting candle/standard/semantics
May 18 15:44:55 Finished candle/standard/semantics                             1m38s   1GB
May 18 15:44:55 Starting candle/standard/monadic
May 18 15:46:31 Finished candle/standard/monadic                               1m36s   1GB
May 18 15:46:31 Starting candle/standard/ml_kernel
May 18 15:51:38 Finished candle/standard/ml_kernel                             5m06s   5GB
May 18 15:51:38 Starting candle/standard/opentheory
May 18 16:00:24 Finished candle/standard/opentheory                            8m45s   4GB
May 18 16:00:24 Starting candle/standard/opentheory/compilation
May 18 16:31:47 Finished candle/standard/opentheory/compilation               31m22s  12GB
May 18 16:31:47 Starting candle/standard/opentheory/compilation/proofs
May 18 16:32:23 Finished candle/standard/opentheory/compilation/proofs           36s   3GB
May 18 16:32:23 Starting candle/overloading/syntax
May 18 16:34:43 FAILED: candle/overloading/syntax
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Starting work on README.md
Starting work on holSyntaxTheory
Starting work on holSyntaxRenamingTheory
README.md                                                                                                                                       real:    0s  user:    0s     OK
holSyntaxRenamingTheory                                                                                                                         real:    8s  user:    8s     OK
holSyntaxTheory                                                                                                                                 real:   25s  user:   24s     OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory                                                                                                                            real:  100s  user:   98s     OK
Starting work on holBoolSyntaxTheory
Starting work on holSyntaxCyclicityTheory
holSyntaxCyclicityTheory                                                                                                                        real:   12s  user:   12sFAIL<1>
       (LR_TYPE_SUBST (EL (PRE n) rs') (SND (EL (PRE n) pqs)))
 
 failed.
 Failed to prove theorem sol_ex_non_orth.
 
 Exception raised at Tactical.FIRST_ASSUM:
  (THEN1 on line 1457)
 error in quse /home/myreen/regression/cakeml-1228/candle/overloading/syntax/holSyntaxCyclicityScript.sml : HOL_ERR {message = " (THEN1 on line 1457)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1228/candle/overloading/syntax/holSyntaxCyclicityScript : HOL_ERR {message = " (THEN1 on line 1457)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 1457)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
holBoolSyntaxTheory                                                                                                                                                     M-KILLED