Job 1507

CakeML:5a688a5290c54751b19a8c1389f83d474845d80e
  Fix allProof [Mar 31 13:14:27]
#811 (eval)
Merging into:d97d41235164d0340739418a6b941f7722d54535
  Merge pull request #823 from CakeML/arm64-apple [Mar 30 09:38:10]
HOL:80660c1a566218670f3e343cb742e51723b19cd7
  recovered old definition of real_random_variable_def [Apr 02 06:32:43]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 06 09:34:06 Claimed job
Apr 06 09:34:14 Building HOL
Apr 06 09:49:01 Starting developers
Apr 06 09:49:03 Finished developers                                               2s 137MB
Apr 06 09:49:03 Starting developers/bin
Apr 06 09:49:09 Finished developers/bin                                           5s   1GB
Apr 06 09:49:09 Starting semantics/ffi
Apr 06 09:49:19 Finished semantics/ffi                                            9s 298MB
Apr 06 09:49:20 Starting semantics
Apr 06 09:50:53 Finished semantics                                             1m32s   1GB
Apr 06 09:50:53 Starting semantics/proofs
Apr 06 09:54:25 Finished semantics/proofs                                      3m31s   1GB
Apr 06 09:54:25 Starting basis/pure
Apr 06 09:57:09 Finished basis/pure                                            2m44s   1GB
Apr 06 09:57:10 Starting translator
Apr 06 10:00:26 Finished translator                                            3m16s   2GB
Apr 06 10:00:27 Starting compiler/parsing
Apr 06 10:01:37 Finished compiler/parsing                                      1m09s   3GB
Apr 06 10:01:37 Starting characteristic
Apr 06 10:07:18 Finished characteristic                                        5m41s   3GB
Apr 06 10:07:18 Starting translator/monadic
Apr 06 10:09:04 Finished translator/monadic                                    1m45s   2GB
Apr 06 10:09:04 Starting basis
Apr 06 10:53:19 Finished basis                                                44m14s  28GB
Apr 06 10:53:19 Starting compiler/inference
Apr 06 10:54:32 Finished compiler/inference                                    1m12s   2GB
Apr 06 10:54:32 Starting compiler/backend/reg_alloc
Apr 06 10:55:40 Finished compiler/backend/reg_alloc                            1m07s   1GB
Apr 06 10:55:40 Starting compiler/backend/gc
Apr 06 10:59:16 Finished compiler/backend/gc                                   3m35s   3GB
Apr 06 10:59:16 Starting compiler/backend
Apr 06 11:04:20 Finished compiler/backend                                      5m04s   5GB
Apr 06 11:04:20 Starting compiler/encoders/asm
Apr 06 11:04:43 Finished compiler/encoders/asm                                   22s   1GB
Apr 06 11:04:43 Starting compiler/encoders/x64
Apr 06 11:05:46 Finished compiler/encoders/x64                                 1m03s   1GB
Apr 06 11:05:46 Starting compiler/encoders/arm7
Apr 06 11:07:48 Finished compiler/encoders/arm7                                2m01s   1GB
Apr 06 11:07:48 Starting compiler/encoders/arm8
Apr 06 11:08:27 Finished compiler/encoders/arm8                                  38s   1GB
Apr 06 11:08:27 Starting compiler/encoders/mips
Apr 06 11:09:53 Finished compiler/encoders/mips                                1m25s   1GB
Apr 06 11:09:53 Starting compiler/encoders/riscv
Apr 06 11:11:30 Finished compiler/encoders/riscv                               1m36s   1GB
Apr 06 11:11:30 Starting compiler/encoders/ag32
Apr 06 11:11:49 Finished compiler/encoders/ag32                                  18s 948MB
Apr 06 11:11:49 Starting compiler/backend/x64
Apr 06 11:12:08 Finished compiler/backend/x64                                    19s   1GB
Apr 06 11:12:08 Starting compiler/backend/arm7
Apr 06 11:12:29 Finished compiler/backend/arm7                                   20s   1GB
Apr 06 11:12:29 Starting compiler/backend/arm8
Apr 06 11:12:50 Finished compiler/backend/arm8                                   20s   1GB
Apr 06 11:12:50 Starting compiler/backend/mips
Apr 06 11:13:11 Finished compiler/backend/mips                                   20s   1GB
Apr 06 11:13:11 Starting compiler/backend/riscv
Apr 06 11:13:32 Finished compiler/backend/riscv                                  20s   1GB
Apr 06 11:13:32 Starting compiler/backend/ag32
Apr 06 11:14:43 Finished compiler/backend/ag32                                 1m10s   2GB
Apr 06 11:14:43 Starting compiler/parsing/proofs
Apr 06 11:20:35 Finished compiler/parsing/proofs                               5m52s   2GB
Apr 06 11:20:36 Starting compiler/inference/proofs
Apr 06 11:23:10 Finished compiler/inference/proofs                             2m34s   2GB
Apr 06 11:23:10 Starting compiler/backend/semantics
Apr 06 11:50:02 Finished compiler/backend/semantics                           26m52s   4GB
Apr 06 11:50:02 Starting compiler/backend/reg_alloc/proofs
Apr 06 11:53:23 Finished compiler/backend/reg_alloc/proofs                     3m20s   1GB
Apr 06 11:53:23 Starting compiler/backend/proofs
Apr 06 12:47:08 Finished compiler/backend/proofs                              53m44s  14GB
Apr 06 12:47:09 Starting compiler/encoders/x64/proofs
Apr 06 12:56:44 Finished compiler/encoders/x64/proofs                          9m35s   6GB
Apr 06 12:56:44 Starting compiler/encoders/arm7/proofs
Apr 06 13:09:37 Finished compiler/encoders/arm7/proofs                        12m52s   5GB
Apr 06 13:09:37 Starting compiler/encoders/arm8/proofs
Apr 06 13:16:07 Finished compiler/encoders/arm8/proofs                         6m30s   4GB
Apr 06 13:16:07 Starting compiler/encoders/mips/proofs
Apr 06 13:25:46 Finished compiler/encoders/mips/proofs                         9m38s   6GB
Apr 06 13:25:46 Starting compiler/encoders/riscv/proofs
Apr 06 13:34:11 Finished compiler/encoders/riscv/proofs                        8m24s   3GB
Apr 06 13:34:11 Starting compiler/encoders/ag32/proofs
Apr 06 13:36:31 Finished compiler/encoders/ag32/proofs                         2m19s   1GB
Apr 06 13:36:31 Starting compiler/backend/x64/proofs
Apr 06 13:36:54 Finished compiler/backend/x64/proofs                             22s   2GB
Apr 06 13:36:54 Starting compiler/backend/arm7/proofs
Apr 06 13:37:19 Finished compiler/backend/arm7/proofs                            24s   2GB
Apr 06 13:37:19 Starting compiler/backend/arm8/proofs
Apr 06 13:37:41 Finished compiler/backend/arm8/proofs                            21s   1GB
Apr 06 13:37:41 Starting compiler/backend/mips/proofs
Apr 06 13:38:03 Finished compiler/backend/mips/proofs                            22s   1GB
Apr 06 13:38:03 Starting compiler/backend/riscv/proofs
Apr 06 13:38:26 Finished compiler/backend/riscv/proofs                           22s   2GB
Apr 06 13:38:27 Starting compiler/backend/ag32/proofs
Apr 06 13:50:25 Finished compiler/backend/ag32/proofs                         11m58s   3GB
Apr 06 13:50:25 Starting compiler/proofs
Apr 06 13:52:21 Finished compiler/proofs                                       1m56s   6GB
Apr 06 13:52:22 Starting candle/set-theory
Apr 06 13:52:52 Finished candle/set-theory                                       30s   1GB
Apr 06 13:52:52 Starting candle/syntax-lib
Apr 06 13:53:04 Finished candle/syntax-lib                                       10s 807MB
Apr 06 13:53:04 Starting candle/standard/syntax
Apr 06 13:54:54 Finished candle/standard/syntax                                1m50s   1GB
Apr 06 13:54:54 Starting candle/standard/semantics
Apr 06 13:56:40 Finished candle/standard/semantics                             1m45s   2GB
Apr 06 13:56:40 Starting candle/standard/monadic
Apr 06 13:58:25 Finished candle/standard/monadic                               1m44s   2GB
Apr 06 13:58:25 Starting candle/standard/ml_kernel
Apr 06 14:03:53 Finished candle/standard/ml_kernel                             5m27s   5GB
Apr 06 14:03:53 Starting candle/overloading/syntax
Apr 06 14:07:08 Finished candle/overloading/syntax                             3m14s   1GB
Apr 06 14:07:09 Starting candle/overloading/semantics
Apr 06 14:19:18 Finished candle/overloading/semantics                         12m09s   7GB
Apr 06 14:19:18 Starting characteristic/examples
Apr 06 14:20:38 Finished characteristic/examples                               1m19s   4GB
Apr 06 14:20:38 Starting tutorial/solutions
Apr 06 14:36:07 Finished tutorial/solutions                                   15m28s  18GB
Apr 06 14:36:07 Starting translator/monadic/examples
Apr 06 14:39:32 Finished translator/monadic/examples                           3m24s   4GB
Apr 06 14:39:32 Starting examples
Apr 06 14:48:15 Finished examples                                              8m42s   6GB
Apr 06 14:48:15 Starting examples/compilation/x64
Apr 06 17:10:34 Finished examples/compilation/x64                           2h22m19s  24GB
Apr 06 17:10:34 Starting examples/compilation/x64/proofs
Apr 06 17:12:36 Finished examples/compilation/x64/proofs                       2m01s   3GB
Apr 06 17:12:36 Starting examples/compilation/ag32
Apr 06 17:45:34 Finished examples/compilation/ag32                            32m57s  17GB
Apr 06 17:45:34 Starting examples/compilation/ag32/proofs
Apr 06 17:46:25 Finished examples/compilation/ag32/proofs                        51s   5GB
Apr 06 17:46:25 Starting examples/cost
Apr 06 18:41:08 Finished examples/cost                                        54m42s  19GB
Apr 06 18:41:08 Starting examples/lpr_checker
Apr 06 18:45:05 Finished examples/lpr_checker                                  3m57s   6GB
Apr 06 18:45:05 Starting examples/lpr_checker/compilation
Apr 06 19:03:25 Finished examples/lpr_checker/compilation                     18m19s  17GB
Apr 06 19:03:25 Starting examples/lpr_checker/compilation/proofs
Apr 06 19:04:10 Finished examples/lpr_checker/compilation/proofs                 45s   4GB
Apr 06 19:04:10 Starting examples/lpr_checker/array
Apr 06 19:18:09 Finished examples/lpr_checker/array                           13m58s   5GB
Apr 06 19:18:10 Starting examples/lpr_checker/array/compilation
Apr 06 19:37:31 Finished examples/lpr_checker/array/compilation               19m21s  14GB
Apr 06 19:37:31 Starting examples/lpr_checker/array/compilation/proofs
Apr 06 19:38:21 Finished examples/lpr_checker/array/compilation/proofs           49s   5GB
Apr 06 19:38:22 Starting examples/opentheory
Apr 06 19:47:58 Finished examples/opentheory                                   9m35s   6GB
Apr 06 19:47:58 Starting examples/opentheory
Apr 06 19:47:59 Finished examples/opentheory                                      0s 100MB
Apr 06 19:47:59 Starting examples/opentheory/compilation
Apr 06 20:17:56 Finished examples/opentheory/compilation                      29m56s  26GB
Apr 06 20:17:56 Starting examples/opentheory/compilation/proofs
Apr 06 20:18:41 Finished examples/opentheory/compilation/proofs                  44s   4GB
Apr 06 20:18:41 Starting examples/opentheory/compilation/ag32
Apr 06 20:51:43 Finished examples/opentheory/compilation/ag32                 33m02s  25GB
Apr 06 20:51:43 Starting examples/opentheory/compilation/ag32/proofs
Apr 06 20:53:16 Finished examples/opentheory/compilation/ag32/proofs           1m32s   6GB
Apr 06 20:53:17 Starting translator/okasaki-examples
Apr 06 20:57:38 Finished translator/okasaki-examples                           4m20s   3GB
Apr 06 20:57:38 Starting translator/other-examples
Apr 06 20:59:41 Finished translator/other-examples                             2m03s   2GB
Apr 06 20:59:42 Starting compiler/parsing/tests
Apr 06 21:00:06 Finished compiler/parsing/tests                                  24s 627MB
Apr 06 21:00:06 Starting compiler/inference/tests
Apr 06 21:07:22 Finished compiler/inference/tests                              7m15s   5GB
Apr 06 21:07:22 Starting compiler/bootstrap/translation
Apr 06 23:32:27 Finished compiler/bootstrap/translation                     2h25m04s  57GB
Apr 06 23:32:27 Starting unverified/sexpr-bootstrap/x64/64
Apr 06 23:44:40 Finished unverified/sexpr-bootstrap/x64/64                    12m12s   8GB
Apr 06 23:44:40 Starting unverified/sexpr-bootstrap/x64/32
Apr 06 23:55:03 Finished unverified/sexpr-bootstrap/x64/32                    10m23s   8GB
Apr 06 23:55:03 Starting compiler/benchmarks
Apr 07 00:32:49 Finished compiler/benchmarks                                  37m45s   2GB
Apr 07 00:32:49 Starting semantics/alt_semantics
Apr 07 00:32:57 Finished semantics/alt_semantics                                  8s 412MB
Apr 07 00:32:58 Starting semantics/alt_semantics/proofs
Apr 07 00:33:47 FAILED: semantics/alt_semantics/proofs
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Starting work on README.md
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
README.md                                                                     real:    0s  user:    0s     OK
bigSmallInvariantsTheory                                                      real:    3s  user:    2s     OK
determTheory                                                                  real:   11s  user:   10s     OK
Starting work on bigClockTheory
bigStepPropsTheory                                                            real:   21s  user:   20s     OK
bigClockTheory                                                                real:   22s  user:   21s     OK
Starting work on bigSmallEquivTheory
Starting work on interpTheory
interpTheory                                                                  real:   14s  user:   14sFAIL<1>
 
 evaluate_dec T env st (Denv s) (st',r)
 
 Failed to prove theorem run_eval_decs_spec.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/myreen/regression/cakeml-1507/semantics/alt_semantics/proofs/interpScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1507/semantics/alt_semantics/proofs/interpScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
bigSmallEquivTheory                                                                                   M-KILLED