Job 1563

CakeML:67fd272ad040a95fd349fe9a288ee581405236eb
  Remove a typo [Aug 01 11:49:52]
#831 (pancake)
Merging into:76ed0b05089a77059dee72d197fc56c3dae661e8
  Merge pull request #829 from CakeML/help [Jun 18 08:39:57]
HOL:86ba104c9158cbe3b2faf47bbaefb92817c65f14
  Improve some theorem statement indentation [Jul 28 00:08:30]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 01 16:51:29 Claimed job
Aug 01 16:51:30 Reusing HOL
Aug 01 16:51:36 Starting developers
Aug 01 16:51:36 Finished developers                                               0s  36MB
Aug 01 16:51:36 Starting developers/bin
Aug 01 16:51:42 Finished developers/bin                                           5s   1GB
Aug 01 16:51:43 Starting semantics/ffi
Aug 01 16:51:53 Finished semantics/ffi                                           10s 311MB
Aug 01 16:51:53 Starting semantics
Aug 01 16:53:19 Finished semantics                                             1m25s   1GB
Aug 01 16:53:19 Starting semantics/proofs
Aug 01 16:56:54 Finished semantics/proofs                                      3m34s   1GB
Aug 01 16:56:54 Starting semantics/alt_semantics
Aug 01 16:57:03 Finished semantics/alt_semantics                                  8s 425MB
Aug 01 16:57:03 Starting semantics/alt_semantics/proofs
Aug 01 16:59:16 Finished semantics/alt_semantics/proofs                        2m12s   1GB
Aug 01 16:59:16 Starting basis/pure
Aug 01 17:00:10 Finished basis/pure                                              53s   1GB
Aug 01 17:00:10 Starting translator
Aug 01 17:03:29 Finished translator                                            3m19s   2GB
Aug 01 17:03:30 Starting compiler/parsing
Aug 01 17:04:39 Finished compiler/parsing                                      1m08s   4GB
Aug 01 17:04:39 Starting characteristic
Aug 01 17:10:26 Finished characteristic                                        5m46s   3GB
Aug 01 17:10:26 Starting translator/monadic
Aug 01 17:12:11 Finished translator/monadic                                    1m44s   3GB
Aug 01 17:12:11 Starting basis
Aug 01 17:56:40 Finished basis                                                44m29s  42GB
Aug 01 17:56:41 Starting compiler/inference
Aug 01 17:57:48 Finished compiler/inference                                    1m07s   1GB
Aug 01 17:57:49 Starting compiler/backend/reg_alloc
Aug 01 17:58:55 Finished compiler/backend/reg_alloc                            1m06s   2GB
Aug 01 17:58:56 Starting compiler/backend/gc
Aug 01 18:02:25 Finished compiler/backend/gc                                   3m29s   3GB
Aug 01 18:02:25 Starting compiler/backend
Aug 01 18:07:38 Finished compiler/backend                                      5m13s   5GB
Aug 01 18:07:38 Starting compiler/encoders/asm
Aug 01 18:08:01 Finished compiler/encoders/asm                                   22s   1GB
Aug 01 18:08:01 Starting compiler/encoders/x64
Aug 01 18:08:29 Finished compiler/encoders/x64                                   27s   1GB
Aug 01 18:08:29 Starting compiler/encoders/arm7
Aug 01 18:09:20 Finished compiler/encoders/arm7                                  50s   1GB
Aug 01 18:09:20 Starting compiler/encoders/arm8
Aug 01 18:09:34 Finished compiler/encoders/arm8                                  13s   1GB
Aug 01 18:09:34 Starting compiler/encoders/mips
Aug 01 18:09:52 Finished compiler/encoders/mips                                  18s   1GB
Aug 01 18:09:52 Starting compiler/encoders/riscv
Aug 01 18:10:09 Finished compiler/encoders/riscv                                 16s   1GB
Aug 01 18:10:10 Starting compiler/encoders/ag32
Aug 01 18:10:28 Finished compiler/encoders/ag32                                  18s 967MB
Aug 01 18:10:29 Starting compiler/backend/x64
Aug 01 18:10:49 Finished compiler/backend/x64                                    20s   1GB
Aug 01 18:10:49 Starting compiler/backend/arm7
Aug 01 18:11:12 Finished compiler/backend/arm7                                   22s   1GB
Aug 01 18:11:12 Starting compiler/backend/arm8
Aug 01 18:11:32 Finished compiler/backend/arm8                                   20s   1GB
Aug 01 18:11:32 Starting compiler/backend/mips
Aug 01 18:11:53 Finished compiler/backend/mips                                   21s   1GB
Aug 01 18:11:54 Starting compiler/backend/riscv
Aug 01 18:12:15 Finished compiler/backend/riscv                                  21s   1GB
Aug 01 18:12:15 Starting compiler/backend/ag32
Aug 01 18:13:27 Finished compiler/backend/ag32                                 1m11s   2GB
Aug 01 18:13:28 Starting compiler/parsing/proofs
Aug 01 18:19:06 Finished compiler/parsing/proofs                               5m38s   2GB
Aug 01 18:19:06 Starting compiler/inference/proofs
Aug 01 18:21:40 Finished compiler/inference/proofs                             2m33s   3GB
Aug 01 18:21:40 Starting compiler/backend/semantics
Aug 01 18:48:22 Finished compiler/backend/semantics                           26m41s   4GB
Aug 01 18:48:22 Starting compiler/backend/reg_alloc/proofs
Aug 01 18:51:41 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
Aug 01 18:51:41 Starting compiler/backend/proofs
Aug 01 19:45:50 Finished compiler/backend/proofs                              54m07s  29GB
Aug 01 19:45:50 Starting compiler/encoders/x64/proofs
Aug 01 19:55:19 Finished compiler/encoders/x64/proofs                          9m29s   4GB
Aug 01 19:55:19 Starting compiler/encoders/arm7/proofs
Aug 01 20:08:00 Finished compiler/encoders/arm7/proofs                        12m40s   4GB
Aug 01 20:08:00 Starting compiler/encoders/arm8/proofs
Aug 01 20:14:38 Finished compiler/encoders/arm8/proofs                         6m37s   3GB
Aug 01 20:14:38 Starting compiler/encoders/mips/proofs
Aug 01 20:24:24 Finished compiler/encoders/mips/proofs                         9m46s   5GB
Aug 01 20:24:24 Starting compiler/encoders/riscv/proofs
Aug 01 20:32:51 Finished compiler/encoders/riscv/proofs                        8m26s   3GB
Aug 01 20:32:51 Starting compiler/encoders/ag32/proofs
Aug 01 20:35:13 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Aug 01 20:35:13 Starting compiler/backend/x64/proofs
Aug 01 20:35:36 Finished compiler/backend/x64/proofs                             22s   1GB
Aug 01 20:35:36 Starting compiler/backend/arm7/proofs
Aug 01 20:36:00 Finished compiler/backend/arm7/proofs                            24s   1GB
Aug 01 20:36:00 Starting compiler/backend/arm8/proofs
Aug 01 20:36:24 Finished compiler/backend/arm8/proofs                            23s   2GB
Aug 01 20:36:24 Starting compiler/backend/mips/proofs
Aug 01 20:36:47 Finished compiler/backend/mips/proofs                            22s   1GB
Aug 01 20:36:47 Starting compiler/backend/riscv/proofs
Aug 01 20:37:11 Finished compiler/backend/riscv/proofs                           23s   2GB
Aug 01 20:37:11 Starting compiler/backend/ag32/proofs
Aug 01 20:49:26 Finished compiler/backend/ag32/proofs                         12m15s   5GB
Aug 01 20:49:27 Starting compiler/proofs
Aug 01 20:51:15 Finished compiler/proofs                                       1m48s   6GB
Aug 01 20:51:15 Starting candle/set-theory
Aug 01 20:51:46 Finished candle/set-theory                                       30s   1GB
Aug 01 20:51:47 Starting candle/syntax-lib
Aug 01 20:51:58 Finished candle/syntax-lib                                       11s 832MB
Aug 01 20:51:58 Starting candle/standard/syntax
Aug 01 20:53:53 Finished candle/standard/syntax                                1m54s   1GB
Aug 01 20:53:53 Starting candle/standard/semantics
Aug 01 20:55:46 Finished candle/standard/semantics                             1m52s   2GB
Aug 01 20:55:46 Starting candle/standard/monadic
Aug 01 20:57:34 Finished candle/standard/monadic                               1m47s   1GB
Aug 01 20:57:34 Starting candle/standard/ml_kernel
Aug 01 21:03:18 Finished candle/standard/ml_kernel                             5m43s   5GB
Aug 01 21:03:19 Starting candle/overloading/syntax
Aug 01 21:06:31 Finished candle/overloading/syntax                             3m12s   1GB
Aug 01 21:06:31 Starting candle/overloading/semantics
Aug 01 21:18:34 Finished candle/overloading/semantics                         12m03s   9GB
Aug 01 21:18:35 Starting pancake
Aug 01 21:19:34 Finished pancake                                                 58s   1GB
Aug 01 21:19:34 Starting pancake/ffi
Aug 01 21:19:34 Finished pancake/ffi                                              0s   6MB
Aug 01 21:19:34 Starting pancake/semantics
Aug 01 21:21:49 Finished pancake/semantics                                     2m14s   1GB
Aug 01 21:21:49 Starting pancake/proofs
Aug 01 21:34:37 FAILED: pancake/proofs
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[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)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/pancake/semantics[0m
Starting work on loop_callProofTheory
Starting work on loop_removeProofTheory
Starting work on pan_simpProofTheory
Starting work on pan_to_crepProofTheory
loop_callProofTheory                                                                                                                                 real:   23s  user:   23s     OK
Starting work on loop_liveProofTheory
pan_simpProofTheory                                                                                                                                  real:   36s  user:   34s     OK
Starting work on time_to_panProofTheory
loop_liveProofTheory                                                                                                                                 real:   24s  user:   23s     OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory                                                                                                                               real:   94s  user:   93s     OK
Starting work on loop_to_wordProofTheory
pan_to_crepProofTheory                                                                                                                               real:  116s  user:  113s     OK
loop_to_wordProofTheory                                                                                                                              real:   67s  user:   66s     OK
crep_to_loopProofTheory                                                                                                                              real:  130s  user:  125s     OK
Starting work on pan_to_wordProofTheory
pan_to_wordProofTheory                                                                                                                               real:   14s  user:   13s     OK
time_to_panProofTheory                                                                                                                               real:  721s  user:  710sCHEATED
Starting work on time_to_panSemProofTheory
time_to_panSemProofTheory                                                                                                                            real:    9s  user:    8sFAIL<1>
 Saved theorem _____ "observed_io_Axiom"
 Saved theorem _____ "observed_io_induction"
 Saved theorem _____ "observed_io_case_cong"
 Saved theorem _____ "observed_io_case_eq"
 <<HOL message: Defined type: "observed_io">>
 /home/myreen/regression/cakeml-1563/pancake/proofs/time_to_panSemProofScript.sml:64: error: Value or constructor (timed_automata_correct) has not been declared
 Found near [timed_automata_correct]
 error in quse /home/myreen/regression/cakeml-1563/pancake/proofs/time_to_panSemProofScript.sml : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1563/pancake/proofs/time_to_panSemProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"