stdlib: add generated All.v requiring everything in stdlib

doc/changelog/11-standard-library/19914-stdlib-all.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  `Stdlib.All` which does `Require Export` of all other files in the stdlib
+  (`#19914 <https://github.com/coq/coq/pull/19914>`_,
+  by Gaëtan Gilbert).

stdlib/theories/dune

@@ -2,3 +2,8 @@
 (coq.theory
  (name Stdlib)
  (package coq-stdlib))
+
+(rule
+ (targets All.v)
+ (deps (source_tree .))
+ (action (with-stdout-to %{targets} (run ../tools/gen_all.exe))))

stdlib/tools/dune

@@ -0,0 +1,3 @@
+(executable
+ (name gen_all)
+ (libraries unix))

stdlib/tools/gen_all.ml

@@ -0,0 +1,52 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let from = "Stdlib"
+
+let () = Printf.printf "Set Warnings \"-deprecated-library-file,-warn-library-file\".\n\n"
+
+let () = Printf.printf "From %s Require\n" from
+
+let logical_concat prefix f =
+  let f = Filename.remove_extension f in
+  match prefix with
+  | "" -> f
+  | _ -> String.concat "." [prefix; f]
+
+let rec traverse todo todo' = match todo, todo' with
+  | [], [] -> ()
+  |  [], todo :: todo' -> traverse todo todo'
+  | (path,logical) :: todo, todo' ->
+    let todo' = match (Unix.stat path).st_kind with
+      | exception Unix.Unix_error _ -> todo'
+      | S_DIR ->
+        let contents = try Sys.readdir path with Sys_error _ -> [||] in
+        (* sort to get a reproducible ordering *)
+        let () = Array.sort String.compare contents in
+        let contents = Array.to_list contents in
+        let contents = List.map (fun fname ->
+            Filename.concat path fname, logical_concat logical fname)
+            contents
+        in
+        (contents :: todo')
+      | S_REG ->
+        let () =
+          if Filename.extension path = ".v" &&
+             logical <> "All"
+          then Printf.printf "  %s\n" logical
+        in
+        todo'
+      | _ -> todo'
+    in
+    traverse todo todo'
+
+let () = traverse [".", ""] []
+
+let () = Printf.printf ".\n%!"