From 9193769161e1f06b371eed99dfe9e90fec9a14a6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 5 Feb 2020 17:46:07 +0100 Subject: [build] Consolidate stdlib's .v files under a single directory. Currently, `.v` under the `Coq.` prefix are found in both `theories` and `plugins`. Usually these two directories are merged by special loadpath code that allows double-binding of the prefix. This adds some complexity to the build and loadpath system; and in particular, it prevents from handling the `Coq.*` prefix in the simple, `-R theories Coq` standard way. We thus move all `.v` files to theories, leaving `plugins` as an OCaml-only directory, and modify accordingly the loadpath / build infrastructure. Note that in general `plugins/foo/Foo.v` was not self-contained, in the sense that it depended on files in `theories` and files in `theories` depended on it; moreover, Coq saw all these files as belonging to the same namespace so it didn't really care where they lived. This could also imply a performance gain as we now effectively traverse less directories when locating a library. See also discussion in #10003 --- doc/stdlib/dune | 4 +- doc/stdlib/hidden-files | 180 ++++++++++++++++++------------------ doc/stdlib/index-list.html.template | 10 +- doc/stdlib/make-library-index | 2 +- 4 files changed, 97 insertions(+), 99 deletions(-) (limited to 'doc/stdlib') diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 828caecabc..093c7a62b2 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,6 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} @@ -17,7 +16,6 @@ (deps ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) @@ -26,7 +24,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index dbc3a42ee9..60d6039b0f 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1,90 +1,90 @@ -plugins/btauto/Algebra.v -plugins/btauto/Btauto.v -plugins/btauto/Reflect.v -plugins/derive/Derive.v -plugins/extraction/ExtrHaskellBasic.v -plugins/extraction/ExtrHaskellNatInt.v -plugins/extraction/ExtrHaskellNatInteger.v -plugins/extraction/ExtrHaskellNatNum.v -plugins/extraction/ExtrHaskellString.v -plugins/extraction/ExtrHaskellZInt.v -plugins/extraction/ExtrHaskellZInteger.v -plugins/extraction/ExtrHaskellZNum.v -plugins/extraction/ExtrOcamlBasic.v -plugins/extraction/ExtrOcamlBigIntConv.v -plugins/extraction/ExtrOcamlChar.v -plugins/extraction/ExtrOCamlInt63.v -plugins/extraction/ExtrOCamlFloats.v -plugins/extraction/ExtrOcamlIntConv.v -plugins/extraction/ExtrOcamlNatBigInt.v -plugins/extraction/ExtrOcamlNatInt.v -plugins/extraction/ExtrOcamlString.v -plugins/extraction/ExtrOcamlNativeString.v -plugins/extraction/ExtrOcamlZBigInt.v -plugins/extraction/ExtrOcamlZInt.v -plugins/extraction/Extraction.v -plugins/funind/FunInd.v -plugins/funind/Recdef.v -plugins/ltac/Ltac.v -plugins/micromega/Ztac.v -plugins/micromega/DeclConstant.v -plugins/micromega/Env.v -plugins/micromega/EnvRing.v -plugins/micromega/Fourier.v -plugins/micromega/Fourier_util.v -plugins/micromega/Lia.v -plugins/micromega/Lqa.v -plugins/micromega/Lra.v -plugins/micromega/MExtraction.v -plugins/micromega/OrderedRing.v -plugins/micromega/Psatz.v -plugins/micromega/QMicromega.v -plugins/micromega/RMicromega.v -plugins/micromega/Refl.v -plugins/micromega/RingMicromega.v -plugins/micromega/Tauto.v -plugins/micromega/VarMap.v -plugins/micromega/ZCoeff.v -plugins/micromega/ZMicromega.v -plugins/micromega/ZifyInst.v -plugins/micromega/ZifyBool.v -plugins/micromega/ZifyComparison.v -plugins/micromega/ZifyClasses.v -plugins/micromega/Zify.v -plugins/nsatz/Nsatz.v -plugins/omega/Omega.v -plugins/omega/OmegaLemmas.v -plugins/omega/OmegaPlugin.v -plugins/omega/OmegaTactic.v -plugins/omega/PreOmega.v -plugins/quote/Quote.v -plugins/romega/ROmega.v -plugins/romega/ReflOmegaCore.v -plugins/rtauto/Bintree.v -plugins/rtauto/Rtauto.v -plugins/setoid_ring/Algebra_syntax.v -plugins/setoid_ring/ArithRing.v -plugins/setoid_ring/BinList.v -plugins/setoid_ring/Cring.v -plugins/setoid_ring/Field.v -plugins/setoid_ring/Field_tac.v -plugins/setoid_ring/Field_theory.v -plugins/setoid_ring/InitialRing.v -plugins/setoid_ring/Integral_domain.v -plugins/setoid_ring/NArithRing.v -plugins/setoid_ring/Ncring.v -plugins/setoid_ring/Ncring_initial.v -plugins/setoid_ring/Ncring_polynom.v -plugins/setoid_ring/Ncring_tac.v -plugins/setoid_ring/RealField.v -plugins/setoid_ring/Ring.v -plugins/setoid_ring/Ring_base.v -plugins/setoid_ring/Ring_polynom.v -plugins/setoid_ring/Ring_tac.v -plugins/setoid_ring/Ring_theory.v -plugins/setoid_ring/Rings_Q.v -plugins/setoid_ring/Rings_R.v -plugins/setoid_ring/Rings_Z.v -plugins/setoid_ring/ZArithRing.v -plugins/ssr/ssrunder.v -plugins/ssr/ssrsetoid.v +theories/btauto/Algebra.v +theories/btauto/Btauto.v +theories/btauto/Reflect.v +theories/derive/Derive.v +theories/extraction/ExtrHaskellBasic.v +theories/extraction/ExtrHaskellNatInt.v +theories/extraction/ExtrHaskellNatInteger.v +theories/extraction/ExtrHaskellNatNum.v +theories/extraction/ExtrHaskellString.v +theories/extraction/ExtrHaskellZInt.v +theories/extraction/ExtrHaskellZInteger.v +theories/extraction/ExtrHaskellZNum.v +theories/extraction/ExtrOcamlBasic.v +theories/extraction/ExtrOcamlBigIntConv.v +theories/extraction/ExtrOcamlChar.v +theories/extraction/ExtrOCamlInt63.v +theories/extraction/ExtrOCamlFloats.v +theories/extraction/ExtrOcamlIntConv.v +theories/extraction/ExtrOcamlNatBigInt.v +theories/extraction/ExtrOcamlNatInt.v +theories/extraction/ExtrOcamlString.v +theories/extraction/ExtrOcamlNativeString.v +theories/extraction/ExtrOcamlZBigInt.v +theories/extraction/ExtrOcamlZInt.v +theories/extraction/Extraction.v +theories/funind/FunInd.v +theories/funind/Recdef.v +theories/ltac/Ltac.v +theories/micromega/Ztac.v +theories/micromega/DeclConstant.v +theories/micromega/Env.v +theories/micromega/EnvRing.v +theories/micromega/Fourier.v +theories/micromega/Fourier_util.v +theories/micromega/Lia.v +theories/micromega/Lqa.v +theories/micromega/Lra.v +theories/micromega/MExtraction.v +theories/micromega/OrderedRing.v +theories/micromega/Psatz.v +theories/micromega/QMicromega.v +theories/micromega/RMicromega.v +theories/micromega/Refl.v +theories/micromega/RingMicromega.v +theories/micromega/Tauto.v +theories/micromega/VarMap.v +theories/micromega/ZCoeff.v +theories/micromega/ZMicromega.v +theories/micromega/ZifyInst.v +theories/micromega/ZifyBool.v +theories/micromega/ZifyComparison.v +theories/micromega/ZifyClasses.v +theories/micromega/Zify.v +theories/nsatz/Nsatz.v +theories/omega/Omega.v +theories/omega/OmegaLemmas.v +theories/omega/OmegaPlugin.v +theories/omega/OmegaTactic.v +theories/omega/PreOmega.v +theories/quote/Quote.v +theories/romega/ROmega.v +theories/romega/ReflOmegaCore.v +theories/rtauto/Bintree.v +theories/rtauto/Rtauto.v +theories/setoid_ring/Algebra_syntax.v +theories/setoid_ring/ArithRing.v +theories/setoid_ring/BinList.v +theories/setoid_ring/Cring.v +theories/setoid_ring/Field.v +theories/setoid_ring/Field_tac.v +theories/setoid_ring/Field_theory.v +theories/setoid_ring/InitialRing.v +theories/setoid_ring/Integral_domain.v +theories/setoid_ring/NArithRing.v +theories/setoid_ring/Ncring.v +theories/setoid_ring/Ncring_initial.v +theories/setoid_ring/Ncring_polynom.v +theories/setoid_ring/Ncring_tac.v +theories/setoid_ring/RealField.v +theories/setoid_ring/Ring.v +theories/setoid_ring/Ring_base.v +theories/setoid_ring/Ring_polynom.v +theories/setoid_ring/Ring_tac.v +theories/setoid_ring/Ring_theory.v +theories/setoid_ring/Rings_Q.v +theories/setoid_ring/Rings_R.v +theories/setoid_ring/Rings_Z.v +theories/setoid_ring/ZArithRing.v +theories/ssr/ssrunder.v +theories/ssr/ssrsetoid.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index b2ddf36b65..51688e2d9e 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -619,11 +619,11 @@ through the Require Import command.

small scale reflection formalization technique
- plugins/ssrmatching/ssrmatching.v - plugins/ssr/ssrclasses.v - plugins/ssr/ssreflect.v - plugins/ssr/ssrbool.v - plugins/ssr/ssrfun.v + theories/ssrmatching/ssrmatching.v + theories/ssr/ssrclasses.v + theories/ssr/ssreflect.v + theories/ssr/ssrbool.v + theories/ssr/ssrfun.v
Ltac2: diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 732f15b78a..a51308f153 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -8,7 +8,7 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native` +LIBDIRS=`find theories/* user-contrib/* -type d ! -name .coq-native` for k in $LIBDIRS; do if [[ $k =~ "user-contrib" ]]; then -- cgit v1.2.3