<commit_before>(************************************************************************)
(*         *   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)         *)
(************************************************************************)

(**********************************)
(**  Configuration script for Coq *)
(**********************************)
open Printf
open Conf
open Util
open CmdArgs
open CmdArgs.Prefs

let (/) = Filename.concat

let coq_version = "8.15+alpha"
let vo_magic = 81491
let is_a_released_version = false

(** Default OCaml binaries *)

type camlexec = { mutable find : string }
let camlexec = { find = "ocamlfind" }

let reset_caml_find c o = c.find <- o

let coq_annot_flag prefs = if prefs.annot then "-annot" else ""
let coq_bin_annot_flag prefs = if prefs.bin_annot then "-bin-annot" else ""

(* This variable can be overridden only for debug purposes, use with
   care. *)
let coq_safe_string = "-safe-string"
let coq_strict_sequence = "-strict-sequence"

(* Query for the architecture *)
let arch prefs = arch prefs.arch

(** NB: [arch_is_win32] is broader than [os_type_win32], cf. cygwin *)

let arch_is_win32 arch = arch = "win32"

let resolve_binary_suffix arch = if arch_is_win32 arch then ".exe" else ""

(** * Git Precommit Hook *)
let install_precommit_hook prefs =
  let f = ".git/hooks/pre-commit" in
  if dir_exists ".git/hooks" && not (Sys.file_exists f) then begin
    cprintf prefs "Creating pre-commit hook in %s" f;
    let o = open_out f in
    let pr s = fprintf o s in
    pr "#!/bin/sh\n";
    pr "\n";
    pr "if [ -x dev/tools/pre-commit ]; then\n";
    pr "    exec dev/tools/pre-commit\n";
    pr "fi\n";
    close_out o;
    Unix.chmod f 0o775
  end

(** * Browser command *)

let browser prefs arch =
  match prefs.browser with
  | Some b -> b
  | None when arch_is_win32 arch -> "start %s"
  | None when arch = "Darwin" -> "open %s"
  | _ -> "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"

(** * OCaml programs *)
module CamlConf = struct
  type t =
    { camlbin : string
    ; caml_version : string
    ; camllib : string
    ; findlib_version : string
    }
end

let resolve_caml prefs =
  let () =
    try reset_caml_find camlexec (which camlexec.find)
    with Not_found ->
      die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.find ^
           "Please adjust your path or use the -ocamlfind option of ./configure")
  in
  if not (is_executable camlexec.find)
  then die ("Error: cannot find the executable '"^camlexec.find^"'.")
  else
    let findlib_version, _ = run camlexec.find ["query"; "findlib"; "-format"; "%v"] in
    let caml_version, _ = run camlexec.find ["ocamlc";"-version"] in
    let camllib, _ = run camlexec.find ["printconf";"stdlib"] in
    let camlbin = (* TODO beurk beurk beurk *)
      Filename.dirname (Filename.dirname camllib) / "bin/" in
    { CamlConf.camlbin; caml_version; camllib; findlib_version }

(** Caml version as a list of ints [4;0;1] *)
let caml_version_nums { CamlConf.caml_version } =
  generic_version_nums ~name:"the OCaml compiler" caml_version

let check_caml_version prefs caml_version caml_version_nums =
  if caml_version_nums >= [4;5;0] then
    cprintf prefs "You have OCaml %s. Good!" caml_version
  else
    let () = cprintf prefs "Your version of OCaml is %s." caml_version in
    die "You need OCaml 4.05.0 or later."

let check_findlib_version prefs { CamlConf.findlib_version } =
  let findlib_version_nums = generic_version_nums ~name:"findlib" findlib_version in
  if findlib_version_nums >= [1;8;0] then
    cprintf prefs "You have OCamlfind %s. Good!" findlib_version
  else
    let () = cprintf prefs "Your version of OCamlfind is %s." findlib_version in
    die "You need OCamlfind 1.8.0 or later."

