Job 1318

CakeML:478cfe8702e4c49fdad6b5bd829af59f06345a33
  Get past a few build failures [Aug 05 17:17:05]
HOL:a084f49e1bf9a108a354cd01a025118182b72fd5
  emacs-mode: Fix error in detection of end of open declarations [Aug 04 04:40:14]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 05 17:17:33 Claimed job
Aug 05 17:17:39 Reusing HOL
Aug 05 17:17:45 Starting developers
Aug 05 17:17:46 Finished developers                                               0s  32MB
Aug 05 17:17:46 Starting developers/bin
Aug 05 17:17:52 Finished developers/bin                                           6s   1GB
Aug 05 17:17:52 Starting semantics/ffi
Aug 05 17:18:03 Finished semantics/ffi                                           10s 303MB
Aug 05 17:18:03 Starting semantics
Aug 05 17:19:32 Finished semantics                                             1m28s   1GB
Aug 05 17:19:32 Starting semantics/proofs
Aug 05 17:23:05 Finished semantics/proofs                                      3m33s   2GB
Aug 05 17:23:05 Starting semantics/alt_semantics
Aug 05 17:23:14 Finished semantics/alt_semantics                                  9s 426MB
Aug 05 17:23:15 Starting semantics/alt_semantics/proofs
Aug 05 17:25:20 Finished semantics/alt_semantics/proofs                        2m05s   1GB
Aug 05 17:25:20 Starting basis/pure
Aug 05 17:26:15 Finished basis/pure                                              54s   1GB
Aug 05 17:26:15 Starting translator
Aug 05 17:29:02 Finished translator                                            2m46s   1GB
Aug 05 17:29:02 Starting compiler/parsing
Aug 05 17:30:21 Finished compiler/parsing                                      1m18s   4GB
Aug 05 17:30:22 Starting characteristic
Aug 05 17:36:25 Finished characteristic                                        6m03s   5GB
Aug 05 17:36:25 Starting translator/monadic
Aug 05 17:38:10 Finished translator/monadic                                    1m44s   3GB
Aug 05 17:38:10 Starting basis
Aug 05 18:13:01 Finished basis                                                34m49s  37GB
Aug 05 18:13:01 Starting compiler/inference
Aug 05 18:14:10 Finished compiler/inference                                    1m08s   1GB
Aug 05 18:14:10 Starting compiler/backend/reg_alloc
Aug 05 18:15:21 Finished compiler/backend/reg_alloc                            1m10s   1GB
Aug 05 18:15:21 Starting compiler/backend/gc
Aug 05 18:19:03 Finished compiler/backend/gc                                   3m42s   4GB
Aug 05 18:19:03 Starting compiler/backend
Aug 05 18:24:38 Finished compiler/backend                                      5m34s   4GB
Aug 05 18:24:39 Starting compiler/encoders/asm
Aug 05 18:25:03 Finished compiler/encoders/asm                                   24s   1GB
Aug 05 18:25:03 Starting compiler/encoders/x64
Aug 05 18:25:32 Finished compiler/encoders/x64                                   28s   1GB
Aug 05 18:25:32 Starting compiler/encoders/arm7
Aug 05 18:26:25 Finished compiler/encoders/arm7                                  52s   1GB
Aug 05 18:26:25 Starting compiler/encoders/arm8
Aug 05 18:26:39 Finished compiler/encoders/arm8                                  14s   1GB
Aug 05 18:26:39 Starting compiler/encoders/mips
Aug 05 18:26:58 Finished compiler/encoders/mips                                  18s   1GB
Aug 05 18:26:58 Starting compiler/encoders/riscv
Aug 05 18:27:16 Finished compiler/encoders/riscv                                 17s   1GB
Aug 05 18:27:16 Starting compiler/encoders/ag32
Aug 05 18:27:36 Finished compiler/encoders/ag32                                  20s 957MB
Aug 05 18:27:36 Starting compiler/backend/x64
Aug 05 18:27:56 Finished compiler/backend/x64                                    19s   1GB
Aug 05 18:27:57 Starting compiler/backend/arm7
Aug 05 18:28:17 Finished compiler/backend/arm7                                   20s   1GB
Aug 05 18:28:17 Starting compiler/backend/arm8
Aug 05 18:28:37 Finished compiler/backend/arm8                                   19s   1GB
Aug 05 18:28:37 Starting compiler/backend/mips
Aug 05 18:28:58 Finished compiler/backend/mips                                   19s   1GB
Aug 05 18:28:58 Starting compiler/backend/riscv
Aug 05 18:29:19 Finished compiler/backend/riscv                                  21s   1GB
Aug 05 18:29:19 Starting compiler/backend/ag32
Aug 05 18:30:34 Finished compiler/backend/ag32                                 1m15s   2GB
Aug 05 18:30:35 Starting compiler/parsing/proofs
Aug 05 18:32:49 Finished compiler/parsing/proofs                               2m14s   1GB
Aug 05 18:32:49 Starting compiler/inference/proofs
Aug 05 18:35:15 Finished compiler/inference/proofs                             2m25s   1GB
Aug 05 18:35:16 Starting compiler/backend/semantics
Aug 05 19:01:00 Finished compiler/backend/semantics                           25m44s   4GB
Aug 05 19:01:00 Starting compiler/backend/reg_alloc/proofs
Aug 05 19:04:12 Finished compiler/backend/reg_alloc/proofs                     3m11s   1GB
Aug 05 19:04:12 Starting compiler/backend/proofs
Aug 05 19:54:43 Finished compiler/backend/proofs                              50m29s  14GB
Aug 05 19:54:43 Starting compiler/encoders/x64/proofs
Aug 05 20:03:57 Finished compiler/encoders/x64/proofs                          9m13s   8GB
Aug 05 20:03:57 Starting compiler/encoders/arm7/proofs
Aug 05 20:16:30 Finished compiler/encoders/arm7/proofs                        12m32s   3GB
Aug 05 20:16:30 Starting compiler/encoders/arm8/proofs
Aug 05 20:22:44 Finished compiler/encoders/arm8/proofs                         6m13s   3GB
Aug 05 20:22:44 Starting compiler/encoders/mips/proofs
Aug 05 20:32:33 Finished compiler/encoders/mips/proofs                         9m49s   5GB
Aug 05 20:32:33 Starting compiler/encoders/riscv/proofs
Aug 05 20:40:26 Finished compiler/encoders/riscv/proofs                        7m52s   4GB
Aug 05 20:40:26 Starting compiler/encoders/ag32/proofs
Aug 05 20:42:46 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Aug 05 20:42:46 Starting compiler/backend/x64/proofs
Aug 05 20:43:07 Finished compiler/backend/x64/proofs                             20s   1GB
Aug 05 20:43:07 Starting compiler/backend/arm7/proofs
Aug 05 20:43:29 Finished compiler/backend/arm7/proofs                            21s   1GB
Aug 05 20:43:29 Starting compiler/backend/arm8/proofs
Aug 05 20:43:48 Finished compiler/backend/arm8/proofs                            18s   1GB
Aug 05 20:43:48 Starting compiler/backend/mips/proofs
Aug 05 20:44:08 Finished compiler/backend/mips/proofs                            19s   1GB
Aug 05 20:44:08 Starting compiler/backend/riscv/proofs
Aug 05 20:44:30 Finished compiler/backend/riscv/proofs                           21s   1GB
Aug 05 20:44:30 Starting compiler/backend/ag32/proofs
Aug 05 20:56:19 Finished compiler/backend/ag32/proofs                         11m48s   4GB
Aug 05 20:56:19 Starting compiler/proofs
Aug 05 20:57:47 FAILED: compiler/proofs
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/proofs[0m
Starting work on simpleSexpPEGTheory
simpleSexpPEGTheory                                                                                                                                real:    2s  user:    2s     OK
Starting work on simpleSexpParseTheory
simpleSexpParseTheory                                                                                                                              real:   11s  user:   11s     OK
Starting work on compilerTheory
compilerTheory                                                                                                                                     real:   41s  user:   39s     OK
Starting work on compilerProofTheory
compilerProofTheory                                                                                                                                real:   29s  user:   28sFAIL<1>
 parse_prog = parse
 
 failed.
 Failed to prove theorem parse_prog_correct.
 
 Exception raised at Tactical.Q_TAC:
 No parse of quotation leads to success
 error in quse /home/myreen/regression/cakeml-1318/compiler/proofs/compilerProofScript.sml : HOL_ERR {message = "No parse of quotation leads to success", origin_function = "Q_TAC", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1318/compiler/proofs/compilerProofScript : HOL_ERR {message = "No parse of quotation leads to success", origin_function = "Q_TAC", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "No parse of quotation leads to success", origin_function = "Q_TAC", origin_structure = "Tactical"}