Skip to content

Commit c2dee97

Browse files
proux01proux01
authored
Merge pull request #2 from coq/clarify-structure
Clarify structure
2 parents ce2550e + 620b432 commit c2dee97

File tree

785 files changed

+3539
-2103
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

785 files changed

+3539
-2103
lines changed

‎.github/workflows/basic-checks.yml

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
name: Basic checks
2+
on:
3+
pull_request:
4+
push:
5+
branches:
6+
- master
7+
jobs:
8+
basic-checks:
9+
runs-on: ubuntu-latest
10+
steps:
11+
- name: Checkout
12+
uses: actions/checkout@v4
13+
- name: Check for duplicate files
14+
run: dev/tools/check-duplicate-files.sh

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

+58
Original file line numberDiff line numberDiff line change
@@ -7190,6 +7190,64 @@ jobs:
71907190
name: Building/fetching current CI target
71917191
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
71927192
--argstr job "stdlib-refman-html"
7193+
stdlib-subcomponents:
7194+
needs:
7195+
- coq
7196+
runs-on: ubuntu-latest
7197+
steps:
7198+
- name: Determine which commit to initially checkout
7199+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
7200+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
7201+
}}\" >> $GITHUB_ENV\nfi\n"
7202+
- name: Git checkout
7203+
uses: actions/checkout@v4
7204+
with:
7205+
fetch-depth: 0
7206+
ref: ${{ env.target_commit }}
7207+
- name: Determine which commit to test
7208+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
7209+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
7210+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
7211+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
7212+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
7213+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
7214+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
7215+
\ fi\nfi\n"
7216+
- name: Git checkout
7217+
uses: actions/checkout@v4
7218+
with:
7219+
fetch-depth: 0
7220+
ref: ${{ env.tested_commit }}
7221+
- name: Cachix install
7222+
uses: cachix/install-nix-action@v30
7223+
with:
7224+
nix_path: nixpkgs=channel:nixpkgs-unstable
7225+
- name: Cachix setup coq
7226+
uses: cachix/cachix-action@v15
7227+
with:
7228+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
7229+
extraPullNames: coq-community, math-comp
7230+
name: coq
7231+
- id: stepGetDerivation
7232+
name: Getting derivation for current job (stdlib-subcomponents)
7233+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
7234+
\"rocq-9.0\" --argstr job \"stdlib-subcomponents\" \\\n --dry-run 2> err
7235+
> out || (touch fail; true)\n"
7236+
- name: Error reporting
7237+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
7238+
- name: Failure check
7239+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
7240+
- id: stepCheck
7241+
name: Checking presence of CI target for current job
7242+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
7243+
- if: steps.stepCheck.outputs.status == 'built'
7244+
name: 'Building/fetching previous CI target: coq'
7245+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
7246+
--argstr job "coq"
7247+
- if: steps.stepCheck.outputs.status == 'built'
7248+
name: Building/fetching current CI target
7249+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
7250+
--argstr job "stdlib-subcomponents"
71937251
stdlib-test:
71947252
needs:
71957253
- coq

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

