Source file sertop_init.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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin                                         *)
(* Copyright 2016-2019 MINES ParisTech                                  *)
(************************************************************************)
(* Status: Very Experimental                                            *)
(************************************************************************)

(* Init options for coq *)
type async_flags = {
  enable_async  : string option;
  deep_edits    : bool;
  async_workers : int;
}

type coq_opts = {

  (* callback to handle async feedback *)
  fb_handler   : Feedback.feedback -> unit;

  (* callback to load cma/cmo files *)
  ml_load      : (string -> unit) option;

  (* Enable Coq Debug mode *)
  debug        : bool;

}

(**************************************************************************)
(* Low-level, internal Coq initialization                                 *)
(**************************************************************************)
let coq_init opts =

  if opts.debug then begin
    Backtrace.record_backtrace true;
    Flags.debug := true;
  end;

  let load_obj = Sertop_loader.plugin_handler opts.ml_load in

  (* XXX: We may not have to set path once the issue in Coq upstream is fixed. *)
  let add_dir = Sertop_loader.add_ml_path in

  (* Custom toplevel is used for bytecode-to-js dynlink  *)
  let ser_mltop : Mltop.toplevel = let open Mltop in
    { load_obj
    (* We ignore all the other operations for now. *)
    ; use_file = (fun _ -> ())
    ; add_dir
    ; ml_loop  = (fun _ -> ())
    } in
  Mltop.set_top ser_mltop;

  (* Core Coq initialization *)
  Lib.init();

  (* This should be configurable somehow. *)
  Global.set_engagement Declarations.PredicativeSet;
  Global.set_indices_matter false;

  (**************************************************************************)
  (* Feedback setup                                                         *)
  (**************************************************************************)

  (* Initialize logging. *)
  ignore (Feedback.add_feeder opts.fb_handler);

  (**************************************************************************)
  (* Start the STM!!                                                        *)
  (**************************************************************************)
  Stm.init_core ();

  (* End of initialization *)
  ()

(******************************************************************************)
(* Async setup                                                                *)
(******************************************************************************)

(* Set async flags; IMPORTANT, this has to happen before STM.init () ! *)
let process_stm_flags opts = Option.cata (fun coqtop ->

    (* Whether to forward Glob output to the IDE. *)
    let dump_opt = "-no-glob" in

    let open Stm.AsyncOpts in
    let opts =
      { default_opts with
        async_proofs_mode = APon;
        (* Imitate CoqIDE *)
        async_proofs_never_reopen_branch = not opts.deep_edits;
        async_proofs_n_workers    = opts.async_workers;
        async_proofs_n_tacworkers = opts.async_workers;
      } in
    (* async_proofs_worker_priority); *)
    AsyncTaskQueue.async_proofs_flags_for_workers := [dump_opt];
    CoqworkmgrApi.(init High);
    (* Uh! XXXX *)
    for i = 0 to Array.length Sys.argv - 1 do
      Array.set Sys.argv i "-m"
    done;
    Array.set Sys.argv 0 coqtop;
    opts
  ) Stm.AsyncOpts.default_opts opts.enable_async