[coq] remove Config module

Signed-off-by: Enrico Tassi <[email protected]>

Author: gares

src/dune_rules/coq/coq_config.ml

@@ -195,61 +195,58 @@ module Version = struct
   ;;
 end
 
-module Config = struct
-  type t =
-    { coqlib : Path.t
-    ; coqcorelib : Path.t option (* this is not available in Coq < 8.14 *)
-    ; coq_native_compiler_default :
-        string option (* this is not available in Coq < 8.13 *)
-    }
+type t =
+  { coqlib : Path.t
+  ; coqcorelib : Path.t option (* this is not available in Coq < 8.14 *)
+  ; coq_native_compiler_default : string option (* this is not available in Coq < 8.13 *)
+  }
 
-  let impl_config bin =
-    let* _ = Build_system.build_file bin in
-    Memo.of_reproducible_fiber
-    @@ Process.run_capture_lines
-         ~display:Quiet
-         ~stderr_to:
-           (Process.Io.make_stderr
-              ~output_on_success:Swallow
-              ~output_limit:Execution_parameters.Action_output_limit.default)
-         Return
-         bin
-         [ "--config" ]
-  ;;
+let impl_config bin =
+  let* _ = Build_system.build_file bin in
+  Memo.of_reproducible_fiber
+  @@ Process.run_capture_lines
+       ~display:Quiet
+       ~stderr_to:
+         (Process.Io.make_stderr
+            ~output_on_success:Swallow
+            ~output_limit:Execution_parameters.Action_output_limit.default)
+       Return
+       bin
+       [ "--config" ]
+;;
 
-  let config_memo = Memo.create "coq-config" ~input:(module Path) impl_config
+let config_memo = Memo.create "coq-config" ~input:(module Path) impl_config
 
-  let make ~(coqc : Action.Prog.t) =
-    let open Memo.O in
-    let+ config_output =
-      get_output_from_config_or_version ~coqc ~what:"--config" config_memo
-    in
-    let open Result.O in
-    let* config_output = config_output in
-    match Vars.of_lines config_output with
-    | Ok vars ->
-      let coqlib = Vars.get_path vars "COQLIB" in
-      (* this is not available in Coq < 8.14 *)
-      let coqcorelib = Vars.get_path_opt vars "COQCORELIB" in
-      (* this is not available in Coq < 8.13 *)
-      let coq_native_compiler_default = Vars.get_opt vars "COQ_NATIVE_COMPILER_DEFAULT" in
-      Ok { coqlib; coqcorelib; coq_native_compiler_default }
-    | Error msg ->
-      User_error.raise Pp.[ textf "Cannot parse output of coqc --config:"; msg ]
-  ;;
+let make ~(coqc : Action.Prog.t) =
+  let open Memo.O in
+  let+ config_output =
+    get_output_from_config_or_version ~coqc ~what:"--config" config_memo
+  in
+  let open Result.O in
+  let* config_output = config_output in
+  match Vars.of_lines config_output with
+  | Ok vars ->
+    let coqlib = Vars.get_path vars "COQLIB" in
+    (* this is not available in Coq < 8.14 *)
+    let coqcorelib = Vars.get_path_opt vars "COQCORELIB" in
+    (* this is not available in Coq < 8.13 *)
+    let coq_native_compiler_default = Vars.get_opt vars "COQ_NATIVE_COMPILER_DEFAULT" in
+    Ok { coqlib; coqcorelib; coq_native_compiler_default }
+  | Error msg ->
+    User_error.raise Pp.[ textf "Cannot parse output of coqc --config:"; msg ]
+;;
 
-  let by_name { coqlib; coqcorelib; coq_native_compiler_default } name =
-    match name with
-    | "coqlib" -> Some (Value.path coqlib)
-    | "coqcorelib" -> Option.map ~f:Value.path coqcorelib
-    | "coq_native_compiler_default" ->
-      Option.map ~f:Value.string coq_native_compiler_default
-    | _ ->
-      Code_error.raise
-        "Unknown name was requested from coq_config"
-        [ "name", Dyn.string name ]
-  ;;
-end
+let by_name { coqlib; coqcorelib; coq_native_compiler_default } name =
+  match name with
+  | "coqlib" -> Some (Value.path coqlib)
+  | "coqcorelib" -> Option.map ~f:Value.path coqcorelib
+  | "coq_native_compiler_default" ->
+    Option.map ~f:Value.string coq_native_compiler_default
+  | _ ->
+    Code_error.raise
+      "Unknown name was requested from coq_config"
+      [ "name", Dyn.string name ]
+;;
 
 let expand source macro artifacts_host =
   let s = Pform.Macro_invocation.Args.whole macro in
