Clarify structure

.github/workflows/basic-checks.yml

@@ -0,0 +1,14 @@
+name: Basic checks
+on:
+  pull_request:
+  push:
+    branches:
+    - master
+jobs:
+  basic-checks:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+    - name: Check for duplicate files
+      run: dev/tools/check-duplicate-files.sh

.github/workflows/nix-action-rocq-9.0.yml

@@ -7190,6 +7190,64 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
         --argstr job "stdlib-refman-html"
+  stdlib-subcomponents:
+    needs:
+    - coq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{
+        github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha
+        }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{
+        github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{ github.event.repository.html_url
+        }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n  mergeable=$(git
+        merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
+        2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n  if [ -z \"$merge_commit\"\
+        \ -o \"x$mergeable\" != \"x0\" ]; then\n    echo \"tested_commit=${{ github.event.pull_request.head.sha
+        }}\" >> $GITHUB_ENV\n  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
+        \  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v30
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v15
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - id: stepGetDerivation
+      name: Getting derivation for current job (stdlib-subcomponents)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"rocq-9.0\" --argstr job \"stdlib-subcomponents\" \\\n   --dry-run 2> err
+        > out || (touch fail; true)\n"
+    - name: Error reporting
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
+    - name: Failure check
+      run: if [ -e fail ]; then exit 1; else exit 0; fi;
+    - id: stepCheck
+      name: Checking presence of CI target for current job
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
+        --argstr job "stdlib-subcomponents"
   stdlib-test:
     needs:
     - coq

.github/workflows/nix-action-rocq-master.yml

@@ -7316,6 +7316,64 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
         --argstr job "stdlib-refman-html"
+  stdlib-subcomponents:
+    needs:
+    - coq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{
+        github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha
+        }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{
+        github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{ github.event.repository.html_url
+        }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n  mergeable=$(git
+        merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
+        2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n  if [ -z \"$merge_commit\"\
+        \ -o \"x$mergeable\" != \"x0\" ]; then\n    echo \"tested_commit=${{ github.event.pull_request.head.sha
+        }}\" >> $GITHUB_ENV\n  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
+        \  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v30
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v15
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - id: stepGetDerivation
+      name: Getting derivation for current job (stdlib-subcomponents)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"rocq-master\" --argstr job \"stdlib-subcomponents\" \\\n   --dry-run 2>
+        err > out || (touch fail; true)\n"
+    - name: Error reporting
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
+    - name: Failure check
+      run: if [ -e fail ]; then exit 1; else exit 0; fi;
+    - id: stepCheck
+      name: Checking presence of CI target for current job
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
+        --argstr job "stdlib-subcomponents"
   stdlib-test:
     needs:
     - coq

.nix/config.nix

@@ -202,6 +202,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       stdlib-html.job = true;
       stdlib-refman-html.job = true;
       stdlib-test.job = true;
+      stdlib-subcomponents.job = true;
     };
   in {
     "rocq-master".coqPackages = common-bundles // {

.nix/coq-overlays/stdlib-html/default.nix

@@ -8,6 +8,9 @@ coqPackages.lib.overrideCoqDerivation {
   buildPhase = ''
     patchShebangs doc/stdlib/make-library-index
     dev/with-rocq-wrap.sh dune build @stdlib-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
+    # check that the make-depend script still runs
+    patchShebangs dev/tools/make-depends.sh
+    dev/tools/make-depends.sh
   '';
 
   installPhase = ''

.nix/coq-overlays/stdlib-subcomponents/default.nix

@@ -0,0 +1,76 @@
+# CI job to test that we don't break the subcomponent structure of the stdlib,
+# as described in the graph doc/stdlib/depends
+
+{ coq, stdlib, coqPackages }:
+
+let
+  # stdlib subcomponents with their dependencies
+  # when editing this, ensure to keep doc/stdlib/depends in sync
+  components = {
+    "corelib-wrapper" = [ ];
+    "logic" = [ ];
+    "relations" = [ "corelib-wrapper" ];
+    "program" = [ "corelib-wrapper" "logic" ];
+    "classes" = [ "program" "relations" ];
+    "bool" = [ "classes" ];
+    "structures" = [ "bool" ];
+    "arith-base" = [ "structures" ];
+    "positive" = [ "arith-base" ];
+    "narith" = [ "positive" ];
+    "zarith-base" = [ "narith" ];
+    "lists" = [ "arith-base" ];
+    "ring" = [ "zarith-base" "lists" ];
+    "arith" = [ "ring" ];
+    "strings" = [ "arith" ];
+    "lia" = [ "arith" ];
+    "zarith" = [ "lia" ];
+    "qarith-base" = [ "ring" ];
+    "field" = [ "qarith-base" "zarith" ];
+    "lqa" = [ "field" ];
+    "qarith" = [ "field" ];
+    "nsatz" = [ "zarith" "qarith-base" ];
+    "classical-logic" = [ "arith" ];
+    "sets" = [ "classical-logic" ];
+    "vectors" = [ "lists" ];
+    "sorting" = [ "lia" "sets" "vectors" ];
+    "orders-ex" = [ "strings" "sorting" ];
+    "unicode" = [ ];
+    "primitive-int" = [ "unicode" "zarith" ];
+    "primitive-floats" = [ "primitive-int" ];
+    "primitive-array" = [ "primitive-int" ];
+    "primitive-string" = [ "primitive-int" "orders-ex" ];
+    "reals" = [ "nsatz" "lqa" "qarith" "classical-logic" "vectors" ];
+    "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
+    "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
+    "funind" = [ "arith-base" ];
+    "wellfounded" = [ "lists" ];
+    "streams" = [ "logic" ];
+    "rtauto" = [ "positive" "lists" ];
+    "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "wellfounded" "streams" ];
+    "all" = [ "compat" ];
+  };
+
+  stdlib_ = component: let
+    pname = "stdlib-${component}";
+    stdlib-deps = map stdlib_ components.${component};
+    in coqPackages.lib.overrideCoqDerivation ({
+      inherit pname;
+      propagatedBuildInputs = stdlib-deps;
+      useDune = false;
+      mlPlugin = true;
+    } // (if component != "all" then {
+      buildPhase = ''
+        make ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} build-${component}
+      '';
+      installPhase = ''
+        make COQLIBINSTALL=$out/lib/coq/${coq.coq-version}/user-contrib install-${component}
+      '';
+    } else {
+      buildPhase = ''
+        echo "nothing left to build"
+      '';
+      installPhase = ''
+        echo "nothing left to install"
+      '';
+    })) stdlib;
+in stdlib_ "all"

