diff --git a/doc/changes/10631.md b/doc/changes/10631.md new file mode 100644 index 00000000000..b5fef319c0d --- /dev/null +++ b/doc/changes/10631.md @@ -0,0 +1,2 @@ +- Don't depend on coq-stdlib being installed when expanding variables + of the `coq.version` family (#10631, fixes #10629, @gares) \ No newline at end of file diff --git a/src/dune_rules/coq/coq_config.ml b/src/dune_rules/coq/coq_config.ml index 3e3d3c77855..eee4107e8a4 100644 --- a/src/dune_rules/coq/coq_config.ml +++ b/src/dune_rules/coq/coq_config.ml @@ -154,7 +154,7 @@ module Version = struct Return bin (* we pass -boot since this means it will work with just coq-core *) - [ "--print-version"; "-boot" ] + [ "--print-version"; "-boot"; "-noinit" ] ;; let version_memo = Memo.create "coq-and-ocaml-version" ~input:(module Path) impl_version @@ -183,24 +183,20 @@ module Version = struct { version_num; version_string; ocaml_version_string } ;; - let by_name t name = - match t with - | Error msg -> User_error.raise Pp.[ textf "Could not parse coqc version: "; msg ] - | Ok { version_num; version_string; ocaml_version_string } -> - (match name with - | "version.major" -> Num.by_name version_num "major" - | "version.minor" -> Num.by_name version_num "minor" - | "version.revision" -> Num.by_name version_num "revision" - | "version.suffix" -> Num.by_name version_num "suffix" - | "version" -> Some (Value.string version_string) - | "ocaml-version" -> Some (Value.string ocaml_version_string) - | _ -> None) + let by_name { version_num; version_string; ocaml_version_string } name = + match name with + | "version.major" -> Num.by_name version_num "major" + | "version.minor" -> Num.by_name version_num "minor" + | "version.revision" -> Num.by_name version_num "revision" + | "version.suffix" -> Num.by_name version_num "suffix" + | "version" -> Some (Value.string version_string) + | "ocaml-version" -> Some (Value.string ocaml_version_string) + | _ -> None ;; end type t = - { version_info : (Version.t, User_message.Style.t Pp.t) Result.t - ; coqlib : Path.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 *) } @@ -221,19 +217,11 @@ let impl_config bin = let config_memo = Memo.create "coq-config" ~input:(module Path) impl_config -let version ~coqc = - let open Memo.O in - let+ t = Version.make ~coqc in - let open Result.O in - let+ t = t in - t.version_string -;; - 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 - and+ version_info = Version.make ~coqc in + in let open Result.O in let* config_output = config_output in match Vars.of_lines config_output with @@ -243,19 +231,13 @@ let make ~(coqc : Action.Prog.t) = 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 { version_info; coqlib; coqcorelib; coq_native_compiler_default } + Ok { coqlib; coqcorelib; coq_native_compiler_default } | Error msg -> User_error.raise Pp.[ textf "Cannot parse output of coqc --config:"; msg ] ;; -let by_name { version_info; coqlib; coqcorelib; coq_native_compiler_default } name = +let by_name { coqlib; coqcorelib; coq_native_compiler_default } name = match name with - | "version.major" - | "version.minor" - | "version.revision" - | "version.suffix" - | "version" - | "ocaml-version" -> Version.by_name version_info name | "coqlib" -> Some (Value.path coqlib) | "coqcorelib" -> Option.map ~f:Value.path coqcorelib | "coq_native_compiler_default" -> @@ -270,25 +252,34 @@ let expand source macro artifacts_host = let s = Pform.Macro_invocation.Args.whole macro in let open Memo.O in let* coqc = Artifacts.binary artifacts_host ~where:Original_path ~loc:None "coqc" in - let+ t = make ~coqc in - match t with - | Error msg -> - User_error.raise - ~loc:(Dune_lang.Template.Pform.loc source) - [ Pp.textf "Could not expand %%{coq:%s} as running coqc --config failed." s; msg ] - ~hints: - [ Pp.textf - "coqc --config requires the coq-stdlib package in order to function properly." - ] - | Ok t -> - (match by_name t s with - | None -> - User_error.raise - ~loc:(Dune_lang.Template.Pform.loc source) - [ Pp.textf "Unknown Coq configuration variable %S" s ] - | Some v -> - (match v with - | Int x -> [ Dune_lang.Value.String (string_of_int x) ] - | String x -> [ String x ] - | Path x -> Dune_lang.Value.L.paths [ x ])) + let expand m k s = + let+ t = m ~coqc in + match t with + | Error msg -> + User_error.raise + ~loc:(Dune_lang.Template.Pform.loc source) + [ Pp.textf "Could not expand %%{coq:%s} as running coqc failed." s; msg ] + | Ok t -> + (match k t s with + | None -> + User_error.raise + ~loc:(Dune_lang.Template.Pform.loc source) + [ Pp.textf "Unknown Coq configuration variable %S" s ] + | Some v -> + let open Value in + (match v with + | Int x -> [ Dune_lang.Value.String (string_of_int x) ] + | String x -> [ Dune_lang.Value.String x ] + | Path x -> Dune_lang.Value.L.paths [ x ])) + in + match s with + | "version.major" + | "version.minor" + | "version.revision" + | "version.suffix" + | "version" + | "ocaml-version" -> expand Version.make Version.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 ] ;; diff --git a/src/dune_rules/coq/coq_config.mli b/src/dune_rules/coq/coq_config.mli index 72cc5416d31..8f9c848fef3 100644 --- a/src/dune_rules/coq/coq_config.mli +++ b/src/dune_rules/coq/coq_config.mli @@ -1,24 +1,5 @@ open Import -(** Data of a Coq configuration. *) -type t - -(** [version ~coqc] runs coqc --print-version and returns the version of Coq as a string - without having to run coqc --config. Exceptionally, one of the following will happen: - - - Return [Error message] if coqc --print-version exits with a non-zero code. - - Throw a user error if coqc --print-version is not parsable. - - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *) -val version : coqc:Action.Prog.t -> (string, User_message.Style.t Pp.t) result Memo.t - -(** [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 - module Value : sig type t = private | Int of int @@ -31,18 +12,51 @@ module Value : sig val to_dyn : t -> Dyn.t end +module Version : sig + (** Data of a Coq version. *) + type t + + (** [make ~coqc] runs coqc --print-version and returns the version of Coq + and the version of OCaml used to build Coq. + Exceptionally, one of the following will happen: + + - Return [Error message] if coqc --print-version exits with a non-zero code. + - Throw a user error if coqc --print-version 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 field [name] in the Coq + version [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: + + - version.major + - version.minor + - version.revision + - version.suffix + - version + - ocaml-version *) + val by_name : t -> string -> Value.t Option.t +end + +(** Data of a Coq configuration. *) +type t + +(** [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 + (** [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: - - version.major - - version.minor - - version.revision - - version.suffix - - version - - ocaml-version - coqlib - coqcorelib - coq_native_compiler_default *) diff --git a/test/blackbox-tests/test-cases/coq/failed-config.t/run.t b/test/blackbox-tests/test-cases/coq/failed-config.t/run.t index 16d7bd61d79..e2905983d85 100644 --- a/test/blackbox-tests/test-cases/coq/failed-config.t/run.t +++ b/test/blackbox-tests/test-cases/coq/failed-config.t/run.t @@ -101,25 +101,19 @@ Here we query the version of Coq. Due to the expansion of %{coq:_} macros we nee > (echo %{coq:version}))) > EOF -Fails for now, but could be improved in the future. +Succeeds after PR #10631 $ FAIL_CONFIG=1 \ > dune build @version - File "dune", line 4, characters 8-22: - 4 | (echo %{coq:version}))) - ^^^^^^^^^^^^^^ - Error: Could not expand %{coq:version} as running coqc --config failed. - $TESTCASE_ROOT/bin/coqc --config failed with exit code 1. - Hint: coqc --config requires the coq-stdlib package in order to function - properly. - [1] + 8.16.1 Should fail. $ FAIL_VERSION=1 \ > dune build @version - Error: Could not parse coqc version: + File "dune", line 4, characters 8-22: + 4 | (echo %{coq:version}))) + ^^^^^^^^^^^^^^ + Error: Could not expand %{coq:version} as running coqc failed. $TESTCASE_ROOT/bin/coqc --print-version failed with exit code 1. - -> required by %{coq:version} at dune:4 - -> required by alias version in dune:1 [1] Here we query the config. A failing --config will block this value from being realised @@ -139,10 +133,8 @@ Should fail. File "dune", line 4, characters 8-21: 4 | (echo %{coq:coqlib}))) ^^^^^^^^^^^^^ - Error: Could not expand %{coq:coqlib} as running coqc --config failed. + Error: Could not expand %{coq:coqlib} as running coqc failed. $TESTCASE_ROOT/bin/coqc --config failed with exit code 1. - Hint: coqc --config requires the coq-stdlib package in order to function - properly. [1] Should succeed.