Source file `coqc.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
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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)         *)
(************************************************************************)

let coqc_init ((_,color_mode),_) injections ~opts =
  Flags.quiet := true;
  System.trust_file_cache := true;
  Colors.init_color color_mode;
  DebugHook.Intf.(set
    { read_cmd = Coqtop.ltac_debug_parse
    ; submit_answer = Coqtop.ltac_debug_answer
    ; isTerminal = true
    });
  injections

let coqc_specific_usage = Boot.Usage.{
  executable_name = "rocq compile";
  extra_args = "file...";
  extra_options = "\n\
rocq compile specific options:\
\n  -o f.vo                use f.vo as the output file name\
\n  -verbose               compile and output the input file\
\n  -noglob                do not dump globalizations\
\n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
\n  -vos                   process statements but ignore opaque proofs, and produce a .vos file\
\n  -vok                   process the file by loading .vos instead of .vo files for\
\n                         dependencies, and produce an empty .vok file on success\
\n"
}

let coqc_main ((copts,_),stm_opts) injections ~opts =
  Topfmt.(in_phase ~phase:CompilationPhase)
    Ccompile.compile_file opts stm_opts copts injections;

  flush_all();

  if copts.Coqcargs.output_context then begin
    let sigma, env = let e = Global.env () in Evd.from_env e, e in
    let access = Library.indirect_accessor[@@warning "-3"] in
    Feedback.msg_notice Pp.(Flags.(with_option raw_print (fun () ->
        Prettyp.print_full_pure_context access env sigma) ()) ++ fnl ())
  end;
  ()

let coqc_run copts ~opts injections =
  let _feeder = Feedback.add_feeder Coqloop.coqloop_feed in
  try
    coqc_main ~opts copts injections;
    exit 0
  with exn ->
    flush_all();
    Topfmt.print_err_exn exn;
    flush_all();
    let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
    exit exit_code

let fix_stm_opts opts stm_opts = match opts.Coqcargs.compilation_mode with
  | BuildVos ->
    (* We need to disable error resiliency, otherwise some errors
       will be ignored in batch mode. c.f. #6707

       This is not necessary in the vo case as it fully checks the
       document anyways. *)
    let open Stm.AsyncOpts in
    { stm_opts with
      async_proofs_mode = APon;
      async_proofs_n_workers = 0;
      async_proofs_cmd_error_resilience = false;
      async_proofs_tac_error_resilience = FNone;
    }
  | BuildVo | BuildVok -> stm_opts

let custom_coqc : ((Coqcargs.t * Colors.color) * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel
 = Coqtop.{
  parse_extra = (fun opts extras ->
    let color_mode, extras = Colors.parse_extra_colors ~emacs:opts.config.print_emacs extras in
    let stm_opts, extras = Stmargs.parse_args opts extras in
    let coqc_opts = Coqcargs.parse extras in
    let stm_opts = fix_stm_opts coqc_opts stm_opts in
    ((coqc_opts, color_mode), stm_opts), []);
  usage = coqc_specific_usage;
  init_extra = coqc_init;
  run = coqc_run;
  initial_args = Coqargs.default;
}

let main args =
  let () = Memtrace_init.init () in
  Coqtop.start_coq custom_coqc args