Makefile

@@ -6,6 +6,9 @@ all:
 install:
 	$(DUNE) install --root . rocq-stdlib
 
+build-% install-%:
+	+$(MAKE) -C theories $@
+
 # Make of individual .vo
 theories/%.vo:
 	$(DUNE) build $@

dev/doc/structure.md

@@ -0,0 +1,47 @@
+Internal Structure of Stdlib
+============================
+
+For historical reasons, the internal dependency structure of the
+Stdlib library does not match its directory structure. That is, one
+can find many exmaples of files in some directory `A` that depends
+from files in another directory `B`, whereas other files in `B`
+depends from files in `A`. This makes it difficult to understand what
+are the acceptable dependencies in a given file, with developers left
+trying adding dependencies until a circular dependency appears,
+further worsening the current mess.
+
+For backward compatibility reasons, that unfortunate state of affairs
+cannot be easily fixed. However, to better understand the current
+dependencies and mitigate the issue, we document here current tools to
+help somewhat master that situation.
+
+Documentation
+-------------
+
+One can find a graph of dependencies in file
+`doc/stdlib/depends`. This graph is included in the documentation
+built by `make stdlib-html` in directory
+`_build/default/doc/stdlib/html/`. To find the exact files contained
+in each node `<n>` of this graph, one can look at the corresponding
+`theories/Make.<n>` file.
+
+CI testing
+----------
+
+A CI job `stdlib-subcomponents` checks that the above documented
+structure remains valid.
+
+How to Modify the Structure
+---------------------------
+
+When adding a file, it is enough to list it in the appropriate
+`theories/Make.*` file. Note that, for historical reasons, some
+directories are split between different subcomponents. In this case, a
+symlink must be added in the appropriate `_SubComponent` subdirectory
+and only the symlink must be listed in `theories/Make.*`. Look at
+`theories/Make.lists` for an example.
+
+To add or remove a subcomponent, just add or remove the corresponding
+`theories/Make.*` file and adapt `doc/stdlib/depends` and
+`.nix/coq-overlays/stdlib-subcomponents/default.nix`. One can use the
+`dev/tools/make-depends.sh` script to help update the graph.

