Job 1094

CakeML:140e323f1d3496bc8600be71d69785c6a90515a0
  Merge pull request #703 from CakeML/cfletautolib-fix [Nov 15 13:21:16]
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
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Nov 16 07:15:01 Claimed job
Nov 16 07:15:08 Reusing HOL
Nov 16 07:16:06 Starting developers
Nov 16 07:16:10 Finished developers                                               3s  86MB
Nov 16 07:16:10 Starting developers/bin
Nov 16 07:16:17 Finished developers/bin                                           6s 960MB
Nov 16 07:16:17 Starting semantics/ffi
Nov 16 07:16:27 Finished semantics/ffi                                            9s 196MB
Nov 16 07:16:27 Starting semantics
Nov 16 07:17:45 Finished semantics                                             1m17s   1GB
Nov 16 07:17:45 Starting semantics/proofs
Nov 16 07:20:41 Finished semantics/proofs                                      2m56s   1GB
Nov 16 07:20:42 Starting semantics/alt_semantics
Nov 16 07:20:49 Finished semantics/alt_semantics                                  7s 276MB
Nov 16 07:20:49 Starting semantics/alt_semantics/proofs
Nov 16 07:22:38 Finished semantics/alt_semantics/proofs                        1m49s 710MB
Nov 16 07:22:38 Starting basis/pure
Nov 16 07:23:26 Finished basis/pure                                              46s 683MB
Nov 16 07:23:26 Starting translator
Nov 16 07:25:13 Finished translator                                            1m46s   1GB
Nov 16 07:25:13 Starting compiler/parsing
Nov 16 07:26:18 Finished compiler/parsing                                      1m05s   2GB
Nov 16 07:26:18 Starting characteristic
Nov 16 07:31:35 Finished characteristic                                        5m16s   3GB
Nov 16 07:31:35 Starting translator/monadic
Nov 16 07:33:04 Finished translator/monadic                                    1m28s   1GB
Nov 16 07:33:04 Starting basis
Nov 16 07:52:27 Finished basis                                                19m22s   2GB
Nov 16 07:52:27 Starting compiler/inference
Nov 16 07:54:04 Finished compiler/inference                                    1m37s   1GB
Nov 16 07:54:05 Starting compiler/backend/reg_alloc
Nov 16 07:55:05 Finished compiler/backend/reg_alloc                            1m00s   1GB
Nov 16 07:55:05 Starting compiler/backend/gc
Nov 16 07:58:03 Finished compiler/backend/gc                                   2m57s   2GB
Nov 16 07:58:03 Starting compiler/backend
Nov 16 08:01:46 Finished compiler/backend                                      3m42s   2GB
Nov 16 08:01:46 Starting compiler/encoders/asm
Nov 16 08:02:06 Finished compiler/encoders/asm                                   20s 609MB
Nov 16 08:02:07 Starting compiler/encoders/x64
Nov 16 08:02:30 Finished compiler/encoders/x64                                   23s 947MB
Nov 16 08:02:30 Starting compiler/encoders/arm7
Nov 16 08:03:16 Finished compiler/encoders/arm7                                  46s   1GB
Nov 16 08:03:17 Starting compiler/encoders/arm8
Nov 16 08:03:29 Finished compiler/encoders/arm8                                  11s 635MB
Nov 16 08:03:29 Starting compiler/encoders/mips
Nov 16 08:03:45 Finished compiler/encoders/mips                                  16s   1GB
Nov 16 08:03:46 Starting compiler/encoders/riscv
Nov 16 08:03:59 Finished compiler/encoders/riscv                                 13s 859MB
Nov 16 08:03:59 Starting compiler/encoders/ag32
Nov 16 08:04:16 Finished compiler/encoders/ag32                                  16s 573MB
Nov 16 08:04:17 Starting compiler/backend/x64
Nov 16 08:04:33 Finished compiler/backend/x64                                    15s 897MB
Nov 16 08:04:33 Starting compiler/backend/arm7
Nov 16 08:04:52 Finished compiler/backend/arm7                                   18s   1GB
Nov 16 08:04:52 Starting compiler/backend/arm8
Nov 16 08:05:10 Finished compiler/backend/arm8                                   17s   1GB
Nov 16 08:05:10 Starting compiler/backend/mips
Nov 16 08:05:28 Finished compiler/backend/mips                                   17s   1GB
Nov 16 08:05:28 Starting compiler/backend/riscv
Nov 16 08:05:45 Finished compiler/backend/riscv                                  17s   1GB
Nov 16 08:05:45 Starting compiler/backend/ag32
Nov 16 08:06:51 Finished compiler/backend/ag32                                 1m05s   1GB
Nov 16 08:06:51 Starting compiler/parsing/proofs
Nov 16 08:12:23 Finished compiler/parsing/proofs                               5m31s 880MB
Nov 16 08:12:23 Starting compiler/inference/proofs
Nov 16 08:15:08 Finished compiler/inference/proofs                             2m45s   1GB
Nov 16 08:15:08 Starting compiler/backend/semantics
Nov 16 08:21:01 Finished compiler/backend/semantics                            5m52s   1GB
Nov 16 08:21:01 Starting compiler/backend/reg_alloc/proofs
Nov 16 08:24:17 Finished compiler/backend/reg_alloc/proofs                     3m15s 832MB
Nov 16 08:24:18 Starting compiler/backend/proofs
Nov 16 09:03:55 Finished compiler/backend/proofs                              39m36s   4GB
Nov 16 09:03:55 Starting compiler/encoders/x64/proofs
Nov 16 09:12:53 Finished compiler/encoders/x64/proofs                          8m57s   4GB
Nov 16 09:12:53 Starting compiler/encoders/arm7/proofs
Nov 16 09:24:55 Finished compiler/encoders/arm7/proofs                        12m01s   3GB
Nov 16 09:24:55 Starting compiler/encoders/arm8/proofs
Nov 16 09:31:01 Finished compiler/encoders/arm8/proofs                         6m06s   1GB
Nov 16 09:31:02 Starting compiler/encoders/mips/proofs
Nov 16 09:40:15 Finished compiler/encoders/mips/proofs                         9m12s   2GB
Nov 16 09:40:15 Starting compiler/encoders/riscv/proofs
Nov 16 09:48:32 Finished compiler/encoders/riscv/proofs                        8m17s   1GB
Nov 16 09:48:32 Starting compiler/encoders/ag32/proofs
Nov 16 09:50:57 Finished compiler/encoders/ag32/proofs                         2m24s 625MB
Nov 16 09:50:57 Starting compiler/backend/x64/proofs
Nov 16 09:51:14 Finished compiler/backend/x64/proofs                             16s 806MB
Nov 16 09:51:14 Starting compiler/backend/arm7/proofs
Nov 16 09:51:33 Finished compiler/backend/arm7/proofs                            18s   1GB
Nov 16 09:51:33 Starting compiler/backend/arm8/proofs
Nov 16 09:51:49 Finished compiler/backend/arm8/proofs                            16s 839MB
Nov 16 09:51:50 Starting compiler/backend/mips/proofs
Nov 16 09:52:07 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 16 09:52:07 Starting compiler/backend/riscv/proofs
Nov 16 09:52:25 Finished compiler/backend/riscv/proofs                           17s   1GB
Nov 16 09:52:26 Starting compiler/backend/ag32/proofs
Nov 16 10:01:14 Finished compiler/backend/ag32/proofs                          8m48s   2GB
Nov 16 10:01:14 Starting compiler/proofs
Nov 16 10:02:45 Finished compiler/proofs                                       1m30s   3GB
Nov 16 10:02:45 Starting candle/set-theory
Nov 16 10:03:13 Finished candle/set-theory                                       27s 764MB
Nov 16 10:03:13 Starting candle/syntax-lib
Nov 16 10:03:23 Finished candle/syntax-lib                                        9s 612MB
Nov 16 10:03:23 Starting candle/standard/syntax
Nov 16 10:05:05 Finished candle/standard/syntax                                1m41s   1GB
Nov 16 10:05:05 Starting candle/standard/semantics
Nov 16 10:06:43 Finished candle/standard/semantics                             1m37s   1GB
Nov 16 10:06:43 Starting candle/standard/monadic
Nov 16 10:08:17 Finished candle/standard/monadic                               1m33s   1GB
Nov 16 10:08:17 Starting candle/standard/ml_kernel
Nov 16 10:12:08 Finished candle/standard/ml_kernel                             3m51s   3GB
Nov 16 10:12:08 Starting candle/standard/opentheory
Nov 16 10:20:40 Finished candle/standard/opentheory                            8m30s   4GB
Nov 16 10:20:40 Starting candle/standard/opentheory/compilation
Nov 16 10:49:30 Finished candle/standard/opentheory/compilation               28m49s  23GB
Nov 16 10:49:30 Starting candle/standard/opentheory/compilation/proofs
Nov 16 10:50:14 Finished candle/standard/opentheory/compilation/proofs           44s   2GB
Nov 16 10:50:14 Starting characteristic/examples
Nov 16 10:51:39 Finished characteristic/examples                               1m24s   2GB
Nov 16 10:51:39 Starting tutorial/solutions
Nov 16 11:04:37 Finished tutorial/solutions                                   12m57s   6GB
Nov 16 11:04:37 Starting translator/monadic/examples
Nov 16 11:07:34 Finished translator/monadic/examples                           2m56s   2GB
Nov 16 11:07:34 Starting examples
Nov 16 11:16:28 Finished examples                                              8m53s   5GB
Nov 16 11:16:28 Starting examples/compilation/x64
Nov 16 13:18:58 Finished examples/compilation/x64                           2h02m29s  14GB
Nov 16 13:18:58 Starting examples/compilation/x64/proofs
Nov 16 13:20:44 Finished examples/compilation/x64/proofs                       1m45s   2GB
Nov 16 13:20:44 Starting examples/compilation/ag32
Nov 16 13:49:00 Finished examples/compilation/ag32                            28m15s   6GB
Nov 16 13:49:00 Starting examples/compilation/ag32/proofs
Nov 16 13:50:00 Finished examples/compilation/ag32/proofs                        59s   2GB
Nov 16 13:50:00 Starting translator/okasaki-examples
Nov 16 13:54:03 Finished translator/okasaki-examples                           4m02s   2GB
Nov 16 13:54:03 Starting translator/other-examples
Nov 16 13:54:42 Finished translator/other-examples                               38s   1GB
Nov 16 13:54:42 Starting compiler/parsing/tests
Nov 16 13:55:07 Finished compiler/parsing/tests                                  24s 542MB
Nov 16 13:55:07 Starting compiler/inference/tests
Nov 16 13:59:21 Finished compiler/inference/tests                              4m13s   6GB
Nov 16 13:59:21 Starting compiler/bootstrap/translation
Nov 16 16:31:53 Finished compiler/bootstrap/translation                     2h32m31s  40GB
Nov 16 16:31:53 Starting unverified/sexpr-bootstrap/x64/64
Nov 16 16:45:26 Finished unverified/sexpr-bootstrap/x64/64                    13m31s   3GB
Nov 16 16:45:26 Starting unverified/sexpr-bootstrap/x64/32
Nov 16 16:54:49 Finished unverified/sexpr-bootstrap/x64/32                     9m22s   6GB
Nov 16 16:54:50 Starting compiler/benchmarks
Nov 16 16:54:52 Finished compiler/benchmarks                                      2s  26MB
Nov 16 16:54:52 Starting compiler/bootstrap/compilation/x64/64
Nov 17 05:18:58 Finished compiler/bootstrap/compilation/x64/64             12h24m04s  64GB
Nov 17 05:18:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 17 05:22:23 Finished compiler/bootstrap/compilation/x64/64/proofs          3m24s   5GB
Nov 17 05:22:23 Starting compiler/bootstrap/compilation/x64/32
Nov 17 16:27:37 Finished compiler/bootstrap/compilation/x64/32             11h05m12s  64GB
Nov 17 16:27:37 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 17 16:31:25 Finished compiler/bootstrap/compilation/x64/32/proofs          3m48s   5GB
Nov 17 16:31:26 Starting compiler/bootstrap/compilation/ag32/32
Nov 18 04:54:39 Finished compiler/bootstrap/compilation/ag32/32            12h23m13s  64GB
Nov 18 04:54:40 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 18 05:27:48 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: 1985s  user: 1964sFAIL<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"}