Job 1566

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:1dfda82edf04a50d842dac582fd1231a6d07239a
  Remove .HOLMK directories before doing a build [Aug 08 23:49:27]
Machine:oven3 4.19.67.1.amd64-smp

Aug 09 21:02:56 Claimed job
Aug 09 21:03:11 Building HOL
Aug 09 21:28:03 Starting developers
Aug 09 21:28:12 Finished developers                                               8s 132MB
Aug 09 21:28:12 Starting developers/bin
Aug 09 21:28:25 Finished developers/bin                                          13s   1GB
Aug 09 21:28:25 Starting semantics/ffi
Aug 09 21:28:51 Finished semantics/ffi                                           24s 259MB
Aug 09 21:28:51 Starting semantics
Aug 09 21:32:07 Finished semantics                                             3m15s   1GB
Aug 09 21:32:07 Starting semantics/proofs
Aug 09 21:39:59 Finished semantics/proofs                                      7m51s   1GB
Aug 09 21:39:59 Starting semantics/alt_semantics
Aug 09 21:40:21 Finished semantics/alt_semantics                                 21s 337MB
Aug 09 21:40:22 Starting semantics/alt_semantics/proofs
Aug 09 21:45:13 Finished semantics/alt_semantics/proofs                        4m50s 916MB
Aug 09 21:45:13 Starting basis/pure
Aug 09 21:51:17 Finished basis/pure                                            6m04s 911MB
Aug 09 21:51:17 Starting translator
Aug 09 21:58:06 Finished translator                                            6m48s   1GB
Aug 09 21:58:06 Starting compiler/parsing
Aug 09 22:00:47 Finished compiler/parsing                                      2m40s   2GB
Aug 09 22:00:47 Starting characteristic
Aug 09 22:12:39 Finished characteristic                                       11m51s   1GB
Aug 09 22:12:40 Starting translator/monadic
Aug 09 22:16:08 Finished translator/monadic                                    3m28s   1GB
Aug 09 22:16:08 Starting basis
Aug 09 23:51:28 Finished basis                                              1h35m19s  16GB
Aug 09 23:51:28 Starting compiler/inference
Aug 09 23:54:09 Finished compiler/inference                                    2m40s   1GB
Aug 09 23:54:09 Starting compiler/backend/reg_alloc
Aug 09 23:56:19 Finished compiler/backend/reg_alloc                            2m10s   1GB
Aug 09 23:56:19 Starting compiler/backend/gc
Aug 10 00:03:19 Finished compiler/backend/gc                                   6m59s   1GB
Aug 10 00:03:19 Starting compiler/backend
Aug 10 00:12:50 Finished compiler/backend                                      9m30s   3GB
Aug 10 00:12:50 Starting compiler/encoders/asm
Aug 10 00:13:39 Finished compiler/encoders/asm                                   48s 814MB
Aug 10 00:13:40 Starting compiler/encoders/x64
Aug 10 00:15:57 Finished compiler/encoders/x64                                 2m17s   1GB
Aug 10 00:15:58 Starting compiler/encoders/arm7
Aug 10 00:20:31 Finished compiler/encoders/arm7                                4m33s   1GB
Aug 10 00:20:31 Starting compiler/encoders/arm8
Aug 10 00:21:53 Finished compiler/encoders/arm8                                1m21s 618MB
Aug 10 00:21:53 Starting compiler/encoders/mips
Aug 10 00:25:11 Finished compiler/encoders/mips                                3m17s   1GB
Aug 10 00:25:12 Starting compiler/encoders/riscv
Aug 10 00:28:59 Finished compiler/encoders/riscv                               3m47s   1GB
Aug 10 00:29:00 Starting compiler/encoders/ag32
Aug 10 00:29:39 Finished compiler/encoders/ag32                                  39s 814MB
Aug 10 00:29:39 Starting compiler/backend/x64
Aug 10 00:30:23 Finished compiler/backend/x64                                    43s   1GB
Aug 10 00:30:23 Starting compiler/backend/arm7
Aug 10 00:31:06 Finished compiler/backend/arm7                                   42s   1GB
Aug 10 00:31:06 Starting compiler/backend/arm8
Aug 10 00:31:51 Finished compiler/backend/arm8                                   44s   1GB
Aug 10 00:31:51 Starting compiler/backend/mips
Aug 10 00:32:34 Finished compiler/backend/mips                                   42s   1GB
Aug 10 00:32:35 Starting compiler/backend/riscv
Aug 10 00:33:17 Finished compiler/backend/riscv                                  42s   1GB
Aug 10 00:33:17 Starting compiler/backend/ag32
Aug 10 00:35:46 Finished compiler/backend/ag32                                 2m28s   1GB
Aug 10 00:35:47 Starting compiler/parsing/proofs
Aug 10 00:48:22 Finished compiler/parsing/proofs                              12m35s   1GB
Aug 10 00:48:22 Starting compiler/inference/proofs
Aug 10 00:53:52 Finished compiler/inference/proofs                             5m27s   1GB
Aug 10 00:53:52 Starting compiler/backend/semantics
Aug 10 01:56:11 Finished compiler/backend/semantics                         1h02m18s   2GB
Aug 10 01:56:11 Starting compiler/backend/reg_alloc/proofs
Aug 10 02:03:53 Finished compiler/backend/reg_alloc/proofs                     7m41s   1GB
Aug 10 02:03:53 Starting compiler/backend/proofs
Aug 10 03:45:16 Finished compiler/backend/proofs                            1h41m22s  19GB
Aug 10 03:45:16 Starting compiler/encoders/x64/proofs
Aug 10 04:07:00 Finished compiler/encoders/x64/proofs                         21m44s   4GB
Aug 10 04:07:00 Starting compiler/encoders/arm7/proofs
Aug 10 04:36:04 Finished compiler/encoders/arm7/proofs                        29m03s   3GB
Aug 10 04:36:04 Starting compiler/encoders/arm8/proofs
Aug 10 04:51:27 Finished compiler/encoders/arm8/proofs                        15m22s   1GB
Aug 10 04:51:28 Starting compiler/encoders/mips/proofs
Aug 10 05:14:17 Finished compiler/encoders/mips/proofs                        22m48s   2GB
Aug 10 05:14:17 Starting compiler/encoders/riscv/proofs
Aug 10 05:34:04 Finished compiler/encoders/riscv/proofs                       19m46s   1GB
Aug 10 05:34:04 Starting compiler/encoders/ag32/proofs
Aug 10 05:39:44 Finished compiler/encoders/ag32/proofs                         5m39s 856MB
Aug 10 05:39:44 Starting compiler/backend/x64/proofs
Aug 10 05:40:33 Finished compiler/backend/x64/proofs                             48s   1GB
Aug 10 05:40:33 Starting compiler/backend/arm7/proofs
Aug 10 05:41:23 Finished compiler/backend/arm7/proofs                            49s   1GB
Aug 10 05:41:23 Starting compiler/backend/arm8/proofs
Aug 10 05:42:11 Finished compiler/backend/arm8/proofs                            47s   1GB
Aug 10 05:42:11 Starting compiler/backend/mips/proofs
Aug 10 05:43:01 Finished compiler/backend/mips/proofs                            49s   1GB
Aug 10 05:43:01 Starting compiler/backend/riscv/proofs
Aug 10 05:43:46 Finished compiler/backend/riscv/proofs                           44s   1GB
Aug 10 05:43:47 Starting compiler/backend/ag32/proofs
Aug 10 06:11:47 Finished compiler/backend/ag32/proofs                         27m59s   2GB
Aug 10 06:11:47 Starting compiler/proofs
Aug 10 06:15:49 Finished compiler/proofs                                       4m01s   3GB
Aug 10 06:15:49 Starting candle/set-theory
Aug 10 06:16:48 Finished candle/set-theory                                       58s   1GB
Aug 10 06:16:48 Starting candle/syntax-lib
Aug 10 06:17:11 Finished candle/syntax-lib                                       23s 519MB
Aug 10 06:17:12 Starting candle/standard/syntax
Aug 10 06:21:06 Finished candle/standard/syntax                                3m53s   1GB
Aug 10 06:21:06 Starting candle/standard/semantics
Aug 10 06:24:51 Finished candle/standard/semantics                             3m44s   1GB
Aug 10 06:24:51 Starting candle/standard/monadic
Aug 10 06:28:38 Finished candle/standard/monadic                               3m46s   1GB
Aug 10 06:28:38 Starting candle/standard/ml_kernel
Aug 10 06:40:55 Finished candle/standard/ml_kernel                            12m16s   3GB
Aug 10 06:40:55 Starting candle/overloading/syntax
Aug 10 06:47:35 Finished candle/overloading/syntax                             6m39s   1GB
Aug 10 06:47:35 Starting candle/overloading/semantics
Aug 10 07:13:35 Finished candle/overloading/semantics                         25m59s   3GB
Aug 10 07:13:35 Starting pancake
Aug 10 07:15:18 Finished pancake                                               1m42s 772MB
Aug 10 07:15:18 Starting pancake/ffi
Aug 10 07:15:19 Finished pancake/ffi                                              0s   7MB
Aug 10 07:15:19 Starting pancake/semantics
Aug 10 07:20:16 Finished pancake/semantics                                     4m56s   1GB
Aug 10 07:20:16 Starting pancake/proofs
Aug 10 07:46:47 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 README.md
Starting work on loop_callProofTheory
Starting work on loop_removeProofTheory
Starting work on pan_simpProofTheory
README.md                                                                                                                                                                                                    real:    0s  user:    0s     OK
Starting work on pan_to_crepProofTheory
loop_callProofTheory                                                                                                                                                                                         real:   45s  user:   42s     OK
Starting work on loop_liveProofTheory
pan_simpProofTheory                                                                                                                                                                                          real:   67s  user:   64s     OK
Starting work on time_to_panProofTheory
loop_liveProofTheory                                                                                                                                                                                         real:   43s  user:   41s     OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory                                                                                                                                                                                       real:  184s  user:  181s     OK
Starting work on loop_to_wordProofTheory
pan_to_crepProofTheory                                                                                                                                                                                       real:  216s  user:  210s     OK
loop_to_wordProofTheory                                                                                                                                                                                      real:  131s  user:  128s     OK
crep_to_loopProofTheory                                                                                                                                                                                      real:  251s  user:  244s     OK
Starting work on pan_to_wordProofTheory
pan_to_wordProofTheory                                                                                                                                                                                       real:   27s  user:   25s     OK
time_to_panProofTheory                                                                                                                                                                                       real: 1501s  user: 1476sCHEATED
Starting work on time_to_panSemProofTheory
time_to_panSemProofTheory                                                                                                                                                                                    real:   18s  user:   16sFAIL<1>
 Saved theorem _____ "observed_io_distinct"
 Saved theorem _____ "observed_io_nchotomy"
 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">>
 /root/regression/cakeml-1566/pancake/proofs/time_to_panSemProofScript.sml:64: error: Value or constructor (timed_automata_correct) has not been declared
 Found near [timed_automata_correct]
 Uncaught exception: Fail "Static Errors"