Job 1378

CakeML:05bb6c4ce145c198ba5bfe7ff8e609d2d64d530a
  Minor tweaks [Oct 21 12:39:26]
#802 (data-cost)
Merging into:bc1d24030a96270694c72cff1c37f656c1e85a9f
  Disambiguate some terms [Oct 16 13:02:29]
HOL:6c2b347359d14514e88c56ae31d4cf5bff5a5e58
  Merge remote-tracking branch 'origin/develop' into thibault-wip [Oct 19 09:13:50]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Oct 21 12:55:27 Claimed job
Oct 21 12:55:40 Building HOL
Oct 21 13:11:01 Starting developers
Oct 21 13:11:06 Finished developers                                               4s 114MB
Oct 21 13:11:06 Starting developers/bin
Oct 21 13:11:13 Finished developers/bin                                           6s   1GB
Oct 21 13:11:13 Starting semantics/ffi
Oct 21 13:11:24 Finished semantics/ffi                                           10s 245MB
Oct 21 13:11:24 Starting semantics
Oct 21 13:13:00 Finished semantics                                             1m35s   1GB
Oct 21 13:13:01 Starting semantics/proofs
Oct 21 13:16:34 Finished semantics/proofs                                      3m33s 940MB
Oct 21 13:16:34 Starting semantics/alt_semantics
Oct 21 13:16:44 Finished semantics/alt_semantics                                  9s 283MB
Oct 21 13:16:44 Starting semantics/alt_semantics/proofs
Oct 21 13:18:59 Finished semantics/alt_semantics/proofs                        2m14s   1GB
Oct 21 13:18:59 Starting basis/pure
Oct 21 13:22:04 Finished basis/pure                                            3m04s 862MB
Oct 21 13:22:04 Starting translator
Oct 21 13:24:51 Finished translator                                            2m46s   1GB
Oct 21 13:24:51 Starting compiler/parsing
Oct 21 13:26:05 Finished compiler/parsing                                      1m13s   3GB
Oct 21 13:26:05 Starting characteristic
Oct 21 13:32:17 Finished characteristic                                        6m11s   1GB
Oct 21 13:32:17 Starting translator/monadic
Oct 21 13:33:56 Finished translator/monadic                                    1m38s   1GB
Oct 21 13:33:56 Starting basis
Oct 21 14:10:14 Finished basis                                                36m17s  12GB
Oct 21 14:10:14 Starting compiler/inference
Oct 21 14:11:26 Finished compiler/inference                                    1m11s 993MB
Oct 21 14:11:26 Starting compiler/backend/reg_alloc
Oct 21 14:12:32 Finished compiler/backend/reg_alloc                            1m05s   1GB
Oct 21 14:12:32 Starting compiler/backend/gc
Oct 21 14:16:14 Finished compiler/backend/gc                                   3m42s   2GB
Oct 21 14:16:14 Starting compiler/backend
Oct 21 14:21:02 Finished compiler/backend                                      4m47s   3GB
Oct 21 14:21:02 Starting compiler/encoders/asm
Oct 21 14:21:25 Finished compiler/encoders/asm                                   22s 765MB
Oct 21 14:21:25 Starting compiler/encoders/x64
Oct 21 14:22:29 Finished compiler/encoders/x64                                 1m04s 745MB
Oct 21 14:22:29 Starting compiler/encoders/arm7
Oct 21 14:24:29 Finished compiler/encoders/arm7                                1m59s   1GB
Oct 21 14:24:29 Starting compiler/encoders/arm8
Oct 21 14:25:07 Finished compiler/encoders/arm8                                  37s 905MB
Oct 21 14:25:07 Starting compiler/encoders/mips
Oct 21 14:26:32 Finished compiler/encoders/mips                                1m24s 919MB
Oct 21 14:26:32 Starting compiler/encoders/riscv
Oct 21 14:28:10 Finished compiler/encoders/riscv                               1m37s   1GB
Oct 21 14:28:10 Starting compiler/encoders/ag32
Oct 21 14:28:28 Finished compiler/encoders/ag32                                  17s 821MB
Oct 21 14:28:28 Starting compiler/backend/x64
Oct 21 14:28:48 Finished compiler/backend/x64                                    19s   1GB
Oct 21 14:28:48 Starting compiler/backend/arm7
Oct 21 14:29:08 Finished compiler/backend/arm7                                   19s   1GB
Oct 21 14:29:08 Starting compiler/backend/arm8
Oct 21 14:29:27 Finished compiler/backend/arm8                                   18s   1GB
Oct 21 14:29:27 Starting compiler/backend/mips
Oct 21 14:29:45 Finished compiler/backend/mips                                   17s 992MB
Oct 21 14:29:45 Starting compiler/backend/riscv
Oct 21 14:30:05 Finished compiler/backend/riscv                                  19s   1GB
Oct 21 14:30:05 Starting compiler/backend/ag32
Oct 21 14:31:18 Finished compiler/backend/ag32                                 1m13s   1GB
Oct 21 14:31:18 Starting compiler/parsing/proofs
Oct 21 14:37:08 Finished compiler/parsing/proofs                               5m50s   1GB
Oct 21 14:37:09 Starting compiler/inference/proofs
Oct 21 14:39:47 Finished compiler/inference/proofs                             2m38s   1GB
Oct 21 14:39:47 Starting compiler/backend/semantics
Oct 21 15:12:12 Finished compiler/backend/semantics                           32m24s   2GB
Oct 21 15:12:12 Starting compiler/backend/reg_alloc/proofs
Oct 21 15:15:59 Finished compiler/backend/reg_alloc/proofs                     3m46s 952MB
Oct 21 15:15:59 Starting compiler/backend/proofs
Oct 21 16:14:12 Finished compiler/backend/proofs                              58m12s  15GB
Oct 21 16:14:12 Starting compiler/encoders/x64/proofs
Oct 21 16:24:30 Finished compiler/encoders/x64/proofs                         10m17s   5GB
Oct 21 16:24:31 Starting compiler/encoders/arm7/proofs
Oct 21 16:38:33 Finished compiler/encoders/arm7/proofs                        14m01s   3GB
Oct 21 16:38:33 Starting compiler/encoders/arm8/proofs
Oct 21 16:45:37 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Oct 21 16:45:37 Starting compiler/encoders/mips/proofs
Oct 21 16:56:31 Finished compiler/encoders/mips/proofs                        10m54s   2GB
Oct 21 16:56:31 Starting compiler/encoders/riscv/proofs
Oct 21 17:06:01 Finished compiler/encoders/riscv/proofs                        9m29s   1GB
Oct 21 17:06:01 Starting compiler/encoders/ag32/proofs
Oct 21 17:08:51 Finished compiler/encoders/ag32/proofs                         2m49s 680MB
Oct 21 17:08:51 Starting compiler/backend/x64/proofs
Oct 21 17:09:11 Finished compiler/backend/x64/proofs                             20s   1GB
Oct 21 17:09:12 Starting compiler/backend/arm7/proofs
Oct 21 17:09:34 Finished compiler/backend/arm7/proofs                            22s   1GB
Oct 21 17:09:35 Starting compiler/backend/arm8/proofs
Oct 21 17:09:54 Finished compiler/backend/arm8/proofs                            19s   1GB
Oct 21 17:09:55 Starting compiler/backend/mips/proofs
Oct 21 17:10:15 Finished compiler/backend/mips/proofs                            20s   1GB
Oct 21 17:10:15 Starting compiler/backend/riscv/proofs
Oct 21 17:10:35 Finished compiler/backend/riscv/proofs                           19s   1GB
Oct 21 17:10:36 Starting compiler/backend/ag32/proofs
Oct 21 17:24:06 Finished compiler/backend/ag32/proofs                         13m29s   3GB
Oct 21 17:24:06 Starting compiler/proofs
Oct 21 17:25:56 Finished compiler/proofs                                       1m49s   3GB
Oct 21 17:25:56 Starting candle/set-theory
Oct 21 17:26:25 Finished candle/set-theory                                       29s 714MB
Oct 21 17:26:26 Starting candle/syntax-lib
Oct 21 17:26:37 Finished candle/syntax-lib                                       10s 607MB
Oct 21 17:26:37 Starting candle/standard/syntax
Oct 21 17:28:31 Finished candle/standard/syntax                                1m54s 956MB
Oct 21 17:28:32 Starting candle/standard/semantics
Oct 21 17:30:19 Finished candle/standard/semantics                             1m47s   1GB
Oct 21 17:30:19 Starting candle/standard/monadic
Oct 21 17:32:06 Finished candle/standard/monadic                               1m47s 983MB
Oct 21 17:32:06 Starting candle/standard/ml_kernel
Oct 21 17:37:57 Finished candle/standard/ml_kernel                             5m50s   3GB
Oct 21 17:37:57 Starting candle/overloading/syntax
Oct 21 17:41:16 Finished candle/overloading/syntax                             3m18s   1GB
Oct 21 17:41:16 Starting candle/overloading/semantics
Oct 21 17:54:06 Finished candle/overloading/semantics                         12m49s   4GB
Oct 21 17:54:06 Starting characteristic/examples
Oct 21 17:55:27 Finished characteristic/examples                               1m20s   3GB
Oct 21 17:55:27 Starting tutorial/solutions
Oct 21 18:10:18 Finished tutorial/solutions                                   14m50s   7GB
Oct 21 18:10:18 Starting translator/monadic/examples
Oct 21 18:13:32 Finished translator/monadic/examples                           3m12s   2GB
Oct 21 18:13:32 Starting examples
Oct 21 18:22:18 Finished examples                                              8m45s   4GB
Oct 21 18:22:18 Starting examples/compilation/x64
Oct 21 20:40:08 Finished examples/compilation/x64                           2h17m49s  15GB
Oct 21 20:40:08 Starting examples/compilation/x64/proofs
Oct 21 20:41:42 Finished examples/compilation/x64/proofs                       1m33s   2GB
Oct 21 20:41:42 Starting examples/compilation/ag32
Oct 21 21:14:18 Finished examples/compilation/ag32                            32m35s   6GB
Oct 21 21:14:18 Starting examples/compilation/ag32/proofs
Oct 21 21:15:04 Finished examples/compilation/ag32/proofs                        46s   3GB
Oct 21 21:15:05 Starting examples/cost
Oct 21 22:13:18 Finished examples/cost                                        58m12s   8GB
Oct 21 22:13:18 Starting examples/lpr_checker
Oct 21 22:17:18 Finished examples/lpr_checker                                  3m59s   2GB
Oct 21 22:17:18 Starting examples/lpr_checker/compilation
Oct 21 22:34:41 Finished examples/lpr_checker/compilation                     17m23s   9GB
Oct 21 22:34:42 Starting examples/lpr_checker/compilation/proofs
Oct 21 22:35:19 Finished examples/lpr_checker/compilation/proofs                 37s   2GB
Oct 21 22:35:19 Starting examples/lpr_checker/array
Oct 21 22:50:39 Finished examples/lpr_checker/array                           15m19s   3GB
Oct 21 22:50:39 Starting examples/lpr_checker/array/compilation
Oct 21 23:10:15 Finished examples/lpr_checker/array/compilation               19m35s  10GB
Oct 21 23:10:15 Starting examples/lpr_checker/array/compilation/proofs
Oct 21 23:11:03 Finished examples/lpr_checker/array/compilation/proofs           48s   3GB
Oct 21 23:11:03 Starting examples/opentheory
Oct 21 23:21:19 Finished examples/opentheory                                  10m15s   4GB
Oct 22 22:03:48 Resuming examples/opentheory
Oct 22 22:03:49 Finished examples/opentheory                                      1s  17MB
Oct 22 22:03:49 Starting examples/opentheory
Oct 22 22:03:51 Finished examples/opentheory                                      1s  20MB
Oct 22 22:03:51 Starting examples/opentheory/compilation
Oct 22 22:37:27 Finished examples/opentheory/compilation                      33m36s  19GB
Oct 22 22:37:28 Starting examples/opentheory/compilation/proofs
Oct 22 22:38:03 Finished examples/opentheory/compilation/proofs                  35s   2GB
Oct 22 22:38:03 Starting examples/opentheory/compilation/ag32
Oct 22 23:13:30 Finished examples/opentheory/compilation/ag32                 35m25s  15GB
Oct 22 23:13:30 Starting examples/opentheory/compilation/ag32/proofs
Oct 22 23:15:04 Finished examples/opentheory/compilation/ag32/proofs           1m33s   5GB
Oct 22 23:15:04 Starting translator/okasaki-examples
Oct 22 23:19:31 Finished translator/okasaki-examples                           4m27s   1GB
Oct 22 23:19:31 Starting translator/other-examples
Oct 22 23:21:39 Finished translator/other-examples                             2m07s   1GB
Oct 22 23:21:39 Starting compiler/parsing/tests
Oct 22 23:22:05 Finished compiler/parsing/tests                                  26s 520MB
Oct 22 23:22:05 Starting compiler/inference/tests
Oct 22 23:26:51 Finished compiler/inference/tests                              4m45s   3GB
Oct 22 23:26:52 Starting compiler/bootstrap/translation
Oct 23 01:51:01 FAILED: compiler/bootstrap/translation
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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$(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/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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[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/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Starting work on monadic_encTheory
Starting work on README.md
Starting work on to_flatProgTheory
README.md                                       real:    0s  user:    0s     OK
monadic_encTheory                               real:   10s  user:    9s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                             real:   14s  user:   14s     OK
monadic_enc64Theory                             real:   15s  user:   14s     OK
to_flatProgTheory                               real:  454s  user:  448s     OK
Starting work on to_closProgTheory
to_closProgTheory                               real:  477s  user:  471s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                real:  415s  user:  407s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                real:  341s  user:  335s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                               real:  183s  user:  180s     OK
Starting work on lexerProgTheory
lexerProgTheory                                 real:  293s  user:  289s     OK
Starting work on parserProgTheory
parserProgTheory                                real:  526s  user:  515s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                             real: 1043s  user: 1033s     OK
Starting work on inferProgTheory
inferProgTheory                                 real: 1103s  user: 1087s     OK
Starting work on explorerProgTheory
explorerProgTheory                              real:  891s  user:  883s     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                           real:  270s  user:  262s     OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word64ProgTheory                             real: 1244s  user: 1221s     OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                             real: 1262s  user: 1238s     OK
Starting work on to_target32ProgTheory
to_target64ProgTheory                           real:  710s  user:  688s     OK
Starting work on x64ProgTheory
to_target32ProgTheory                           real:  706s  user:  685s     OK
Starting work on arm7ProgTheory
x64ProgTheory                                   real:  235s  user:  227s     OK
Starting work on arm8ProgTheory
arm7ProgTheory                                  real:  299s  user:  292s     OK
Starting work on ag32ProgTheory
arm8ProgTheory                                  real:  262s  user:  252s     OK
Starting work on riscvProgTheory
ag32ProgTheory                                  real:  189s  user:  182s     OK
Starting work on compiler32ProgTheory
compiler32ProgTheory                            real:  185s  user:  177sFAIL<1>
 Translating backend_compile
 Adding nsLookup representation thms for [compiler32Prog_env_22]
 Saved theorem _____ "nsLookup_compiler32Prog_env_23_pfun_eqs"
 error in quse /home/cake/oven/regression/cakeml-1378/compiler/bootstrap/translation/compiler32ProgScript.sml : HOL_ERR {message = "Unproved side condition in the translation of backendTheory.compile_def.", origin_function = "failwith", origin_structure = "??"}
 error in load /home/cake/oven/regression/cakeml-1378/compiler/bootstrap/translation/compiler32ProgScript : HOL_ERR {message = "Unproved side condition in the translation of backendTheory.compile_def.", origin_function = "failwith", origin_structure = "??"}
 
 WARNING: backend_compile has a precondition.
 
 Saved theorem _____ "backend_compile_v_thm"
 Uncaught exception: HOL_ERR {message = "Unproved side condition in the translation of backendTheory.compile_def.", origin_function = "failwith", origin_structure = "??"}
riscvProgTheory                                                         M-KILLED