Job 1424

CakeML:5b960879d6515bc33fd7a0622adeb78daaf4b1e7
  speed up lpr_array [Dec 26 11:10:18]
#809 (lpr)
Merging into:86bded59186b861ecdecf4a8f3019df160b74b98
  fix ramseyScript [Dec 30 02:27:27]
HOL:5921a959757a023b13010b448a2cd05222e641b6
  Prove the converse of PERM_BIJ [Dec 27 00:55:43]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Dec 30 06:31:07 Claimed job
Dec 30 06:31:10 Reusing HOL
Dec 30 06:31:15 Starting developers
Dec 30 06:31:18 Finished developers                                               2s  81MB
Dec 30 06:31:18 Starting developers/bin
Dec 30 06:31:24 Finished developers/bin                                           5s   1GB
Dec 30 06:31:24 Starting semantics/ffi
Dec 30 06:31:34 Finished semantics/ffi                                            9s 284MB
Dec 30 06:31:35 Starting semantics
Dec 30 06:32:59 Finished semantics                                             1m23s   1GB
Dec 30 06:32:59 Starting semantics/proofs
Dec 30 06:36:18 Finished semantics/proofs                                      3m19s   1GB
Dec 30 06:36:18 Starting semantics/alt_semantics
Dec 30 06:36:27 Finished semantics/alt_semantics                                  8s 403MB
Dec 30 06:36:27 Starting semantics/alt_semantics/proofs
Dec 30 06:38:35 Finished semantics/alt_semantics/proofs                        2m08s   1GB
Dec 30 06:38:35 Starting basis/pure
Dec 30 06:39:28 Finished basis/pure                                              52s   1GB
Dec 30 06:39:28 Starting translator
Dec 30 06:42:03 Finished translator                                            2m34s   2GB
Dec 30 06:42:03 Starting compiler/parsing
Dec 30 06:43:11 Finished compiler/parsing                                      1m08s   2GB
Dec 30 06:43:11 Starting characteristic
Dec 30 06:49:10 Finished characteristic                                        5m57s   3GB
Dec 30 06:49:10 Starting translator/monadic
Dec 30 06:50:55 Finished translator/monadic                                    1m44s   2GB
Dec 30 06:50:55 Starting basis
Dec 30 07:24:27 Finished basis                                                33m31s  27GB
Dec 30 07:24:27 Starting compiler/inference
Dec 30 07:25:30 Finished compiler/inference                                    1m02s   1GB
Dec 30 07:25:30 Starting compiler/backend/reg_alloc
Dec 30 07:26:33 Finished compiler/backend/reg_alloc                            1m03s   1GB
Dec 30 07:26:34 Starting compiler/backend/gc
Dec 30 07:29:56 Finished compiler/backend/gc                                   3m22s   3GB
Dec 30 07:29:56 Starting compiler/backend
Dec 30 13:04:43 Resuming compiler/backend
Dec 30 13:04:44 Finished compiler/backend                                         0s  78MB
Dec 30 13:04:44 Starting compiler/encoders/asm
Dec 30 13:05:05 Finished compiler/encoders/asm                                   20s 997MB
Dec 30 13:05:05 Starting compiler/encoders/x64
Dec 30 13:05:32 Finished compiler/encoders/x64                                   26s   1GB
Dec 30 13:05:32 Starting compiler/encoders/arm7
Dec 30 13:06:22 Finished compiler/encoders/arm7                                  50s   1GB
Dec 30 13:06:22 Starting compiler/encoders/arm8
Dec 30 13:06:36 Finished compiler/encoders/arm8                                  13s   1GB
Dec 30 13:06:36 Starting compiler/encoders/mips
Dec 30 13:06:54 Finished compiler/encoders/mips                                  17s   1GB
Dec 30 13:06:55 Starting compiler/encoders/riscv
Dec 30 13:07:11 Finished compiler/encoders/riscv                                 16s   1GB
Dec 30 13:07:11 Starting compiler/encoders/ag32
Dec 30 13:07:29 Finished compiler/encoders/ag32                                  17s 952MB
Dec 30 13:07:29 Starting compiler/backend/x64
Dec 30 13:07:48 Finished compiler/backend/x64                                    18s   1GB
Dec 30 13:07:49 Starting compiler/backend/arm7
Dec 30 13:08:09 Finished compiler/backend/arm7                                   20s   1GB
Dec 30 13:08:09 Starting compiler/backend/arm8
Dec 30 13:08:30 Finished compiler/backend/arm8                                   20s   1GB
Dec 30 13:08:30 Starting compiler/backend/mips
Dec 30 13:08:50 Finished compiler/backend/mips                                   20s   1GB
Dec 30 13:08:51 Starting compiler/backend/riscv
Dec 30 13:09:11 Finished compiler/backend/riscv                                  20s   1GB
Dec 30 13:09:11 Starting compiler/backend/ag32
Dec 30 13:10:22 Finished compiler/backend/ag32                                 1m10s   2GB
Dec 30 13:10:22 Starting compiler/parsing/proofs
Dec 30 13:15:58 Finished compiler/parsing/proofs                               5m36s   3GB
Dec 30 13:15:58 Starting compiler/inference/proofs
Dec 30 13:18:29 Finished compiler/inference/proofs                             2m29s   1GB
Dec 30 13:18:29 Starting compiler/backend/semantics
Dec 30 13:45:43 Finished compiler/backend/semantics                           27m14s   3GB
Dec 30 13:45:43 Starting compiler/backend/reg_alloc/proofs
Dec 30 13:49:02 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
Dec 30 13:49:02 Starting compiler/backend/proofs
Dec 30 14:42:53 Finished compiler/backend/proofs                              53m49s  16GB
Dec 30 14:42:53 Starting compiler/encoders/x64/proofs
Dec 30 14:52:14 Finished compiler/encoders/x64/proofs                          9m21s   6GB
Dec 30 14:52:15 Starting compiler/encoders/arm7/proofs
Dec 30 15:04:47 Finished compiler/encoders/arm7/proofs                        12m32s   9GB
Dec 30 15:04:47 Starting compiler/encoders/arm8/proofs
Dec 30 15:10:59 Finished compiler/encoders/arm8/proofs                         6m12s   3GB
Dec 30 15:11:00 Starting compiler/encoders/mips/proofs
Dec 30 15:20:58 Finished compiler/encoders/mips/proofs                         9m58s   5GB
Dec 30 15:20:58 Starting compiler/encoders/riscv/proofs
Dec 30 15:29:25 Finished compiler/encoders/riscv/proofs                        8m27s   3GB
Dec 30 15:29:25 Starting compiler/encoders/ag32/proofs
Dec 30 15:31:49 Finished compiler/encoders/ag32/proofs                         2m23s   1GB
Dec 30 15:31:49 Starting compiler/backend/x64/proofs
Dec 30 15:32:11 Finished compiler/backend/x64/proofs                             21s   1GB
Dec 30 15:32:11 Starting compiler/backend/arm7/proofs
Dec 30 15:32:34 Finished compiler/backend/arm7/proofs                            22s   1GB
Dec 30 15:32:34 Starting compiler/backend/arm8/proofs
Dec 30 15:32:54 Finished compiler/backend/arm8/proofs                            19s   1GB
Dec 30 15:32:54 Starting compiler/backend/mips/proofs
Dec 30 15:33:16 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 30 15:33:16 Starting compiler/backend/riscv/proofs
Dec 30 15:33:38 Finished compiler/backend/riscv/proofs                           21s   2GB
Dec 30 15:33:38 Starting compiler/backend/ag32/proofs
Dec 30 15:45:40 Finished compiler/backend/ag32/proofs                         12m01s   5GB
Dec 30 15:45:40 Starting compiler/proofs
Dec 30 15:47:20 Finished compiler/proofs                                       1m39s   6GB
Dec 30 15:47:20 Starting candle/set-theory
Dec 30 15:47:48 Finished candle/set-theory                                       28s 922MB
Dec 30 15:47:49 Starting candle/syntax-lib
Dec 30 15:48:00 Finished candle/syntax-lib                                       10s 784MB
Dec 30 15:48:00 Starting candle/standard/syntax
Dec 30 15:49:49 Finished candle/standard/syntax                                1m48s   1GB
Dec 30 15:49:49 Starting candle/standard/semantics
Dec 30 15:51:35 Finished candle/standard/semantics                             1m45s   2GB
Dec 30 15:51:35 Starting candle/standard/monadic
Dec 30 15:53:17 Finished candle/standard/monadic                               1m41s   1GB
Dec 30 15:53:17 Starting candle/standard/ml_kernel
Dec 30 15:58:22 Finished candle/standard/ml_kernel                             5m05s   6GB
Dec 30 15:58:22 Starting candle/overloading/syntax
Dec 30 16:01:33 Finished candle/overloading/syntax                             3m10s   2GB
Dec 30 16:01:33 Starting candle/overloading/semantics
Dec 30 16:13:38 Finished candle/overloading/semantics                         12m04s   9GB
Dec 30 16:13:38 Starting characteristic/examples
Dec 30 16:14:56 Finished characteristic/examples                               1m17s   4GB
Dec 30 16:14:56 Starting tutorial/solutions
Dec 30 16:30:31 Finished tutorial/solutions                                   15m34s  12GB
Dec 30 16:30:31 Starting translator/monadic/examples
Dec 30 16:33:50 Finished translator/monadic/examples                           3m19s   3GB
Dec 30 16:33:50 Starting examples
Dec 30 16:42:30 Finished examples                                              8m39s   7GB
Dec 30 16:42:30 Starting examples/compilation/x64
Dec 30 19:05:44 Finished examples/compilation/x64                           2h23m12s  23GB
Dec 30 19:05:44 Starting examples/compilation/x64/proofs
Dec 30 19:07:41 Finished examples/compilation/x64/proofs                       1m57s   3GB
Dec 30 19:07:41 Starting examples/compilation/ag32
Dec 30 19:41:28 Finished examples/compilation/ag32                            33m46s  11GB
Dec 30 19:41:28 Starting examples/compilation/ag32/proofs
Dec 30 19:42:21 Finished examples/compilation/ag32/proofs                        52s   4GB
Dec 30 19:42:21 Starting examples/cost
Dec 30 20:35:56 Finished examples/cost                                        53m34s  16GB
Dec 30 20:35:56 Starting examples/lpr_checker
Dec 30 20:37:29 FAILED: examples/lpr_checker
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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on README.md
Starting work on satSemTheory
README.md              real:    0s  user:    0s     OK
satSemTheory           real:   11s  user:   10s     OK
Starting work on lprTheory
lprTheory              real:   12s  user:   12s     OK
Starting work on parsingTheory
Starting work on ramseyTheory
parsingTheory          real:   14s  user:   13s     OK
Starting work on lpr_commonProgTheory
ramseyTheory           real:   22s  user:   20s     OK
lpr_commonProgTheory   real:   54s  user:   52sFAIL<1>
 NONE =
 case check_lpr_step x' fml of NONE => NONE | SOME fml' => check_lpr x fml'
 
 Failed to prove theorem parse_and_run_file_eq.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/myreen/regression/cakeml-1424/examples/lpr_checker/lpr_commonProgScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1424/examples/lpr_checker/lpr_commonProgScript : 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"}