Job 1466

CakeML:f3ebdb75b77b7d4d90fa971f3a7a2864fb558095
  Adjust compiler{32,64}Prog for config changes [Feb 04 21:26:53]
#811 (eval)
Merging into:b39b4fb6cf973c84886fd436ede81ae7d70b3603
  Merge pull request #814 from CakeML/export_type [Feb 01 09:56:45]
HOL:8e7bbd4c050ab9a90e53ae4892bbf0fb9f61dcfd
  Simplify a number of proofs in rich_list [Feb 03 23:29:38]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 05 09:21:10 Claimed job
Feb 05 09:21:20 Building HOL
Feb 05 09:35:34 Starting developers
Feb 05 09:35:36 Finished developers                                               2s 101MB
Feb 05 09:35:36 Starting developers/bin
Feb 05 09:35:42 Finished developers/bin                                           5s   1GB
Feb 05 09:35:43 Starting semantics/ffi
Feb 05 09:35:53 Finished semantics/ffi                                           10s 317MB
Feb 05 09:35:53 Starting semantics
Feb 05 09:37:29 Finished semantics                                             1m35s   1GB
Feb 05 09:37:29 Starting semantics/proofs
Feb 05 09:41:03 Finished semantics/proofs                                      3m34s   1GB
Feb 05 09:41:03 Starting basis/pure
Feb 05 09:43:43 Finished basis/pure                                            2m39s   1GB
Feb 05 09:43:43 Starting translator
Feb 05 09:46:59 Finished translator                                            3m15s   2GB
Feb 05 09:46:59 Starting compiler/parsing
Feb 05 09:48:08 Finished compiler/parsing                                      1m08s   5GB
Feb 05 09:48:08 Starting characteristic
Feb 05 09:53:48 Finished characteristic                                        5m39s   3GB
Feb 05 09:53:48 Starting translator/monadic
Feb 05 09:55:33 Finished translator/monadic                                    1m44s   2GB
Feb 05 09:55:33 Starting basis
Feb 05 10:39:54 Finished basis                                                44m20s  29GB
Feb 05 10:39:54 Starting compiler/inference
Feb 05 10:41:06 Finished compiler/inference                                    1m11s   1GB
Feb 05 10:41:06 Starting compiler/backend/reg_alloc
Feb 05 10:42:11 Finished compiler/backend/reg_alloc                            1m04s   1GB
Feb 05 10:42:11 Starting compiler/backend/gc
Feb 05 10:45:47 Finished compiler/backend/gc                                   3m35s   3GB
Feb 05 10:45:47 Starting compiler/backend
Feb 05 10:50:52 Finished compiler/backend                                      5m04s   5GB
Feb 05 10:50:52 Starting compiler/encoders/asm
Feb 05 10:51:14 Finished compiler/encoders/asm                                   21s   1GB
Feb 05 10:51:15 Starting compiler/encoders/x64
Feb 05 10:52:16 Finished compiler/encoders/x64                                 1m01s   1GB
Feb 05 10:52:16 Starting compiler/encoders/arm7
Feb 05 10:54:18 Finished compiler/encoders/arm7                                2m01s   1GB
Feb 05 10:54:18 Starting compiler/encoders/arm8
Feb 05 10:54:56 Finished compiler/encoders/arm8                                  38s   1GB
Feb 05 10:54:56 Starting compiler/encoders/mips
Feb 05 10:56:21 Finished compiler/encoders/mips                                1m24s   1GB
Feb 05 10:56:22 Starting compiler/encoders/riscv
Feb 05 10:57:58 Finished compiler/encoders/riscv                               1m36s   1GB
Feb 05 10:57:58 Starting compiler/encoders/ag32
Feb 05 10:58:16 Finished compiler/encoders/ag32                                  17s 950MB
Feb 05 10:58:17 Starting compiler/backend/x64
Feb 05 10:58:37 Finished compiler/backend/x64                                    20s   1GB
Feb 05 10:58:37 Starting compiler/backend/arm7
Feb 05 10:58:56 Finished compiler/backend/arm7                                   19s   1GB
Feb 05 10:58:57 Starting compiler/backend/arm8
Feb 05 10:59:17 Finished compiler/backend/arm8                                   20s   1GB
Feb 05 10:59:17 Starting compiler/backend/mips
Feb 05 10:59:38 Finished compiler/backend/mips                                   20s   1GB
Feb 05 10:59:39 Starting compiler/backend/riscv
Feb 05 11:00:00 Finished compiler/backend/riscv                                  21s   1GB
Feb 05 11:00:00 Starting compiler/backend/ag32
Feb 05 11:01:11 Finished compiler/backend/ag32                                 1m11s   2GB
Feb 05 11:01:12 Starting compiler/parsing/proofs
Feb 05 11:07:00 Finished compiler/parsing/proofs                               5m48s   2GB
Feb 05 11:07:00 Starting compiler/inference/proofs
Feb 05 11:09:33 Finished compiler/inference/proofs                             2m32s   2GB
Feb 05 11:09:33 Starting compiler/backend/semantics
Feb 05 11:36:36 Finished compiler/backend/semantics                           27m02s   4GB
Feb 05 11:36:36 Starting compiler/backend/reg_alloc/proofs
Feb 05 11:39:56 Finished compiler/backend/reg_alloc/proofs                     3m18s   2GB
Feb 05 11:39:56 Starting compiler/backend/proofs
Feb 05 12:34:08 Finished compiler/backend/proofs                              54m11s  16GB
Feb 05 12:34:08 Starting compiler/encoders/x64/proofs
Feb 05 12:43:40 Finished compiler/encoders/x64/proofs                          9m31s   6GB
Feb 05 12:43:41 Starting compiler/encoders/arm7/proofs
Feb 05 12:56:05 Finished compiler/encoders/arm7/proofs                        12m23s  11GB
Feb 05 12:56:05 Starting compiler/encoders/arm8/proofs
Feb 05 13:02:20 Finished compiler/encoders/arm8/proofs                         6m15s   4GB
Feb 05 13:02:21 Starting compiler/encoders/mips/proofs
Feb 05 13:12:09 Finished compiler/encoders/mips/proofs                         9m47s   6GB
Feb 05 13:12:09 Starting compiler/encoders/riscv/proofs
Feb 05 13:20:23 Finished compiler/encoders/riscv/proofs                        8m14s   3GB
Feb 05 13:20:24 Starting compiler/encoders/ag32/proofs
Feb 05 13:22:45 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Feb 05 13:22:45 Starting compiler/backend/x64/proofs
Feb 05 13:23:08 Finished compiler/backend/x64/proofs                             22s   2GB
Feb 05 13:23:08 Starting compiler/backend/arm7/proofs
Feb 05 13:23:31 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 05 13:23:31 Starting compiler/backend/arm8/proofs
Feb 05 13:23:51 Finished compiler/backend/arm8/proofs                            20s   1GB
Feb 05 13:23:52 Starting compiler/backend/mips/proofs
Feb 05 13:24:14 Finished compiler/backend/mips/proofs                            22s   1GB
Feb 05 13:24:14 Starting compiler/backend/riscv/proofs
Feb 05 13:24:38 Finished compiler/backend/riscv/proofs                           24s   2GB
Feb 05 13:24:38 Starting compiler/backend/ag32/proofs
Feb 05 13:36:48 Finished compiler/backend/ag32/proofs                         12m09s   5GB
Feb 05 13:36:49 Starting compiler/proofs
Feb 05 13:38:48 Finished compiler/proofs                                       1m58s   6GB
Feb 05 13:38:48 Starting candle/set-theory
Feb 05 13:39:17 Finished candle/set-theory                                       29s   1GB
Feb 05 13:39:17 Starting candle/syntax-lib
Feb 05 13:39:28 Finished candle/syntax-lib                                       11s 781MB
Feb 05 13:39:29 Starting candle/standard/syntax
Feb 05 13:41:18 Finished candle/standard/syntax                                1m49s   2GB
Feb 05 13:41:18 Starting candle/standard/semantics
Feb 05 13:43:06 Finished candle/standard/semantics                             1m47s   2GB
Feb 05 13:43:06 Starting candle/standard/monadic
Feb 05 13:44:50 Finished candle/standard/monadic                               1m43s   1GB
Feb 05 13:44:50 Starting candle/standard/ml_kernel
Feb 05 13:50:26 Finished candle/standard/ml_kernel                             5m35s   5GB
Feb 05 13:50:26 Starting candle/overloading/syntax
Feb 05 13:53:36 Finished candle/overloading/syntax                             3m10s   1GB
Feb 05 13:53:36 Starting candle/overloading/semantics
Feb 05 14:05:43 Finished candle/overloading/semantics                         12m06s   9GB
Feb 05 14:05:44 Starting characteristic/examples
Feb 05 14:07:03 Finished characteristic/examples                               1m19s   4GB
Feb 05 14:07:04 Starting tutorial/solutions
Feb 05 14:22:45 Finished tutorial/solutions                                   15m41s  15GB
Feb 05 14:22:45 Starting translator/monadic/examples
Feb 05 14:26:10 Finished translator/monadic/examples                           3m24s   3GB
Feb 05 14:26:10 Starting examples
Feb 05 14:35:04 Finished examples                                              8m54s   8GB
Feb 05 14:35:05 Starting examples/compilation/x64
Feb 05 16:58:05 Finished examples/compilation/x64                           2h22m59s  24GB
Feb 05 16:58:05 Starting examples/compilation/x64/proofs
Feb 05 17:00:05 Finished examples/compilation/x64/proofs                       2m00s   3GB
Feb 05 17:00:05 Starting examples/compilation/ag32
Feb 05 17:33:23 Finished examples/compilation/ag32                            33m17s  10GB
Feb 05 17:33:23 Starting examples/compilation/ag32/proofs
Feb 05 17:34:14 Finished examples/compilation/ag32/proofs                        51s   5GB
Feb 05 17:34:14 Starting examples/cost
Feb 05 17:48:40 FAILED: examples/cost
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$(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$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Starting work on README.md
Starting work on costPropsTheory
Starting work on size_ofPropsTheory
Starting work on miniBasisProgTheory
README.md                                                                     real:    0s  user:    0s     OK
size_ofPropsTheory                                                            real:   30s  user:   29s     OK
miniBasisProgTheory                                                           real:   31s  user:   29s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                                               real:   99s  user:   95s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                             real:  648s  user:  711s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                                                            real:  647s  user:  691s     OK
Starting work on pureLoopProofTheory
allProgTheory                                                                 real:  652s  user:  700s     OK
Starting work on allProofTheory
allProofTheory                                                                real:  111s  user:  105sFAIL<1>
 Saved definition __ "repbool_to_tsl_def"
 Saved induction ___ "repbool_to_tsl_ind"
 Saved theorem _____ "repbool_list_to_tsl_SOME"
 Saved definition __ "repbool_list_safe_def"
 Saved definition __ "repbool_safe_heap_def"
 Saved theorem _____ "repbool_list_size_of_rm"
 Saved theorem _____ "repbool_list_seen_MEM"
 error in quse /home/myreen/regression/cakeml-1466/examples/cost/allProofScript.sml : HOL_ERR {message = "on line 212, characters 19-22:\nCouldn't infer type for overloaded name  _ record selectcode", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load /home/myreen/regression/cakeml-1466/examples/cost/allProofScript : HOL_ERR {message = "on line 212, characters 19-22:\nCouldn't infer type for overloaded name  _ record selectcode", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 212, characters 19-22:\nCouldn't infer type for overloaded name  _ record selectcode", origin_function = "type-analysis", origin_structure = "Preterm"}
cyesProgTheory                                                                                        M-KILLED
lcgLoopProofTheory                                                                                    M-KILLED
pureLoopProofTheory                                                                                   M-KILLED