Overview

Job 886

CakeML:4f331e690829ce68efcc59ba19bd90b8852623e1
  Fix stray old theorem syntax in compiler backend
#635 (thm)
Merging into:c3cbbfd27bd9e1f2836f8f307279178dc76ac571
  Merge pull request #650 from CakeML/tweak-how-to
HOL:f6c660ddb3151f18cd07b606f2439087858abe20
  Further polish Definition documentation (incl. schematic attribute)
Machine:brain12 4.14.89.1.amd64-smp x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               2s  30MB
 Starting developers/bin
 Finished developers/bin                                           9s 936MB
 Starting semantics/ffi
 Finished semantics/ffi                                           18s 245MB
 Starting semantics
 Finished semantics                                             2m29s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      5m41s   1GB
 Starting basis/pure
 Finished basis/pure                                            1m31s 706MB
 Starting translator
 Finished translator                                            3m08s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m46s   2GB
 Starting characteristic
 Finished characteristic                                       10m14s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    3m02s   1GB
 Starting basis
 Finished basis                                                31m46s   2GB
 Starting compiler/inference
 Finished compiler/inference                                    3m34s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m40s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  16m33s   2GB
 Starting compiler/backend
 Finished compiler/backend                                         9s 305MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  27MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m58s 964MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                3m18s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                1m00s 902MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                2m16s 936MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               2m33s   1GB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  32s 788MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    38s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   42s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   41s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   42s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  38s 825MB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 2m12s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                              10m50s 924MB
 Starting compiler/inference/proofs
 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"