+58
Original file line numberDiff line numberDiff line change
@@ -7316,6 +7316,64 @@ jobs:
73167316
name: Building/fetching current CI target
73177317
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
73187318
--argstr job "stdlib-refman-html"
7319+
stdlib-subcomponents:
7320+
needs:
7321+
- coq
7322+
runs-on: ubuntu-latest
7323+
steps:
7324+
- name: Determine which commit to initially checkout
7325+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
7326+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
7327+
}}\" >> $GITHUB_ENV\nfi\n"
7328+
- name: Git checkout
7329+
uses: actions/checkout@v4
7330+
with:
7331+
fetch-depth: 0
7332+
ref: ${{ env.target_commit }}
7333+
- name: Determine which commit to test
7334+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
7335+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
7336+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
7337+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
7338+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
7339+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
7340+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
7341+
\ fi\nfi\n"
7342+
- name: Git checkout
7343+
uses: actions/checkout@v4
7344+
with:
7345+
fetch-depth: 0
7346+
ref: ${{ env.tested_commit }}
7347+
- name: Cachix install
7348+
uses: cachix/install-nix-action@v30
7349+
with:
7350+
nix_path: nixpkgs=channel:nixpkgs-unstable
7351+
- name: Cachix setup coq
7352+
uses: cachix/cachix-action@v15
7353+
with:
7354+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
7355+
extraPullNames: coq-community, math-comp
7356+
name: coq
7357+
- id: stepGetDerivation
7358+
name: Getting derivation for current job (stdlib-subcomponents)
7359+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
7360+
\"rocq-master\" --argstr job \"stdlib-subcomponents\" \\\n --dry-run 2>
7361+
err > out || (touch fail; true)\n"
7362+
- name: Error reporting
7363+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
7364+
- name: Failure check
7365+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
7366+
- id: stepCheck
7367+
name: Checking presence of CI target for current job
7368+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
7369+
- if: steps.stepCheck.outputs.status == 'built'
7370+
name: 'Building/fetching previous CI target: coq'
7371+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
7372+
--argstr job "coq"
7373+
- if: steps.stepCheck.outputs.status == 'built'
7374+
name: Building/fetching current CI target
7375+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
7376+
--argstr job "stdlib-subcomponents"
73197377
stdlib-test:
73207378
needs:
73217379
- coq

‎.nix/config.nix

+1
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,7 @@ with builtins; with (import <nixpkgs> {}).lib;
202202
stdlib-html.job = true;
203203
stdlib-refman-html.job = true;
204204
stdlib-test.job = true;
205+
stdlib-subcomponents.job = true;
205206
};
206207
in {
207208
"rocq-master".coqPackages = common-bundles // {

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

+3
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,9 @@ coqPackages.lib.overrideCoqDerivation {
88
buildPhase = ''
99
patchShebangs doc/stdlib/make-library-index
1010
dev/with-rocq-wrap.sh dune build @stdlib-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
11+
# check that the make-depend script still runs
12+
patchShebangs dev/tools/make-depends.sh
13+
dev/tools/make-depends.sh
1114
'';
1215

1316
installPhase = ''

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

+76
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
# CI job to test that we don't break the subcomponent structure of the stdlib,
2+
# as described in the graph doc/stdlib/depends
3+
4+
{ coq, stdlib, coqPackages }:
5+
6+
let
7+
# stdlib subcomponents with their dependencies
8+
# when editing this, ensure to keep doc/stdlib/depends in sync
9+
components = {
10+
"corelib-wrapper" = [ ];
11+
"logic" = [ ];
12+
"relations" = [ "corelib-wrapper" ];
13+
"program" = [ "corelib-wrapper" "logic" ];
14+
"classes" = [ "program" "relations" ];
15+
"bool" = [ "classes" ];
16+
"structures" = [ "bool" ];
17+
"arith-base" = [ "structures" ];
18+
"positive" = [ "arith-base" ];
19+
"narith" = [ "positive" ];
20+
"zarith-base" = [ "narith" ];
21+
"lists" = [ "arith-base" ];
22+
"ring" = [ "zarith-base" "lists" ];
23+
"arith" = [ "ring" ];
24+
"strings" = [ "arith" ];
25+
"lia" = [ "arith" ];
26+
"zarith" = [ "lia" ];
27+
"qarith-base" = [ "ring" ];
28+
"field" = [ "qarith-base" "zarith" ];
29+
"lqa" = [ "field" ];
30+
"qarith" = [ "field" ];
31+
"nsatz" = [ "zarith" "qarith-base" ];
32+
"classical-logic" = [ "arith" ];
33+
"sets" = [ "classical-logic" ];
34+
"vectors" = [ "lists" ];
35+
"sorting" = [ "lia" "sets" "vectors" ];
36+
"orders-ex" = [ "strings" "sorting" ];
37+
"unicode" = [ ];
38+
"primitive-int" = [ "unicode" "zarith" ];
39+
"primitive-floats" = [ "primitive-int" ];
40+
"primitive-array" = [ "primitive-int" ];
41+
"primitive-string" = [ "primitive-int" "orders-ex" ];
42+
"reals" = [ "nsatz" "lqa" "qarith" "classical-logic" "vectors" ];
43+
"fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
44+
"extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
45+
"funind" = [ "arith-base" ];
46+
"wellfounded" = [ "lists" ];
47+
"streams" = [ "logic" ];
48+
"rtauto" = [ "positive" "lists" ];
49+
"compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "wellfounded" "streams" ];
50+
"all" = [ "compat" ];
51+
};
52+
53+
stdlib_ = component: let
54+
pname = "stdlib-${component}";
55+
stdlib-deps = map stdlib_ components.${component};
56+
in coqPackages.lib.overrideCoqDerivation ({
57+
inherit pname;
58+
propagatedBuildInputs = stdlib-deps;
59+
useDune = false;
60+
mlPlugin = true;
61+
} // (if component != "all" then {
62+
buildPhase = ''
63+
make ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} build-${component}
64+
'';
65+
installPhase = ''
66+
make COQLIBINSTALL=$out/lib/coq/${coq.coq-version}/user-contrib install-${component}
67+
'';
68+
} else {
69+
buildPhase = ''
70+
echo "nothing left to build"
71+
'';
72+
installPhase = ''
73+
echo "nothing left to install"
74+
'';
75+
})) stdlib;
76+
in stdlib_ "all"

