Overview

Job 1094

CakeML:140e323f1d3496bc8600be71d69785c6a90515a0
  Merge pull request #703 from CakeML/cfletautolib-fix
HOL:ca71e46c32fd6a11162c9640ee7006dfe1c6fabd
  Remove unnecessary CLINE_OPTIONS in tests that break Moscow ML build
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

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               3s  86MB
 Starting developers/bin
 Finished developers/bin                                           6s 960MB
 Starting semantics/ffi
 Finished semantics/ffi                                            9s 196MB
 Starting semantics
 Finished semantics                                             1m17s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m56s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  7s 276MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        1m49s 710MB
 Starting basis/pure
 Finished basis/pure                                              46s 683MB
 Starting translator
 Finished translator                                            1m46s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m05s   2GB
 Starting characteristic
 Finished characteristic                                        5m16s   3GB
 Starting translator/monadic
 Finished translator/monadic                                    1m28s   1GB
 Starting basis
 Finished basis                                                19m22s   2GB
 Starting compiler/inference
 Finished compiler/inference                                    1m37s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m00s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   2m57s   2GB
 Starting compiler/backend
 Finished compiler/backend                                      3m42s   2GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   20s 609MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   23s 947MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                  46s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  11s 635MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  16s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 13s 859MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  16s 573MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    15s 897MB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   17s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   17s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  17s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m05s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m31s 880MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m45s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            5m52s   1GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m15s 832MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              39m36s   4GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          8m57s   4GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        12m01s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m06s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                         9m12s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m17s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m24s 625MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             16s 806MB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            18s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            16s 839MB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            17s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           17s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          8m48s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m30s   3GB
 Starting candle/set-theory
 Finished candle/set-theory                                       27s 764MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                        9s 612MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m41s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m37s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m33s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             3m51s   3GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            8m30s   4GB
 Starting candle/standard/opentheory/compilation
 Finished candle/standard/opentheory/compilation               28m49s  23GB
 Starting candle/standard/opentheory/compilation/proofs
 Finished candle/standard/opentheory/compilation/proofs           44s   2GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m24s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   12m57s   6GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           2m56s   2GB
 Starting examples
 Finished examples                                              8m53s   5GB
 Starting examples/compilation/x64
 Finished examples/compilation/x64                           2h02m29s  14GB
 Starting examples/compilation/x64/proofs
 Finished examples/compilation/x64/proofs                       1m45s   2GB
 Starting examples/compilation/ag32
 Finished examples/compilation/ag32                            28m15s   6GB
 Starting examples/compilation/ag32/proofs
 Finished examples/compilation/ag32/proofs                        59s   2GB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                           4m02s   2GB
 Starting translator/other-examples
 Finished translator/other-examples                               38s   1GB
 Starting compiler/parsing/tests
 Finished compiler/parsing/tests                                  24s 542MB
 Starting compiler/inference/tests
 Finished compiler/inference/tests                              4m13s   6GB
 Starting compiler/bootstrap/translation
 Finished compiler/bootstrap/translation                     2h32m31s  40GB
 Starting unverified/sexpr-bootstrap/x64/64
 Finished unverified/sexpr-bootstrap/x64/64                    13m31s   3GB
 Starting unverified/sexpr-bootstrap/x64/32
 Finished unverified/sexpr-bootstrap/x64/32                     9m22s   6GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      2s  26MB
 Starting compiler/bootstrap/compilation/x64/64
 Finished compiler/bootstrap/compilation/x64/64             12h24m04s  64GB
 Starting compiler/bootstrap/compilation/x64/64/proofs
 Finished compiler/bootstrap/compilation/x64/64/proofs          3m24s   5GB
 Starting compiler/bootstrap/compilation/x64/32
 Finished compiler/bootstrap/compilation/x64/32             11h05m12s  64GB
 Starting compiler/bootstrap/compilation/x64/32/proofs
 Finished compiler/bootstrap/compilation/x64/32/proofs          3m48s   5GB
 Starting compiler/bootstrap/compilation/ag32/32
 Finished compiler/bootstrap/compilation/ag32/32            12h23m13s  64GB
 Starting compiler/bootstrap/compilation/ag32/32/proofs
 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"}