@@ -282,8 +279,7 @@ let expand source macro artifacts_host =
   | "version.suffix"
   | "version"
   | "ocaml-version" -> expand Version.make Version.by_name s
-  | "coqlib" | "coqcorelib" | "coq_native_compiler_default" ->
-    expand Config.make Config.by_name s
+  | "coqlib" | "coqcorelib" | "coq_native_compiler_default" -> expand make by_name s
   | _ ->
     Code_error.raise "Unknown name was requested from coq_config" [ "name", Dyn.string s ]
 ;;

src/dune_rules/coq/coq_config.mli

@@ -40,29 +40,27 @@ module Version : sig
   val by_name : t -> string -> Value.t Option.t
 end
 
-module Config : sig
-  (** Data of a Coq configuration. *)
-  type t
+(** Data of a Coq configuration. *)
+type t
 
-  (** [make ~coqc] runs coqc --config and returns the configuration data. Exceptionally, one
-      of the following will happen:
+(** [make ~coqc] runs coqc --config and returns the configuration data. Exceptionally, one
+    of the following will happen:
 
-      - Return [Error message] if coqc --config exits with a non-zero code.
-      - Throw a user error if coqc --config is not parsable.
-      - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *)
-  val make : coqc:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
+    - Return [Error message] if coqc --config exits with a non-zero code.
+    - Throw a user error if coqc --config is not parsable.
+    - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *)
+val make : coqc:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
 
-  (** [by_name t name] returns the value of the option [name] in the Coq
-      configuration [t]. If the value is not available then [None] is returned.
-      Throws a code error if an invalid [name] is requested.
+(** [by_name t name] returns the value of the option [name] in the Coq
+    configuration [t]. If the value is not available then [None] is returned.
+    Throws a code error if an invalid [name] is requested.
 
-      Currently supported names are:
+    Currently supported names are:
 
-      - coqlib
-      - coqcorelib
-      - coq_native_compiler_default *)
-  val by_name : t -> string -> Value.t Option.t
-end
+    - coqlib
+    - coqcorelib
+    - coq_native_compiler_default *)
+val by_name : t -> string -> Value.t Option.t
 
 val expand
   :  Dune_lang.Template.Pform.t

src/dune_rules/coq/coq_path.ml

@@ -24,7 +24,7 @@ let cmxs_directories t = t.cmxs_directories
 let stdlib t = t.stdlib
 
 let config_path_exn coq_config key =
-  Coq_config.Config.by_name coq_config key
+  Coq_config.by_name coq_config key
   |> function
   | Some path ->
     path
@@ -47,7 +47,7 @@ let config_path_exn coq_config key =
 let config_path ~default coq_config key =
   Option.value
     ~default:(Coq_config.Value.path default)
-    (Coq_config.Config.by_name coq_config key)
+    (Coq_config.by_name coq_config key)
   |> function
   | Coq_config.Value.Path p -> p (* We have found a path for key *)
   | path ->
@@ -175,7 +175,7 @@ let scan_vo root_path =
 
 let of_coq_install coqc =
   let open Memo.O in
-  let* coq_config = Coq_config.Config.make ~coqc:(Ok coqc) in
+  let* coq_config = Coq_config.make ~coqc:(Ok coqc) in
   match coq_config with
   | Error msg ->
     User_warning.emit

src/dune_rules/coq/coq_rules.ml

@@ -117,11 +117,11 @@ let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) =
     then Memo.return Coq_mode.VoOnly
     else
       let* coqc = coqc ~sctx ~dir ~loc:buildable.loc in
-      let+ config = Coq_config.Config.make ~coqc in
+      let+ config = Coq_config.make ~coqc in
       (match config with
        | Error _ -> Coq_mode.VoOnly
        | Ok config ->
-         (match Coq_config.Config.by_name config "coq_native_compiler_default" with
+         (match Coq_config.by_name config "coq_native_compiler_default" with
           | Some (String "yes") | Some (String "ondemand") -> Coq_mode.Native
           | _ -> Coq_mode.VoOnly))
 ;;