Move stdlib

Author: proux01

.gitignore

@@ -161,3 +161,6 @@ bin
 theories/dune
 user-contrib/Ltac2/dune
 /test-suite/test_suite_config.inc
+
+.wrappers
+rocq-stdlib-doc.opam

stdlib/CONTRIBUTING.md CONTRIBUTING.md

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

stdlib/INSTALL.md INSTALL.md

@@ -8,16 +8,18 @@ authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
-bug-reports: "https://github.com/coq/coq/issues"
+bug-reports: "https://github.com/coq/stdlib/issues"
 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"
@@ -29,4 +31,3 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/coq/coq.git"

stdlib/LICENSE LICENSE

@@ -15,7 +15,7 @@
 (maintainers "The Rocq standard library development team")
 (authors "The Rocq development team, INRIA, CNRS, and contributors")
 ; This generates bug-reports and dev-repo
-(source (github coq/coq))
+(source (github coq/stdlib))
 (homepage https://coq.inria.fr/)
 (documentation "https://coq.github.io/doc/")
 (version dev)

Makefile

@@ -21,14 +21,14 @@ authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
-bug-reports: "https://github.com/coq/coq/issues"
+bug-reports: "https://github.com/coq/stdlib/issues"
 depends: [
   "dune" {>= "3.8"}
   "rocq-runtime"
   "rocq-core" {= version}
   "odoc" {with-doc}
 ]
-dev-repo: "git+https://github.com/coq/coq.git"
+dev-repo: "git+https://github.com/coq/stdlib.git"
 build: [
   ["dune" "subst"] {dev}
   [

stdlib/Makefile.ci Makefile.ci

@@ -0,0 +1,15 @@
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dev/with-rocq-wrap.sh"
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]

stdlib/README.md README.md

@@ -145,7 +145,7 @@ all: run
 else
 all:
 	$(MAKE) run | tee time-of-build.log
-	python ../../tools/make-one-time-file.py --real time-of-build.log
+	python ../tools/make-one-time-file.py --real time-of-build.log
 	$(MAKE) report
 endif
 endif