From e4cd8ee893296e59bc796a6f160e33528d0ac907 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 12 Nov 2024 16:27:15 +0100 Subject: [PATCH] Declare ML Module allow plugin names not containing `.` NB we stop calling `expand_path_macros` on the string as plugin names are not paths anymore. --- .../proof-engine/vernacular-commands.rst | 1 - vernac/mltop.ml | 32 ++++++++++++------- vernac/synterp.ml | 22 ------------- 3 files changed, 20 insertions(+), 35 deletions(-) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 2b52c357ae0b..ef9a620e7b93 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -662,7 +662,6 @@ file is a particular case of a module called a *library file*. Loads OCaml plugins and their dependencies dynamically. The :n:`@string` arguments must be valid `findlib `_ plugin names, for example ``coq-core.plugins.ltac``. - They must also contain a `.` to disambiguate against the removed non-findlib loading method. Effects (such as adding new commands) from the explicitly requested plugin are activated, but effects from implicitly loaded diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 0ddb3148e96a..3911ceb3f555 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -31,9 +31,6 @@ open Pp module Fl_internals = struct - (* Check that [m] is a findlib library name *) - let validate_lib_name m = String.index_opt m '.' <> None - (* Fl_split.in_words is not exported *) let fl_split_in_words s = (* splits s in words separated by commas and/or whitespace *) @@ -106,13 +103,6 @@ end = struct module Errors = struct - let plugin_name_should_contain_dot m = - CErrors.user_err - Pp.(str Format.(asprintf "%s is not a valid plugin name anymore." m) ++ spc() ++ - str "Plugins should be loaded using their public name" ++ spc () ++ - str "according to findlib, for example package-name.foo and not " ++ - str "foo_plugin.") - let plugin_name_invalid_format m = CErrors.user_err Pp.(str Format.(asprintf "%s is not a valid plugin name." m) ++ spc () ++ @@ -125,8 +115,6 @@ end = struct let of_package m = match String.split_on_char ':' m with | [ lib ] -> - if not (Fl_internals.validate_lib_name lib) - then Errors.plugin_name_should_contain_dot lib; { lib } | ([] | _ :: _) -> Errors.plugin_name_invalid_format m @@ -392,8 +380,28 @@ let inMLModule : ml_module_object -> Libobject.obj = subst_function = (fun (_,o) -> o); classify_function = classify_ml_objects } +let warn_legacy_loading = + let name = "legacy-loading-removed" in + CWarnings.create ~name (fun name -> + Pp.(str "Legacy loading plugin method has been removed from Coq, \ + and the `:` syntax is deprecated, and its first \ + argument ignored; please remove \"" ++ + str name ++ str ":\" from your Declare ML")) + +let inspect_legacy_decl l = + match String.split_on_char ':' l with + | [lib] -> lib + | [cmxs; lib] -> + warn_legacy_loading cmxs; + lib + | bad -> + let bad = String.concat ":" bad in + CErrors.user_err Pp.(str "bad package name: " ++ str bad ++ str " .") + +let remove_legacy_decls = List.map inspect_legacy_decl let declare_ml_modules local l = + let l = remove_legacy_decls l in let mnames = List.map PluginSpec.of_package l in if Lib.sections_are_opened() then CErrors.user_err Pp.(str "Cannot Declare ML Module while sections are opened."); diff --git a/vernac/synterp.ml b/vernac/synterp.ml index c21287afb50b..b2c52bd1c092 100644 --- a/vernac/synterp.ml +++ b/vernac/synterp.ml @@ -321,30 +321,8 @@ let synterp_require ~intern from export qidl = let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename -let warn_legacy_loading = - let name = "legacy-loading-removed" in - CWarnings.create ~name (fun name -> - Pp.(str "Legacy loading plugin method has been removed from Coq, \ - and the `:` syntax is deprecated, and its first \ - argument ignored; please remove \"" ++ - str name ++ str ":\" from your Declare ML")) - -let inspect_legacy_decl l = - match String.split_on_char ':' l with - | [lib] -> lib - | [cmxs; lib] -> - warn_legacy_loading cmxs; - lib - | bad -> - let bad = String.concat ":" bad in - CErrors.user_err Pp.(str "bad package name: " ++ str bad ++ str " .") - -let remove_legacy_decls = List.map inspect_legacy_decl - let synterp_declare_ml_module ~local l = let local = Option.default false local in - let l = remove_legacy_decls l in - let l = List.map expand l in Mltop.declare_ml_modules local l let warn_chdir = CWarnings.create ~name:"change-dir-deprecated" ~category:Deprecation.Version.v8_20