Job 785

CakeML:987a0367d297d926d763919e92ffc28c1a4992aa
  Merge branch 'master' into vstte18 [Apr 10 12:49:56]
#629 (vstte18)
Merging into:dd8ca4fca024b5b629a7c3ed7d3d4b1844c82f3d
  Merge pull request #628 from CakeML/ThmSetData-API-change [Apr 10 21:53:38]
HOL:729baf5e526741114f4346767d17d0da3a1b6c20
  Remove (generated file) Thm-sig.sml when cleaning src/thm [Apr 07 04:31:14]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 10 22:02:00 Claimed job
Apr 10 22:02:04 Reusing HOL
Apr 10 22:02:09 Starting developers
Apr 10 22:02:10 Finished developers                                               0s  22MB
Apr 10 22:02:10 Starting developers/bin
Apr 10 22:02:45 Finished developers/bin                                          34s 142MB
Apr 10 22:02:45 Starting semantics/ffi
Apr 10 22:02:54 Finished semantics/ffi                                            7s 228MB
Apr 10 22:02:54 Starting semantics
Apr 10 22:04:11 Finished semantics                                             1m17s   1GB
Apr 10 22:04:12 Starting semantics/proofs
Apr 10 22:07:07 Finished semantics/proofs                                      2m54s   1GB
Apr 10 22:07:08 Starting basis/pure
Apr 10 22:07:52 Finished basis/pure                                              43s 639MB
Apr 10 22:07:52 Starting translator
Apr 10 22:09:28 Finished translator                                            1m34s   1GB
Apr 10 22:09:28 Starting compiler/parsing
Apr 10 22:10:24 Finished compiler/parsing                                        56s   2GB
Apr 10 22:10:25 Starting characteristic
Apr 10 22:15:27 Finished characteristic                                        5m01s   2GB
Apr 10 22:15:27 Starting translator/monadic
Apr 10 22:16:49 Finished translator/monadic                                    1m22s   1GB
Apr 10 22:16:50 Starting basis
Apr 10 22:33:34 Finished basis                                                16m43s   2GB
Apr 10 22:33:34 Starting compiler/inference
Apr 10 22:35:03 Finished compiler/inference                                    1m28s   1GB
Apr 10 22:35:03 Starting compiler/backend/reg_alloc
Apr 10 22:35:52 Finished compiler/backend/reg_alloc                              49s   1GB
Apr 10 22:35:53 Starting compiler/backend/gc
Apr 10 22:43:41 Finished compiler/backend/gc                                   7m48s   2GB
Apr 10 22:43:42 Starting compiler/backend
Apr 10 22:43:43 Finished compiler/backend                                         0s  42MB
Apr 10 22:43:43 Starting compiler/encoders/asm
Apr 10 22:43:44 Finished compiler/encoders/asm                                    0s  32MB
Apr 10 22:43:44 Starting compiler/encoders/x64
Apr 10 22:44:07 Finished compiler/encoders/x64                                   22s 913MB
Apr 10 22:44:07 Starting compiler/encoders/arm6
Apr 10 22:44:51 Finished compiler/encoders/arm6                                  43s 906MB
Apr 10 22:44:52 Starting compiler/encoders/arm8
Apr 10 22:45:03 Finished compiler/encoders/arm8                                  10s 609MB
Apr 10 22:45:03 Starting compiler/encoders/mips
Apr 10 22:45:20 Finished compiler/encoders/mips                                  15s 921MB
Apr 10 22:45:20 Starting compiler/encoders/riscv
Apr 10 22:45:33 Finished compiler/encoders/riscv                                 12s 707MB
Apr 10 22:45:34 Starting compiler/encoders/ag32
Apr 10 22:45:49 Finished compiler/encoders/ag32                                  14s 673MB
Apr 10 22:45:49 Starting compiler/backend/x64
Apr 10 22:46:05 Finished compiler/backend/x64                                    15s   1GB
Apr 10 22:46:05 Starting compiler/backend/arm6
Apr 10 22:46:22 Finished compiler/backend/arm6                                   16s   1GB
Apr 10 22:46:22 Starting compiler/backend/arm8
Apr 10 22:46:39 Finished compiler/backend/arm8                                   16s 978MB
Apr 10 22:46:39 Starting compiler/backend/mips
Apr 10 22:46:55 Finished compiler/backend/mips                                   15s   1GB
Apr 10 22:46:55 Starting compiler/backend/riscv
Apr 10 22:47:11 Finished compiler/backend/riscv                                  15s   1GB
Apr 10 22:47:12 Starting compiler/backend/ag32
Apr 10 22:48:17 Finished compiler/backend/ag32                                 1m05s   1GB
Apr 10 22:48:17 Starting compiler/parsing/proofs
Apr 10 22:53:43 Finished compiler/parsing/proofs                               5m25s 946MB
Apr 10 22:53:43 Starting compiler/inference/proofs
Apr 10 22:56:20 Finished compiler/inference/proofs                             2m35s   1GB
Apr 10 22:56:20 Starting compiler/backend/semantics
Apr 10 23:03:13 Finished compiler/backend/semantics                            6m52s   2GB
Apr 10 23:03:14 Starting compiler/backend/reg_alloc/proofs
Apr 10 23:05:49 Finished compiler/backend/reg_alloc/proofs                     2m34s   1GB
Apr 10 23:05:49 Starting compiler/backend/proofs
Apr 10 23:43:12 Finished compiler/backend/proofs                              37m22s   4GB
Apr 10 23:43:13 Starting compiler/encoders/x64/proofs
Apr 10 23:52:15 Finished compiler/encoders/x64/proofs                          9m02s   4GB
Apr 10 23:52:16 Starting compiler/encoders/arm6/proofs
Apr 11 00:04:36 Finished compiler/encoders/arm6/proofs                        12m19s   3GB
Apr 11 00:04:37 Starting compiler/encoders/arm8/proofs
Apr 11 00:10:11 Finished compiler/encoders/arm8/proofs                         5m34s 963MB
Apr 11 00:10:11 Starting compiler/encoders/mips/proofs
Apr 11 00:19:28 Finished compiler/encoders/mips/proofs                         9m16s   2GB
Apr 11 00:19:28 Starting compiler/encoders/riscv/proofs
Apr 11 00:27:43 Finished compiler/encoders/riscv/proofs                        8m14s   1GB
Apr 11 00:27:44 Starting compiler/encoders/ag32/proofs
Apr 11 00:30:11 Finished compiler/encoders/ag32/proofs                         2m26s 686MB
Apr 11 00:30:11 Starting compiler/backend/x64/proofs
Apr 11 00:30:28 Finished compiler/backend/x64/proofs                             16s   1GB
Apr 11 00:30:28 Starting compiler/backend/arm6/proofs
Apr 11 00:30:47 Finished compiler/backend/arm6/proofs                            18s   1GB
Apr 11 00:30:47 Starting compiler/backend/arm8/proofs
Apr 11 00:31:03 Finished compiler/backend/arm8/proofs                            15s   1GB
Apr 11 00:31:03 Starting compiler/backend/mips/proofs
Apr 11 00:31:20 Finished compiler/backend/mips/proofs                            16s   1GB
Apr 11 00:31:20 Starting compiler/backend/riscv/proofs
Apr 11 00:31:37 Finished compiler/backend/riscv/proofs                           16s   1GB
Apr 11 00:31:38 Starting compiler/backend/ag32/proofs
Apr 11 00:37:08 FAILED: compiler/backend/ag32/proofs
]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-785/basis]0;Holmake: ~/regression/cakeml-785/basis/pure]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/balanced_bst]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-785/basis/pure]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-785/basis/pure]0;Holmake: ~/regression/cakeml-785/misc]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-785/misc]0;Holmake: ~/regression/cakeml-785/developers]0;Holmake: ~/regression/cakeml-785/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-785/misc]0;Holmake: ~/regression/cakeml-785/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-785/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-785/misc]0;Holmake: ~/regression/cakeml-785/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-785/basis/pure]0;Holmake: ~/regression/cakeml-785/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-785/basis]0;Holmake: ~/regression/cakeml-785/characteristic]0;Holmake: ~/regression/cakeml-785/compiler/parsing]0;Holmake: ~/regression/cakeml-785/semantics]0;Holmake: ~/regression/cakeml-785/semantics/ffi]0;Holmake: ~/regression/cakeml-785/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-785/semantics]0;Holmake: ~/regression/cakeml-785/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-785/compiler/parsing]0;Holmake: ~/regression/cakeml-785/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-785/characteristic]0;Holmake: ~/regression/cakeml-785/semantics/proofs]0;Holmake: ~/regression/cakeml-785/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-785/characteristic]0;Holmake: ~/regression/cakeml-785/translator]0;Holmake: ~/regression/cakeml-785/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-785/characteristic]0;Holmake: ~/regression/cakeml-785/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-785/basis]0;Holmake: ~/regression/cakeml-785/translator/monadic]0;Holmake: ~/regression/cakeml-785/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-785/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-785/translator/monadic]0;Holmake: ~/regression/cakeml-785/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-785/basis]0;Holmake: ~/regression/cakeml-785/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../..]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../..]0;Holmake: ../../reg_alloc]0;Holmake: ~/regression/cakeml-785/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-785/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../../reg_alloc]0;Holmake: ../../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../..]0;Holmake: ../../../encoders/asm]0;Holmake: ../../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ..]0;Holmake: ../../../encoders/ag32]0;Holmake: ../../../encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: .]0;Holmake: ../../proofs]0;Holmake: ../../gc]0;Holmake: ../../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: ../../proofs]0;Holmake: ../../reg_alloc/proofs]0;Holmake: ../../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: ../../proofs]0;Holmake: ../../semantics]0;Holmake: ../../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: ../../proofs]0;Holmake: ../../proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
]0;Holmake: .]0;Holmake: ../../../encoders/ag32/proofs]0;Holmake: ../../../encoders/ag32/proofs[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32/proofs[0m
Starting work on ag32_progTheory
Starting work on ag32_configProofTheory
Starting work on README.md
README.md                                                                                                  OK
ag32_configProofTheory                                                                                     OK
Starting work on ag32_machine_configTheory
ag32_progTheory                                                                                            OK
Starting work on ag32_ffi_codeProofTheory
ag32_machine_configTheory                                                                                  OK
Starting work on ag32_memoryProofTheory
ag32_ffi_codeProofTheory                                                                                   OK
ag32_memoryProofTheory                                                                                     OK
Starting work on ag32_basis_ffiProofTheory
ag32_basis_ffiProofTheory                                                                         FAILED! <1>
 
 which has type
 
 : -> ( # string) list
 
 unification failure message: Attempt to unify different type operators: mlstring$mlstring and list$list
 
 error in quse /home/myreen/regression/cakeml-785/compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml : HOL_ERR {message = "in compiler-generated text:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(f :(mlstring # mlstring) list -> (mlstring # mlstring) list) (x :IO_fs).\n    x with files updated_by f\n\non line 722, characters 7-14\n\nwhich has type\n\n:((mlstring # mlstring) list -> (mlstring # mlstring) list) -> IO_fs -> IO_fs\n\nto\n\n(K\n   [((IOStream :mlstring -> \206\177) (strlit \"stdout\"),(\"\" :string ));\n    (IOStream (strlit \"stderr\"),(\"\" :string ));\n    (IOStream (strlit \"stdin\"),(inp :string))] :\206\178 -> (\206\177 # string) list)\n\nin compiler-generated text\n\nwhich has type\n\n:\206\178 -> (\206\177 # string) list\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load ag32_basis_ffiProofScript : HOL_ERR {message = "in compiler-generated text:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(f :(mlstring # mlstring) list -> (mlstring # mlstring) list) (x :IO_fs).\n    x with files updated_by f\n\non line 722, characters 7-14\n\nwhich has type\n\n:((mlstring # mlstring) list -> (mlstring # mlstring) list) -> IO_fs -> IO_fs\n\nto\n\n(K\n   [((IOStream :mlstring -> \206\177) (strlit \"stdout\"),(\"\" :string ));\n    (IOStream (strlit \"stderr\"),(\"\" :string ));\n    (IOStream (strlit \"stdin\"),(inp :string))] :\206\178 -> (\206\177 # string) list)\n\nin compiler-generated text\n\nwhich has type\n\n:\206\178 -> (\206\177 # string) list\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "in compiler-generated text:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(f :(mlstring # mlstring) list -> (mlstring # mlstring) list) (x :IO_fs).\n    x with files updated_by f\n\non line 722, characters 7-14\n\nwhich has type\n\n:((mlstring # mlstring) list -> (mlstring # mlstring) list) -> IO_fs -> IO_fs\n\nto\n\n(K\n   [((IOStream :mlstring -> \206\177) (strlit \"stdout\"),(\"\" :string ));\n    (IOStream (strlit \"stderr\"),(\"\" :string ));\n    (IOStream (strlit \"stdin\"),(inp :string))] :\206\178 -> (\206\177 # string) list)\n\nin compiler-generated text\n\nwhich has type\n\n:\206\178 -> (\206\177 # string) list\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}