Job 886

CakeML:4f331e690829ce68efcc59ba19bd90b8852623e1
  Fix stray old theorem syntax in compiler backend [May 20 07:25:56]
#635 (thm)
Merging into:c3cbbfd27bd9e1f2836f8f307279178dc76ac571
  Merge pull request #650 from CakeML/tweak-how-to [May 17 12:31:32]
HOL:f6c660ddb3151f18cd07b606f2439087858abe20
  Further polish Definition documentation (incl. schematic attribute) [May 16 14:38:46]
Machine:brain12 4.14.89.1.amd64-smp x86_64 GNU/Linux

May 20 10:26:21 Claimed job
May 20 10:26:25 Reusing HOL
May 20 10:27:20 Starting developers
May 20 10:27:23 Finished developers                                               2s  30MB
May 20 10:27:23 Starting developers/bin
May 20 10:27:33 Finished developers/bin                                           9s 936MB
May 20 10:27:33 Starting semantics/ffi
May 20 10:27:52 Finished semantics/ffi                                           18s 245MB
May 20 10:27:52 Starting semantics
May 20 10:30:22 Finished semantics                                             2m29s   1GB
May 20 10:30:22 Starting semantics/proofs
May 20 10:36:04 Finished semantics/proofs                                      5m41s   1GB
May 20 10:36:04 Starting basis/pure
May 20 10:37:36 Finished basis/pure                                            1m31s 706MB
May 20 10:37:36 Starting translator
May 20 10:40:45 Finished translator                                            3m08s   1GB
May 20 10:40:45 Starting compiler/parsing
May 20 10:42:32 Finished compiler/parsing                                      1m46s   2GB
May 20 10:42:32 Starting characteristic
May 20 10:52:47 Finished characteristic                                       10m14s   2GB
May 20 10:52:47 Starting translator/monadic
May 20 10:55:50 Finished translator/monadic                                    3m02s   1GB
May 20 10:55:50 Starting basis
May 20 11:27:37 Finished basis                                                31m46s   2GB
May 20 11:27:37 Starting compiler/inference
May 20 11:31:12 Finished compiler/inference                                    3m34s   1GB
May 20 11:31:12 Starting compiler/backend/reg_alloc
May 20 11:32:53 Finished compiler/backend/reg_alloc                            1m40s   1GB
May 20 11:32:54 Starting compiler/backend/gc
May 20 11:49:27 Finished compiler/backend/gc                                  16m33s   2GB
May 20 11:49:27 Starting compiler/backend
May 20 11:49:37 Finished compiler/backend                                         9s 305MB
May 20 11:49:37 Starting compiler/encoders/asm
May 20 11:49:38 Finished compiler/encoders/asm                                    1s  27MB
May 20 11:49:39 Starting compiler/encoders/x64
May 20 11:51:37 Finished compiler/encoders/x64                                 1m58s 964MB
May 20 11:51:37 Starting compiler/encoders/arm6
May 20 11:54:56 Finished compiler/encoders/arm6                                3m18s   1GB
May 20 11:54:56 Starting compiler/encoders/arm8
May 20 11:55:57 Finished compiler/encoders/arm8                                1m00s 902MB
May 20 11:55:57 Starting compiler/encoders/mips
May 20 11:58:14 Finished compiler/encoders/mips                                2m16s 936MB
May 20 11:58:14 Starting compiler/encoders/riscv
May 20 12:00:47 Finished compiler/encoders/riscv                               2m33s   1GB
May 20 12:00:48 Starting compiler/encoders/ag32
May 20 12:01:20 Finished compiler/encoders/ag32                                  32s 788MB
May 20 12:01:20 Starting compiler/backend/x64
May 20 12:01:59 Finished compiler/backend/x64                                    38s   1GB
May 20 12:02:00 Starting compiler/backend/arm6
May 20 12:02:43 Finished compiler/backend/arm6                                   42s   1GB
May 20 12:02:43 Starting compiler/backend/arm8
May 20 12:03:24 Finished compiler/backend/arm8                                   41s   1GB
May 20 12:03:25 Starting compiler/backend/mips
May 20 12:04:07 Finished compiler/backend/mips                                   42s   1GB
May 20 12:04:07 Starting compiler/backend/riscv
May 20 12:04:46 Finished compiler/backend/riscv                                  38s 825MB
May 20 12:04:47 Starting compiler/backend/ag32
May 20 12:07:00 Finished compiler/backend/ag32                                 2m12s   1GB
May 20 12:07:00 Starting compiler/parsing/proofs
May 20 12:17:51 Finished compiler/parsing/proofs                              10m50s 924MB
May 20 12:17:51 Starting compiler/inference/proofs
May 20 12:23:14 FAILED: compiler/inference/proofs
]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/unification/triangular/first-order]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: ..]0;Holmake: /local/hbecker/regression/cakeml-886/basis/pure]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/balanced_bst]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: /local/hbecker/regression/cakeml-886/basis/pure]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/context-free]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
Starting work on regexp2dfa
regexp2dfa                                                                                                                       OK
]0;Holmake: /local/hbecker/regression/cakeml-886/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-886/misc]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: /local/hbecker/regression/cakeml-886/misc]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple]0;Holmake: /local/hbecker/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: /local/hbecker/regression/cakeml-886/misc]0;Holmake: /local/hbecker/regression/cakeml-886/developers]0;Holmake: /local/hbecker/regression/cakeml-886/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: /local/hbecker/regression/cakeml-886/misc]0;Holmake: /local/hbecker/regression/cakeml-886/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/cakeml-886/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: /local/hbecker/regression/cakeml-886/misc]0;Holmake: /local/hbecker/regression/cakeml-886/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: /local/hbecker/regression/cakeml-886/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-886/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: /local/hbecker/regression/cakeml-886/semantics]0;Holmake: /local/hbecker/regression/cakeml-886/semantics/ffi]0;Holmake: /local/hbecker/regression/cakeml-886/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: /local/hbecker/regression/cakeml-886/semantics]0;Holmake: /local/hbecker/regression/cakeml-886/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ..]0;Holmake: /local/hbecker/regression/cakeml-886/semantics/proofs]0;Holmake: /local/hbecker/regression/cakeml-886/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/inference
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/inference/proofs
Starting work on inferPropsTheory
Starting work on README.md
README.md                                                                                                                        OK
inferPropsTheory                                                                                                                 OK
Starting work on envRelTheory
Starting work on type_dCanonTheory
envRelTheory                                                                                                                     OK
Starting work on infer_eCompleteTheory
Starting work on infer_eSoundTheory
type_dCanonTheory                                                                                                                OK
infer_eSoundTheory                                                                                                               OK
infer_eCompleteTheory                                                                                                            OK
Starting work on type_eDetermTheory
type_eDetermTheory                                                                                                               OK
Starting work on inferCompleteTheory
Starting work on inferSoundTheory
inferSoundTheory                                                                                                                 OK
inferCompleteTheory                                                                                                     FAILED! <1>
   Theorem infer_ds_complete
   [
      QUOTE
      " (*#loc 1372 4*)type_ds T tenv ds ids tenv' \226\136\167\n   env_rel tenv ienv \226\136\167\n   (* do you need both of these? *)\n   inf_set_tids_ienv (count st1.next_id) ienv \226\136\167\n   set_tids_tenv (count st1.next_id) tenv \226\136\167\n   DISJOINT ids (count st1.next_id) \226\136\167\n   start_type_id \226\137\164 st1.next_id\n   \226\135\146\n   \226\136\131g mapped_tenv' ienv' st2.\n     infer_ds ienv ds st1 = (Success ienv', st2) \226\136\167\n     (*\n     BIJ g (count st1.next_id \226\136\170 count ids) (count (st1.next_id + ids)) \226\136\167\n     *)\n     tenv_equiv (remap_tenv g tenv') mapped_tenv' \226\136\167\n     env_rel mapped_tenv' ienv' \226\136\167\n     st2.next_id = st1.next_id + CARD ids"
      ]
   (
   ... \\ ... \\ asm_exists_tac \\ fs [...] \\
   goal_assum (first_assum o ... ...) \\
   goal_assum (first_assum o ... ... mp_tac))
 Uncaught exception: Fail "Static Errors"