Skip to content

Commit 1303da0

Browse files
CohenCyrilCohenCyril
committed
WIP
1 parent fbbb9e6 commit 1303da0

5 files changed

Lines changed: 139 additions & 4 deletions

File tree

‎.nix/nixpkgs.nix‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
fetchTarball {
2+
url = "https://github.com/CohenCyril/nixpkgs/archive/d84a118938cd8dccffe8a72083f98209d28d1af2.tar.gz";
3+
sha256 = "0yn68b6lc6sxy3v0lgask5bfpwa1jm5xzxqlp12h0mlly9475hpk";
4+
}

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

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,128 @@
1+
{
2+
lib,
3+
mkRocqDerivation,
4+
mathcomp,
5+
mathcomp-finmap,
6+
mathcomp-bigenough,
7+
rocqnavi,
8+
stdlib,
9+
single ? false,
10+
rocq-core,
11+
version ? null,
12+
}@args:
13+
14+
let
15+
repo = "analysis";
16+
owner = "math-comp";
17+
18+
release."1.16.0".sha256 = "sha256-L0dCbxEqxI8rFv6OOEoIT/U3GKX37ageU9yw2H6hrWY=";
19+
20+
defaultVersion =
21+
let
22+
case = rocq: mc: out: {
23+
cases = [
24+
rocq
25+
mc
26+
];
27+
inherit out;
28+
};
29+
in
30+
with lib.versions;
31+
lib.switch
32+
[ rocq-core.rocq-version mathcomp.version ]
33+
[
34+
(case (range "9.0" "9.1") (range "2.4.0" "2.5.0") "1.16.0")
35+
]
36+
null;
37+
38+
# list of analysis packages sorted by dependency order
39+
packages = {
40+
"classical" = [ ];
41+
"reals" = [ "classical" ];
42+
"analysis" = [ "reals" ];
43+
"experimental-reals" = [ "analysis" ];
44+
"reals-stdlib" = [ "reals" ];
45+
"analysis-stdlib" = [
46+
"analysis"
47+
"reals-stdlib"
48+
];
49+
};
50+
51+
mathcomp_ =
52+
package:
53+
let
54+
classical-deps = [
55+
mathcomp.algebra
56+
mathcomp-finmap
57+
];
58+
experimental-reals-deps = [ mathcomp-bigenough ];
59+
analysis-deps = [
60+
mathcomp.field
61+
mathcomp-bigenough
62+
];
63+
intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
64+
pkgpath =
65+
let
66+
case = case: out: { inherit case out; };
67+
in
68+
lib.switch package [
69+
(case "single" ".")
70+
(case "analysis" "theories")
71+
(case "experimental-reals" "experimental_reals")
72+
(case "reals-stdlib" "reals_stdlib")
73+
(case "analysis-stdlib" "analysis_stdlib")
74+
] package;
75+
pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
76+
derivation = mkRocqDerivation {
77+
inherit
78+
version
79+
pname
80+
defaultVersion
81+
release
82+
repo
83+
owner
84+
;
85+
86+
namePrefix = [
87+
"rocq-core"
88+
"mathcomp"
89+
];
90+
91+
nativeBuildInputs = [ rocqnavi ];
92+
93+
propagatedBuildInputs =
94+
intra-deps
95+
++ lib.optionals (lib.elem package [
96+
"classical"
97+
"single"
98+
]) classical-deps
99+
++ lib.optionals (lib.elem package [
100+
"experimental-reals"
101+
"single"
102+
]) experimental-reals-deps
103+
++ lib.optionals (lib.elem package [
104+
"analysis"
105+
"single"
106+
]) analysis-deps
107+
++ lib.optional (lib.elem package [
108+
"reals-stdlib"
109+
"analysis-stdlib"
110+
"single"
111+
]) stdlib;
112+
113+
preBuild = ''
114+
cd ${pkgpath}
115+
'';
116+
117+
meta = {
118+
description = "Analysis library compatible with Mathematical Components";
119+
maintainers = [ lib.maintainers.cohencyril ];
120+
license = lib.licenses.cecill-c;
121+
};
122+
123+
passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
124+
};
125+
in
126+
derivation;
127+
in
128+
mathcomp_ (if single then "single" else "analysis")

‎Makefile.common‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -98,14 +98,16 @@ GIT_HASH := $(shell git describe --tags --exact-match 2>/dev/null || git rev-par
9898

9999
$(DOCDIR)/dependency_graph.pre:
100100
mkdir -p $(DOCDIR)
101-
coqdep -f _CoqProject | perl etc/builddoc_dependency_dot.pl > $(DOCDIR)/dependency_graph.pre
101+
$(COQDEP) -f _CoqProject | perl etc/builddoc_dependency_dot.pl > $(DOCDIR)/dependency_graph.pre
102102

103103
$(DOCDIR)/dependency_graph.dot: $(DOCDIR)/dependency_graph.pre
104104
tred $(DOCDIR)/dependency_graph.pre > $(DOCDIR)/dependency_graph.dot
105105

106-
html: build $(DOCDIR)/dependency_graph.dot
106+
$(DOCDIR)/hierarchy_graph.dot:
107107
etc/rocqnavi_generate-hierarchy-graph.sh $(DOCDIR)/hierarchy_graph.dot
108-
find . -name "*.v" -or -name "*.glob" | grep -v "/\." | grep -v "_opam/" | xargs rocqnavi \
108+
109+
html: build $(DOCDIR)/dependency_graph.dot $(DOCDIR)/hierarchy_graph.dot
110+
find . -name "*.v" -or -name "*.glob" | grep -v "/\." | grep -v "_opam/" | rocqnavi \
109111
-title "Mathcomp Analysis $(GIT_HASH)" \
110112
-d $(DOCDIR) -Q theories mathcomp.analysis \
111113
-Q classical mathcomp.classical \

‎bin/coqtop‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rocq top $*

‎etc/rocqnavi_generate-hierarchy-graph.sh‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
DST=$1
2-
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
2+
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
33
From HB Require Import structures.
44
Require Import mathcomp.classical.all_classical.
55
Require Import mathcomp.analysis.all_analysis.

0 commit comments

Comments
 (0)