Job 806

CakeML:399b058e56b33256cbf0ee55326d01009bccbe21
  Fix ag32_basis_ffi [Apr 15 18:44:38]
#629 (vstte18)
Merging into:0e4fa06ab0d36c1241d6932a06a3ca93303d0c19
  Remove compute-attribute-losing save_thm in Candle's monadic kernel [Apr 19 07:40:16]
HOL:057a3046e41b50db616e5d385e9b63e940b4957e
  Deal with bad rebindings of theorems under src/ [Apr 15 07:09:08]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 19 10:45:02 Claimed job
Apr 19 10:45:07 Reusing HOL
Apr 19 10:45:54 Starting developers
Apr 19 10:45:57 Finished developers                                               2s  20MB
Apr 19 10:45:57 Starting developers/bin
Apr 19 10:47:09 Finished developers/bin                                        1m12s 918MB
Apr 19 10:47:10 Starting semantics/ffi
Apr 19 10:47:20 Finished semantics/ffi                                            9s 230MB
Apr 19 10:47:20 Starting semantics
Apr 19 10:48:41 Finished semantics                                             1m21s 987MB
Apr 19 10:48:41 Starting semantics/proofs
Apr 19 10:51:37 Finished semantics/proofs                                      2m55s   1GB
Apr 19 10:51:37 Starting basis/pure
Apr 19 10:52:25 Finished basis/pure                                              47s 811MB
Apr 19 10:52:25 Starting translator
Apr 19 10:54:05 Finished translator                                            1m40s   1GB
Apr 19 10:54:06 Starting compiler/parsing
Apr 19 10:55:03 Finished compiler/parsing                                        56s   1GB
Apr 19 10:55:03 Starting characteristic
Apr 19 11:00:16 Finished characteristic                                        5m12s   1GB
Apr 19 11:00:16 Starting translator/monadic
Apr 19 11:01:46 Finished translator/monadic                                    1m29s   1GB
Apr 19 11:01:46 Starting basis
Apr 19 11:18:28 Finished basis                                                16m41s   3GB
Apr 19 11:18:28 Starting compiler/inference
Apr 19 11:20:00 Finished compiler/inference                                    1m31s   1GB
Apr 19 11:20:00 Starting compiler/backend/reg_alloc
Apr 19 11:20:54 Finished compiler/backend/reg_alloc                              53s   1GB
Apr 19 11:20:54 Starting compiler/backend/gc
Apr 19 11:28:53 Finished compiler/backend/gc                                   7m58s   1GB
Apr 19 11:28:54 Starting compiler/backend
Apr 19 11:28:57 Finished compiler/backend                                         2s  28MB
Apr 19 11:28:57 Starting compiler/encoders/asm
Apr 19 11:28:58 Finished compiler/encoders/asm                                    1s  17MB
Apr 19 11:28:58 Starting compiler/encoders/x64
Apr 19 11:29:23 Finished compiler/encoders/x64                                   24s 726MB
Apr 19 11:29:23 Starting compiler/encoders/arm6
Apr 19 11:30:09 Finished compiler/encoders/arm6                                  45s 655MB
Apr 19 11:30:10 Starting compiler/encoders/arm8
Apr 19 11:30:23 Finished compiler/encoders/arm8                                  13s 813MB
Apr 19 11:30:24 Starting compiler/encoders/mips
Apr 19 11:30:41 Finished compiler/encoders/mips                                  17s 843MB
Apr 19 11:30:41 Starting compiler/encoders/riscv
Apr 19 11:30:56 Finished compiler/encoders/riscv                                 14s 859MB
Apr 19 11:30:56 Starting compiler/encoders/ag32
Apr 19 11:31:14 Finished compiler/encoders/ag32                                  17s 774MB
Apr 19 11:31:14 Starting compiler/backend/x64
Apr 19 11:31:31 Finished compiler/backend/x64                                    16s 806MB
Apr 19 11:31:31 Starting compiler/backend/arm6
Apr 19 11:31:52 Finished compiler/backend/arm6                                   20s   1GB
Apr 19 11:31:52 Starting compiler/backend/arm8
Apr 19 11:32:10 Finished compiler/backend/arm8                                   17s 990MB
Apr 19 11:32:10 Starting compiler/backend/mips
Apr 19 11:32:29 Finished compiler/backend/mips                                   18s   1GB
Apr 19 11:32:30 Starting compiler/backend/riscv
Apr 19 11:32:49 Finished compiler/backend/riscv                                  19s   1GB
Apr 19 11:32:49 Starting compiler/backend/ag32
Apr 19 11:33:57 Finished compiler/backend/ag32                                 1m07s   1GB
Apr 19 11:33:57 Starting compiler/parsing/proofs
Apr 19 11:39:26 Finished compiler/parsing/proofs                               5m28s   1GB
Apr 19 11:39:26 Starting compiler/inference/proofs
Apr 19 11:42:06 Finished compiler/inference/proofs                             2m39s   1GB
Apr 19 11:42:06 Starting compiler/backend/semantics
Apr 19 11:48:58 Finished compiler/backend/semantics                            6m51s   2GB
Apr 19 11:48:58 Starting compiler/backend/reg_alloc/proofs
Apr 19 11:51:39 Finished compiler/backend/reg_alloc/proofs                     2m40s 803MB
Apr 19 11:51:39 Starting compiler/backend/proofs
Apr 19 12:28:38 Finished compiler/backend/proofs                              36m58s   3GB
Apr 19 12:28:38 Starting compiler/encoders/x64/proofs
Apr 19 12:37:32 Finished compiler/encoders/x64/proofs                          8m53s   4GB
Apr 19 12:37:33 Starting compiler/encoders/arm6/proofs
Apr 19 12:49:39 Finished compiler/encoders/arm6/proofs                        12m06s   3GB
Apr 19 12:49:40 Starting compiler/encoders/arm8/proofs
Apr 19 12:55:02 Finished compiler/encoders/arm8/proofs                         5m21s   1GB
Apr 19 12:55:02 Starting compiler/encoders/mips/proofs
Apr 19 13:04:12 Finished compiler/encoders/mips/proofs                         9m10s   2GB
Apr 19 13:04:12 Starting compiler/encoders/riscv/proofs
Apr 19 13:12:27 Finished compiler/encoders/riscv/proofs                        8m14s   1GB
Apr 19 13:12:27 Starting compiler/encoders/ag32/proofs
Apr 19 13:14:51 Finished compiler/encoders/ag32/proofs                         2m23s 874MB
Apr 19 13:14:51 Starting compiler/backend/x64/proofs
Apr 19 13:15:13 Finished compiler/backend/x64/proofs                             20s 829MB
Apr 19 13:15:13 Starting compiler/backend/arm6/proofs
Apr 19 13:15:35 Finished compiler/backend/arm6/proofs                            22s   1GB
Apr 19 13:15:36 Starting compiler/backend/arm8/proofs
Apr 19 13:15:55 Finished compiler/backend/arm8/proofs                            18s 809MB
Apr 19 13:15:55 Starting compiler/backend/mips/proofs
Apr 19 13:16:15 Finished compiler/backend/mips/proofs                            19s 900MB
Apr 19 13:16:16 Starting compiler/backend/riscv/proofs
Apr 19 13:16:36 Finished compiler/backend/riscv/proofs                           20s   1GB
Apr 19 13:16:37 Starting compiler/backend/ag32/proofs
Apr 19 13:25:23 Finished compiler/backend/ag32/proofs                          8m46s   2GB
Apr 19 13:25:23 Starting compiler/proofs
Apr 19 13:26:49 Finished compiler/proofs                                       1m25s   3GB
Apr 19 13:26:49 Starting candle/set-theory
Apr 19 13:27:16 Finished candle/set-theory                                       27s 675MB
Apr 19 13:27:17 Starting candle/syntax-lib
Apr 19 13:27:28 Finished candle/syntax-lib                                       11s 576MB
Apr 19 13:27:28 Starting candle/standard/syntax
Apr 19 13:29:14 Finished candle/standard/syntax                                1m45s   1GB
Apr 19 13:29:14 Starting candle/standard/semantics
Apr 19 13:30:52 Finished candle/standard/semantics                             1m37s   1GB
Apr 19 13:30:52 Starting candle/standard/monadic
Apr 19 13:32:26 Finished candle/standard/monadic                               1m33s   1GB
Apr 19 13:32:26 Starting candle/standard/ml_kernel
Apr 19 13:36:22 Finished candle/standard/ml_kernel                             3m55s   3GB
Apr 19 13:36:22 Starting candle/standard/opentheory
Apr 19 13:38:58 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"}