Job 1229

CakeML: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 18 11:36:21 Claimed job
May 18 11:36:30 Building HOL
May 18 11:49:32 Starting developers
May 18 11:49:36 Finished developers                                               4s 108MB
May 18 11:49:37 Starting developers/bin
May 18 11:49:44 Finished developers/bin                                           7s   1GB
May 18 11:49:44 Starting semantics/ffi
May 18 11:49:55 Finished semantics/ffi                                           10s 237MB
May 18 11:49:55 Starting semantics
May 18 11:51:27 Finished semantics                                             1m32s   1GB
May 18 11:51:28 Starting semantics/proofs
May 18 11:54:58 Finished semantics/proofs                                      3m30s 877MB
May 18 11:54:59 Starting semantics/alt_semantics
May 18 11:55:07 Finished semantics/alt_semantics                                  8s 298MB
May 18 11:55:07 Starting semantics/alt_semantics/proofs
May 18 11:57:21 Finished semantics/alt_semantics/proofs                        2m13s 936MB
May 18 11:57:21 Starting basis/pure
May 18 12:00:27 Finished basis/pure                                            3m05s 851MB
May 18 12:00:27 Starting translator
May 18 12:03:07 Finished translator                                            2m40s   1GB
May 18 12:03:07 Starting compiler/parsing
May 18 12:04:20 Finished compiler/parsing                                      1m12s   2GB
May 18 12:04:20 Starting characteristic
May 18 12:10:23 Finished characteristic                                        6m03s   1GB
May 18 12:10:24 Starting translator/monadic
May 18 12:12:03 Finished translator/monadic                                    1m39s   1GB
May 18 12:12:03 Starting basis
May 18 12:45:40 Finished basis                                                33m36s  17GB
May 18 12:45:40 Starting compiler/inference
May 18 12:46:50 Finished compiler/inference                                    1m10s   1GB
May 18 12:46:50 Starting compiler/backend/reg_alloc
May 18 12:47:54 Finished compiler/backend/reg_alloc                            1m03s   1GB
May 18 12:47:54 Starting compiler/backend/gc
May 18 12:51:29 Finished compiler/backend/gc                                   3m34s   2GB
May 18 12:51:29 Starting compiler/backend
May 18 12:56:08 Finished compiler/backend                                      4m38s   4GB
May 18 12:56:08 Starting compiler/encoders/asm
May 18 12:56:30 Finished compiler/encoders/asm                                   22s 807MB
May 18 12:56:30 Starting compiler/encoders/x64
May 18 12:57:30 Finished compiler/encoders/x64                                   59s 898MB
May 18 12:57:30 Starting compiler/encoders/arm7
May 18 12:59:21 Finished compiler/encoders/arm7                                1m50s   1GB
May 18 12:59:21 Starting compiler/encoders/arm8
May 18 12:59:55 Finished compiler/encoders/arm8                                  33s 565MB
May 18 12:59:55 Starting compiler/encoders/mips
May 18 13:01:07 Finished compiler/encoders/mips                                1m11s 912MB
May 18 13:01:08 Starting compiler/encoders/riscv
May 18 13:02:33 Finished compiler/encoders/riscv                               1m25s   1GB
May 18 13:02:34 Starting compiler/encoders/ag32
May 18 13:02:51 Finished compiler/encoders/ag32                                  17s 822MB
May 18 13:02:51 Starting compiler/backend/x64
May 18 13:03:09 Finished compiler/backend/x64                                    17s   1GB
May 18 13:03:10 Starting compiler/backend/arm7
May 18 13:03:30 Finished compiler/backend/arm7                                   20s   1GB
May 18 13:03:31 Starting compiler/backend/arm8
May 18 13:03:49 Finished compiler/backend/arm8                                   18s   1GB
May 18 13:03:49 Starting compiler/backend/mips
May 18 13:04:09 Finished compiler/backend/mips                                   19s   1GB
May 18 13:04:09 Starting compiler/backend/riscv
May 18 13:04:28 Finished compiler/backend/riscv                                  19s   1GB
May 18 13:04:29 Starting compiler/backend/ag32
May 18 13:05:42 Finished compiler/backend/ag32                                 1m13s   1GB
May 18 13:05:42 Starting compiler/parsing/proofs
May 18 13:11:34 Finished compiler/parsing/proofs                               5m51s   1GB
May 18 13:11:34 Starting compiler/inference/proofs
May 18 13:14:11 Finished compiler/inference/proofs                             2m37s   1GB
May 18 13:14:11 Starting compiler/backend/semantics
May 18 13:45:42 Finished compiler/backend/semantics                           31m30s   2GB
May 18 13:45:43 Starting compiler/backend/reg_alloc/proofs
May 18 13:49:27 Finished compiler/backend/reg_alloc/proofs                     3m43s 721MB
May 18 13:49:27 Starting compiler/backend/proofs
May 18 14:56:35 Finished compiler/backend/proofs                            1h07m07s  13GB
May 18 14:56:35 Starting compiler/encoders/x64/proofs
May 18 15:06:36 Finished compiler/encoders/x64/proofs                         10m01s   4GB
May 18 15:06:37 Starting compiler/encoders/arm7/proofs
May 18 15:20:16 Finished compiler/encoders/arm7/proofs                        13m38s   3GB
May 18 15:20:16 Starting compiler/encoders/arm8/proofs
May 18 15:27:07 Finished compiler/encoders/arm8/proofs                         6m50s   1GB
May 18 15:27:07 Starting compiler/encoders/mips/proofs
May 18 15:37:45 Finished compiler/encoders/mips/proofs                        10m38s   2GB
May 18 15:37:45 Starting compiler/encoders/riscv/proofs
May 18 15:46:55 Finished compiler/encoders/riscv/proofs                        9m09s   1GB
May 18 15:46:55 Starting compiler/encoders/ag32/proofs
May 18 15:49:39 Finished compiler/encoders/ag32/proofs                         2m43s 831MB
May 18 15:49:39 Starting compiler/backend/x64/proofs
May 18 15:49:59 Finished compiler/backend/x64/proofs                             19s 928MB
May 18 15:49:59 Starting compiler/backend/arm7/proofs
May 18 15:50:20 Finished compiler/backend/arm7/proofs                            20s   1GB
May 18 15:50:20 Starting compiler/backend/arm8/proofs
May 18 15:50:40 Finished compiler/backend/arm8/proofs                            19s   1GB
May 18 15:50:40 Starting compiler/backend/mips/proofs
May 18 15:51:01 Finished compiler/backend/mips/proofs                            20s   1GB
May 18 15:51:01 Starting compiler/backend/riscv/proofs
May 18 15:51:22 Finished compiler/backend/riscv/proofs                           20s 843MB
May 18 15:51:22 Starting compiler/backend/ag32/proofs
May 18 16:05:04 Finished compiler/backend/ag32/proofs                         13m42s   3GB
May 18 16:05:05 Starting compiler/proofs
May 18 16:06:53 Finished compiler/proofs                                       1m48s   3GB
May 18 16:06:53 Starting candle/set-theory
May 18 16:07:22 Finished candle/set-theory                                       28s 802MB
May 18 16:07:22 Starting candle/syntax-lib
May 18 16:07:33 Finished candle/syntax-lib                                       10s 683MB
May 18 16:07:33 Starting candle/standard/syntax
May 18 16:09:26 Finished candle/standard/syntax                                1m53s 985MB
May 18 16:09:26 Starting candle/standard/semantics
May 18 16:11:13 Finished candle/standard/semantics                             1m46s   1GB
May 18 16:11:13 Starting candle/standard/monadic
May 18 16:12:58 Finished candle/standard/monadic                               1m44s   1GB
May 18 16:12:58 Starting candle/standard/ml_kernel
May 18 16:18:33 Finished candle/standard/ml_kernel                             5m35s   4GB
May 18 16:18:33 Starting candle/standard/opentheory
May 18 16:28:07 Finished candle/standard/opentheory                            9m33s   4GB
May 18 16:28:07 Starting candle/standard/opentheory/compilation
May 18 16:59:44 Finished candle/standard/opentheory/compilation               31m36s  20GB
May 18 16:59:44 Starting candle/standard/opentheory/compilation/proofs
May 18 17:00:23 Finished candle/standard/opentheory/compilation/proofs           38s   3GB
May 18 17:00:23 Starting candle/overloading/syntax
May 18 17:02:54 FAILED: candle/overloading/syntax
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle/syntax-lib
Starting work on README.md
Starting work on holSyntaxTheory
Starting work on holSyntaxRenamingTheory
README.md                                       real:    0s  user:    0s     OK
holSyntaxRenamingTheory                         real:    9s  user:    8s     OK
holSyntaxTheory                                 real:   25s  user:   23s     OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory                            real:  111s  user:  108s     OK
Starting work on holBoolSyntaxTheory
Starting work on holSyntaxCyclicityTheory
holSyntaxCyclicityTheory                        real:   13s  user:   12sFAIL<1>
     monotone (dependency ctxt)  mg_sol_seq rs' (TAKE n pqs) 
     path_starting_at ctxt k rs' (TAKE n pqs) 
     is_instance_LR (LR_TYPE_SUBST (EL (PRE n) rs') (SND (EL (PRE n) pqs)))
       (FST (EL n pqs)) 
     is_instance_LR (FST (EL n pqs))
       (LR_TYPE_SUBST (EL (PRE n) rs') (SND (EL (PRE n) pqs)))
 
 failed.
 Failed to prove theorem sol_ex_non_orth.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 1457)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
holBoolSyntaxTheory                                                     M-KILLED