WIP

.nix/nixpkgs.nix

@@ -0,0 +1,4 @@
+fetchTarball {
+         url = "https://github.com/CohenCyril/nixpkgs/archive/d84a118938cd8dccffe8a72083f98209d28d1af2.tar.gz";
+         sha256 = "0yn68b6lc6sxy3v0lgask5bfpwa1jm5xzxqlp12h0mlly9475hpk";
+       }

.nix/rocq-overlays/mathcomp-analysis/default.nix

@@ -0,0 +1,128 @@
+{
+  lib,
+  mkRocqDerivation,
+  mathcomp,
+  mathcomp-finmap,
+  mathcomp-bigenough,
+  rocqnavi,
+  stdlib,
+  single ? false,
+  rocq-core,
+  version ? null,
+}@args:
+
+let
+  repo = "analysis";
+  owner = "math-comp";
+
+  release."1.16.0".sha256 = "sha256-L0dCbxEqxI8rFv6OOEoIT/U3GKX37ageU9yw2H6hrWY=";
+
+  defaultVersion =
+    let
+      case = rocq: mc: out: {
+        cases = [
+          rocq
+          mc
+        ];
+        inherit out;
+      };
+    in
+    with lib.versions;
+    lib.switch
+      [ rocq-core.rocq-version mathcomp.version ]
+      [
+        (case (range "9.0" "9.1") (range "2.4.0" "2.5.0") "1.16.0")
+      ]
+      null;
+
+  # list of analysis packages sorted by dependency order
+  packages = {
+    "classical" = [ ];
+    "reals" = [ "classical" ];
+    "analysis" = [ "reals" ];
+    "experimental-reals" = [ "analysis" ];
+    "reals-stdlib" = [ "reals" ];
+    "analysis-stdlib" = [
+      "analysis"
+      "reals-stdlib"
+    ];
+  };
+
+  mathcomp_ =
+    package:
+    let
+      classical-deps = [
+        mathcomp.algebra
+        mathcomp-finmap
+      ];
+      experimental-reals-deps = [ mathcomp-bigenough ];
+      analysis-deps = [
+        mathcomp.field
+        mathcomp-bigenough
+      ];
+      intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
+      pkgpath =
+        let
+          case = case: out: { inherit case out; };
+        in
+        lib.switch package [
+          (case "single" ".")
+          (case "analysis" "theories")
+          (case "experimental-reals" "experimental_reals")
+          (case "reals-stdlib" "reals_stdlib")
+          (case "analysis-stdlib" "analysis_stdlib")
+        ] package;
+      pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
+      derivation = mkRocqDerivation {
+        inherit
+          version
+          pname
+          defaultVersion
+          release
+          repo
+          owner
+          ;
+
+        namePrefix = [
+          "rocq-core"
+          "mathcomp"
+        ];
+
+        nativeBuildInputs = [ rocqnavi ];
+
+        propagatedBuildInputs =
+          intra-deps
+          ++ lib.optionals (lib.elem package [
+            "classical"
+            "single"
+          ]) classical-deps
+          ++ lib.optionals (lib.elem package [
+            "experimental-reals"
+            "single"
+          ]) experimental-reals-deps
+          ++ lib.optionals (lib.elem package [
+            "analysis"
+            "single"
+          ]) analysis-deps
+          ++ lib.optional (lib.elem package [
+            "reals-stdlib"
+            "analysis-stdlib"
+            "single"
+          ]) stdlib;
+
+        preBuild = ''
+          cd ${pkgpath}
+        '';
+
+        meta = {
+          description = "Analysis library compatible with Mathematical Components";
+          maintainers = [ lib.maintainers.cohencyril ];
+          license = lib.licenses.cecill-c;
+        };
+
+        passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
+      };
+    in
+    derivation;
+in
+mathcomp_ (if single then "single" else "analysis")

Makefile.common

@@ -98,14 +98,16 @@ GIT_HASH := $(shell git describe --tags --exact-match 2>/dev/null || git rev-par
 
 $(DOCDIR)/dependency_graph.pre:
 	mkdir -p $(DOCDIR)
-	coqdep -f _CoqProject | perl etc/builddoc_dependency_dot.pl > $(DOCDIR)/dependency_graph.pre
+	$(COQDEP) -f _CoqProject | perl etc/builddoc_dependency_dot.pl > $(DOCDIR)/dependency_graph.pre
 
 $(DOCDIR)/dependency_graph.dot: $(DOCDIR)/dependency_graph.pre
 	tred $(DOCDIR)/dependency_graph.pre > $(DOCDIR)/dependency_graph.dot
 
-html: build $(DOCDIR)/dependency_graph.dot
+$(DOCDIR)/hierarchy_graph.dot:
 	etc/rocqnavi_generate-hierarchy-graph.sh $(DOCDIR)/hierarchy_graph.dot
-	find . -name "*.v" -or -name "*.glob" | grep -v "/\." | grep -v "_opam/" | xargs rocqnavi \
+
+html: build $(DOCDIR)/dependency_graph.dot $(DOCDIR)/hierarchy_graph.dot
+	find . -name "*.v" -or -name "*.glob" | grep -v "/\." | grep -v "_opam/" | rocqnavi \
 	-title "Mathcomp Analysis $(GIT_HASH)" \
 	-d $(DOCDIR) -Q theories mathcomp.analysis \
 	-Q classical mathcomp.classical \

bin/coqtop

@@ -0,0 +1 @@
+rocq top $*

etc/rocqnavi_generate-hierarchy-graph.sh

@@ -1,5 +1,5 @@
 DST=$1
-coqtop -Q classical mathcomp.classical -Q reals mathcomp.reals -Q reals_stdlib mathcomp.reals_stdlib -Q experimental_reals mathcomp.experimental_reals -Q theories mathcomp.analysis -Q analysis_stdlib mathcomp.analysis_stdlib <<EOF
+rocq top -Q classical mathcomp.classical -Q reals mathcomp.reals -Q reals_stdlib mathcomp.reals_stdlib -Q experimental_reals mathcomp.experimental_reals -Q theories mathcomp.analysis -Q analysis_stdlib mathcomp.analysis_stdlib <<EOF
 From HB Require Import structures.
 Require Import mathcomp.classical.all_classical.
 Require Import mathcomp.analysis.all_analysis.