Merge pull request #105 from proux01/compile-make

Enable compilation with rocq makefile

.github/workflows/basic-checks.yml

@@ -12,3 +12,5 @@ jobs:
       uses: actions/checkout@v4
     - name: Check for duplicate files
       run: dev/tools/check-duplicate-files.sh
+    - name: Check that All.v is up to date
+      run: dev/tools/check-all.sh

.gitignore

@@ -134,6 +134,8 @@ ide/coqide/index_urls.txt
 .lia.cache
 .nia.cache
 .nra.cache
+theories/Makefile.coq
+theories/Makefile.coq.conf
 
 # emacs save files
 *~

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

@@ -59,19 +59,12 @@ let
       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;
+    }) stdlib;
 in stdlib_ "all"

Makefile

@@ -1,17 +1,20 @@
 DUNE=dev/with-rocq-wrap.sh dune
 
-all:
+all install:
+	+$(MAKE) -C theories $@
+
+dune:
 	$(DUNE) build -p rocq-stdlib @install
 
-install:
+dune-install:
 	$(DUNE) install --root . rocq-stdlib
 
 build-% install-%:
 	+$(MAKE) -C theories $@
 
 # Make of individual .vo
 theories/%.vo:
-	$(DUNE) build $@
+	+$(MAKE) -C theories $*.vo
 
 refman-html:
 	$(DUNE) build --root . --no-buffer @refman-html

coq-stdlib.opam

@@ -9,25 +9,10 @@ license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/stdlib/issues"
+dev-repo: "git+https://github.com/coq/stdlib.git"
 depends: [
-  "dune" {>= "3.8"}
   "coq-core"
   "rocq-stdlib" {= version}
-  "odoc" {with-doc}
 ]
-dev-repo: "git+https://github.com/coq/stdlib.git"
 build: [
-  ["dune" "subst"] {dev}
-  [
-    "dev/with-rocq-wrap.sh"
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
 ]

coq-stdlib.opam.template

@@ -1,15 +1,6 @@
+depends: [
+  "coq-core"
+  "rocq-stdlib" {= version}
+]
 build: [
-  ["dune" "subst"] {dev}
-  [
-    "dev/with-rocq-wrap.sh"
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
 ]

dev/doc/structure.md

@@ -36,9 +36,9 @@ 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
+directories are split between different subcomponents. In this case,
+the new line in the `theories/Make.*` file must contain the
+appropriate `_SubComponent` fake subdirectory. Look at
 `theories/Make.lists` for an example.
 
 To add or remove a subcomponent, just add or remove the corresponding

dev/tools/check-all.sh

@@ -0,0 +1,20 @@
+#!/bin/sh
+
+# Check that theories/All/All.v is up to date
+
+ALL_FILES=all_files__
+ACTUAL_FILES=actual_files__
+
+rm -f ${ALL_FILES} ${ACTUAL_FILES}
+grep "Require" theories/All/All.v | sed -e 's/From.*Require.*Export.*[.]\([a-zA-Z]\)/\1/' | sort > ${ALL_FILES}
+(for f in $(find theories -name "*.v" -type f) ; do basename ${f%v} ; done) | grep -v "^All[.]$" | sort > ${ACTUAL_FILES}
+
+if $(diff -q ${ALL_FILES} ${ACTUAL_FILES} > /dev/null) ; then
+  echo "theories/All/All.v is up to date."
+else
+  echo "Error: theories/All/All.v needs some update:"
+  diff -u ${ALL_FILES} ${ACTUAL_FILES}
+  exit 1
+fi
+
+rm -f ${ALL_FILES} ${ACTUAL_FILES}

dev/tools/make-depends.sh

@@ -1,15 +1,9 @@
 #!/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
+THEORIES="theories"
 
 declare -A FILE_PKG
 
@@ -42,10 +36,10 @@ done
 echo "node [shape=rectangle, style=filled, color=\"#ff540a\", URL=\"#\\N\"];";
 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.}
+        src=${src#theories.}
         srcf="$(echo ${src%.vo} | tr '.' '/').v"
         for d in $dst; do
-            d=${d#_build.default.theories.}
+            d=${d#theories.}
             df="$(echo ${d%.vo} | tr '.' '/').v"
             if [ -z ${FILE_PKG[${df}]:-""} ] ; then continue ; fi
             # File dependencies

doc/stdlib/index-list.html.template

@@ -694,4 +694,11 @@ through the <tt>From Stdlib Require Import</tt> command.</p>
     theories/Compat/AdmitAxiom.v
     theories/Compat/Stdlib818.v
   </dd>
+
+  <dt> <a name="all"></a><b>All</b>:
+    Require the whole Stdlib
+  </dt>
+  <dd>
+    (theories/All/All.v)
+  </dd>
 </dl>

rocq-stdlib.opam

@@ -22,25 +22,14 @@ license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/stdlib/issues"
+dev-repo: "git+https://github.com/coq/stdlib.git"
 depends: [
-  "dune" {>= "3.8"}
   "rocq-runtime"
-  "rocq-core" {= version}
-  "odoc" {with-doc}
+  "rocq-core" {>= "9.0"}
 ]
-dev-repo: "git+https://github.com/coq/stdlib.git"
 build: [
-  ["dune" "subst"] {dev}
-  [
-    "dev/with-rocq-wrap.sh"
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
+  [make "-j" jobs]
+]
+install: [
+  [make "install"]
 ]

rocq-stdlib.opam.template

@@ -1,15 +1,10 @@
+depends: [
+  "rocq-runtime"
+  "rocq-core" {>= "9.0"}
+]
 build: [
-  ["dune" "subst"] {dev}
-  [
-    "dev/with-rocq-wrap.sh"
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
+  [make "-j" jobs]
+]
+install: [
+  [make "install"]
 ]