‎Makefile

+3
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@ all:
66
install:
77
$(DUNE) install --root . rocq-stdlib
88

9+
build-% install-%:
10+
+$(MAKE) -C theories $@
11+
912
# Make of individual .vo
1013
theories/%.vo:
1114
$(DUNE) build $@

‎dev/doc/structure.md

+49
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
Internal Structure of Stdlib
2+
============================
3+
4+
For historical reasons, the internal dependency structure of the
5+
Stdlib library does not match its directory structure. That is, one
6+
can find many exmaples of files in some directory `A` that depends
7+
from files in another directory `B`, whereas other files in `B`
8+
depends from files in `A`. This makes it difficult to understand what
9+
are the acceptable dependencies in a given file, with developers left
10+
trying adding dependencies until a circular dependency appears,
11+
further worsening the current mess.
12+
13+
For backward compatibility reasons, that unfortunate state of affairs
14+
cannot be easily fixed. However, to better understand the current
15+
dependencies and mitigate the issue, we document here current tools to
16+
help somewhat master that situation.
17+
18+
Documentation
19+
-------------
20+
21+
One can find a graph of dependencies in file
22+
`doc/stdlib/depends`. This graph is included in the documentation
23+
built by `make stdlib-html` in directory
24+
`_build/default/doc/stdlib/html/`. To find the exact files contained
25+
in each node `<n>` of this graph, one can look at the corresponding
26+
`theories/Make.<n>` file.
27+
28+
CI testing
29+
----------
30+
31+
A CI job `stdlib-subcomponents` checks that the above documented
32+
structure remains valid.
33+
34+
How to Modify the Structure
35+
---------------------------
36+
37+
When adding a file, it is enough to list it in the appropriate
38+
`theories/Make.*` file. Note that, for historical reasons, some
39+
directories are split between different subcomponents. In this case, a
40+
symlink must be added in the appropriate `_SubComponent` subdirectory
41+
and only the symlink must be listed in `theories/Make.*`. Look at
42+
`theories/Make.lists` for an example.
43+
44+
To add or remove a subcomponent, just add or remove the corresponding
45+
`theories/Make.*` file and adapt `doc/stdlib/depends` and
46+
`.nix/coq-overlays/stdlib-subcomponents/default.nix`. One can use the
47+
`dev/tools/make-depends.sh` script to help update the graph (the line
48+
below `File dependencies` can be uncommented to better understand
49+
which files are responsible for some subcomponent dependency).

