diff --git a/CHANGES.md b/CHANGES.md index 6ca1ebebb69d..00f496ada777 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -370,6 +370,9 @@ Unreleased diff` command can be used to just display the promotion without applying it. (#6160, fixes #5368, @emillon) +- Coq versions < 8.10 are not supported anymore; Coq build language + versions 0.1 and 0.2 have been removed in consequence (# , @ejgallego) + 3.5.0 (2022-10-19) ------------------ diff --git a/bin/coq/coqtop.ml b/bin/coq/coqtop.ml index dca91c4d4850..b0c6d496b745 100644 --- a/bin/coq/coqtop.ml +++ b/bin/coq/coqtop.ml @@ -85,7 +85,7 @@ let term = let stanza = Dune_rules.Coq_sources.lookup_module coq_src coq_module in - let args, use_stdlib, coq_lang_version, wrapper_name, mode = + let args, use_stdlib, wrapper_name, mode = match stanza with | None -> User_error.raise @@ -96,14 +96,12 @@ let term = ( Dune_rules.Coq_rules.coqtop_args_theory ~sctx ~dir ~dir_contents:dc theory coq_module , theory.buildable.use_stdlib - , theory.buildable.coq_lang_version , Dune_rules.Coq_lib_name.wrapper (snd theory.name) , theory.buildable.mode ) | Some (`Extraction extr) -> ( Dune_rules.Coq_rules.coqtop_args_extraction ~sctx ~dir extr coq_module , extr.buildable.use_stdlib - , extr.buildable.coq_lang_version , "DuneExtraction" , extr.buildable.mode ) in @@ -118,7 +116,7 @@ let term = | Some mode -> mode in Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name - ~mode ~coq_lang_version coq_module + ~mode coq_module in Action_builder.(run deps_of) Eager in diff --git a/doc/coq.rst b/doc/coq.rst index 8291babda40a..0cabc197ec3c 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -134,10 +134,10 @@ The semantics of the fields are: Interproject composition has been available since :ref:`Coq lang 0.4`. - As of today, Dune cannot depend on installed Coq theories. This restriction - will be lifted in the future. Note that composition with the Coq standard - library is supported, but in this case the ``Coq`` prefix has been made - available in a qualified way, since :ref:`Coq lang 0.2`. + As of today, Dune cannot depend on installed Coq theories. This + restriction will be lifted in the future. Note that composition with + the Coq standard library is supported, but in this case the ``Coq`` + prefix is available in a qualified way. You may still use installed libraries in your Coq project, but there is currently no way for Dune to know about it. @@ -254,9 +254,6 @@ file: The supported Coq language versions (not the version of Coq) are: -- ``0.1``: Basic Coq theory support. -- ``0.2``: Support for the ``theories`` field and composition of theories in the - same scope. - ``0.3``: Support for ``(mode native)`` requires Coq >= 8.10 (and Dune >= 2.9 for Coq >= 8.14). - ``0.4``: Support for interproject composition of theories. @@ -267,6 +264,9 @@ The supported Coq language versions (not the version of Coq) are: and ``(mode native)`` is deprecated. The ``dev`` profile also no longer disables native compilation. +Coq language versions ``0.1`` and ``0.2`` have been deprecated in +Dune 3.6, and removed in Dune 3.7. + .. _coq-lang-1.0: Coq Language Version 1.0 diff --git a/doc/hacking.rst b/doc/hacking.rst index 6ac6a7068ee5..03cd19fe23c8 100644 --- a/doc/hacking.rst +++ b/doc/hacking.rst @@ -252,7 +252,7 @@ Such languages must be enabled in the ``dune`` project file separately: .. code:: dune (lang dune 3.8) - (using coq 0.7) + (using coq 0.8) If such extensions are experimental, it's recommended that they pass ``~experimental:true``, and that their versions are below 1.0. diff --git a/src/dune_rules/coq/coq_lib.ml b/src/dune_rules/coq/coq_lib.ml index d0a9d5c8f3e1..f4b9a006f1b8 100644 --- a/src/dune_rules/coq/coq_lib.ml +++ b/src/dune_rules/coq/coq_lib.ml @@ -242,29 +242,6 @@ module Error = struct @@ User_message.make ~annots ~loc ?hints [ Pp.textf "Theory %S has not been found." name ] - module Hidden_reason = struct - type t = - | LackOfTheoryComposition - | LackOfInstalledComposition - end - - let hidden_without_composition ~loc ~reason name = - let name = Coq_lib_name.to_string name in - let reason = - match reason with - | Hidden_reason.LackOfTheoryComposition -> - Pp.textf - "Upgrade coq lang to 0.4 to enable composition with theories in a \ - different scope." - | LackOfInstalledComposition -> - Pp.textf - "Upgrade coq lang to 0.8 to enable composition with installed \ - theories." - in - Resolve.Memo.fail - @@ User_message.make ~annots ~loc - [ Pp.textf "Theory %s not found in the current scope." name; reason ] - let private_deps_not_allowed ~loc name = let name = Coq_lib_name.to_string name in Resolve.Memo.fail @@ -352,16 +329,9 @@ module DB = struct | Some parent -> boot_library_id parent) module rec R : sig - val resolve_boot : - t - -> coq_lang_version:Dune_sexp.Syntax.Version.t - -> (Loc.t * lib) option Resolve.Memo.t - - val resolve : - t - -> coq_lang_version:Dune_sexp.Syntax.Version.t - -> Loc.t * Coq_lib_name.t - -> lib Resolve.Memo.t + val resolve_boot : t -> (Loc.t * lib) option Resolve.Memo.t + + val resolve : t -> Loc.t * Coq_lib_name.t -> lib Resolve.Memo.t end = struct open R @@ -408,20 +378,17 @@ module DB = struct Option.to_list boot @ theories else theories - let resolve_boot ~coq_lang_version ~coq_db (boot_id : Id.t option) = + let resolve_boot ~coq_db (boot_id : Id.t option) = match boot_id with | Some boot_id -> let open Resolve.Memo.O in - let+ lib = - resolve ~coq_lang_version coq_db (boot_id.loc, boot_id.name) - in + let+ lib = resolve coq_db (boot_id.loc, boot_id.name) in Some (boot_id.loc, lib) | None -> Resolve.Memo.return None - let resolve_theory ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id - (loc, theory_name) = + let resolve_theory ~allow_private_deps ~coq_db ~boot_id (loc, theory_name) = let open Resolve.Memo.O in - let* theory = resolve ~coq_lang_version coq_db (loc, theory_name) in + let* theory = resolve coq_db (loc, theory_name) in let* () = Resolve.Memo.lift @@ check_boot ~boot_id theory in let+ () = if allow_private_deps then Resolve.Memo.return () @@ -433,17 +400,13 @@ module DB = struct in (loc, theory) - let resolve_theories ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id - theories = - let f = - resolve_theory ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id - in + let resolve_theories ~allow_private_deps ~coq_db ~boot_id theories = + let f = resolve_theory ~allow_private_deps ~coq_db ~boot_id in Resolve.Memo.List.map theories ~f let create_from_stanza_impl (coq_db, db, dir, (s : Coq_stanza.Theory.t)) = let name = s.name in let id = Id.create ~path:(Path.build dir) ~name in - let coq_lang_version = s.buildable.coq_lang_version in let open Memo.O in let boot_id = if s.boot then None else boot_library_id coq_db in let allow_private_deps = Option.is_none s.package in @@ -452,9 +415,9 @@ module DB = struct resolve_plugins ~db ~allow_private_deps ~name:(snd name) s.buildable.plugins and+ theories = - resolve_theories ~coq_db ~coq_lang_version ~allow_private_deps ~boot_id + resolve_theories ~coq_db ~allow_private_deps ~boot_id s.buildable.theories - and+ boot = resolve_boot ~coq_lang_version ~coq_db boot_id in + and+ boot = resolve_boot ~coq_db boot_id in let theories = maybe_add_boot ~boot ~use_stdlib ~is_boot:s.boot theories in @@ -538,30 +501,20 @@ module DB = struct type t = | Found_stanza of Lib.DB.t * Path.Build.t * Coq_stanza.Theory.t | Found_path of Coq_path.t - | Hidden of Error.Hidden_reason.t | Not_found end - let find coq_db ~coq_lang_version name : Resolve_final_result.t = + let find coq_db name : Resolve_final_result.t = match find coq_db name with | Not_found -> Not_found - | Theory (mldb, dir, stanza) when coq_lang_version >= (0, 4) -> - Found_stanza (mldb, dir, stanza) - | Legacy_theory cp when coq_lang_version >= (0, 8) -> Found_path cp - | Legacy_theory cp when Coq_path.stdlib cp -> Found_path cp - | Legacy_theory _ -> Hidden LackOfInstalledComposition - | Theory (mldb, dir, stanza) -> ( - match coq_db.resolve name with - | Not_found -> Hidden LackOfTheoryComposition - | Theory _ | Redirect _ | Legacy_theory _ -> - Found_stanza (mldb, dir, stanza)) + | Theory (mldb, dir, stanza) -> Found_stanza (mldb, dir, stanza) + | Legacy_theory cp -> Found_path cp (** Our final final resolve is used externally, and should return the library data found from the previous iterations. *) - let resolve coq_db ~coq_lang_version (loc, name) = - match find coq_db ~coq_lang_version name with + let resolve coq_db (loc, name) = + match find coq_db name with | Not_found -> Error.theory_not_found ~loc name - | Hidden reason -> Error.hidden_without_composition ~loc ~reason name | Found_stanza (db, dir, stanza) -> let open Memo.O in let+ theory = create_from_stanza coq_db db dir stanza in @@ -575,9 +528,9 @@ module DB = struct let+ theory = create_from_coqpath ~boot_id cp in Legacy theory - let resolve_boot coq_db ~coq_lang_version = + let resolve_boot coq_db = let boot_id = boot_library_id coq_db in - resolve_boot ~coq_lang_version ~coq_db boot_id + resolve_boot ~coq_db boot_id end include R @@ -664,8 +617,7 @@ module DB = struct { parent; resolve; boot_id } (* Resolve helpers *) - let find_many t theories ~coq_lang_version = - Resolve.Memo.List.map theories ~f:(resolve ~coq_lang_version t) + let find_many t theories = Resolve.Memo.List.map theories ~f:(resolve t) end let theories_closure = function diff --git a/src/dune_rules/coq/coq_lib.mli b/src/dune_rules/coq/coq_lib.mli index ebe1fbcfa89d..ff8981600df3 100644 --- a/src/dune_rules/coq/coq_lib.mli +++ b/src/dune_rules/coq/coq_lib.mli @@ -65,20 +65,9 @@ module DB : sig libraries are installed, we would infer the right amount of information. *) val create_from_coqpaths : Coq_path.t list -> t - val find_many : - t - -> (Loc.t * Coq_lib_name.t) list - -> coq_lang_version:Dune_sexp.Syntax.Version.t - -> lib list Resolve.Memo.t - - val resolve_boot : - t - -> coq_lang_version:Dune_sexp.Syntax.Version.t - -> (Loc.t * lib) option Resolve.Memo.t - - val resolve : - t - -> coq_lang_version:Dune_sexp.Syntax.Version.t - -> Loc.t * Coq_lib_name.t - -> lib Resolve.Memo.t + val find_many : t -> (Loc.t * Coq_lib_name.t) list -> lib list Resolve.Memo.t + + val resolve_boot : t -> (Loc.t * lib) option Resolve.Memo.t + + val resolve : t -> Loc.t * Coq_lib_name.t -> lib Resolve.Memo.t end diff --git a/src/dune_rules/coq/coq_mode.ml b/src/dune_rules/coq/coq_mode.ml index a2ffeffbbe34..195107fc526d 100644 --- a/src/dune_rules/coq/coq_mode.ml +++ b/src/dune_rules/coq/coq_mode.ml @@ -7,7 +7,6 @@ where mode was not supported, this allows us support older Coq compiler versions with coq-lang < 0.3 *) type t = - | Legacy | VoOnly | Native | VosOnly diff --git a/src/dune_rules/coq/coq_mode.mli b/src/dune_rules/coq/coq_mode.mli index f2d227aa9833..4a2eace63d3e 100644 --- a/src/dune_rules/coq/coq_mode.mli +++ b/src/dune_rules/coq/coq_mode.mli @@ -7,7 +7,6 @@ where mode was not supported, this allows us support older Coq compiler versions with coq-lang < 0.3 *) type t = - | Legacy | VoOnly | Native | VosOnly diff --git a/src/dune_rules/coq/coq_module.ml b/src/dune_rules/coq/coq_module.ml index 7b144857dda6..288d69bb2079 100644 --- a/src/dune_rules/coq/coq_module.ml +++ b/src/dune_rules/coq/coq_module.ml @@ -88,7 +88,7 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode = ( Path.Build.relative vo_dir x , Filename.(concat (concat install_vo_dir ".coq-native") x) )) cmxs_obj - | VoOnly | VosOnly | Legacy -> [] + | VoOnly | VosOnly -> [] in let obj_files = match obj_files_mode with diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index b5a7b865d6a6..536ca0c4f6f1 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/src/dune_rules/coq/coq_rules.ml @@ -18,11 +18,7 @@ module Util : sig val ml_pack_files : Lib.t -> Path.t list val meta_info : - loc:Loc.t option - -> version:int * int - -> context:Context_name.t - -> Lib.t - -> Path.t option + loc:Loc.t option -> context:Context_name.t -> Lib.t -> Path.t option (** Given a list of library names, we try to resolve them in order, returning the first one that exists. *) @@ -56,7 +52,7 @@ end = struct in List.concat_map plugins ~f:to_mlpack - let meta_info ~loc ~version ~context (lib : Lib.t) = + let meta_info ~loc ~context (lib : Lib.t) = let name = Lib.name lib |> Lib_name.to_string in match Lib_info.status (Lib.info lib) with | Public (_, pkg) -> @@ -69,11 +65,10 @@ end = struct Some (Path.build meta_i) | Installed -> None | Installed_private | Private _ -> - let is_error = version >= (0, 6) in - let text = if is_error then "not supported" else "deprecated" in - User_warning.emit ?loc ~is_error - [ Pp.textf "Using private library %s as a Coq plugin is %s" name text ]; - None + User_error.raise ?loc + [ Pp.textf "Using private library %s as a Coq plugin is not supported" + name + ] (* CR alizter: move this to Lib.DB *) @@ -96,24 +91,16 @@ let coqc ~loc ~dir ~sctx = let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) = match buildable.mode with - | Some x -> - if - buildable.coq_lang_version < (0, 7) - && Profile.is_dev (Super_context.context sctx).profile - then Memo.return Coq_mode.VoOnly - else Memo.return x + | Some x -> Memo.return x | None -> ( - if buildable.coq_lang_version < (0, 3) then Memo.return Coq_mode.Legacy - else if buildable.coq_lang_version < (0, 7) then Memo.return Coq_mode.VoOnly - else - let* coqc = coqc ~sctx ~dir ~loc:buildable.loc in - let+ config = Coq_config.make_opt ~coqc in - match config with - | None -> Coq_mode.VoOnly - | Some config -> ( - match Coq_config.by_name config "coq_native_compiler_default" with - | Some (String "yes") | Some (String "ondemand") -> Coq_mode.Native - | _ -> Coq_mode.VoOnly)) + let* coqc = coqc ~sctx ~dir ~loc:buildable.loc in + let+ config = Coq_config.make_opt ~coqc in + match config with + | None -> Coq_mode.VoOnly + | Some config -> ( + match Coq_config.by_name config "coq_native_compiler_default" with + | Some (String "yes") | Some (String "ondemand") -> Coq_mode.Native + | _ -> Coq_mode.VoOnly)) let coq_flags ~dir ~stanza_flags ~expander ~sctx = let open Action_builder.O in @@ -132,17 +119,16 @@ let theories_flags ~theories_deps = let+ libs = theories_deps in Command.Args.S (List.map ~f:theory_coqc_flag libs)) -let boot_flags ~coq_lang_version t : _ Command.Args.t = - let boot_flag = if coq_lang_version >= (0, 8) then [ "-boot" ] else [] in +let boot_flags t : _ Command.Args.t = match t with (* We are compiling the prelude itself [should be replaced with (per_file ...) flags] *) - | `Bootstrap_prelude -> As ("-noinit" :: boot_flag) + | `Bootstrap_prelude -> As [ "-noinit"; "-boot" ] (* No special case *) - | `No_boot | `Bootstrap _ -> As boot_flag + | `No_boot | `Bootstrap _ -> As [ "-boot" ] -let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags - ~coq_lang_version : _ Command.Args.t list = +let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags : + _ Command.Args.t list = let file_flags : _ Command.Args.t list = [ Dyn (Resolve.Memo.read ml_flags) ; theories_flags ~theories_deps @@ -151,7 +137,7 @@ let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags ; A wrapper_name ] in - [ boot_flags ~coq_lang_version boot_type; S file_flags ] + [ boot_flags boot_type; S file_flags ] let native_includes ~dir = let* scope = Scope.DB.find_by_dir dir in @@ -197,7 +183,6 @@ let setup_native_theory_includes ~sctx ~theories_deps ~theory_dirs = let coqc_native_flags ~sctx ~dir ~theories_deps ~theory_dirs ~(mode : Coq_mode.t) = match mode with - | Legacy -> Command.Args.empty | VoOnly -> Command.Args.As [ "-w" @@ -274,11 +259,8 @@ let ml_pack_and_meta_rule ~context ~all_libs (buildable : Coq_stanza.Buildable.t) : unit Action_builder.t = (* coqdep expects an mlpack file next to the sources otherwise it will omit the cmxs deps *) - let coq_lang_version = buildable.coq_lang_version in let plugin_loc = List.hd_opt buildable.plugins |> Option.map ~f:fst in - let meta_info = - Util.meta_info ~loc:plugin_loc ~version:coq_lang_version ~context - in + let meta_info = Util.meta_info ~loc:plugin_loc ~context in (* If the mlpack files don't exist, don't fail *) Action_builder.all_unit [ Action_builder.paths (List.filter_map ~f:meta_info all_libs) @@ -312,12 +294,10 @@ let ml_flags_and_ml_pack_rule ~context ~lib_db ~theories_deps and add `Init.Prelude.vo` as a dependency; there is a further special case when compiling the prelude, in this case we also need to tell Coq not to try to load the prelude. *) -let boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module = +let boot_type ~dir ~use_stdlib ~wrapper_name coq_module = let* scope = Scope.DB.find_by_dir dir in let+ boot_lib = - scope |> Scope.coq_libs - |> Coq_lib.DB.resolve_boot ~coq_lang_version - |> Resolve.Memo.read_memo + scope |> Scope.coq_libs |> Coq_lib.DB.resolve_boot |> Resolve.Memo.read_memo in if use_stdlib then match boot_lib with @@ -341,22 +321,20 @@ let dep_theory_file ~dir ~wrapper_name = |> Path.Build.set_extension ~ext:".theory.d" let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name - ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule ~coq_lang_version - coq_modules = + ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule coq_modules = let* boot_type = (* If coq_modules are empty it doesn't really matter, so we take the more conservative path and pass -boot, we don't care here about -noinit as coqdep ignores it *) match coq_modules with | [] -> Memo.return `Bootstrap_prelude - | m :: _ -> boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version m + | m :: _ -> boot_type ~dir ~use_stdlib ~wrapper_name m in (* coqdep needs the full source + plugin's mlpack to be present :( *) let sources = List.rev_map ~f:Coq_module.source coq_modules in let file_flags = [ Command.Args.S - (coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags - ~coq_lang_version) + (coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags) ; As [ "-dyndep"; "opt"; "-vos" ] ; Deps sources ] @@ -441,8 +419,7 @@ let deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module = Action_builder.paths deps let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog - ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs ~coq_lang_version - coq_module = + ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs coq_module = let+ coq_stanza_flags = let+ expander = Super_context.expander sctx ~dir in let coq_flags = @@ -475,7 +452,6 @@ let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog in let file_flags = coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags - ~coq_lang_version in match coq_prog with | `Coqc -> @@ -488,11 +464,9 @@ let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog let setup_coqc_rule ~loc ~dir ~sctx ~coqc_dir ~file_targets ~stanza_flags ~theories_deps ~mode ~wrapper_name ~use_stdlib ~ml_flags ~theory_dirs - ~coq_lang_version coq_module = + coq_module = (* Process coqdep and generate rules *) - let* boot_type = - boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module - in + let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in let* coqc = coqc ~loc ~dir ~sctx in let obj_files = Coq_module.obj_files ~wrapper_name ~mode ~obj_files_mode:Coq_module.Build @@ -502,8 +476,7 @@ let setup_coqc_rule ~loc ~dir ~sctx ~coqc_dir ~file_targets ~stanza_flags let target_obj_files = Command.Args.Hidden_targets obj_files in let* args = generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~stanza_flags ~ml_flags - ~theories_deps ~theory_dirs ~mode ~coq_lang_version ~coq_prog:`Coqc - coq_module + ~theories_deps ~theory_dirs ~mode ~coq_prog:`Coqc coq_module in let deps_of = deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module in let open Action_builder.With_targets.O in @@ -636,10 +609,10 @@ let setup_coqdoc_rules ~sctx ~dir ~theories_deps (s : Coq_stanza.Theory.t) rule `Html >>> rule `Latex (* Common context for a theory, deps and rules *) -let theory_context ~context ~scope ~coq_lang_version ~name buildable = +let theory_context ~context ~scope ~name buildable = let theory = let coq_lib_db = Scope.coq_libs scope in - Coq_lib.DB.resolve coq_lib_db ~coq_lang_version name + Coq_lib.DB.resolve coq_lib_db name in let theories_deps = Resolve.Memo.bind theory ~f:(fun theory -> @@ -653,17 +626,15 @@ let theory_context ~context ~scope ~coq_lang_version ~name buildable = (theory, theories_deps, ml_flags, mlpack_rule) (* Common context for extraction, almost the same than above *) -let extraction_context ~context ~scope ~coq_lang_version - (buildable : Coq_stanza.Buildable.t) = +let extraction_context ~context ~scope (buildable : Coq_stanza.Buildable.t) = let coq_lib_db = Scope.coq_libs scope in let theories_deps = - Resolve.Memo.List.map buildable.theories - ~f:(Coq_lib.DB.resolve coq_lib_db ~coq_lang_version) + Resolve.Memo.List.map buildable.theories ~f:(Coq_lib.DB.resolve coq_lib_db) in (* Extraction requires a boot library so we do this unconditionally - for now. We must do this because it can happne that + for now. We must do this because it can happen that s.buildable.theories is empty *) - let boot = Coq_lib.DB.resolve_boot ~coq_lang_version coq_lib_db in + let boot = Coq_lib.DB.resolve_boot coq_lib_db in let theories_deps = let open Resolve.Memo.O in let+ boot = boot @@ -680,11 +651,10 @@ let extraction_context ~context ~scope ~coq_lang_version let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) = let* scope = Scope.DB.find_by_dir dir in - let coq_lang_version = s.buildable.coq_lang_version in let name = s.name in let theory, theories_deps, ml_flags, mlpack_rule = let context = Super_context.context sctx |> Context.name in - theory_context ~context ~scope ~coq_lang_version ~name s.buildable + theory_context ~context ~scope ~name s.buildable in let wrapper_name = Coq_lib_name.wrapper (snd s.name) in let use_stdlib = s.buildable.use_stdlib in @@ -711,39 +681,35 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) = let* mode = select_native_mode ~sctx ~dir s.buildable in (* First we setup the rule calling coqdep *) setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name - ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule ~coq_lang_version - coq_modules + ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule coq_modules >>> Memo.parallel_iter coq_modules ~f: (setup_coqc_rule ~loc ~dir ~sctx ~file_targets:[] ~stanza_flags ~coqc_dir ~theories_deps ~mode ~wrapper_name ~use_stdlib ~ml_flags - ~coq_lang_version ~theory_dirs) + ~theory_dirs) (* And finally the coqdoc rules *) >>> setup_coqdoc_rules ~sctx ~dir ~theories_deps s coq_modules let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) coq_module = let* scope = Scope.DB.find_by_dir dir in - let coq_lang_version = s.buildable.coq_lang_version in let name = s.name in let _theory, theories_deps, ml_flags, _mlpack_rule = let context = Super_context.context sctx |> Context.name in - theory_context ~context ~scope ~coq_lang_version ~name s.buildable + theory_context ~context ~scope ~name s.buildable in let wrapper_name = Coq_lib_name.wrapper (snd s.name) in let* mode = select_native_mode ~sctx ~dir s.buildable in let name = snd s.name in let use_stdlib = s.buildable.use_stdlib in - let* boot_type = - boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module - in + let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in let* coq_dir_contents = Dir_contents.coq dir_contents in let theory_dirs = Coq_sources.directories coq_dir_contents ~name |> Path.Build.Set.of_list in generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog:`Coqtop ~stanza_flags:s.buildable.flags ~ml_flags ~theories_deps ~theory_dirs - ~coq_lang_version coq_module + coq_module (******************************************************************************) (* Install rules *) @@ -868,11 +834,10 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents in let loc = s.buildable.loc in let use_stdlib = s.buildable.use_stdlib in - let coq_lang_version = s.buildable.coq_lang_version in let* scope = Scope.DB.find_by_dir dir in let theories_deps, ml_flags, mlpack_rule = let context = Super_context.context sctx |> Context.name in - extraction_context ~context ~scope ~coq_lang_version s.buildable + extraction_context ~context ~scope s.buildable in let source_rule = let open Action_builder.O in @@ -882,35 +847,30 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents in let* mode = select_native_mode ~sctx ~dir s.buildable in setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name - ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule ~coq_lang_version - [ coq_module ] + ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule [ coq_module ] >>> setup_coqc_rule ~file_targets ~stanza_flags:s.buildable.flags ~sctx ~loc ~coqc_dir:dir coq_module ~dir ~theories_deps ~mode ~wrapper_name - ~use_stdlib:s.buildable.use_stdlib ~ml_flags ~coq_lang_version + ~use_stdlib:s.buildable.use_stdlib ~ml_flags ~theory_dirs:Path.Build.Set.empty let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module = let use_stdlib = s.buildable.use_stdlib in - let coq_lang_version = s.buildable.coq_lang_version in let* scope = Scope.DB.find_by_dir dir in let theories_deps, ml_flags, _mlpack_rule = let context = Super_context.context sctx |> Context.name in - extraction_context ~context ~scope ~coq_lang_version s.buildable + extraction_context ~context ~scope s.buildable in let wrapper_name = "DuneExtraction" in - let* boot_type = - boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module - in + let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in let* mode = select_native_mode ~sctx ~dir s.buildable in generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog:`Coqtop ~stanza_flags:s.buildable.flags ~ml_flags ~theories_deps - ~theory_dirs:Path.Build.Set.empty ~coq_lang_version coq_module + ~theory_dirs:Path.Build.Set.empty coq_module (* Version for export *) -let deps_of ~dir ~use_stdlib ~wrapper_name ~mode ~coq_lang_version coq_module = +let deps_of ~dir ~use_stdlib ~wrapper_name ~mode coq_module = let open Action_builder.O in let* boot_type = - Action_builder.of_memo - (boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module) + Action_builder.of_memo (boot_type ~dir ~use_stdlib ~wrapper_name coq_module) in deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module diff --git a/src/dune_rules/coq/coq_rules.mli b/src/dune_rules/coq/coq_rules.mli index e1ea1c8feba1..3edf42463577 100644 --- a/src/dune_rules/coq/coq_rules.mli +++ b/src/dune_rules/coq/coq_rules.mli @@ -14,7 +14,6 @@ val deps_of : -> use_stdlib:bool -> wrapper_name:string -> mode:Coq_mode.t - -> coq_lang_version:Dune_sexp.Syntax.Version.t -> Coq_module.t -> unit Dune_engine.Action_builder.t diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml index 1d49ad22b839..d465c8644816 100644 --- a/src/dune_rules/coq/coq_stanza.ml +++ b/src/dune_rules/coq/coq_stanza.ml @@ -13,17 +13,14 @@ let coq_syntax = ; ((0, 8), `Since (3, 8)) ] -let already_warned = ref false - let get_coq_syntax () = let* version = Dune_lang.Syntax.get_exn coq_syntax in - if version < (0, 8) && not !already_warned then ( - already_warned := true; - User_warning.emit + if version < (0, 8) then + User_error.raise [ Pp.text - "Coq Language Versions lower than 0.8 have been deprecated in Dune \ - 3.8 and will be removed in Dune 3.9" - ]); + "Coq Language Versions lower than 0.8 have been removed in Dune 3.8, \ + please upgrade to (coq lang 0.8) or later if available" + ]; return version module Coqpp = struct @@ -85,11 +82,7 @@ module Buildable = struct >>> repeat (located Lib_name.decode)) and+ plugins = field "plugins" (repeat (located Lib_name.decode)) ~default:[] - and+ theories = - field "theories" - (Dune_lang.Syntax.since coq_syntax (0, 2) >>> repeat Coq_lib_name.decode) - ~default:[] - in + and+ theories = field "theories" (repeat Coq_lib_name.decode) ~default:[] in let plugins = merge_plugins_libraries ~plugins ~libraries in { flags; mode; use_stdlib; coq_lang_version; plugins; theories; loc } end diff --git a/test/blackbox-tests/test-cases/coq/base-unsound.t/dune-project b/test/blackbox-tests/test-cases/coq/base-unsound.t/dune-project index 1735137151ce..23ca7faaa0e5 100644 --- a/test/blackbox-tests/test-cases/coq/base-unsound.t/dune-project +++ b/test/blackbox-tests/test-cases/coq/base-unsound.t/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.7) +(lang dune 2.8) -(using coq 0.1) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/base.t/dune b/test/blackbox-tests/test-cases/coq/base.t/dune index 2f52deff96df..22abdac08fcc 100644 --- a/test/blackbox-tests/test-cases/coq/base.t/dune +++ b/test/blackbox-tests/test-cases/coq/base.t/dune @@ -4,6 +4,6 @@ (modules :standard) (synopsis "Test Coq library")) -(alias - (name default) +(rule + (alias default) (action (echo "%{read:base.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/base.t/dune-project b/test/blackbox-tests/test-cases/coq/base.t/dune-project index ec6655bea0e9..23ca7faaa0e5 100644 --- a/test/blackbox-tests/test-cases/coq/base.t/dune-project +++ b/test/blackbox-tests/test-cases/coq/base.t/dune-project @@ -1,3 +1,3 @@ -(lang dune 1.9) +(lang dune 2.8) -(using coq 0.1) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project index 9ef6b81a34a1..23ca7faaa0e5 100644 --- a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.5) +(lang dune 2.8) -(using coq 0.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project index 9ef6b81a34a1..23ca7faaa0e5 100644 --- a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.5) +(lang dune 2.8) -(using coq 0.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/A/dune-project index 9ef6b81a34a1..23ca7faaa0e5 100644 --- a/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/A/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/A/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.5) +(lang dune 2.8) -(using coq 0.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/B/dune-project index 9ef6b81a34a1..23ca7faaa0e5 100644 --- a/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/B/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/B/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.5) +(lang dune 2.8) -(using coq 0.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-plugin.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-plugin.t/dune-project index 9ef6b81a34a1..23ca7faaa0e5 100644 --- a/test/blackbox-tests/test-cases/coq/compose-plugin.t/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-plugin.t/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.5) +(lang dune 2.8) -(using coq 0.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project index 9ef6b81a34a1..23ca7faaa0e5 100644 --- a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.5) +(lang dune 2.8) -(using coq 0.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/extract.t b/test/blackbox-tests/test-cases/coq/extract.t index 3658985f2514..52744a80c38b 100644 --- a/test/blackbox-tests/test-cases/coq/extract.t +++ b/test/blackbox-tests/test-cases/coq/extract.t @@ -1,6 +1,6 @@ $ cat >dune-project < (lang dune 2.5) - > (using coq 0.2) + > (lang dune 2.8) + > (using coq 0.3) > EOF $ cat >extract.v <