dev/tools/check-duplicate-files.sh

@@ -0,0 +1,30 @@
+#!/bin/sh
+
+# Check for duplicate files
+# Those would yield ambiguity when doing "From Stdlib Require File.".
+# There are already a few in the prelude, let's not add more.
+
+# Files that are already duplicate
+DUPLICATE_FILES=" \
+  Byte.v \
+  Tactics.v \
+  Tauto.v \
+  Wf.v \
+"
+
+ALL_FILES=all_files__
+ALL_FILES_UNIQ=all_files_uniq__
+
+rm -f ${ALL_FILES} ${ALL_FILES_UNIQ}
+(for f in $(find theories -name "*.v" -type f) ; do basename $f ; done) | sort > ${ALL_FILES}
+(uniq ${ALL_FILES} ; for f in ${DUPLICATE_FILES} ; do echo $f ; done) | sort > ${ALL_FILES_UNIQ}
+
+if $(diff -q ${ALL_FILES_UNIQ} ${ALL_FILES} > /dev/null) ; then
+  echo "No files with duplicate name."
+else
+  echo "Error: Some files bear the same name:"
+  diff ${ALL_FILES_UNIQ} ${ALL_FILES}
+  exit 1
+fi
+
+rm -f ${ALL_FILES} ${ALL_FILES_UNIQ}

dev/tools/make-depends.sh

@@ -0,0 +1,56 @@
+#!/bin/bash
+
+# this should be called from root as
+# % dune build -p rocq-stdlib
+# % dev/tools/make-depends.sh
+
+THEORIES="_build/default/theories"
+if [ ! -d ${THEORIES} ] ; then
+    echo "Error: ${THEORIES} doesn't exist, run first"
+    echo "% dune build -p rocq-stdlib"
+    exit 1
+fi
+
+declare -A FILE_PKG
+
+# Associate each *.v source file to its corresponding <pkg>,
+# according to theories/Make.<pkg>
+FILE_PKG["All.v"]="all"
+for makefile in theories/Make.* ; do
+    PKG=${makefile#theories/Make.}
+    for f in $(cat ${makefile} | sed -e 's/#.*//;s/-.*//' | grep -v '^[ \t]*$') ; do
+        f=$(echo ${f} | sed -e 's,/_[^/]*,,')
+        if [ -n ${FILE_PKG[${f}]:-""} ] ; then
+            echo "Error: File ${f} appears in both theories/Make.${FILE_PKG[${f}]} and theories/Make.${PKG}."
+            exit 1
+        fi
+        FILE_PKG[${f}]=${PKG}
+    done
+done
+
+# Check that each *.v file in theories appears in some <pkg>
+for f in $(find ${THEORIES} -name "*.v") ; do
+    f=$(echo ${f} | sed -e "s,${THEORIES}/,,")
+    if [ -z ${FILE_PKG[${f}]} ] ; then
+        echo "Error: File ${f} is not listed in any theories/Make.* file."
+        exit 1
+    fi
+done
+
+# Retrieve dependencies and build graph
+(echo "digraph stdlib_deps {";
+echo "node [shape=ellipse, style=filled, color=lightblue];";
+rocq dep -Q ${THEORIES} Stdlib ${THEORIES} | sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*v//p' | \
+    while read src dst; do
+        src=${src#_build.default.theories.}
+        srcf="$(echo ${src%.vo} | tr '.' '/').v"
+        for d in $dst; do
+            d=${d#_build.default.theories.}
+            df="$(echo ${d%.vo} | tr '.' '/').v"
+            if [ -z ${FILE_PKG[${df}]:-""} ] ; then continue ; fi
+            # File dependencies
+            # echo "\"${src}\" -> \"${d%.vo}\" ;"
+            echo "\"${FILE_PKG[${srcf}]}\" -> \"${FILE_PKG[${df}]}\" ;"
+        done
+    done
+echo "}") | tred