Skip to content

Commit

Permalink
[coq] Enable memprof_limits token-based interruption
Browse files Browse the repository at this point in the history
This is a preliminary patch.
  • Loading branch information
ejgallego committed Apr 3, 2024
1 parent ad92494 commit 066523d
Show file tree
Hide file tree
Showing 4 changed files with 5 additions and 2 deletions.
1 change: 1 addition & 0 deletions compiler/driver.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ let go args =
let root_state = coq_init ~debug in
let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
let default = Coq.Workspace.default ~debug ~cmdline in
let () = Coq.Limits.start () in
let token = Coq.Limits.Token.create () in
let workspaces =
List.map
Expand Down
2 changes: 2 additions & 0 deletions controller/coq_lsp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,8 @@ let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =

let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
require_libraries delay =
Coq.Limits.start ();

(* Try to be sane w.r.t. \r\n in Windows *)
Stdlib.set_binary_mode_in stdin true;
Stdlib.set_binary_mode_out stdout true;
Expand Down
2 changes: 1 addition & 1 deletion coq/limits.ml
Original file line number Diff line number Diff line change
Expand Up @@ -46,4 +46,4 @@ module Coq : Intf = struct
end

module Mp = Limits_mp_impl
include Coq
include Mp
2 changes: 1 addition & 1 deletion vendor/coq
Submodule coq updated 1 files
+1 −4 library/global.ml

0 comments on commit 066523d

Please sign in to comment.