Job 579

CakeML:7f186d7f39326e4d0d2d6bd42dc02463c6fcef3c
  Fix a few proofs in lab_to_targetProof [Nov 22 23:57:56]
#561 (print-types)
Merging into:19b073895fb32a069a88cf2b55eb0a4f0216e156
  Merge pull request #557 from CakeML/issue-538 [Nov 22 14:28:23]
HOL:acd07026761c91f65c78d51b8e16234614fa2712
  Fix Holmake's wildcard fn to interpret arg as multiple patterns [Nov 23 06:07:36]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Nov 23 15:25:28 Claimed job
Nov 23 15:26:06 Building HOL
Nov 23 15:33:55 Starting developers/bin
Nov 23 15:34:27 Finished developers/bin                                          31s 140MB
Nov 23 15:34:28 Starting semantics/ffi
Nov 23 15:35:04 Finished semantics/ffi                                           35s 405MB
Nov 23 15:35:05 Starting semantics
Nov 23 15:36:28 Finished semantics                                             1m21s   1GB
Nov 23 15:36:28 Starting semantics/proofs
Nov 23 15:39:18 Finished semantics/proofs                                      2m49s   1GB
Nov 23 15:39:19 Starting basis/pure
Nov 23 15:42:54 Finished basis/pure                                            3m34s 812MB
Nov 23 15:42:55 Starting translator
Nov 23 15:45:57 Finished translator                                            3m01s   1GB
Nov 23 15:45:58 Starting compiler/parsing
Nov 23 15:47:15 Finished compiler/parsing                                      1m16s   1GB
Nov 23 15:47:15 Starting characteristic
Nov 23 15:49:41 Finished characteristic                                        2m25s   1GB
Nov 23 15:49:42 Starting translator/monadic
Nov 23 15:51:06 Finished translator/monadic                                    1m23s   1GB
Nov 23 15:51:07 Starting basis
Nov 23 16:06:55 Finished basis                                                15m47s   2GB
Nov 23 16:06:56 Starting compiler/inference
Nov 23 16:08:34 Finished compiler/inference                                    1m38s   1GB
Nov 23 16:08:35 Starting compiler/backend/reg_alloc
Nov 23 16:09:21 Finished compiler/backend/reg_alloc                              45s 984MB
Nov 23 16:09:22 Starting compiler/backend/gc
Nov 23 16:16:42 Finished compiler/backend/gc                                   7m19s   1GB
Nov 23 16:16:43 Starting compiler/backend
Nov 23 16:16:46 Finished compiler/backend                                         1s  17MB
Nov 23 16:16:46 Starting compiler/encoders/asm
Nov 23 16:16:48 Finished compiler/encoders/asm                                    0s  15MB
Nov 23 16:16:49 Starting compiler/encoders/x64
Nov 23 16:17:38 Finished compiler/encoders/x64                                   48s 659MB
Nov 23 16:17:39 Starting compiler/encoders/arm6
Nov 23 16:19:20 Finished compiler/encoders/arm6                                1m39s   1GB
Nov 23 16:19:20 Starting compiler/encoders/arm8
Nov 23 16:19:45 Finished compiler/encoders/arm8                                  23s 450MB
Nov 23 16:19:46 Starting compiler/encoders/mips
Nov 23 16:20:42 Finished compiler/encoders/mips                                  55s 855MB
Nov 23 16:20:42 Starting compiler/encoders/riscv
Nov 23 16:21:43 Finished compiler/encoders/riscv                                 59s 910MB
Nov 23 16:21:43 Starting compiler/backend/x64
Nov 23 16:22:00 Finished compiler/backend/x64                                    15s 754MB
Nov 23 16:22:01 Starting compiler/backend/arm6
Nov 23 16:22:20 Finished compiler/backend/arm6                                   18s   1GB
Nov 23 16:22:21 Starting compiler/backend/arm8
Nov 23 16:22:39 Finished compiler/backend/arm8                                   17s   1GB
Nov 23 16:22:40 Starting compiler/backend/mips
Nov 23 16:22:57 Finished compiler/backend/mips                                   17s 864MB
Nov 23 16:22:58 Starting compiler/backend/riscv
Nov 23 16:23:17 Finished compiler/backend/riscv                                  17s   1GB
Nov 23 16:23:17 Starting compiler/parsing/proofs
Nov 23 16:29:23 Finished compiler/parsing/proofs                               6m05s 858MB
Nov 23 16:29:24 Starting compiler/inference/proofs
Nov 23 16:32:17 Finished compiler/inference/proofs                             2m52s   1GB
Nov 23 16:32:18 Starting compiler/backend/semantics
Nov 23 16:41:22 Finished compiler/backend/semantics                            9m03s   3GB
Nov 23 16:41:23 Starting compiler/backend/reg_alloc/proofs
Nov 23 16:44:07 Finished compiler/backend/reg_alloc/proofs                     2m42s 575MB
Nov 23 16:44:08 Starting compiler/backend/proofs
Nov 23 17:28:12 Finished compiler/backend/proofs                              44m02s   3GB
Nov 23 17:28:12 Starting compiler/encoders/x64/proofs
Nov 23 17:35:55 Finished compiler/encoders/x64/proofs                          7m41s   4GB
Nov 23 17:35:55 Starting compiler/encoders/arm6/proofs
Nov 23 17:43:46 Finished compiler/encoders/arm6/proofs                         7m49s   3GB
Nov 23 17:43:46 Starting compiler/encoders/arm8/proofs
Nov 23 17:49:15 Finished compiler/encoders/arm8/proofs                         5m28s   1GB
Nov 23 17:49:16 Starting compiler/encoders/mips/proofs
Nov 23 17:56:42 Finished compiler/encoders/mips/proofs                         7m24s   2GB
Nov 23 17:56:42 Starting compiler/encoders/riscv/proofs
Nov 23 18:04:45 Finished compiler/encoders/riscv/proofs                        8m01s 813MB
Nov 23 18:04:46 Starting compiler/backend/x64/proofs
Nov 23 18:05:07 Finished compiler/backend/x64/proofs                             19s   1GB
Nov 23 18:05:07 Starting compiler/backend/arm6/proofs
Nov 23 18:05:29 Finished compiler/backend/arm6/proofs                            21s   1GB
Nov 23 18:05:30 Starting compiler/backend/arm8/proofs
Nov 23 18:05:49 Finished compiler/backend/arm8/proofs                            18s   1GB
Nov 23 18:05:50 Starting compiler/backend/mips/proofs
Nov 23 18:06:11 Finished compiler/backend/mips/proofs                            19s 843MB
Nov 23 18:06:11 Starting compiler/backend/riscv/proofs
Nov 23 18:06:32 Finished compiler/backend/riscv/proofs                           19s   1GB
Nov 23 18:06:32 Starting compiler/proofs
Nov 23 18:07:51 Finished compiler/proofs                                       1m17s   1GB
Nov 23 18:07:51 Starting candle/set-theory
Nov 23 18:08:21 Finished candle/set-theory                                       28s 625MB
Nov 23 18:08:21 Starting candle/syntax-lib
Nov 23 18:08:32 Finished candle/syntax-lib                                        9s 590MB
Nov 23 18:08:32 Starting candle/standard/syntax
Nov 23 18:10:04 Finished candle/standard/syntax                                1m30s 597MB
Nov 23 18:10:04 Starting candle/standard/semantics
Nov 23 18:11:24 Finished candle/standard/semantics                             1m18s 867MB
Nov 23 18:11:25 Starting candle/standard/monadic
Nov 23 18:12:59 Finished candle/standard/monadic                               1m33s 806MB
Nov 23 18:13:00 Starting candle/standard/ml_kernel
Nov 23 18:28:33 Finished candle/standard/ml_kernel                            15m31s   2GB
Nov 23 18:28:34 Starting candle/standard/opentheory
Nov 23 18:36:00 Finished candle/standard/opentheory                            7m25s   4GB
Nov 23 18:36:00 Starting candle/standard/opentheory/compilation
Nov 23 19:11:11 Finished candle/standard/opentheory/compilation               35m09s  21GB
Nov 23 19:11:12 Starting candle/standard/opentheory/compilation/proofs
Nov 23 19:11:50 Finished candle/standard/opentheory/compilation/proofs           37s   5GB
Nov 23 19:11:51 Starting characteristic/examples
Nov 23 19:13:21 Finished characteristic/examples                               1m29s   2GB
Nov 23 19:13:21 Starting tutorial/solutions
Nov 23 19:26:51 Finished tutorial/solutions                                   13m28s   6GB
Nov 23 19:26:52 Starting translator/monadic/examples
Nov 23 19:28:36 Finished translator/monadic/examples                           1m43s   2GB
Nov 23 19:28:37 Starting examples
Nov 23 19:30:14 FAILED: examples
]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/formal-languages]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ../basis]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-acd07026761c91f65c78d51b8e16234614fa2712/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developers[1mWorking in ../developers[0m
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../misc]0;Holmake: ../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../basis]0;Holmake: ../characteristic]0;Holmake: ../compiler/parsing]0;Holmake: ../semantics]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../compiler/parsing]0;Holmake: ../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../characteristic]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../characteristic]0;Holmake: ../translator]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semantics[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
]0;Holmake: ../translator]0;Holmake: ../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../characteristic]0;Holmake: ../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../basis]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadic/monad_base]0;Holmake: ../translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../basis]0;Holmake: ../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on heap
Starting work on README.md
README.md                                           OK
heap                                                OK
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on doubleProgTheory
lcsTheory                                           OK
Starting work on diffTheory
diffTheory                                          OK
Starting work on diffProgTheory
catProgTheory                                       OK
Starting work on echoProgTheory
diffProgTheory                             FAILED! <1>
 Saved theorem _____ "nsLookup_auto_env_15_pfun_eqs"
 
 WARNING: diff_alg2 has a precondition.
 
 Saved theorem _____ "diff_alg2_v_thm"
 error in quse /home/myreen/regression/cakeml-579/examples/diffProgScript.sml : HOL_ERR {message = "theorem diffProg$diff_with_lcs_side_def not found", origin_function = "fetch", origin_structure = "DB"}
 error in load diffProgScript : HOL_ERR {message = "theorem diffProg$diff_with_lcs_side_def not found", origin_function = "fetch", origin_structure = "DB"}
 Updating longest_common_suffix_length_v_thm
 Saved theorem _____ "longest_common_suffix_length_v_thm"
 Uncaught exception: HOL_ERR {message = "theorem diffProg$diff_with_lcs_side_def not found", origin_function = "fetch", origin_structure = "DB"}
quicksortProgTheory                           M-KILLED
doubleProgTheory                              M-KILLED
echoProgTheory                                M-KILLED