Job 1262

CakeML:a4e49ad3305bd6af11dc757d1e39747841e97179
  Fix a few calls to compile_x64 [Jun 09 19:36:08]
#738 (export_update)
Merging into:30d1750b37e638af75fbb1f0a438859aef1fee04
  Fix a broken script [Jun 08 17:54:39]
HOL:ac7497223d5845f2709250fa8fdcb566cbc2e1ae
  emacs-mode: make regexp searching case-sensitive; SOME not a q'fier [Jun 03 04:25:22]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 09 19:36:21 Claimed job
Jun 09 19:36:23 Reusing HOL
Jun 09 19:36:28 Starting developers
Jun 09 19:36:31 Finished developers                                               2s  87MB
Jun 09 19:36:31 Starting developers/bin
Jun 09 19:36:38 Finished developers/bin                                           6s   1GB
Jun 09 19:36:38 Starting semantics/ffi
Jun 09 19:36:47 Finished semantics/ffi                                            9s 260MB
Jun 09 19:36:47 Starting semantics
Jun 09 19:38:08 Finished semantics                                             1m20s   1GB
Jun 09 19:38:08 Starting semantics/proofs
Jun 09 19:41:22 Finished semantics/proofs                                      3m13s 882MB
Jun 09 19:41:23 Starting semantics/alt_semantics
Jun 09 19:41:30 Finished semantics/alt_semantics                                  7s 313MB
Jun 09 19:41:31 Starting semantics/alt_semantics/proofs
Jun 09 19:43:34 Finished semantics/alt_semantics/proofs                        2m02s 854MB
Jun 09 19:43:34 Starting basis/pure
Jun 09 19:44:22 Finished basis/pure                                              48s   1GB
Jun 09 19:44:22 Starting translator
Jun 09 19:46:58 Finished translator                                            2m35s   1GB
Jun 09 19:46:58 Starting compiler/parsing
Jun 09 19:48:05 Finished compiler/parsing                                      1m06s   2GB
Jun 09 19:48:05 Starting characteristic
Jun 09 19:53:50 Finished characteristic                                        5m44s   1GB
Jun 09 19:53:50 Starting translator/monadic
Jun 09 19:55:25 Finished translator/monadic                                    1m34s   1GB
Jun 09 19:55:25 Starting basis
Jun 09 20:26:26 Finished basis                                                31m00s  21GB
Jun 09 20:26:26 Starting compiler/inference
Jun 09 20:27:26 Finished compiler/inference                                      59s 908MB
Jun 09 20:27:26 Starting compiler/backend/reg_alloc
Jun 09 20:28:29 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jun 09 20:28:29 Starting compiler/backend/gc
Jun 09 20:31:42 Finished compiler/backend/gc                                   3m12s   1GB
Jun 09 20:31:42 Starting compiler/backend
Jun 09 20:36:10 Finished compiler/backend                                      4m28s   3GB
Jun 09 20:36:10 Starting compiler/encoders/asm
Jun 09 20:36:31 Finished compiler/encoders/asm                                   20s 682MB
Jun 09 20:36:31 Starting compiler/encoders/x64
Jun 09 20:36:55 Finished compiler/encoders/x64                                   23s 826MB
Jun 09 20:36:55 Starting compiler/encoders/arm7
Jun 09 20:37:43 Finished compiler/encoders/arm7                                  47s 701MB
Jun 09 20:37:43 Starting compiler/encoders/arm8
Jun 09 20:37:56 Finished compiler/encoders/arm8                                  12s 933MB
Jun 09 20:37:56 Starting compiler/encoders/mips
Jun 09 20:38:13 Finished compiler/encoders/mips                                  17s 924MB
Jun 09 20:38:13 Starting compiler/encoders/riscv
Jun 09 20:38:29 Finished compiler/encoders/riscv                                 15s 953MB
Jun 09 20:38:29 Starting compiler/encoders/ag32
Jun 09 20:38:46 Finished compiler/encoders/ag32                                  17s 815MB
Jun 09 20:38:47 Starting compiler/backend/x64
Jun 09 20:39:03 Finished compiler/backend/x64                                    16s   1GB
Jun 09 20:39:03 Starting compiler/backend/arm7
Jun 09 20:39:23 Finished compiler/backend/arm7                                   19s   1GB
Jun 09 20:39:23 Starting compiler/backend/arm8
Jun 09 20:39:40 Finished compiler/backend/arm8                                   17s 962MB
Jun 09 20:39:40 Starting compiler/backend/mips
Jun 09 20:39:59 Finished compiler/backend/mips                                   18s   1GB
Jun 09 20:39:59 Starting compiler/backend/riscv
Jun 09 20:40:17 Finished compiler/backend/riscv                                  18s   1GB
Jun 09 20:40:17 Starting compiler/backend/ag32
Jun 09 20:41:24 Finished compiler/backend/ag32                                 1m06s   1GB
Jun 09 20:41:24 Starting compiler/parsing/proofs
Jun 09 20:47:05 Finished compiler/parsing/proofs                               5m40s   1GB
Jun 09 20:47:05 Starting compiler/inference/proofs
Jun 09 20:49:26 Finished compiler/inference/proofs                             2m20s   1GB
Jun 09 20:49:26 Starting compiler/backend/semantics
Jun 09 21:17:01 Finished compiler/backend/semantics                           27m34s   2GB
Jun 09 21:17:01 Starting compiler/backend/reg_alloc/proofs
Jun 09 21:20:23 Finished compiler/backend/reg_alloc/proofs                     3m21s 836MB
Jun 09 21:20:23 Starting compiler/backend/proofs
Jun 09 22:13:21 Finished compiler/backend/proofs                              52m57s  15GB
Jun 09 22:13:21 Starting compiler/encoders/x64/proofs
Jun 09 22:22:34 Finished compiler/encoders/x64/proofs                          9m13s   5GB
Jun 09 22:22:35 Starting compiler/encoders/arm7/proofs
Jun 09 22:34:51 Finished compiler/encoders/arm7/proofs                        12m16s   3GB
Jun 09 22:34:51 Starting compiler/encoders/arm8/proofs
Jun 09 22:41:05 Finished compiler/encoders/arm8/proofs                         6m14s   1GB
Jun 09 22:41:06 Starting compiler/encoders/mips/proofs
Jun 09 22:50:40 Finished compiler/encoders/mips/proofs                         9m33s   3GB
Jun 09 22:50:40 Starting compiler/encoders/riscv/proofs
Jun 09 22:59:08 Finished compiler/encoders/riscv/proofs                        8m27s 977MB
Jun 09 22:59:08 Starting compiler/encoders/ag32/proofs
Jun 09 23:01:36 Finished compiler/encoders/ag32/proofs                         2m27s 794MB
Jun 09 23:01:36 Starting compiler/backend/x64/proofs
Jun 09 23:01:55 Finished compiler/backend/x64/proofs                             19s   1GB
Jun 09 23:01:56 Starting compiler/backend/arm7/proofs
Jun 09 23:02:17 Finished compiler/backend/arm7/proofs                            21s   1GB
Jun 09 23:02:17 Starting compiler/backend/arm8/proofs
Jun 09 23:02:37 Finished compiler/backend/arm8/proofs                            19s   1GB
Jun 09 23:02:37 Starting compiler/backend/mips/proofs
Jun 09 23:02:57 Finished compiler/backend/mips/proofs                            19s   1GB
Jun 09 23:02:57 Starting compiler/backend/riscv/proofs
Jun 09 23:03:17 Finished compiler/backend/riscv/proofs                           20s   1GB
Jun 09 23:03:17 Starting compiler/backend/ag32/proofs
Jun 09 23:16:03 Finished compiler/backend/ag32/proofs                         12m45s   1GB
Jun 09 23:16:03 Starting compiler/proofs
Jun 09 23:17:31 Finished compiler/proofs                                       1m27s   2GB
Jun 09 23:17:31 Starting candle/set-theory
Jun 09 23:17:58 Finished candle/set-theory                                       26s 859MB
Jun 09 23:17:59 Starting candle/syntax-lib
Jun 09 23:18:09 Finished candle/syntax-lib                                       10s 688MB
Jun 09 23:18:09 Starting candle/standard/syntax
Jun 09 23:19:55 Finished candle/standard/syntax                                1m46s   1GB
Jun 09 23:19:56 Starting candle/standard/semantics
Jun 09 23:21:36 Finished candle/standard/semantics                             1m40s   1GB
Jun 09 23:21:36 Starting candle/standard/monadic
Jun 09 23:23:13 Finished candle/standard/monadic                               1m36s   1GB
Jun 09 23:23:13 Starting candle/standard/ml_kernel
Jun 09 23:28:25 Finished candle/standard/ml_kernel                             5m11s   3GB
Jun 09 23:28:25 Starting candle/standard/opentheory
Jun 09 23:37:18 Finished candle/standard/opentheory                            8m52s   4GB
Jun 09 23:37:18 Starting candle/standard/opentheory/compilation
Jun 10 00:08:53 Finished candle/standard/opentheory/compilation               31m34s  17GB
Jun 10 00:08:53 Starting candle/standard/opentheory/compilation/proofs
Jun 10 00:09:28 Finished candle/standard/opentheory/compilation/proofs           35s   3GB
Jun 10 00:09:29 Starting candle/overloading/syntax
Jun 10 00:12:31 Finished candle/overloading/syntax                             3m01s   1GB
Jun 10 00:12:31 Starting candle/overloading/semantics
Jun 10 00:19:28 Finished candle/overloading/semantics                          6m55s   2GB
Jun 10 00:19:28 Starting characteristic/examples
Jun 10 00:20:41 Finished characteristic/examples                               1m12s   2GB
Jun 10 00:20:41 Starting tutorial/solutions
Jun 10 00:34:43 Finished tutorial/solutions                                   14m01s   8GB
Jun 10 00:34:43 Starting translator/monadic/examples
Jun 10 00:37:51 Finished translator/monadic/examples                           3m07s   2GB
Jun 10 00:37:51 Starting examples
Jun 10 00:46:03 Finished examples                                              8m12s   3GB
Jun 10 00:46:03 Starting examples/compilation/x64
Jun 10 03:00:29 Finished examples/compilation/x64                           2h14m25s  14GB
Jun 10 03:00:29 Starting examples/compilation/x64/proofs
Jun 10 03:02:04 Finished examples/compilation/x64/proofs                       1m34s   2GB
Jun 10 03:02:04 Starting examples/compilation/ag32
Jun 10 03:32:39 Finished examples/compilation/ag32                            30m34s   6GB
Jun 10 03:32:39 Starting examples/compilation/ag32/proofs
Jun 10 03:33:19 Finished examples/compilation/ag32/proofs                        40s   2GB
Jun 10 03:33:19 Starting examples/cost
Jun 10 04:19:10 Finished examples/cost                                        45m50s   7GB
Jun 10 04:19:10 Starting examples/lpr_checker
Jun 10 04:22:50 Finished examples/lpr_checker                                  3m40s   2GB
Jun 10 04:22:51 Starting examples/lpr_checker/compilation
Jun 10 04:40:09 Finished examples/lpr_checker/compilation                     17m17s   9GB
Jun 10 04:40:09 Starting examples/lpr_checker/compilation/proofs
Jun 10 04:40:46 Finished examples/lpr_checker/compilation/proofs                 37s   3GB
Jun 10 04:40:46 Starting examples/lpr_checker/array
Jun 10 04:50:26 Finished examples/lpr_checker/array                            9m39s   2GB
Jun 10 04:50:26 Starting examples/lpr_checker/array/compilation
Jun 10 05:08:17 Finished examples/lpr_checker/array/compilation               17m50s   9GB
Jun 10 05:08:17 Starting examples/lpr_checker/array/compilation/proofs
Jun 10 05:09:04 Finished examples/lpr_checker/array/compilation/proofs           47s   4GB
Jun 10 05:09:05 Starting translator/okasaki-examples
Jun 10 05:13:18 Finished translator/okasaki-examples                           4m13s   1GB
Jun 10 05:13:18 Starting translator/other-examples
Jun 10 05:15:11 Finished translator/other-examples                             1m52s   1GB
Jun 10 05:15:11 Starting compiler/parsing/tests
Jun 10 05:15:35 Finished compiler/parsing/tests                                  24s 619MB
Jun 10 05:15:35 Starting compiler/inference/tests
Jun 10 05:20:06 Finished compiler/inference/tests                              4m29s   4GB
Jun 10 05:20:06 Starting compiler/bootstrap/translation
Jun 10 07:26:22 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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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:    9s  user:    9s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory                                                                                                                                 real:   14s  user:   13s     OK
monadic_enc32Theory                                                                                                                                 real:   14s  user:   14s     OK
to_flatProgTheory                                                                                                                                   real:  396s  user:  391s     OK
Starting work on to_closProgTheory
to_closProgTheory                                                                                                                                   real:  399s  user:  394s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                                                                                                    real:  367s  user:  360s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                                                                                                    real:  313s  user:  307s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                                                                   real:  166s  user:  163s     OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                                                                     real:  250s  user:  247s     OK
Starting work on parserProgTheory
parserProgTheory                                                                                                                                    real:  488s  user:  479s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                                                                                                 real:  917s  user:  906s     OK
Starting work on inferProgTheory
inferProgTheory                                                                                                                                     real:  985s  user:  974s     OK
Starting work on explorerProgTheory
explorerProgTheory                                                                                                                                  real:  718s  user:  714s     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                                                                                               real:  251s  user:  245s     OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word64ProgTheory                                                                                                                                 real: 1009s  user:  993s     OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                                                                                                                                 real: 1021s  user: 1003s     OK
Starting work on to_target32ProgTheory
to_target64ProgTheory                                                                                                                               real:  647s  user:  630s     OK
Starting work on x64ProgTheory
to_target32ProgTheory                                                                                                                               real:  650s  user:  632s     OK
Starting work on arm7ProgTheory
x64ProgTheory                                                                                                                                       real:  262s  user:  253s     OK
Starting work on arm8ProgTheory
arm7ProgTheory                                                                                                                                      real:  272s  user:  267s     OK
Starting work on ag32ProgTheory
ag32ProgTheory                                                                                                                                      real:  190s  user:  183s     OK
Starting work on compiler32ProgTheory
arm8ProgTheory                                                                                                                                      real:  252s  user:  245s     OK
Starting work on riscvProgTheory
compiler32ProgTheory                                                                                                                                real:  183s  user:  176sFAIL<1>
 Saved theorem _____ "export_split16_v_thm"
 Translating export_preamble
 Saved theorem _____ "export_preamble_refs_def"
 Saved theorem _____ "nsLookup_compiler32Prog_env_25_pfun_eqs"
 Saved theorem _____ "export_preamble_v_thm"
 /home/myreen/regression/cakeml-1262/compiler/bootstrap/translation/compiler32ProgScript.sml:97: error: Value or constructor (space_line_def) has not been declared
 Found near translate space_line_def
 error in quse /home/myreen/regression/cakeml-1262/compiler/bootstrap/translation/compiler32ProgScript.sml : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1262/compiler/bootstrap/translation/compiler32ProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
riscvProgTheory                                                                                                                                                             M-KILLED