Job 1505

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:7cfa01a77558af8c5a6c045cd38e9544d3bd324c
  Start of an example setting up a simple-minded FOL proof system [Mar 30 03:26:34]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 31 19:11:38 Claimed job
Mar 31 19:11:44 Building HOL
Mar 31 19:28:05 Starting developers
Mar 31 19:28:09 Finished developers                                               4s 111MB
Mar 31 19:28:09 Starting developers/bin
Mar 31 19:28:16 Finished developers/bin                                           6s   1GB
Mar 31 19:28:17 Starting semantics/ffi
Mar 31 19:28:28 Finished semantics/ffi                                           11s 243MB
Mar 31 19:28:28 Starting semantics
Mar 31 19:30:06 Finished semantics                                             1m37s   1GB
Mar 31 19:30:07 Starting semantics/proofs
Mar 31 19:33:59 Finished semantics/proofs                                      3m51s   1GB
Mar 31 19:33:59 Starting basis/pure
Mar 31 19:37:02 Finished basis/pure                                            3m02s 887MB
Mar 31 19:37:02 Starting translator
Mar 31 19:40:43 Finished translator                                            3m40s   1GB
Mar 31 19:40:43 Starting compiler/parsing
Mar 31 19:42:00 Finished compiler/parsing                                      1m16s   2GB
Mar 31 19:42:00 Starting characteristic
Mar 31 19:47:55 Finished characteristic                                        5m55s   1GB
Mar 31 19:47:56 Starting translator/monadic
Mar 31 19:49:38 Finished translator/monadic                                    1m41s   1GB
Mar 31 19:49:38 Starting basis
Mar 31 20:37:45 Finished basis                                                48m06s  15GB
Mar 31 20:37:45 Starting compiler/inference
Mar 31 20:39:03 Finished compiler/inference                                    1m18s   1GB
Mar 31 20:39:04 Starting compiler/backend/reg_alloc
Mar 31 20:40:15 Finished compiler/backend/reg_alloc                            1m10s   1GB
Mar 31 20:40:15 Starting compiler/backend/gc
Mar 31 20:44:06 Finished compiler/backend/gc                                   3m50s   2GB
Mar 31 20:44:06 Starting compiler/backend
Mar 31 20:49:17 Finished compiler/backend                                      5m10s   3GB
Mar 31 20:49:18 Starting compiler/encoders/asm
Mar 31 20:49:41 Finished compiler/encoders/asm                                   23s 720MB
Mar 31 20:49:41 Starting compiler/encoders/x64
Mar 31 20:50:48 Finished compiler/encoders/x64                                 1m06s   1GB
Mar 31 20:50:48 Starting compiler/encoders/arm7
Mar 31 20:53:00 Finished compiler/encoders/arm7                                2m11s   1GB
Mar 31 20:53:00 Starting compiler/encoders/arm8
Mar 31 20:53:40 Finished compiler/encoders/arm8                                  39s 919MB
Mar 31 20:53:40 Starting compiler/encoders/mips
Mar 31 20:55:17 Finished compiler/encoders/mips                                1m36s   1GB
Mar 31 20:55:17 Starting compiler/encoders/riscv
Mar 31 20:57:08 Finished compiler/encoders/riscv                               1m51s   1GB
Mar 31 20:57:08 Starting compiler/encoders/ag32
Mar 31 20:57:27 Finished compiler/encoders/ag32                                  18s 512MB
Mar 31 20:57:27 Starting compiler/backend/x64
Mar 31 20:57:47 Finished compiler/backend/x64                                    19s   1GB
Mar 31 20:57:48 Starting compiler/backend/arm7
Mar 31 20:58:10 Finished compiler/backend/arm7                                   21s   1GB
Mar 31 20:58:10 Starting compiler/backend/arm8
Mar 31 20:58:30 Finished compiler/backend/arm8                                   20s   1GB
Mar 31 20:58:30 Starting compiler/backend/mips
Mar 31 20:58:51 Finished compiler/backend/mips                                   20s   1GB
Mar 31 20:58:51 Starting compiler/backend/riscv
Mar 31 20:59:12 Finished compiler/backend/riscv                                  20s   1GB
Mar 31 20:59:12 Starting compiler/backend/ag32
Mar 31 21:00:26 Finished compiler/backend/ag32                                 1m13s   1GB
Mar 31 21:00:26 Starting compiler/parsing/proofs
Mar 31 21:06:38 Finished compiler/parsing/proofs                               6m12s   1GB
Mar 31 21:06:39 Starting compiler/inference/proofs
Mar 31 21:09:20 Finished compiler/inference/proofs                             2m41s   1GB
Mar 31 21:09:20 Starting compiler/backend/semantics
Mar 31 21:42:34 Finished compiler/backend/semantics                           33m13s   2GB
Mar 31 21:42:34 Starting compiler/backend/reg_alloc/proofs
Mar 31 21:46:22 Finished compiler/backend/reg_alloc/proofs                     3m47s 853MB
Mar 31 21:46:22 Starting compiler/backend/proofs
Mar 31 22:45:14 Finished compiler/backend/proofs                              58m51s  14GB
Mar 31 22:45:14 Starting compiler/encoders/x64/proofs
Mar 31 22:55:47 Finished compiler/encoders/x64/proofs                         10m32s   4GB
Mar 31 22:55:47 Starting compiler/encoders/arm7/proofs
Mar 31 23:10:02 Finished compiler/encoders/arm7/proofs                        14m15s   3GB
Mar 31 23:10:02 Starting compiler/encoders/arm8/proofs
Mar 31 23:17:22 Finished compiler/encoders/arm8/proofs                         7m19s   1GB
Mar 31 23:17:22 Starting compiler/encoders/mips/proofs
Mar 31 23:28:06 Finished compiler/encoders/mips/proofs                        10m43s   3GB
Mar 31 23:28:06 Starting compiler/encoders/riscv/proofs
Mar 31 23:37:57 Finished compiler/encoders/riscv/proofs                        9m50s   1GB
Mar 31 23:37:57 Starting compiler/encoders/ag32/proofs
Mar 31 23:40:46 Finished compiler/encoders/ag32/proofs                         2m48s 667MB
Mar 31 23:40:46 Starting compiler/backend/x64/proofs
Mar 31 23:41:09 Finished compiler/backend/x64/proofs                             22s   1GB
Mar 31 23:41:09 Starting compiler/backend/arm7/proofs
Mar 31 23:41:34 Finished compiler/backend/arm7/proofs                            24s   1GB
Mar 31 23:41:35 Starting compiler/backend/arm8/proofs
Mar 31 23:41:58 Finished compiler/backend/arm8/proofs                            23s   1GB
Mar 31 23:41:58 Starting compiler/backend/mips/proofs
Mar 31 23:42:21 Finished compiler/backend/mips/proofs                            22s   1GB
Mar 31 23:42:21 Starting compiler/backend/riscv/proofs
Mar 31 23:42:44 Finished compiler/backend/riscv/proofs                           22s   1GB
Mar 31 23:42:45 Starting compiler/backend/ag32/proofs
Mar 31 23:56:25 Finished compiler/backend/ag32/proofs                         13m40s   3GB
Mar 31 23:56:25 Starting compiler/proofs
Mar 31 23:58:25 Finished compiler/proofs                                       1m59s   3GB
Mar 31 23:58:26 Starting candle/set-theory
Mar 31 23:58:55 Finished candle/set-theory                                       29s 955MB
Mar 31 23:58:56 Starting candle/syntax-lib
Mar 31 23:59:06 Finished candle/syntax-lib                                       10s 661MB
Mar 31 23:59:07 Starting candle/standard/syntax
Apr 01 00:01:04 Finished candle/standard/syntax                                1m56s 896MB
Apr 01 00:01:04 Starting candle/standard/semantics
Apr 01 00:02:54 Finished candle/standard/semantics                             1m49s   1GB
Apr 01 00:02:54 Starting candle/standard/monadic
Apr 01 00:04:46 Finished candle/standard/monadic                               1m51s   1GB
Apr 01 00:04:47 Starting candle/standard/ml_kernel
Apr 01 00:11:00 Finished candle/standard/ml_kernel                             6m13s   4GB
Apr 01 00:11:00 Starting candle/overloading/syntax
Apr 01 00:14:23 Finished candle/overloading/syntax                             3m22s   1GB
Apr 01 00:14:23 Starting candle/overloading/semantics
Apr 01 00:27:24 Finished candle/overloading/semantics                         13m00s   3GB
Apr 01 00:27:24 Starting characteristic/examples
Apr 01 00:28:49 Finished characteristic/examples                               1m24s   2GB
Apr 01 00:28:49 Starting tutorial/solutions
Apr 01 00:45:34 Finished tutorial/solutions                                   16m44s   8GB
Apr 01 00:45:34 Starting translator/monadic/examples
Apr 01 00:48:56 Finished translator/monadic/examples                           3m21s   2GB
Apr 01 00:48:57 Starting examples
Apr 01 00:58:00 Finished examples                                              9m02s   4GB
Apr 01 00:58:00 Starting examples/compilation/x64
Apr 01 03:28:49 Finished examples/compilation/x64                           2h30m48s  15GB
Apr 01 03:28:49 Starting examples/compilation/x64/proofs
Apr 01 03:30:40 Finished examples/compilation/x64/proofs                       1m50s   3GB
Apr 01 03:30:40 Starting examples/compilation/ag32
Apr 01 04:05:48 Finished examples/compilation/ag32                            35m07s   7GB
Apr 01 04:05:48 Starting examples/compilation/ag32/proofs
Apr 01 04:06:36 Finished examples/compilation/ag32/proofs                        47s   2GB
Apr 01 04:06:36 Starting examples/cost
Apr 01 05:06:39 Finished examples/cost                                      1h00m03s   8GB
Apr 01 05:06:40 Starting examples/lpr_checker
Apr 01 05:10:56 Finished examples/lpr_checker                                  4m15s   4GB
Apr 01 05:10:56 Starting examples/lpr_checker/compilation
Apr 01 05:30:16 Finished examples/lpr_checker/compilation                     19m19s  10GB
Apr 01 05:30:16 Starting examples/lpr_checker/compilation/proofs
Apr 01 05:30:57 Finished examples/lpr_checker/compilation/proofs                 41s   3GB
Apr 01 05:30:57 Starting examples/lpr_checker/array
Apr 01 05:46:40 Finished examples/lpr_checker/array                           15m42s   3GB
Apr 01 05:46:40 Starting examples/lpr_checker/array/compilation
Apr 01 06:07:31 Finished examples/lpr_checker/array/compilation               20m50s  11GB
Apr 01 06:07:31 Starting examples/lpr_checker/array/compilation/proofs
Apr 01 06:08:20 Finished examples/lpr_checker/array/compilation/proofs           48s   3GB
Apr 01 06:08:20 Starting examples/opentheory
Apr 01 06:18:37 Finished examples/opentheory                                  10m16s   5GB
Apr 01 06:18:37 Starting examples/opentheory
Apr 01 06:18:38 Finished examples/opentheory                                      1s  19MB
Apr 01 06:18:39 Starting examples/opentheory/compilation
Apr 01 06:52:27 Finished examples/opentheory/compilation                      33m48s  18GB
Apr 01 06:52:28 Starting examples/opentheory/compilation/proofs
Apr 01 06:53:13 Finished examples/opentheory/compilation/proofs                  45s   3GB
Apr 01 06:53:13 Starting examples/opentheory/compilation/ag32
Apr 01 07:28:53 Finished examples/opentheory/compilation/ag32                 35m40s  14GB
Apr 01 07:28:54 Starting examples/opentheory/compilation/ag32/proofs
Apr 01 07:30:33 Finished examples/opentheory/compilation/ag32/proofs           1m38s   5GB
Apr 01 07:30:33 Starting translator/okasaki-examples
Apr 01 07:35:23 Finished translator/okasaki-examples                           4m49s   1GB
Apr 01 07:35:23 Starting translator/other-examples
Apr 01 07:37:31 Finished translator/other-examples                             2m07s   1GB
Apr 01 07:37:32 Starting compiler/parsing/tests
Apr 01 07:37:59 Finished compiler/parsing/tests                                  26s 637MB
Apr 01 07:37:59 Starting compiler/inference/tests
Apr 01 07:46:22 Finished compiler/inference/tests                              8m22s   7GB
Apr 01 07:46:22 Starting compiler/bootstrap/translation
Apr 01 10:34:05 Finished compiler/bootstrap/translation                     2h47m42s  24GB
Apr 01 10:34:05 Starting unverified/sexpr-bootstrap/x64/64
Apr 01 10:45:40 Finished unverified/sexpr-bootstrap/x64/64                    11m34s   8GB
Apr 01 10:45:40 Starting unverified/sexpr-bootstrap/x64/32
Apr 01 10:55:45 Finished unverified/sexpr-bootstrap/x64/32                    10m04s   8GB
Apr 01 10:55:45 Starting compiler/benchmarks
Apr 01 10:55:47 Finished compiler/benchmarks                                      1s  23MB
Apr 01 10:55:47 Starting semantics/alt_semantics
Apr 01 10:55:57 Finished semantics/alt_semantics                                  9s 344MB
Apr 01 10:55:57 Starting semantics/alt_semantics/proofs
Apr 01 10:56: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 bigSmallInvariantsScript
Starting work on determTheory
Starting work on bigStepPropsTheory
bigSmallInvariantsScript                        real:    0s  user:    0s     OK
Starting work on README.md
Starting work on bigSmallInvariantsTheory
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:   22s  user:   21s     OK
bigClockTheory                                  real:   23s  user:   23s     OK
Starting work on bigSmallEquivTheory
Starting work on interpTheory
interpTheory                                    real:   13s  user:   12sFAIL<1>
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/cake/oven/regression/cakeml-1505/semantics/alt_semantics/proofs/interpScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/cake/oven/regression/cakeml-1505/semantics/alt_semantics/proofs/interpScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 First unsolved sub-goal is
 
 evaluate_dec T env st (Denv s) (st',r)
 
 Failed to prove theorem run_eval_decs_spec.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
bigSmallEquivTheory                                                     M-KILLED