Job 1406

CakeML:cb2e995d52faec1af4ad8ef925ca3122eacc7647
  Make compiler optimise n2w o ORD and CHR o w2n [Dec 01 11:03:40]
#808 (ord-chr-word8)
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 13:03:13 Claimed job
Dec 01 13:03:16 Reusing HOL
Dec 01 13:03:22 Starting developers
Dec 01 13:03:25 Finished developers                                               2s 105MB
Dec 01 13:03:25 Starting developers/bin
Dec 01 13:03:31 Finished developers/bin                                           6s   1GB
Dec 01 13:03:32 Starting semantics/ffi
Dec 01 13:03:42 Finished semantics/ffi                                            9s 292MB
Dec 01 13:03:42 Starting semantics
Dec 01 13:05:05 Finished semantics                                             1m22s   1GB
Dec 01 13:05:05 Starting semantics/proofs
Dec 01 13:08:23 Finished semantics/proofs                                      3m18s   2GB
Dec 01 13:08:24 Starting semantics/alt_semantics
Dec 01 13:08:32 Finished semantics/alt_semantics                                  7s 408MB
Dec 01 13:08:32 Starting semantics/alt_semantics/proofs
Dec 01 13:10:38 Finished semantics/alt_semantics/proofs                        2m06s   1GB
Dec 01 13:10:38 Starting basis/pure
Dec 01 13:11:32 Finished basis/pure                                              51s   1GB
Dec 01 13:11:32 Starting translator
Dec 01 13:14:10 Finished translator                                            2m37s   2GB
Dec 01 13:14:10 Starting compiler/parsing
Dec 01 13:15:22 Finished compiler/parsing                                      1m12s   4GB
Dec 01 13:15:22 Starting characteristic
Dec 01 13:22:41 Finished characteristic                                        7m18s   3GB
Dec 01 13:22:41 Starting translator/monadic
Dec 01 13:24:28 Finished translator/monadic                                    1m46s   3GB
Dec 01 13:24:28 Starting basis
Dec 01 14:06:22 Finished basis                                                41m53s  26GB
Dec 01 14:06:22 Starting compiler/inference
Dec 01 14:07:55 Finished compiler/inference                                    1m32s   2GB
Dec 01 14:07:55 Starting compiler/backend/reg_alloc
Dec 01 14:09:29 Finished compiler/backend/reg_alloc                            1m33s   1GB
Dec 01 14:09:29 Starting compiler/backend/gc
Dec 01 14:15:05 Finished compiler/backend/gc                                   5m35s   2GB
Dec 01 14:15:05 Starting compiler/backend
Dec 01 14:23:34 Finished compiler/backend                                      8m28s   4GB
Dec 01 14:23:35 Starting compiler/encoders/asm
Dec 01 14:24:07 Finished compiler/encoders/asm                                   32s   1GB
Dec 01 14:24:07 Starting compiler/encoders/x64
Dec 01 14:24:52 Finished compiler/encoders/x64                                   45s   1GB
Dec 01 14:24:52 Starting compiler/encoders/arm7
Dec 01 14:26:09 Finished compiler/encoders/arm7                                1m16s   1GB
Dec 01 14:26:10 Starting compiler/encoders/arm8
Dec 01 14:26:33 Finished compiler/encoders/arm8                                  22s   1GB
Dec 01 14:26:33 Starting compiler/encoders/mips
Dec 01 14:27:03 Finished compiler/encoders/mips                                  29s   1GB
Dec 01 14:27:03 Starting compiler/encoders/riscv
Dec 01 14:27:29 Finished compiler/encoders/riscv                                 25s   1GB
Dec 01 14:27:29 Starting compiler/encoders/ag32
Dec 01 14:27:59 Finished compiler/encoders/ag32                                  29s 907MB
Dec 01 14:27:59 Starting compiler/backend/x64
Dec 01 14:28:30 Finished compiler/backend/x64                                    30s   1GB
Dec 01 14:28:30 Starting compiler/backend/arm7
Dec 01 14:29:03 Finished compiler/backend/arm7                                   32s   1GB
Dec 01 14:29:03 Starting compiler/backend/arm8
Dec 01 14:29:32 Finished compiler/backend/arm8                                   28s   1GB
Dec 01 14:29:32 Starting compiler/backend/mips
Dec 01 14:30:02 Finished compiler/backend/mips                                   29s   1GB
Dec 01 14:30:02 Starting compiler/backend/riscv
Dec 01 14:30:35 Finished compiler/backend/riscv                                  32s   1GB
Dec 01 14:30:35 Starting compiler/backend/ag32
Dec 01 14:32:26 Finished compiler/backend/ag32                                 1m50s   2GB
Dec 01 14:32:26 Starting compiler/parsing/proofs
Dec 01 14:39:52 Finished compiler/parsing/proofs                               7m25s   2GB
Dec 01 14:39:52 Starting compiler/inference/proofs
Dec 01 14:44:03 Finished compiler/inference/proofs                             4m10s   2GB
Dec 01 14:44:03 Starting compiler/backend/semantics
Dec 01 15:16:45 Finished compiler/backend/semantics                           32m41s   3GB
Dec 01 15:16:45 Starting compiler/backend/reg_alloc/proofs
Dec 01 15:20:05 Finished compiler/backend/reg_alloc/proofs                     3m19s   1GB
Dec 01 15:20:05 Starting compiler/backend/proofs
Dec 01 16:13:41 Finished compiler/backend/proofs                              53m35s  23GB
Dec 01 16:13:41 Starting compiler/encoders/x64/proofs
Dec 01 16:23:03 Finished compiler/encoders/x64/proofs                          9m21s   4GB
Dec 01 16:23:03 Starting compiler/encoders/arm7/proofs
Dec 01 16:35:32 Finished compiler/encoders/arm7/proofs                        12m28s   5GB
Dec 01 16:35:32 Starting compiler/encoders/arm8/proofs
Dec 01 16:41:54 Finished compiler/encoders/arm8/proofs                         6m21s   3GB
Dec 01 16:41:54 Starting compiler/encoders/mips/proofs
Dec 01 16:51:46 Finished compiler/encoders/mips/proofs                         9m52s   3GB
Dec 01 16:51:46 Starting compiler/encoders/riscv/proofs
Dec 01 17:00:05 Finished compiler/encoders/riscv/proofs                        8m18s   3GB
Dec 01 17:00:05 Starting compiler/encoders/ag32/proofs
Dec 01 17:02:27 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Dec 01 17:02:27 Starting compiler/backend/x64/proofs
Dec 01 17:02:49 Finished compiler/backend/x64/proofs                             21s   1GB
Dec 01 17:02:49 Starting compiler/backend/arm7/proofs
Dec 01 17:03:12 Finished compiler/backend/arm7/proofs                            23s   1GB
Dec 01 17:03:12 Starting compiler/backend/arm8/proofs
Dec 01 17:03:32 Finished compiler/backend/arm8/proofs                            20s   1GB
Dec 01 17:03:32 Starting compiler/backend/mips/proofs
Dec 01 17:03:54 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 01 17:03:54 Starting compiler/backend/riscv/proofs
Dec 01 17:04:17 Finished compiler/backend/riscv/proofs                           23s   2GB
Dec 01 17:04:18 Starting compiler/backend/ag32/proofs
Dec 01 17:16:22 Finished compiler/backend/ag32/proofs                         12m04s   4GB
Dec 01 17:16:22 Starting compiler/proofs
Dec 01 17:18:02 Finished compiler/proofs                                       1m39s   6GB
Dec 01 17:18:03 Starting candle/set-theory
Dec 01 17:18:33 Finished candle/set-theory                                       29s   1GB
Dec 01 17:18:33 Starting candle/syntax-lib
Dec 01 17:18:44 Finished candle/syntax-lib                                       10s 818MB
Dec 01 17:18:44 Starting candle/standard/syntax
Dec 01 17:20:34 Finished candle/standard/syntax                                1m50s   1GB
Dec 01 17:20:34 Starting candle/standard/semantics
Dec 01 17:22:20 Finished candle/standard/semantics                             1m45s   2GB
Dec 01 17:22:20 Starting candle/standard/monadic
Dec 01 17:24:02 Finished candle/standard/monadic                               1m41s   1GB
Dec 01 17:24:02 Starting candle/standard/ml_kernel
Dec 01 17:29:17 Finished candle/standard/ml_kernel                             5m14s   6GB
Dec 01 17:29:17 Starting candle/overloading/syntax
Dec 01 17:32:28 Finished candle/overloading/syntax                             3m10s   2GB
Dec 01 17:32:28 Starting candle/overloading/semantics
Dec 01 17:44:34 Finished candle/overloading/semantics                         12m06s   9GB
Dec 01 17:44:35 Starting characteristic/examples
Dec 01 17:45:52 Finished characteristic/examples                               1m17s   4GB
Dec 01 17:45:53 Starting tutorial/solutions
Dec 01 18:01:04 Finished tutorial/solutions                                   15m10s  16GB
Dec 01 18:01:04 Starting translator/monadic/examples
Dec 01 18:04:22 Finished translator/monadic/examples                           3m18s   3GB
Dec 01 18:04:22 Starting examples
Dec 01 18:13:04 Finished examples                                              8m41s   7GB
Dec 01 18:13:04 Starting examples/compilation/x64
Dec 01 20:34:28 Finished examples/compilation/x64                           2h21m23s  30GB
Dec 01 20:34:28 Starting examples/compilation/x64/proofs
Dec 01 20:36:21 Finished examples/compilation/x64/proofs                       1m52s   3GB
Dec 01 20:36:21 Starting examples/compilation/ag32
Dec 01 21:09:50 Finished examples/compilation/ag32                            33m28s  10GB
Dec 01 21:09:50 Starting examples/compilation/ag32/proofs
Dec 01 21:10:42 Finished examples/compilation/ag32/proofs                        52s   4GB
Dec 01 21:10:43 Starting examples/cost
Dec 01 22:04:32 Finished examples/cost                                        53m48s  19GB
Dec 01 22:04:32 Starting examples/lpr_checker
Dec 01 22:08:20 Finished examples/lpr_checker                                  3m47s   3GB
Dec 01 22:08:20 Starting examples/lpr_checker/compilation
Dec 01 22:26:48 Finished examples/lpr_checker/compilation                     18m27s  13GB
Dec 01 22:26:48 Starting examples/lpr_checker/compilation/proofs
Dec 01 22:27:30 Finished examples/lpr_checker/compilation/proofs                 42s   3GB
Dec 01 22:27:30 Starting examples/lpr_checker/array
Dec 01 22:41:08 Finished examples/lpr_checker/array                           13m37s   5GB
Dec 01 22:41:08 Starting examples/lpr_checker/array/compilation
Dec 01 22:59:57 Finished examples/lpr_checker/array/compilation               18m49s  18GB
Dec 01 22:59:57 Starting examples/lpr_checker/array/compilation/proofs
Dec 01 23:00:46 Finished examples/lpr_checker/array/compilation/proofs           48s   4GB
Dec 01 23:00:46 Starting examples/opentheory
Dec 01 23:07:29 FAILED: examples/opentheory
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$(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$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Starting work on README.md
Starting work on prettyTheory
README.md                                                                                                                             real:    0s  user:    0s     OK
prettyTheory                                                                                                                          real:   20s  user:   19s     OK
Starting work on readerTheory
readerTheory                                                                                                                          real:   50s  user:   48s     OK
Starting work on reader_initTheory
reader_initTheory                                                                                                                     real:   22s  user:   21s     OK
Starting work on readerProofTheory
readerProofTheory                                                                                                                     real:   60s  user:   59s     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                                                                                                 real:   17s  user:   16s     OK
reader_commonProgTheory                                                                                                               real:  247s  user:  243sFAIL<1>
      (Refv init_context_v)}
 
 failed.
 Failed to prove theorem HOL_STORE_init_precond.
 
 Exception raised at folTools.FOL_FIND:
 no solution found (THEN1 on line 236) (THEN1 on line 246) (THEN1 on line 248) (THEN1 on line 258) (THEN1 on line 260)
 error in quse /home/myreen/regression/cakeml-1406/examples/opentheory/reader_commonProgScript.sml : HOL_ERR {message = "no solution found (THEN1 on line 236) (THEN1 on line 246) (THEN1 on line 248) (THEN1 on line 258) (THEN1 on line 260)", origin_function = "FOL_FIND", origin_structure = "folTools"}
 error in load /home/myreen/regression/cakeml-1406/examples/opentheory/reader_commonProgScript : HOL_ERR {message = "no solution found (THEN1 on line 236) (THEN1 on line 246) (THEN1 on line 248) (THEN1 on line 258) (THEN1 on line 260)", origin_function = "FOL_FIND", origin_structure = "folTools"}
 Uncaught exception: HOL_ERR {message = "no solution found (THEN1 on line 236) (THEN1 on line 246) (THEN1 on line 248) (THEN1 on line 258) (THEN1 on line 260)", origin_function = "FOL_FIND", origin_structure = "folTools"}