Overview

Job 806

CakeML:399b058e56b33256cbf0ee55326d01009bccbe21
  Fix ag32_basis_ffi
#629 (vstte18)
Merging into:0e4fa06ab0d36c1241d6932a06a3ca93303d0c19
  Remove compute-attribute-losing save_thm in Candle's monadic kernel
HOL:057a3046e41b50db616e5d385e9b63e940b4957e
  Deal with bad rebindings of theorems under src/
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               2s  20MB
 Starting developers/bin
 Finished developers/bin                                        1m12s 918MB
 Starting semantics/ffi
 Finished semantics/ffi                                            9s 230MB
 Starting semantics
 Finished semantics                                             1m21s 987MB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m55s   1GB
 Starting basis/pure
 Finished basis/pure                                              47s 811MB
 Starting translator
 Finished translator                                            1m40s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                        56s   1GB
 Starting characteristic
 Finished characteristic                                        5m12s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m29s   1GB
 Starting basis
 Finished basis                                                16m41s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m31s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              53s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   7m58s   1GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  28MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  17MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   24s 726MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                  45s 655MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  13s 813MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  17s 843MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 14s 859MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  17s 774MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    16s 806MB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   20s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   17s 990MB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   18s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  19s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m07s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m28s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m39s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            6m51s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     2m40s 803MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              36m58s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          8m53s   4GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        12m06s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         5m21s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                         9m10s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m14s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m23s 874MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             20s 829MB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            22s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            18s 809MB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            19s 900MB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           20s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          8m46s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m25s   3GB
 Starting candle/set-theory
 Finished candle/set-theory                                       27s 675MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       11s 576MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m45s   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                             3m55s   3GB
 Starting candle/standard/opentheory
 FAILED: candle/standard/opentheory
]0;Holmake: ~/oven/regression/cakeml-806/basis/pure]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-806/basis/pure]0;Holmake: ~/oven/regression/cakeml-806/misc]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-806/misc]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-806/misc]0;Holmake: ~/oven/regression/cakeml-806/developers]0;Holmake: ~/oven/regression/cakeml-806/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-806/misc]0;Holmake: ~/oven/regression/cakeml-806/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-806/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-806/misc]0;Holmake: ~/oven/regression/cakeml-806/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-806/basis/pure]0;Holmake: ~/oven/regression/cakeml-806/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-806/basis]0;Holmake: ~/oven/regression/cakeml-806/characteristic]0;Holmake: ~/oven/regression/cakeml-806/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-806/semantics]0;Holmake: ~/oven/regression/cakeml-806/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-806/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-806/semantics]0;Holmake: ~/oven/regression/cakeml-806/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-806/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-806/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-806/characteristic]0;Holmake: ~/oven/regression/cakeml-806/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-806/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-806/characteristic]0;Holmake: ~/oven/regression/cakeml-806/translator]0;Holmake: ~/oven/regression/cakeml-806/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-806/characteristic]0;Holmake: ~/oven/regression/cakeml-806/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-806/basis]0;Holmake: ~/oven/regression/cakeml-806/translator/monadic]0;Holmake: ~/oven/regression/cakeml-806/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-806/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-806/translator/monadic]0;Holmake: ~/oven/regression/cakeml-806/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-806/basis]0;Holmake: ~/oven/regression/cakeml-806/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ../ml_kernel]0;Holmake: ../monadic]0;Holmake: ../syntax]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-libWorking in $(CAKEMLDIR)/candle/syntax-lib
]0;Holmake: ../syntax]0;Holmake: ../syntaxWorking in $(CAKEMLDIR)/candle/standard/syntax
]0;Holmake: ../monadic]0;Holmake: ../monadicWorking in $(CAKEMLDIR)/candle/standard/monadic
]0;Holmake: ../ml_kernel]0;Holmake: ../ml_kernelWorking in $(CAKEMLDIR)/candle/standard/ml_kernel
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../../set-theory]0;Holmake: ../../set-theoryWorking in $(CAKEMLDIR)/candle/set-theory
]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/candle/standard/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/candle/standard/opentheory
Starting work on prettyTheory
Starting work on README.md
README.md                                                                    OK
prettyTheory                                                                 OK
Starting work on readerTheory
readerTheory                                                                 OK
Starting work on reader_initTheory
reader_initTheory                                                            OK
Starting work on readerProofTheory
readerProofTheory                                                   FAILED! <1>
 
 which has type
 
 :inode
 
 unification failure message: Attempt to unify different type operators: mlstring$mlstring and fsFFI$inode
 
 error in quse /home/cake/oven/regression/cakeml-806/candle/standard/opentheory/readerProofScript.sml : HOL_ERR {message = "on line 1728, characters 36-58:\n\nType inference failure: unable to infer a type for the application of\n\nall_lines (fs :IO_fs)\n\non line 1728, characters 22-59\n\nwhich has type\n\n:mlstring -> mlstring list\n\nto\n\nUStream (strlit \"stdin\")\n\non line 1728, characters 36-58\n\nwhich has type\n\n:inode\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and fsFFI$inode\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load readerProofScript : HOL_ERR {message = "on line 1728, characters 36-58:\n\nType inference failure: unable to infer a type for the application of\n\nall_lines (fs :IO_fs)\n\non line 1728, characters 22-59\n\nwhich has type\n\n:mlstring -> mlstring list\n\nto\n\nUStream (strlit \"stdin\")\n\non line 1728, characters 36-58\n\nwhich has type\n\n:inode\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and fsFFI$inode\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 1728, characters 36-58:\n\nType inference failure: unable to infer a type for the application of\n\nall_lines (fs :IO_fs)\n\non line 1728, characters 22-59\n\nwhich has type\n\n:mlstring -> mlstring list\n\nto\n\nUStream (strlit \"stdin\")\n\non line 1728, characters 36-58\n\nwhich has type\n\n:inode\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and fsFFI$inode\n", origin_function = "type-analysis", origin_structure = "Preterm"}