package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file common_compile.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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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)         *)
(************************************************************************)

open Pp

let fatal_error msg =
  Topfmt.std_logger Feedback.Error msg;
  flush_all ();
  exit 1

let warn_file_no_extension =
  CWarnings.create ~name:"file-no-extension" ~category:CWarnings.CoreCategories.filesystem
         (fun (f,ext) ->
          str "File \"" ++ str f ++
            strbrk "\" has been implicitly expanded to \"" ++
            str f ++ str ext ++ str "\"")

let ensure_ext ext f =
  if Filename.check_suffix f ext then f
  else begin
    warn_file_no_extension (f,ext);
    f ^ ext
  end

let safe_chop_extension f =
  try Filename.chop_extension f with _ -> f

let ensure_bname src tgt =
  let src, tgt = Filename.basename src, Filename.basename tgt in
  let src, tgt = safe_chop_extension src, safe_chop_extension tgt in
  if src <> tgt then
    fatal_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
                   str "Source: " ++ str src                                                ++ fnl () ++
                   str "Target: " ++ str tgt)

let ensure ~ext ~src ~tgt = ensure_bname src tgt; ensure_ext ext tgt

let ensure_exists f =
  if not (Sys.file_exists f) then
    fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f))

let ensure_exists_with_prefix ~src ~tgt:f_out ~src_ext ~tgt_ext =
  let long_f_dot_src = ensure ~ext:src_ext ~src ~tgt:src in
  ensure_exists long_f_dot_src;
  let long_f_dot_tgt = match f_out with
    | None -> safe_chop_extension long_f_dot_src ^ tgt_ext
    | Some f -> ensure ~ext:tgt_ext ~src:long_f_dot_src ~tgt:f in
  long_f_dot_src, long_f_dot_tgt

let ensure_no_pending_proofs ~filename s =
  match s.Vernacstate.interp.lemmas with
  | Some lemmas ->
      let pfs = Vernacstate.LemmaStack.get_all_proof_names lemmas in
      fatal_error (str "There are pending proofs in file " ++ str filename ++ str": "
                    ++ (pfs
                        |> List.rev
                        |> prlist_with_sep pr_comma Names.Id.print)
                    ++ str ".");
  | None ->
    let pm = s.Vernacstate.interp.program in
    let what_for = Pp.str ("file " ^ filename) in
    NeList.iter (fun pm -> Declare.Obls.check_solved_obligations ~what_for ~pm) pm
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct