package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/src/rocq-runtime.clib/memprof_coq.ml.html
Source file memprof_coq.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
# 1 "clib/memprof_coq.std.ml" let is_interrupted _ = false [@@inline] module Resource_bind = struct let ( let& ) f scope = f ~scope end (* We do our own Mutex_aux for OCaml 5.x *) module Mutex_aux = Mutex_aux module Thread_map_core = struct open Resource_bind module IMap = Map.Make ( struct type t = int let compare = Stdlib.compare end) type 'a t = { mutex : Mutex.t ; mutable map : 'a IMap.t } let create () = { mutex = Mutex.create () ; map = IMap.empty } let current_thread () = Thread.id (Thread.self ()) let get s = (* Concurrent threads do not alter the value for the current thread, so we do not need a lock. *) IMap.find_opt (current_thread ()) s.map (* For set and clear we need a lock *) let set s v = let& () = Mutex_aux.with_lock s.mutex in let new_map = match v with | None -> IMap.remove (current_thread ()) s.map | Some v -> IMap.add (current_thread ()) v s.map in s.map <- new_map let _clear s = let& () = Mutex_aux.with_lock s.mutex in s.map <- IMap.empty end module Masking = struct (* There's no mechanism to block OCaml's async exceptions, so without memprof there is nothing interesting to do. *) let with_resource ~acquire arg ~scope ~(release : _ -> unit) = let r = acquire arg in Fun.protect ~finally:(fun () -> release r) (fun () -> scope r) end module Thread_map = struct include Thread_map_core let with_value tls ~value ~scope = let old_value = get tls in (* FIXME: needs proper masking here as there is a race between resources and asynchronous exceptions. For now, it is exception-safe only for exceptions arising from Memprof_callbacks. *) Masking.with_resource ~acquire:(fun () -> set tls (Some value)) () ~scope ~release:(fun () -> set tls old_value) end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>