‎dev/tools/check-duplicate-files.sh

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#!/bin/sh
2+
3+
# Check for duplicate files
4+
# Those would yield ambiguity when doing "From Stdlib Require File.".
5+
# There are already a few in the prelude, let's not add more.
6+
7+
# Files that are already duplicate
8+
DUPLICATE_FILES=" \
9+
Byte.v \
10+
Tactics.v \
11+
Tauto.v \
12+
Wf.v \
13+
"
14+
15+
ALL_FILES=all_files__
16+
ALL_FILES_UNIQ=all_files_uniq__
17+
18+
rm -f ${ALL_FILES} ${ALL_FILES_UNIQ}
19+
(for f in $(find theories -name "*.v" -type f) ; do basename $f ; done) | sort > ${ALL_FILES}
20+
(uniq ${ALL_FILES} ; for f in ${DUPLICATE_FILES} ; do echo $f ; done) | sort > ${ALL_FILES_UNIQ}
21+
22+
if $(diff -q ${ALL_FILES_UNIQ} ${ALL_FILES} > /dev/null) ; then
23+
echo "No files with duplicate name."
24+
else
25+
echo "Error: Some files bear the same name:"
26+
diff ${ALL_FILES_UNIQ} ${ALL_FILES}
27+
exit 1
28+
fi
29+
30+
rm -f ${ALL_FILES} ${ALL_FILES_UNIQ}

‎dev/tools/make-depends.sh

+57
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
#!/bin/bash
2+
3+
# this should be called from root as
4+
# % dune build -p rocq-stdlib
5+
# % dev/tools/make-depends.sh
6+
7+
THEORIES="_build/default/theories"
8+
if [ ! -d ${THEORIES} ] ; then
9+
echo "Error: ${THEORIES} doesn't exist, run first"
10+
echo "% dune build -p rocq-stdlib"
11+
exit 1
12+
fi
13+
14+
declare -A FILE_PKG
15+
16+
# Associate each *.v source file to its corresponding <pkg>,
17+
# according to theories/Make.<pkg>
18+
FILE_PKG["All.v"]="all"
19+
for makefile in theories/Make.* ; do
20+
PKG=${makefile#theories/Make.}
21+
for f in $(cat ${makefile} | sed -e 's/#.*//;s/-.*//' | grep -v '^[ \t]*$') ; do
22+
f=$(echo ${f} | sed -e 's,/_[^/]*,,')
23+
if [ -n ${FILE_PKG[${f}]:-""} ] ; then
24+
echo "Error: File ${f} appears in both theories/Make.${FILE_PKG[${f}]} and theories/Make.${PKG}."
25+
exit 1
26+
fi
27+
FILE_PKG[${f}]=${PKG}
28+
done
29+
done
30+
31+
# Check that each *.v file in theories appears in some <pkg>
32+
for f in $(find ${THEORIES} -name "*.v") ; do
33+
f=$(echo ${f} | sed -e "s,${THEORIES}/,,")
34+
if [ -z ${FILE_PKG[${f}]} ] ; then
35+
echo "Error: File ${f} is not listed in any theories/Make.* file."
36+
exit 1
37+
fi
38+
done
39+
40+
# Retrieve dependencies and build graph
41+
(echo "digraph stdlib_deps {";
42+
echo "node [shape=rectangle, style=filled, color=\"#ff540a\", URL=\"#\\N\"];";
43+
rocq dep -Q ${THEORIES} Stdlib ${THEORIES} | sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*v//p' | \
44+
while read src dst; do
45+
src=${src#_build.default.theories.}
46+
srcf="$(echo ${src%.vo} | tr '.' '/').v"
47+
for d in $dst; do
48+
d=${d#_build.default.theories.}
49+
df="$(echo ${d%.vo} | tr '.' '/').v"
50+
if [ -z ${FILE_PKG[${df}]:-""} ] ; then continue ; fi
51+
# File dependencies
52+
# echo "\"(${src}) ${FILE_PKG[${srcf}]}\" -> \"${FILE_PKG[${df}]} (${d%.vo})\" ;"
53+
# Subcomponent dependencies
54+
echo "\"${FILE_PKG[${srcf}]}\" -> \"${FILE_PKG[${df}]}\" ;"
55+
done
56+
done
57+
echo "}") | tred

0 commit comments

Comments
 (0)