diff --git a/src/dune_rules/coq_config.ml b/src/dune_rules/coq_config.ml index 4c154fb4d37..0a9e230e9eb 100644 --- a/src/dune_rules/coq_config.ml +++ b/src/dune_rules/coq_config.ml @@ -17,8 +17,6 @@ module Vars : sig val get_path : t -> string -> Path.t - val get_bool : t -> ?default:bool -> string -> bool - val of_lines : string list -> (t, User_message.Style.t Pp.t) result exception E of User_message.Style.t Pp.t @@ -53,14 +51,6 @@ end = struct | None -> fail "Variable %S not found." var let get_path t var = get t var |> Path.of_string - - let get_bool t ?(default = false) var = - match get_opt t var with - | None -> default - | Some s -> ( - match String.uncapitalize s with - | "true" | "yes" | "1" -> true - | _ -> default) end module Version = struct @@ -76,11 +66,7 @@ module Version = struct let regex = let open Re in seq - [ rep digit |> group - ; char '.' - ; rep digit |> group - ; rep any |> group - ] + [ rep digit |> group; char '.'; rep digit |> group; rep any |> group ] |> compile in let open Result.O in @@ -102,7 +88,7 @@ module Version = struct | None -> Result.Error Pp.(textf "Could not parse int: %S." minor) in let suffix = Group.get groups 3 in - Result.Ok { major; minor; suffix} + Result.Ok { major; minor; suffix } let by_name { major; minor; suffix } name : Value.t option = match name with @@ -160,13 +146,6 @@ end type t = { version_info : (Version.t, User_message.Style.t Pp.t) Result.t ; coqlib : Path.t - ; coqcorelib : Path.t - ; docdir : Path.t - ; ocamlfind : Path.t - ; camlflags : string - ; warn : string - ; hasnatdynlink : bool - ; coq_src_subdirs : string list ; coq_native_compiler_default : string } @@ -197,44 +176,14 @@ let make ~bin = ] | Ok vars -> let coqlib = Vars.get_path vars "COQLIB" in - let coqcorelib = Vars.get_path vars "COQCORELIB" in - let docdir = Vars.get_path vars "DOCDIR" in - let ocamlfind = Vars.get_path vars "OCAMLFIND" in - let camlflags = Vars.get vars "CAMLFLAGS" in - let warn = Vars.get vars "WARN" in - let hasnatdynlink = Vars.get_bool vars "HASNATDYNLINK" in - let coq_src_subdirs = - Vars.get vars "COQ_SRC_SUBDIRS" |> String.split ~on:' ' - in let coq_native_compiler_default = Vars.get vars "COQ_NATIVE_COMPILER_DEFAULT" in - { version_info - ; coqlib - ; coqcorelib - ; docdir - ; ocamlfind - ; camlflags - ; warn - ; hasnatdynlink - ; coq_src_subdirs - ; coq_native_compiler_default - } + { version_info; coqlib; coq_native_compiler_default } -let by_name - { version_info - ; coqlib - ; coqcorelib - ; docdir - ; ocamlfind - ; camlflags - ; warn - ; hasnatdynlink - ; coq_src_subdirs - ; coq_native_compiler_default - } name : Value.t option = +let by_name { version_info; coqlib; coq_native_compiler_default } name : + Value.t option = match name with - (* TODO check names *) | "version.major" | "version.minor" | "version.revision" @@ -242,12 +191,5 @@ let by_name | "version" | "ocaml-version" -> Version.by_name version_info name | "coqlib" -> Some (Path coqlib) - | "coqcorelib" -> Some (Path coqcorelib) - | "docdir" -> Some (Path docdir) - | "ocamlfind" -> Some (Path ocamlfind) - | "camlflags" -> Some (String camlflags) - | "warn" -> Some (String warn) - | "hasnatdynlink" -> Some (Bool hasnatdynlink) - | "coq_src_subdirs" -> Some (Strings coq_src_subdirs) | "coq_native_compiler_default" -> Some (String coq_native_compiler_default) | _ -> None diff --git a/test/blackbox-tests/test-cases/coq/coq-config.t/dune b/test/blackbox-tests/test-cases/coq/coq-config.t/dune index 38898568da7..fe61d87f955 100644 --- a/test/blackbox-tests/test-cases/coq/coq-config.t/dune +++ b/test/blackbox-tests/test-cases/coq/coq-config.t/dune @@ -4,25 +4,26 @@ config.output (progn (echo "COQLIB=%{coq:coqlib}\n") - (echo "COQCORELIB=%{coq:coqcorelib}\n") - (echo "DOCDIR=%{coq:docdir}\n") - (echo "OCAMLFIND=%{coq:ocamlfind}\n") - (echo "CAMLFLAGS=%{coq:camlflags}\n") - (echo "WARN=%{coq:warn}\n") - (echo "HASNATDYNLINK=%{coq:hasnatdynlink}\n") - (echo "COQ_SRC_SUBDIRS=%{coq:coq_src_subdirs}\n") (echo "COQ_NATIVE_COMPILER_DEFAULT=%{coq:coq_native_compiler_default}\n") (echo "") - (echo "The Coq Proof Assistant, version %{coq:version}\n") - (echo "compiled with OCaml %{coq:ocaml-version}\n") - (echo "The Coq Proof Assistant, version %{coq:version.major}.%{coq:version.minor}%{coq:version.suffix}\n") - (echo "compiled with OCaml %{coq:ocaml-version}\n"))))) + (echo "%{coq:version} %{coq:ocaml-version}\n") + (echo + "%{coq:version.major}.%{coq:version.minor}%{coq:version.suffix} %{coq:ocaml-version}\n"))))) (rule (action (with-outputs-to config.expected (progn - (run %{bin:coqc} --config) - (run %{bin:coqc} --version) - (run %{bin:coqc} --version))))) + (pipe-outputs + ; We need to scrub ignored config values + (run %{bin:coqc} --config) + (run sed "/^COQCORELIB=/d") + (run sed "/^DOCDIR=/d") + (run sed "/^OCAMLFIND=/d") + (run sed "/^CAMLFLAGS=/d") + (run sed "/^WARN=/d") + (run sed "/^HASNATDYNLINK=/d") + (run sed "/^COQ_SRC_SUBDIRS=/d")) + (run %{bin:coqc} -print-version) + (run %{bin:coqc} -print-version))))) diff --git a/test/blackbox-tests/test-cases/coq/coq-config.t/run.t b/test/blackbox-tests/test-cases/coq/coq-config.t/run.t index 27e49eee805..12246201342 100644 --- a/test/blackbox-tests/test-cases/coq/coq-config.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coq-config.t/run.t @@ -1,6 +1,8 @@ -We test the coq-config macro +Testing the Coq macro $ dune build - $ diff _build/default/config.output _build/default/config.expected + $ cd _build/default +Testing the output of the version and configuration values + $ diff config.output config.expected