Job 1405

CakeML:5cbf6f598f6ad03c2c9768595c9f7f3eedc2ddae
  Use cached real addr of Global [Dec 01 07:31:38]
#807 (issue797)
Merging into:3157c56dfe1eab23ef37b3cefb8fca2cced396c5
  Merge pull request #804 from CakeML/currheap [Nov 17 07:22:18]
HOL:77016ef7b01f987f1f684e825ac1d79feb8d454a
  emacs-mode: fix bug in previous caused by variable masking [Nov 27 05:03:03]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Dec 01 08:45:58 Claimed job
Dec 01 08:46:07 Building HOL
Dec 01 09:02:29 Starting developers
Dec 01 09:02:29 Finished developers                                               0s  37MB
Dec 01 09:02:30 Starting developers/bin
Dec 01 09:02:36 Finished developers/bin                                           6s   1GB
Dec 01 09:02:36 Starting semantics/ffi
Dec 01 09:02:47 Finished semantics/ffi                                           10s 279MB
Dec 01 09:02:47 Starting semantics
Dec 01 09:04:33 Finished semantics                                             1m45s   2GB
Dec 01 09:04:33 Starting semantics/proofs
Dec 01 09:08:04 Finished semantics/proofs                                      3m31s   1GB
Dec 01 09:08:04 Starting semantics/alt_semantics
Dec 01 09:08:14 Finished semantics/alt_semantics                                  9s 391MB
Dec 01 09:08:14 Starting semantics/alt_semantics/proofs
Dec 01 09:10:32 Finished semantics/alt_semantics/proofs                        2m17s   1GB
Dec 01 09:10:32 Starting basis/pure
Dec 01 09:13:25 Finished basis/pure                                            2m53s   1GB
Dec 01 09:13:25 Starting translator
Dec 01 09:16:13 Finished translator                                            2m47s   2GB
Dec 01 09:16:13 Starting compiler/parsing
Dec 01 09:17:30 Finished compiler/parsing                                      1m16s   4GB
Dec 01 09:17:30 Starting characteristic
Dec 01 09:23:44 Finished characteristic                                        6m13s   3GB
Dec 01 09:23:44 Starting translator/monadic
Dec 01 09:25:35 Finished translator/monadic                                    1m50s   3GB
Dec 01 09:25:35 Starting basis
Dec 01 10:01:52 Finished basis                                                36m16s  42GB
Dec 01 10:01:52 Starting compiler/inference
Dec 01 10:03:06 Finished compiler/inference                                    1m13s   2GB
Dec 01 10:03:06 Starting compiler/backend/reg_alloc
Dec 01 10:04:14 Finished compiler/backend/reg_alloc                            1m07s   1GB
Dec 01 10:04:14 Starting compiler/backend/gc
Dec 01 10:08:30 Finished compiler/backend/gc                                   4m16s   5GB
Dec 01 10:08:30 Starting compiler/backend
Dec 01 10:14:19 Finished compiler/backend                                      5m48s   5GB
Dec 01 10:14:19 Starting compiler/encoders/asm
Dec 01 10:14:43 Finished compiler/encoders/asm                                   23s   1GB
Dec 01 10:14:43 Starting compiler/encoders/x64
Dec 01 10:15:48 Finished compiler/encoders/x64                                 1m04s   1GB
Dec 01 10:15:48 Starting compiler/encoders/arm7
Dec 01 10:17:55 Finished compiler/encoders/arm7                                2m07s   1GB
Dec 01 10:17:55 Starting compiler/encoders/arm8
Dec 01 10:18:35 Finished compiler/encoders/arm8                                  40s   1GB
Dec 01 10:18:36 Starting compiler/encoders/mips
Dec 01 10:20:06 Finished compiler/encoders/mips                                1m30s   1GB
Dec 01 10:20:07 Starting compiler/encoders/riscv
Dec 01 10:21:52 Finished compiler/encoders/riscv                               1m45s   1GB
Dec 01 10:21:52 Starting compiler/encoders/ag32
Dec 01 10:22:11 Finished compiler/encoders/ag32                                  19s 908MB
Dec 01 10:22:11 Starting compiler/backend/x64
Dec 01 10:22:33 Finished compiler/backend/x64                                    20s   1GB
Dec 01 10:22:33 Starting compiler/backend/arm7
Dec 01 10:22:55 Finished compiler/backend/arm7                                   22s   1GB
Dec 01 10:22:56 Starting compiler/backend/arm8
Dec 01 10:23:17 Finished compiler/backend/arm8                                   20s   1GB
Dec 01 10:23:17 Starting compiler/backend/mips
Dec 01 10:23:37 Finished compiler/backend/mips                                   20s   1GB
Dec 01 10:23:37 Starting compiler/backend/riscv
Dec 01 10:24:00 Finished compiler/backend/riscv                                  22s   1GB
Dec 01 10:24:00 Starting compiler/backend/ag32
Dec 01 10:25:17 Finished compiler/backend/ag32                                 1m17s   2GB
Dec 01 10:25:17 Starting compiler/parsing/proofs
Dec 01 10:31:07 Finished compiler/parsing/proofs                               5m49s   2GB
Dec 01 10:31:07 Starting compiler/inference/proofs
Dec 01 10:33:39 Finished compiler/inference/proofs                             2m31s   2GB
Dec 01 10:33:39 Starting compiler/backend/semantics
Dec 01 11:01:25 Finished compiler/backend/semantics                           27m45s   3GB
Dec 01 11:01:25 Starting compiler/backend/reg_alloc/proofs
Dec 01 11:04:47 Finished compiler/backend/reg_alloc/proofs                     3m21s   1GB
Dec 01 11:04:47 Starting compiler/backend/proofs
Dec 01 11:58:43 Finished compiler/backend/proofs                              53m55s  16GB
Dec 01 11:58:43 Starting compiler/encoders/x64/proofs
Dec 01 12:07:59 Finished compiler/encoders/x64/proofs                          9m15s   7GB
Dec 01 12:07:59 Starting compiler/encoders/arm7/proofs
Dec 01 12:20:30 Finished compiler/encoders/arm7/proofs                        12m30s   6GB
Dec 01 12:20:30 Starting compiler/encoders/arm8/proofs
Dec 01 12:26:46 Finished compiler/encoders/arm8/proofs                         6m16s   4GB
Dec 01 12:26:47 Starting compiler/encoders/mips/proofs
Dec 01 12:36:47 Finished compiler/encoders/mips/proofs                         9m59s   8GB
Dec 01 12:36:47 Starting compiler/encoders/riscv/proofs
Dec 01 12:45:08 Finished compiler/encoders/riscv/proofs                        8m21s   3GB
Dec 01 12:45:09 Starting compiler/encoders/ag32/proofs
Dec 01 12:47:31 Finished compiler/encoders/ag32/proofs                         2m22s   2GB
Dec 01 12:47:31 Starting compiler/backend/x64/proofs
Dec 01 12:47:53 Finished compiler/backend/x64/proofs                             22s   2GB
Dec 01 12:47:54 Starting compiler/backend/arm7/proofs
Dec 01 12:48:16 Finished compiler/backend/arm7/proofs                            22s   1GB
Dec 01 12:48:16 Starting compiler/backend/arm8/proofs
Dec 01 12:48:36 Finished compiler/backend/arm8/proofs                            19s   1GB
Dec 01 12:48:36 Starting compiler/backend/mips/proofs
Dec 01 12:48:59 Finished compiler/backend/mips/proofs                            23s   1GB
Dec 01 12:49:00 Starting compiler/backend/riscv/proofs
Dec 01 12:49:22 Finished compiler/backend/riscv/proofs                           21s   2GB
Dec 01 12:49:22 Starting compiler/backend/ag32/proofs
Dec 01 13:01:27 Finished compiler/backend/ag32/proofs                         12m04s   5GB
Dec 01 13:01:27 Starting compiler/proofs
Dec 01 13:03:12 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)/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
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:   12s  user:   12s     OK
Starting work on compilerTheory
compilerTheory                                                                                                                                     real:   44s  user:   42s     OK
Starting work on compilerProofTheory
compilerProofTheory                                                                                                                                real:   44s  user:   41sFAIL<1>
 Saved theorem _____ "infertype_prog_correct"
 Saved theorem _____ "compile_tap_compile"
 Saved definition __ "read_limits_def"
 Saved definition __ "is_safe_for_space_def"
 Saved CHEAT _______ "compile_correct_gen"
 Saved CHEAT _______ "compile_correct_lemma"
 Saved CHEAT _______ "compile_correct_safe_for_space"
 error in quse /home/myreen/regression/cakeml-1405/compiler/proofs/compilerProofScript.sml : HOL_ERR {message = "predicate not true", origin_function = "assert", origin_structure = "Lib"}
 error in load /home/myreen/regression/cakeml-1405/compiler/proofs/compilerProofScript : HOL_ERR {message = "predicate not true", origin_function = "assert", origin_structure = "Lib"}
 Uncaught exception: HOL_ERR {message = "predicate not true", origin_function = "assert", origin_structure = "Lib"}