(** Explanation of disabled warnings:
    4: fragile pattern matching: too common in the code and too annoying to avoid in general
    9: missing fields in a record pattern: too common in the code and not worth the bother
    27: innocuous unused variable: innocuous
    41: ambiguous constructor or label: too common
    42: disambiguated counstructor or label: too common
    44: "open" shadowing already defined identifier: too common, especially when some are aliases
    45: "open" shadowing a label or constructor: see 44
    48: implicit elimination of optional arguments: too common
    58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
    67: "unused functor parameter" seems totally bogus
    68: "This pattern depends on mutable state" no idea what it means, dune builds don't display it
    70: ".ml file without .mli file" bogus warning when used generally
*)

let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-58-67-68-70"
let coq_warn_error prefs =
    if prefs.warn_error
    then "-warn-error +a"
    else ""

(* Flags used to compile Coq and plugins (via coq_makefile) *)
let caml_flags coq_annot_flag coq_bin_annot_flag =
  Printf.sprintf "-thread -rectypes %s %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string coq_strict_sequence

(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
let coq_caml_flags = coq_warn_error

(** * Native compiler *)

let msg_byteonly =
  "Only the bytecode version of Coq will be available."

let msg_no_ocamlopt () =
  warn "Cannot find the OCaml native-code compiler.\n%s" msg_byteonly

let msg_no_dynlink_cmxa prefs =
  warn "Cannot find native-code dynlink library.\n%s" msg_byteonly;
  cprintf prefs "For building a native-code Coq, you may try to first";
  cprintf prefs "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)";
  cprintf prefs "and then run ./configure -natdynlink no"

let check_native prefs camlenv =<commit_msg>[coq_makefile] Use a concrete list of enabled warnings<commit_after>(************************************************************************)
(*         *   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)         *)
(************************************************************************)

(**********************************)
(**  Configuration script for Coq *)
(**********************************)
open Printf
open Conf
open Util
open CmdArgs
open CmdArgs.Prefs

let (/) = Filename.concat

let coq_version = "8.15+alpha"
let vo_magic = 81491
let is_a_released_version = false

(** Default OCaml binaries *)

type camlexec = { mutable find : string }
let camlexec = { find = "ocamlfind" }

let reset_caml_find c o = c.find <- o

let coq_annot_flag prefs = if prefs.annot then "-annot" else ""
let coq_bin_annot_flag prefs = if prefs.bin_annot then "-bin-annot" else ""

(* This variable can be overridden only for debug purposes, use with
   care. *)
let coq_safe_string = "-safe-string"
let coq_strict_sequence = "-strict-sequence"

(* Query for the architecture *)
let arch prefs = arch prefs.arch

(** NB: [arch_is_win32] is broader than [os_type_win32], cf. cygwin *)

let arch_is_win32 arch = arch = "win32"

let resolve_binary_suffix arch = if arch_is_win32 arch then ".exe" else ""

(** * Git Precommit Hook *)
let install_precommit_hook prefs =
  let f = ".git/hooks/pre-commit" in
  if dir_exists ".git/hooks" && not (Sys.file_exists f) then begin
    cprintf prefs "Creating pre-commit hook in %s" f;
    let o = open_out f in
    let pr s = fprintf o s in
    pr "#!/bin/sh\n";
    pr "\n";
    pr "if [ -x dev/tools/pre-commit ]; then\n";
    pr "    exec dev/tools/pre-commit\n";
    pr "fi\n";
    close_out o;
    Unix.chmod f 0o775
  end

(** * Browser command *)

let browser prefs arch =
  match prefs.browser with
  | Some b -> b
  | None when arch_is_win32 arch -> "start %s"
  | None when arch = "Darwin" -> "open %s"
  | _ -> "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"

(** * OCaml programs *)
module CamlConf = struct
  type t =
    { camlbin : string
    ; caml_version : string
    ; camllib : string
    ; findlib_version : string
    }
