Job 609

CakeML:583572eb9c634f521665ea7c32211eaa0d9072f2
  Fix mangled Theorem statement [Dec 04 05:09:44]
#572 (cleanup)
Merging into:8b46c3a87cb343ec13b54a05bfb531841eb60955
  Fix bug in tag_name (picks an unused cons name) [Dec 03 04:19:52]
HOL:e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6
  Fix bug in proof (18934f7cf gave 2 theorems same name) [Dec 04 10:59:11]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Dec 04 11:03:28 Claimed job
Dec 04 11:06:04 Building HOL
Dec 04 11:13:36 Starting developers
Dec 04 11:13:37 Finished developers                                               0s  28MB
Dec 04 11:13:38 Starting developers/bin
Dec 04 11:14:11 Finished developers/bin                                          33s 201MB
Dec 04 11:14:12 Starting semantics/ffi
Dec 04 11:14:47 Finished semantics/ffi                                           33s 468MB
Dec 04 11:14:47 Starting semantics
Dec 04 11:16:16 Finished semantics                                             1m28s 978MB
Dec 04 11:16:17 Starting semantics/proofs
Dec 04 11:19:19 Finished semantics/proofs                                      3m00s   1GB
Dec 04 11:19:20 Starting basis/pure
Dec 04 11:22:55 Finished basis/pure                                            3m34s 821MB
Dec 04 11:22:56 Starting translator
Dec 04 11:24:11 Finished translator                                            1m13s 905MB
Dec 04 11:24:12 Starting compiler/parsing
Dec 04 11:25:28 Finished compiler/parsing                                      1m15s   2GB
Dec 04 11:25:29 Starting characteristic
Dec 04 11:27:59 Finished characteristic                                        2m28s   1GB
Dec 04 11:27:59 Starting translator/monadic
Dec 04 11:29:25 Finished translator/monadic                                    1m24s   1GB
Dec 04 11:29:26 Starting basis
Dec 04 11:45:36 Finished basis                                                16m09s   2GB
Dec 04 11:45:37 Starting compiler/inference
Dec 04 11:47:33 Finished compiler/inference                                    1m55s   1GB
Dec 04 11:47:34 Starting compiler/backend/reg_alloc
Dec 04 11:48:21 Finished compiler/backend/reg_alloc                              45s   1GB
Dec 04 11:48:21 Starting compiler/backend/gc
Dec 04 11:55:48 Finished compiler/backend/gc                                   7m25s   2GB
Dec 04 11:55:48 Starting compiler/backend
Dec 04 11:55:51 Finished compiler/backend                                         1s  18MB
Dec 04 11:55:52 Starting compiler/encoders/asm
Dec 04 11:55:54 Finished compiler/encoders/asm                                    0s  16MB
Dec 04 11:55:55 Starting compiler/encoders/x64
Dec 04 11:56:43 Finished compiler/encoders/x64                                   47s 507MB
Dec 04 11:56:44 Starting compiler/encoders/arm6
Dec 04 11:58:24 Finished compiler/encoders/arm6                                1m39s   1GB
Dec 04 11:58:25 Starting compiler/encoders/arm8
Dec 04 11:58:49 Finished compiler/encoders/arm8                                  23s 518MB
Dec 04 11:58:50 Starting compiler/encoders/mips
Dec 04 11:59:47 Finished compiler/encoders/mips                                  56s 910MB
Dec 04 11:59:48 Starting compiler/encoders/riscv
Dec 04 12:00:48 Finished compiler/encoders/riscv                                 59s 949MB
Dec 04 12:00:49 Starting compiler/encoders/ag32
Dec 04 12:01:06 Finished compiler/encoders/ag32                                  15s 730MB
Dec 04 12:01:06 Starting compiler/backend/x64
Dec 04 12:01:24 Finished compiler/backend/x64                                    16s   1GB
Dec 04 12:01:25 Starting compiler/backend/arm6
Dec 04 12:01:44 Finished compiler/backend/arm6                                   18s   1GB
Dec 04 12:01:45 Starting compiler/backend/arm8
Dec 04 12:02:02 Finished compiler/backend/arm8                                   16s 948MB
Dec 04 12:02:03 Starting compiler/backend/mips
Dec 04 12:02:22 Finished compiler/backend/mips                                   18s   1GB
Dec 04 12:02:23 Starting compiler/backend/riscv
Dec 04 12:02:42 Finished compiler/backend/riscv                                  17s   1GB
Dec 04 12:02:42 Starting compiler/backend/ag32
Dec 04 12:03:56 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 04 12:03:56 Starting compiler/parsing/proofs
Dec 04 12:10:05 Finished compiler/parsing/proofs                               6m07s 806MB
Dec 04 12:10:05 Starting compiler/inference/proofs
Dec 04 12:12:57 Finished compiler/inference/proofs                             2m50s   1GB
Dec 04 12:12:57 Starting compiler/backend/semantics
Dec 04 12:13:11 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"
   [
      QUOTE
      " (*#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