Job 609

  Fix mangled Theorem statement
#572 (cleanup)
Merging into:8b46c3a87cb343ec13b54a05bfb531841eb60955
  Fix bug in tag_name (picks an unused cons name)
  Fix bug in proof (18934f7cf gave 2 theorems same name)
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               0s  28MB
 Starting developers/bin
 Finished developers/bin                                          33s 201MB
 Starting semantics/ffi
 Finished semantics/ffi                                           33s 468MB
 Starting semantics
 Finished semantics                                             1m28s 978MB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m00s   1GB
 Starting basis/pure
 Finished basis/pure                                            3m34s 821MB
 Starting translator
 Finished translator                                            1m13s 905MB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m15s   2GB
 Starting characteristic
 Finished characteristic                                        2m28s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m24s   1GB
 Starting basis
 Finished basis                                                16m09s   2GB
 Starting compiler/inference
 Finished compiler/inference                                    1m55s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              45s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   7m25s   2GB
 Starting compiler/backend
 Finished compiler/backend                                         1s  18MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  16MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   47s 507MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                1m39s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  23s 518MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  56s 910MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 59s 949MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  15s 730MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    16s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   16s 948MB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   18s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  17s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m12s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               6m07s 806MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m50s   1GB
 Starting compiler/backend/semantics
 FAILED: compiler/backend/semantics
]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/balanced_bst]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ../../../translator/monadic/monad_base]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../translator/monadic/monad_base]0;Holmake: ../../../translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../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: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
Starting work on wordSemTheory
backendPropsTheory                                  OK
Starting work on patSemTheory
flatSemTheory                              FAILED! <1>
 Found near
   tDefine "evaluate"
      " (*#loc 505 39*)\n  (evaluate (env:flatSem$environment) (s:'ffi flatSem$state) ([]:flatLang$exp list) = (s,Rval [])) \226\136\167\n  (evaluate env s (e1::e2::es) =\n    case fix_clock s (evaluate env s [e1]) of\n    | (s, Rval v) =>\n        (case evaluate env s (e2::es) of\n         | (s, Rval vs) => (s, Rval (HD v::vs))\n         | res => res)\n    | res => res) \226\136\167\n  (evaluate env s [Lit _ l] = (s, Rval [Litv l])) \226\136\167\n  (evaluate env s [Raise _ e] =\n   case evaluate env s [e] of\n   | (s, Rval v) => (s, Rerr (Rraise (HD v)))\n   | res => res) \226\136\167\n  (evaluate env s [Handle _ e pes] =\n   case fix_clock s (evaluate env s [e]) of\n   | (s, Rerr (Rraise v)) => evaluate_match env s v pes v\n   | res => res) \226\136\167\n  (evaluate env s [Con _ NONE es] =\n    if env.check_ctor then\n      case evaluate env s (REVERSE es) of\n      | (s, Rval vs) => (s,Rval [Conv NONE (REVERSE vs)])\n      | res => res\n    else\n      (s, Rerr (Rabort Rtype_error))) \226\136\167\n  (evaluate env s [Con _ (SOME cn) es] =\n    if env.check_ctor \226\136\167 (cn, LENGTH es) \226\136\137 env.c then\n      (s, Rerr (Rabort Rtype_error))\n    else\n      case evaluate env s (REVERSE es) of\n      | (s, Rval vs) => (s, Rval [Conv (SOME cn) (REVERSE vs)])\n      | res => res) \226\136\167\n  (evaluate env s [Var_local _ n] = (s,\n   case ALOOKUP env.v n of\n   | SOME v => Rval [v]\n   | NONE => Rerr (Rabort Rtype_error))) \226\136\167\n  (evaluate env s [Fun _ n e] = (s, Rval [Closure env.v n e])) \226\136\167\n  (evaluate env s [App _ op es] =\n   case fix_clock s (evaluate env s (REVERSE es)) of\n   | (s, Rval vs) =>\n       if op = flatLang$Opapp then\n         (case flatSem$do_opapp (REVERSE vs) of\n          | SOME (env', e) =>\n            if s.clock = 0 then\n              (s, Rerr (Rabort Rtimeout_error))\n            else\n              evaluate (env with v := env') (dec_clock s) [e]\n          | NONE => (s, Rerr (Rabort Rtype_error)))\n       else\n       (case (do_app env.check_ctor s op (REVERSE vs)) of\n        | NONE => (s, Rerr (Rabort Rtype_error))\n        | SOME (s',r) => (s', list_result r))\n   | res => res) \226\136\167\n  (evaluate env s [If _ e1 e2 e3] =\n   case fix_clock s (evaluate env s [e1]) of\n   | (s, Rval vs) =>\n     (case do_if (HD vs) e2 e3 of\n      | SOME e => evaluate env s [e]\n      | NONE => (s, Rerr (Rabort Rtype_error)))\n   | res => res) \226\136\167\n  (evaluate env s [Mat _ e pes] =\n   case fix_clock s (evaluate env s [e]) of\n   | (s, Rval v) =>\n       evaluate_match env s (HD v) pes bind_exn_v\n   | res => res) \226\136\167\n  (evaluate env s [Let _ n e1 e2] =\n   case fix_clock s (evaluate env s [e1]) of\n   | (s, Rval vs) => evaluate (env with v updated_by opt_bind n (HD vs)) s [e2]\n   | res => res) \226\136\167\n  (evaluate env s [Letrec _ funs e] =\n   if ALL_DISTINCT (MAP FST funs)\n   then evaluate (env with v := build_rec_env funs env.v env.v) s [e]\n   else (s, Rerr (Rabort Rtype_error))) \226\136\167\n  (evaluate_match (env:flatSem$environment) s v [] err_v =\n    if env.exh_pat then\n      (s, Rerr(Rabort Rtype_error))\n    else\n      (s, Rerr(Rraise err_v))) \226\136\167\n  (evaluate_match env s v ((p,e)::pes) err_v =\n   if ALL_DISTINCT (pat_bindings p []) then\n     case pmatch env s.refs p v [] of\n     | Match env_v' => evaluate (env with v := env_v' ++ env.v) s [e]\n     | No_match => evaluate_match env s v pes err_v\n     | _ => (s, Rerr(Rabort Rtype_error))\n   else (s, Rerr(Rabort Rtype_error)))"
   ... >> ... >> ... ... >> imp_res_tac fix_clock_IMP >>
   imp_res_tac do_if_either_or >> rw [])
 Uncaught exception: Fail "Static Errors"
closSemTheory                                 M-KILLED
wordSemTheory                                 M-KILLED
patSemTheory                                  M-KILLED