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
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
(************************************************************************)
(*         *   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
  ; error_recovery : bool
  }

type coq_opts = {

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

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

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

  (* Allow SProp *)
  allow_sprop  : bool;
  indices_matter : bool;
}

(**************************************************************************)
(* Low-level, internal Coq initialization                                 *)
(**************************************************************************)

(* Reference to feedback_handler *)
let fb = ref 0

let coq_init opts out_fmt =

  if opts.debug then begin
    Printexc.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. *)
    ; 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 opts.indices_matter;

  (* --allow-sprop in agreement with coq v8.11  *)
  Global.set_allow_sprop opts.allow_sprop;

  (* XXX fixme *)
  Flags.set_native_compiler false;

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

  (* Initialize logging. *)
  fb := Feedback.add_feeder (opts.fb_handler out_fmt);

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

  (* End of initialization *)
  ()

let update_fb_handler ~pp_feed out_fmt =
  Feedback.del_feeder !fb;
  fb := Feedback.add_feeder (pp_feed out_fmt)

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

(* Set async flags; IMPORTANT, this has to happen before STM.init () ! *)
let process_stm_flags opts =
  let stm_opts = Stm.AsyncOpts.default_opts in
  (* Process error resilience *)
  let async_proofs_tac_error_resilience, async_proofs_cmd_error_resilience =
    if opts.error_recovery
    then `All, true
    else `None, false
  in
  let stm_opts =
    { stm_opts with
      async_proofs_tac_error_resilience
    ; async_proofs_cmd_error_resilience }
  in
  (* Enable async mode if requested *)
  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 =
      { stm_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_opts opts.enable_async