Job 1511

CakeML:ccf55f97b51233520e4ee648c9a46d8e89b9cfbd
  Use prim_src_config in various to_dataBootstraps [Apr 16 11:41:25]
#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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 16 13:56:54 Claimed job
Apr 16 13:57:00 Building HOL
Apr 16 14:13:29 Starting developers
Apr 16 14:13:34 Finished developers                                               4s 111MB
Apr 16 14:13:34 Starting developers/bin
Apr 16 14:13:41 Finished developers/bin                                           6s   1GB
Apr 16 14:13:42 Starting semantics/ffi
Apr 16 14:13:53 Finished semantics/ffi                                           11s 244MB
Apr 16 14:13:53 Starting semantics
Apr 16 14:15:31 Finished semantics                                             1m37s   1GB
Apr 16 14:15:32 Starting semantics/proofs
Apr 16 14:19:23 Finished semantics/proofs                                      3m51s   1GB
Apr 16 14:19:23 Starting semantics/alt_semantics
Apr 16 14:19:33 Finished semantics/alt_semantics                                  9s 329MB
Apr 16 14:19:33 Starting semantics/alt_semantics/proofs
Apr 16 14:21:56 Finished semantics/alt_semantics/proofs                        2m22s 821MB
Apr 16 14:21:56 Starting basis/pure
Apr 16 14:25:05 Finished basis/pure                                            3m07s 875MB
Apr 16 14:25:05 Starting translator
Apr 16 14:28:44 Finished translator                                            3m38s   1GB
Apr 16 14:28:44 Starting compiler/parsing
Apr 16 14:30:02 Finished compiler/parsing                                      1m17s   2GB
Apr 16 14:30:02 Starting characteristic
Apr 16 14:36:00 Finished characteristic                                        5m58s   1GB
Apr 16 14:36:00 Starting translator/monadic
Apr 16 14:37:44 Finished translator/monadic                                    1m43s   1GB
Apr 16 14:37:44 Starting basis
Apr 16 15:25:06 Finished basis                                                47m21s  18GB
Apr 16 15:25:07 Starting compiler/inference
Apr 16 15:26:26 Finished compiler/inference                                    1m18s   1GB
Apr 16 15:26:26 Starting compiler/backend/reg_alloc
Apr 16 15:27:35 Finished compiler/backend/reg_alloc                            1m09s   1GB
Apr 16 15:27:36 Starting compiler/backend/gc
Apr 16 15:31:27 Finished compiler/backend/gc                                   3m51s   2GB
Apr 16 15:31:27 Starting compiler/backend
Apr 16 15:36:36 Finished compiler/backend                                      5m08s   3GB
Apr 16 15:36:36 Starting compiler/encoders/asm
Apr 16 15:36:59 Finished compiler/encoders/asm                                   23s 650MB
Apr 16 15:37:00 Starting compiler/encoders/x64
Apr 16 15:38:07 Finished compiler/encoders/x64                                 1m07s 744MB
Apr 16 15:38:07 Starting compiler/encoders/arm7
Apr 16 15:40:20 Finished compiler/encoders/arm7                                2m12s   1GB
Apr 16 15:40:20 Starting compiler/encoders/arm8
Apr 16 15:41:00 Finished compiler/encoders/arm8                                  39s 558MB
Apr 16 15:41:00 Starting compiler/encoders/mips
Apr 16 15:42:37 Finished compiler/encoders/mips                                1m36s   1GB
Apr 16 15:42:37 Starting compiler/encoders/riscv
Apr 16 15:44:28 Finished compiler/encoders/riscv                               1m51s   1GB
Apr 16 15:44:29 Starting compiler/encoders/ag32
Apr 16 15:44:48 Finished compiler/encoders/ag32                                  18s 869MB
Apr 16 15:44:48 Starting compiler/backend/x64
Apr 16 15:45:08 Finished compiler/backend/x64                                    19s   1GB
Apr 16 15:45:08 Starting compiler/backend/arm7
Apr 16 15:45:30 Finished compiler/backend/arm7                                   21s   1GB
Apr 16 15:45:30 Starting compiler/backend/arm8
Apr 16 15:45:50 Finished compiler/backend/arm8                                   19s   1GB
Apr 16 15:45:50 Starting compiler/backend/mips
Apr 16 15:46:11 Finished compiler/backend/mips                                   20s   1GB
Apr 16 15:46:12 Starting compiler/backend/riscv
Apr 16 15:46:32 Finished compiler/backend/riscv                                  20s   1GB
Apr 16 15:46:32 Starting compiler/backend/ag32
Apr 16 15:47:46 Finished compiler/backend/ag32                                 1m13s   1GB
Apr 16 15:47:47 Starting compiler/parsing/proofs
Apr 16 15:53:56 Finished compiler/parsing/proofs                               6m09s   1GB
Apr 16 15:53:56 Starting compiler/inference/proofs
Apr 16 15:56:34 Finished compiler/inference/proofs                             2m37s   1GB
Apr 16 15:56:35 Starting compiler/backend/semantics
Apr 16 16:29:27 Finished compiler/backend/semantics                           32m52s   2GB
Apr 16 16:29:27 Starting compiler/backend/reg_alloc/proofs
Apr 16 16:33:18 Finished compiler/backend/reg_alloc/proofs                     3m49s 885MB
Apr 16 16:33:18 Starting compiler/backend/proofs
Apr 16 17:32:07 Finished compiler/backend/proofs                              58m47s  20GB
Apr 16 17:32:07 Starting compiler/encoders/x64/proofs
Apr 16 17:42:39 Finished compiler/encoders/x64/proofs                         10m31s   4GB
Apr 16 17:42:39 Starting compiler/encoders/arm7/proofs
Apr 16 17:56:54 Finished compiler/encoders/arm7/proofs                        14m14s   6GB
Apr 16 17:56:54 Starting compiler/encoders/arm8/proofs
Apr 16 18:04:20 Finished compiler/encoders/arm8/proofs                         7m25s   1GB
Apr 16 18:04:20 Starting compiler/encoders/mips/proofs
Apr 16 18:15:01 Finished compiler/encoders/mips/proofs                        10m40s   3GB
Apr 16 18:15:01 Starting compiler/encoders/riscv/proofs
Apr 16 18:24:45 Finished compiler/encoders/riscv/proofs                        9m43s 983MB
Apr 16 18:24:45 Starting compiler/encoders/ag32/proofs
Apr 16 18:27:36 Finished compiler/encoders/ag32/proofs                         2m50s 686MB
Apr 16 18:27:36 Starting compiler/backend/x64/proofs
Apr 16 18:27:58 Finished compiler/backend/x64/proofs                             22s   1GB
Apr 16 18:27:59 Starting compiler/backend/arm7/proofs
Apr 16 18:28:24 Finished compiler/backend/arm7/proofs                            24s   1GB
Apr 16 18:28:24 Starting compiler/backend/arm8/proofs
Apr 16 18:28:47 Finished compiler/backend/arm8/proofs                            22s   1GB
Apr 16 18:28:47 Starting compiler/backend/mips/proofs
Apr 16 18:29:11 Finished compiler/backend/mips/proofs                            23s   1GB
Apr 16 18:29:11 Starting compiler/backend/riscv/proofs
Apr 16 18:29:34 Finished compiler/backend/riscv/proofs                           23s   1GB
Apr 16 18:29:34 Starting compiler/backend/ag32/proofs
Apr 16 18:43:08 Finished compiler/backend/ag32/proofs                         13m33s   4GB
Apr 16 18:43:08 Starting compiler/proofs
Apr 17 08:43:58 Resuming compiler/proofs
Apr 17 08:45:41 Finished compiler/proofs                                       1m43s   3GB
Apr 17 08:45:42 Starting candle/set-theory
Apr 17 08:46:11 Finished candle/set-theory                                       29s 690MB
Apr 17 08:46:11 Starting candle/syntax-lib
Apr 17 08:46:22 Finished candle/syntax-lib                                       10s 677MB
Apr 17 08:46:23 Starting candle/standard/syntax
Apr 17 08:48:19 Finished candle/standard/syntax                                1m56s   1GB
Apr 17 08:48:20 Starting candle/standard/semantics
Apr 17 08:50:08 Finished candle/standard/semantics                             1m47s   1GB
Apr 17 08:50:08 Starting candle/standard/monadic
Apr 17 08:52:00 Finished candle/standard/monadic                               1m51s   1GB
Apr 17 08:52:00 Starting candle/standard/ml_kernel
Apr 17 08:58:13 Finished candle/standard/ml_kernel                             6m13s   5GB
Apr 17 08:58:13 Starting candle/overloading/syntax
Apr 17 09:01:36 Finished candle/overloading/syntax                             3m22s   1GB
Apr 17 09:01:36 Starting candle/overloading/semantics
Apr 17 09:14:53 Finished candle/overloading/semantics                         13m16s   2GB
Apr 17 09:14:53 Starting characteristic/examples
Apr 17 09:16:16 Finished characteristic/examples                               1m22s   2GB
Apr 17 09:16:16 Starting tutorial/solutions
Apr 17 09:32:46 Finished tutorial/solutions                                   16m29s   8GB
Apr 17 09:32:46 Starting translator/monadic/examples
Apr 17 09:36:11 Finished translator/monadic/examples                           3m24s   3GB
Apr 17 09:36:11 Starting examples
Apr 17 09:45:23 Finished examples                                              9m10s   3GB
Apr 17 09:45:23 Starting examples/compilation/x64
Apr 17 12:17:15 Finished examples/compilation/x64                           2h31m51s  14GB
Apr 17 12:17:15 Starting examples/compilation/x64/proofs
Apr 17 12:19:07 Finished examples/compilation/x64/proofs                       1m51s   3GB
Apr 17 12:19:07 Starting examples/compilation/ag32
Apr 17 12:54:35 Finished examples/compilation/ag32                            35m27s   7GB
Apr 17 12:54:35 Starting examples/compilation/ag32/proofs
Apr 17 12:55:31 Finished examples/compilation/ag32/proofs                        56s   3GB
Apr 17 12:55:32 Starting examples/cost
Apr 17 13:55:25 Finished examples/cost                                        59m52s   7GB
Apr 17 13:55:25 Starting examples/lpr_checker
Apr 17 13:59:38 Finished examples/lpr_checker                                  4m12s   3GB
Apr 17 13:59:38 Starting examples/lpr_checker/compilation
Apr 17 14:18:50 Finished examples/lpr_checker/compilation                     19m11s  10GB
Apr 17 14:18:50 Starting examples/lpr_checker/compilation/proofs
Apr 17 14:19:32 Finished examples/lpr_checker/compilation/proofs                 41s   3GB
Apr 17 14:19:32 Starting examples/lpr_checker/array
Apr 17 14:35:15 Finished examples/lpr_checker/array                           15m42s   3GB
Apr 17 14:35:15 Starting examples/lpr_checker/array/compilation
Apr 17 14:56:28 Finished examples/lpr_checker/array/compilation               21m12s  13GB
Apr 17 14:56:28 Starting examples/lpr_checker/array/compilation/proofs
Apr 17 14:57:17 Finished examples/lpr_checker/array/compilation/proofs           48s   3GB
Apr 17 14:57:17 Starting examples/opentheory
Apr 17 15:07:41 Finished examples/opentheory                                  10m23s   6GB
Apr 17 15:07:41 Starting examples/opentheory
Apr 17 15:07:42 Finished examples/opentheory                                      1s  18MB
Apr 17 15:07:42 Starting examples/opentheory/compilation
Apr 17 15:41:55 Finished examples/opentheory/compilation                      34m12s  24GB
Apr 17 15:41:55 Starting examples/opentheory/compilation/proofs
Apr 17 15:42:40 Finished examples/opentheory/compilation/proofs                  44s   3GB
Apr 17 15:42:40 Starting examples/opentheory/compilation/ag32
Apr 17 16:18:21 Finished examples/opentheory/compilation/ag32                 35m40s  19GB
Apr 17 16:18:21 Starting examples/opentheory/compilation/ag32/proofs
Apr 17 16:20:03 Finished examples/opentheory/compilation/ag32/proofs           1m41s   5GB
Apr 17 16:20:03 Starting translator/okasaki-examples
Apr 17 16:24:53 Finished translator/okasaki-examples                           4m49s   1GB
Apr 17 16:24:53 Starting translator/other-examples
Apr 17 16:27:01 Finished translator/other-examples                             2m07s   1GB
Apr 17 16:27:01 Starting compiler/parsing/tests
Apr 17 16:27:28 Finished compiler/parsing/tests                                  26s 584MB
Apr 17 16:27:29 Starting compiler/inference/tests
Apr 17 16:35:45 Finished compiler/inference/tests                              8m16s   4GB
Apr 17 16:35:45 Starting compiler/bootstrap/translation
Apr 17 19:20:36 Finished compiler/bootstrap/translation                     2h44m50s  28GB
Apr 17 19:20:36 Starting unverified/sexpr-bootstrap/x64/64
Apr 17 19:32:07 Finished unverified/sexpr-bootstrap/x64/64                    11m30s   8GB
Apr 17 19:32:07 Starting unverified/sexpr-bootstrap/x64/32
Apr 17 19:42:04 Finished unverified/sexpr-bootstrap/x64/32                     9m57s   8GB
Apr 17 19:42:04 Starting compiler/benchmarks
Apr 17 19:42:07 Finished compiler/benchmarks                                      1s  26MB
Apr 17 19:42:07 Starting compiler/bootstrap/compilation/x64/64
Apr 17 19:43:35 FAILED: compiler/bootstrap/compilation/x64/64
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/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                       real:    0s  user:    0s     OK
cake-sexpr-32                                   real:   77s  user:   72s     OK
cake-sexpr-64                                   real:   78s  user:   73s     OK
to_dataBootstrapTheory                          real:   86s  user:   81sFAIL<1>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL message: Created theory "to_dataBootstrap">>
 error in quse /home/cake/oven/regression/cakeml-1511/compiler/bootstrap/compilation/x64/64/to_dataBootstrapScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1511/compiler/bootstrap/compilation/x64/64/to_dataBootstrapScript : Fail "Static Errors"
 Saved definition __ "init_conf_def"
 /home/cake/oven/regression/cakeml-1511/compiler/bootstrap/compilation/x64/64/to_dataBootstrapScript.sml:52: error: Value or constructor (cs) has not been declared
 Found near
   save_thm ("to_data_x64_thm", ... ... compiler64_prog_thm "data_prog_x64")
 Uncaught exception: Fail "Static Errors"