end

let resolve_caml prefs =
  let () =
    try reset_caml_find camlexec (which camlexec.find)
    with Not_found ->
      die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.find ^
           "Please adjust your path or use the -ocamlfind option of ./configure")
  in
  if not (is_executable camlexec.find)
  then die ("Error: cannot find the executable '"^camlexec.find^"'.")
  else
    let findlib_version, _ = run camlexec.find ["query"; "findlib"; "-format"; "%v"] in
    let caml_version, _ = run camlexec.find ["ocamlc";"-version"] in
    let camllib, _ = run camlexec.find ["printconf";"stdlib"] in
    let camlbin = (* TODO beurk beurk beurk *)
      Filename.dirname (Filename.dirname camllib) / "bin/" in
    { CamlConf.camlbin; caml_version; camllib; findlib_version }

(** Caml version as a list of ints [4;0;1] *)
let caml_version_nums { CamlConf.caml_version } =
  generic_version_nums ~name:"the OCaml compiler" caml_version

let check_caml_version prefs caml_version caml_version_nums =
  if caml_version_nums >= [4;5;0] then
    cprintf prefs "You have OCaml %s. Good!" caml_version
  else
    let () = cprintf prefs "Your version of OCaml is %s." caml_version in
    die "You need OCaml 4.05.0 or later."

let check_findlib_version prefs { CamlConf.findlib_version } =
  let findlib_version_nums = generic_version_nums ~name:"findlib" findlib_version in
  if findlib_version_nums >= [1;8;0] then
    cprintf prefs "You have OCamlfind %s. Good!" findlib_version
  else
    let () = cprintf prefs "Your version of OCamlfind is %s." findlib_version in
    die "You need OCamlfind 1.8.0 or later."

(** Note, these warnings are only used in Coq Makefile *)
(** Explanation of enabled/disabled warnings:
    4: fragile pattern matching: too common in the code and too annoying to avoid in general
    9: missing fields in a record pattern: too common in the code and not worth the bother
    27: innocuous unused variable: innocuous
    41: ambiguous constructor or label: too common
    42: disambiguated counstructor or label: too common
    44: "open" shadowing already defined identifier: too common, especially when some are aliases
    45: "open" shadowing a label or constructor: see 44
    48: implicit elimination of optional arguments: too common
    58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
    67: "unused functor parameter" seems totally bogus
    68: "This pattern depends on mutable state" no idea what it means, dune builds don't display it
    70: ".ml file without .mli file" bogus warning when used generally
*)

(* Note, we list all warnings to be complete *)
let coq_warnings = "-w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70"
let coq_warn_error prefs =
    if prefs.warn_error
    then "-warn-error +a"
    else ""

(* Flags used to compile Coq and plugins (via coq_makefile) *)
let caml_flags coq_annot_flag coq_bin_annot_flag =
  Printf.sprintf "-thread -rectypes %s %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string coq_strict_sequence

(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
let coq_caml_flags = coq_warn_error

(** * Native compiler *)

let msg_byteonly =
  "Only the bytecode version of Coq will be available."

let msg_no_ocamlopt () =
  warn "Cannot find the OCaml native-code compiler.\n%s" msg_byteonly

let msg_no_dynlink_cmxa prefs =
  warn "Cannot find native-code dynlink library.\n%s" msg_byteonly;
  cprintf prefs "For building a native-code Coq, you may try to first";
  cprintf prefs "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)";
  cprintf prefs "and then run ./configure -natdynlink no"

let check_native prefs camlenv =
{'fraction_non_alphanumeric': 0.1428457616316125, 'fraction_numerical': 0.016411727214786488, 'mean_word_length': 3.5432500904813606, 'pattern_counts': {'":': 2, '<': 7, '<?xml version=': 0, '>': 17, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7193974', 'n_tokens_mistral': 4230, 'n_tokens_neox': 4055, 'n_words': 1406}