Job 1089

CakeML:2680f32a69334bea368d0928d98b6f1fccd1f15d
  Fix translation of parserProg given new validAddSym constant [Nov 12 05:58:45]
#695 (ocaml-infixes)
Merging into:dee8a5c2ef96f2f6ba0c0a583d7d6a655470840d
  Merge pull request #704 from CakeML/sexpr-bootstrap-fix [Nov 14 07:43:57]
HOL:ca71e46c32fd6a11162c9640ee7006dfe1c6fabd
  Remove unnecessary CLINE_OPTIONS in tests that break Moscow ML build [Nov 13 22:33:35]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 14 07:45:16 Claimed job
Nov 14 07:45:30 Building HOL
Nov 14 07:56:13 Starting developers
Nov 14 07:56:17 Finished developers                                               3s  81MB
Nov 14 07:56:17 Starting developers/bin
Nov 14 07:56:24 Finished developers/bin                                           6s 960MB
Nov 14 07:56:24 Starting semantics/ffi
Nov 14 07:56:34 Finished semantics/ffi                                            9s 230MB
Nov 14 07:56:34 Starting semantics
Nov 14 07:58:00 Finished semantics                                             1m25s   1GB
Nov 14 07:58:00 Starting semantics/proofs
Nov 14 08:01:00 Finished semantics/proofs                                      2m59s   1GB
Nov 14 08:01:00 Starting semantics/alt_semantics
Nov 14 08:01:08 Finished semantics/alt_semantics                                  7s 316MB
Nov 14 08:01:08 Starting semantics/alt_semantics/proofs
Nov 14 08:02:57 Finished semantics/alt_semantics/proofs                        1m48s 694MB
Nov 14 08:02:57 Starting basis/pure
Nov 14 08:05:44 Finished basis/pure                                            2m46s 804MB
Nov 14 08:05:44 Starting translator
Nov 14 08:07:32 Finished translator                                            1m47s   1GB
Nov 14 08:07:32 Starting compiler/parsing
Nov 14 08:08:38 Finished compiler/parsing                                      1m05s   2GB
Nov 14 08:08:38 Starting characteristic
Nov 14 08:13:52 Finished characteristic                                        5m14s   1GB
Nov 14 08:13:53 Starting translator/monadic
Nov 14 08:15:19 Finished translator/monadic                                    1m26s   1GB
Nov 14 08:15:20 Starting basis
Nov 14 08:34:48 Finished basis                                                19m28s   2GB
Nov 14 08:34:48 Starting compiler/inference
Nov 14 08:36:33 Finished compiler/inference                                    1m44s   1GB
Nov 14 08:36:34 Starting compiler/backend/reg_alloc
Nov 14 08:37:33 Finished compiler/backend/reg_alloc                              59s   1GB
Nov 14 08:37:33 Starting compiler/backend/gc
Nov 14 08:40:44 Finished compiler/backend/gc                                   3m11s   2GB
Nov 14 08:40:44 Starting compiler/backend
Nov 14 08:44:26 Finished compiler/backend                                      3m41s   2GB
Nov 14 08:44:26 Starting compiler/encoders/asm
Nov 14 08:44:46 Finished compiler/encoders/asm                                   19s 808MB
Nov 14 08:44:46 Starting compiler/encoders/x64
Nov 14 08:45:40 Finished compiler/encoders/x64                                   53s 594MB
Nov 14 08:45:40 Starting compiler/encoders/arm7
Nov 14 08:47:20 Finished compiler/encoders/arm7                                1m39s   1GB
Nov 14 08:47:20 Starting compiler/encoders/arm8
Nov 14 08:47:52 Finished compiler/encoders/arm8                                  31s 882MB
Nov 14 08:47:52 Starting compiler/encoders/mips
Nov 14 08:48:59 Finished compiler/encoders/mips                                1m06s 962MB
Nov 14 08:48:59 Starting compiler/encoders/riscv
Nov 14 08:50:19 Finished compiler/encoders/riscv                               1m19s 792MB
Nov 14 08:50:19 Starting compiler/encoders/ag32
Nov 14 08:50:36 Finished compiler/encoders/ag32                                  16s 561MB
Nov 14 08:50:36 Starting compiler/backend/x64
Nov 14 08:50:53 Finished compiler/backend/x64                                    17s   1GB
Nov 14 08:50:54 Starting compiler/backend/arm7
Nov 14 08:51:12 Finished compiler/backend/arm7                                   18s   1GB
Nov 14 08:51:12 Starting compiler/backend/arm8
Nov 14 08:51:29 Finished compiler/backend/arm8                                   16s   1GB
Nov 14 08:51:29 Starting compiler/backend/mips
Nov 14 08:51:47 Finished compiler/backend/mips                                   17s   1GB
Nov 14 08:51:47 Starting compiler/backend/riscv
Nov 14 08:52:05 Finished compiler/backend/riscv                                  17s   1GB
Nov 14 08:52:05 Starting compiler/backend/ag32
Nov 14 08:53:10 Finished compiler/backend/ag32                                 1m04s   1GB
Nov 14 08:53:10 Starting compiler/parsing/proofs
Nov 14 08:58:42 Finished compiler/parsing/proofs                               5m31s   1GB
Nov 14 08:58:42 Starting compiler/inference/proofs
Nov 14 09:01:26 Finished compiler/inference/proofs                             2m43s   1GB
Nov 14 09:01:26 Starting compiler/backend/semantics
Nov 14 09:07:21 Finished compiler/backend/semantics                            5m54s   2GB
Nov 14 09:07:21 Starting compiler/backend/reg_alloc/proofs
Nov 14 09:10:34 Finished compiler/backend/reg_alloc/proofs                     3m13s   1GB
Nov 14 09:10:35 Starting compiler/backend/proofs
Nov 14 09:50:47 Finished compiler/backend/proofs                              40m11s   4GB
Nov 14 09:50:47 Starting compiler/encoders/x64/proofs
Nov 14 09:59:47 Finished compiler/encoders/x64/proofs                          8m59s   4GB
Nov 14 09:59:47 Starting compiler/encoders/arm7/proofs
Nov 14 10:12:00 Finished compiler/encoders/arm7/proofs                        12m12s   3GB
Nov 14 10:12:00 Starting compiler/encoders/arm8/proofs
Nov 14 10:18:08 Finished compiler/encoders/arm8/proofs                         6m07s   1GB
Nov 14 10:18:08 Starting compiler/encoders/mips/proofs
Nov 14 10:27:26 Finished compiler/encoders/mips/proofs                         9m18s   2GB
Nov 14 10:27:26 Starting compiler/encoders/riscv/proofs
Nov 14 10:35:40 Finished compiler/encoders/riscv/proofs                        8m13s   1GB
Nov 14 10:35:40 Starting compiler/encoders/ag32/proofs
Nov 14 10:38:00 Finished compiler/encoders/ag32/proofs                         2m20s 998MB
Nov 14 10:38:01 Starting compiler/backend/x64/proofs
Nov 14 10:38:18 Finished compiler/backend/x64/proofs                             16s 795MB
Nov 14 10:38:18 Starting compiler/backend/arm7/proofs
Nov 14 10:38:37 Finished compiler/backend/arm7/proofs                            18s 811MB
Nov 14 10:38:37 Starting compiler/backend/arm8/proofs
Nov 14 10:38:54 Finished compiler/backend/arm8/proofs                            16s 760MB
Nov 14 10:38:54 Starting compiler/backend/mips/proofs
Nov 14 10:39:13 Finished compiler/backend/mips/proofs                            19s 864MB
Nov 14 10:39:13 Starting compiler/backend/riscv/proofs
Nov 14 10:39:32 Finished compiler/backend/riscv/proofs                           18s   1GB
Nov 14 10:39:32 Starting compiler/backend/ag32/proofs
Nov 14 10:48:25 Finished compiler/backend/ag32/proofs                          8m52s   2GB
Nov 14 10:48:25 Starting compiler/proofs
Nov 14 10:50:04 Finished compiler/proofs                                       1m38s   3GB
Nov 14 10:50:04 Starting candle/set-theory
Nov 14 10:50:30 Finished candle/set-theory                                       26s 763MB
Nov 14 10:50:31 Starting candle/syntax-lib
Nov 14 10:50:41 Finished candle/syntax-lib                                        9s 635MB
Nov 14 10:50:41 Starting candle/standard/syntax
Nov 14 10:52:24 Finished candle/standard/syntax                                1m43s 889MB
Nov 14 10:52:24 Starting candle/standard/semantics
Nov 14 10:54:02 Finished candle/standard/semantics                             1m37s   1GB
Nov 14 10:54:02 Starting candle/standard/monadic
Nov 14 10:55:36 Finished candle/standard/monadic                               1m33s   1GB
Nov 14 10:55:36 Starting candle/standard/ml_kernel
Nov 14 10:59:22 Finished candle/standard/ml_kernel                             3m45s   3GB
Nov 14 10:59:22 Starting candle/standard/opentheory
Nov 14 11:07:52 Finished candle/standard/opentheory                            8m30s   4GB
Nov 14 11:07:52 Starting candle/standard/opentheory/compilation
Nov 14 11:36:49 Finished candle/standard/opentheory/compilation               28m56s  22GB
Nov 14 11:36:50 Starting candle/standard/opentheory/compilation/proofs
Nov 14 11:37:43 Finished candle/standard/opentheory/compilation/proofs           53s   2GB
Nov 14 11:37:43 Starting characteristic/examples
Nov 14 11:39:11 Finished characteristic/examples                               1m27s   2GB
Nov 14 11:39:11 Starting tutorial/solutions
Nov 14 11:52:27 Finished tutorial/solutions                                   13m15s   7GB
Nov 14 11:52:27 Starting translator/monadic/examples
Nov 14 11:55:21 Finished translator/monadic/examples                           2m53s   2GB
Nov 14 11:55:21 Starting examples
Nov 14 12:04:24 Finished examples                                              9m03s   4GB
Nov 14 12:04:24 Starting examples/compilation/x64
Nov 14 14:07:21 Finished examples/compilation/x64                           2h02m56s  21GB
Nov 14 14:07:21 Starting examples/compilation/x64/proofs
Nov 14 14:09:21 Finished examples/compilation/x64/proofs                       1m59s   2GB
Nov 14 14:09:21 Starting examples/compilation/ag32
Nov 14 14:37:34 Finished examples/compilation/ag32                            28m12s   6GB
Nov 14 14:37:34 Starting examples/compilation/ag32/proofs
Nov 14 14:38:15 Finished examples/compilation/ag32/proofs                        40s   3GB
Nov 14 14:38:15 Starting translator/okasaki-examples
Nov 14 14:42:19 Finished translator/okasaki-examples                           4m03s   1GB
Nov 14 14:42:19 Starting translator/other-examples
Nov 14 14:44:10 Finished translator/other-examples                             1m50s   1GB
Nov 14 14:44:10 Starting compiler/parsing/tests
Nov 14 14:44:34 Finished compiler/parsing/tests                                  24s 518MB
Nov 14 14:44:34 Starting compiler/inference/tests
Nov 14 14:48:48 Finished compiler/inference/tests                              4m14s   3GB
Nov 14 14:48:49 Starting compiler/bootstrap/translation
Nov 14 17:18:41 Finished compiler/bootstrap/translation                     2h29m51s  40GB
Nov 14 17:18:41 Starting unverified/sexpr-bootstrap/x64/64
Nov 14 17:31:25 Finished unverified/sexpr-bootstrap/x64/64                    12m43s   3GB
Nov 14 17:31:25 Starting unverified/sexpr-bootstrap/x64/32
Nov 14 17:40:52 Finished unverified/sexpr-bootstrap/x64/32                     9m27s   5GB
Nov 14 17:40:52 Starting compiler/benchmarks
Nov 14 17:40:54 Finished compiler/benchmarks                                      1s  38MB
Nov 14 17:40:55 Starting compiler/bootstrap/compilation/x64/64
Nov 15 06:02:44 Finished compiler/bootstrap/compilation/x64/64             12h21m49s  64GB
Nov 15 06:02:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 15 06:07:05 Finished compiler/bootstrap/compilation/x64/64/proofs          4m20s   6GB
Nov 15 06:07:05 Starting compiler/bootstrap/compilation/x64/32
Nov 15 17:47:57 Finished compiler/bootstrap/compilation/x64/32             11h40m50s  64GB
Nov 15 17:47:57 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 15 17:51:09 Finished compiler/bootstrap/compilation/x64/32/proofs          3m12s   4GB
Nov 15 17:51:10 Starting compiler/bootstrap/compilation/ag32/32
Nov 16 06:40:46 Finished compiler/bootstrap/compilation/ag32/32            12h49m35s  64GB
Nov 16 06:40:46 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 16 07:01:12 FAILED: compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/unification/triangular
Scanning $(HOLDIR)/examples/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Starting work on README.md
Starting work on ag32BootstrapProofTheory
README.md                                       real:    0s  user:    0s     OK
ag32BootstrapProofTheory                        real: 1223s  user: 1203sFAIL<1>
      out = explode current_build_info_str  err = ""
    else
      (let
         (cout,cerr) = compile_32 (TL cl) inp
       in
         out = explode (concat (append cout))  err = explode cerr))
 
 failed.
 Failed to prove theorem cake_extract_writes.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 319) (THEN1 on line 323) (THEN1 on line 327) (THEN1 on line 298) (THEN1 on line 337) (THEN1 on line 395) (THEN1 on line 412) (THEN1 on line 424)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}