diff options
| -rw-r--r-- | checker/check.mllib | 2 | ||||
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 14 | ||||
| -rw-r--r-- | lib/clib.mllib | 2 | ||||
| -rw-r--r-- | lib/control.ml | 16 |
5 files changed, 18 insertions, 18 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 9f0bc200c..766eb4182 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -12,8 +12,8 @@ Option Store Exninfo Backtrace -Control Flags +Control Pp_control Pp Loc diff --git a/dev/printers.mllib b/dev/printers.mllib index d9f4aacce..29eae1620 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -12,12 +12,12 @@ Option Store Exninfo Backtrace -Control IStream Pp_control Loc Compat Flags +Control Pp Segmenttree Unicodetable diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c96371f26..6a8f3ddd7 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -265,15 +265,6 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true | FLOCKED -> assert false -let steps = ref 0 - -let slave_process = - let rec f = ref (fun () -> - match !Flags.async_proofs_mode with - | Flags.APonParallel n -> let b = n > 0 in f := (fun () -> b); !f () - | _ -> f := (fun () -> false); !f ()) in - fun () -> !f () - let unfold_projection infos p c = if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with @@ -290,11 +281,6 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Control.check_for_interrupt (); - incr steps; - if !steps = 10000 && slave_process () then begin - Thread.yield (); - steps := 0; - end; (* First head reduce both terms *) let whd = whd_stack (infos_with_reds infos betaiotazeta) in let rec whd_both (t1,stk1) (t2,stk2) = diff --git a/lib/clib.mllib b/lib/clib.mllib index cd8964f02..ed4894cb9 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -12,11 +12,11 @@ Option Store Exninfo Backtrace -Control IArray IStream Pp_control Flags +Control Pp Deque CObj diff --git a/lib/control.ml b/lib/control.ml index 9573614fd..8ce3334f5 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -10,8 +10,22 @@ let interrupt = ref false +let steps = ref 0 + +let slave_process = + let rec f = ref (fun () -> + match !Flags.async_proofs_mode with + | Flags.APonParallel n -> let b = n > 0 in f := (fun () -> b); !f () + | _ -> f := (fun () -> false); !f ()) in + fun () -> !f () + let check_for_interrupt () = - if !interrupt then begin interrupt := false; raise Sys.Break end + if !interrupt then begin interrupt := false; raise Sys.Break end; + incr steps; + if !steps = 10000 && slave_process () then begin + Thread.yield (); + steps := 0; + end (** This function does not work on windows, sigh... *) let unix_timeout n f e = |