Skip to content

Commit f018a11

Browse files
jwiegleyjwiegley
authored
Update flake.lock and change default version to Rocq 9.1 (#167)
1 parent 3e1e0ba commit f018a11

File tree

2 files changed

+78
-17
lines changed

2 files changed

+78
-17
lines changed

‎flake.lock‎

Lines changed: 3 additions & 3 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix‎

Lines changed: 75 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,14 @@
1111
let pkgs = import nixpkgs { inherit system; };
1212
in rec {
1313
packages = rec {
14-
equations = coqPackages: with pkgs.${coqPackages}; pkgs.stdenv.mkDerivation rec {
14+
equations = coqPackages: with pkgs.${coqPackages};
15+
let
16+
useDune = coqPackages == "coqPackages_9_0" || coqPackages == "coqPackages_9_1";
17+
rocqPackages = if coqPackages == "coqPackages_9_0" then "rocqPackages_9_0"
18+
else if coqPackages == "coqPackages_9_1" then "rocqPackages_9_1"
19+
else null;
20+
stdlib = if rocqPackages != null then pkgs.${rocqPackages}.stdlib else null;
21+
in pkgs.stdenv.mkDerivation rec {
1522
name = "coq${coq.coq-version}-equations-${version}";
1623
version = "1.3";
1724

@@ -53,21 +60,56 @@
5360
then {
5461
rev = "v1.3.1-8.20";
5562
sha256 = "sha256-u8LB1KiACM5zVaoL7dSdHYvZgX7pf30VuqtjLLGuTzc=";
63+
} else {}) //
64+
(if coqPackages == "coqPackages_9_0"
65+
then {
66+
rev = "v1.3.1-9.0";
67+
sha256 = "sha256-186Z0/wCuGAjIvG1LoYBMPooaC6HmnKWowYXuR0y6bA=";
68+
} else {}) //
69+
(if coqPackages == "coqPackages_9_1"
70+
then {
71+
rev = "v1.3.1-9.1";
72+
sha256 = "sha256-LtYbAR3jt+JbYcqP+m1n3AZhAWSMIeOZtmdSJwg7L1A=";
5673
} else {}));
5774

58-
phases = [
59-
"unpackPhase" "configurePhase" "buildPhase" "checkPhase" "installPhase"
60-
];
61-
75+
nativeBuildInputs = pkgs.lib.optionals useDune [ pkgs.dune_3 ];
6276
buildInputs = [
6377
coq coq.ocaml coq.findlib
78+
] ++ pkgs.lib.optionals useDune [
79+
coq.ocamlPackages.ppx_optcomp
80+
] ++ pkgs.lib.optionals (stdlib != null) [
81+
stdlib
6482
];
6583
enableParallelBuilding = true;
6684

67-
configurePhase = "coq_makefile -f _CoqProject -o Makefile.coq";
68-
checkPhase = "make examples test-suite";
69-
70-
installFlags = [
85+
buildPhase = if useDune
86+
then "dune build -p rocq-equations @install"
87+
else "make";
88+
89+
configurePhase = if useDune
90+
then ""
91+
else "coq_makefile -f _CoqProject -o Makefile.coq";
92+
93+
checkPhase = if useDune
94+
then ""
95+
else "make examples test-suite";
96+
97+
# For Dune-based builds (Rocq 9.0/9.1), install to standard locations
98+
installPhase = if useDune
99+
then ''
100+
# Install using Dune's standard layout
101+
# Dune installs Coq theories to $libdir/coq/user-contrib/
102+
dune install rocq-equations --prefix=$out --libdir=$out/lib/ocaml
103+
104+
# Create symlink for standard Coq layout compatibility
105+
# Dune puts files in lib/ocaml/coq/user-contrib/
106+
# We symlink to lib/coq/VERSION/user-contrib/ for coq_makefile
107+
mkdir -p $out/lib/coq/${coq.coq-version}
108+
ln -sf $out/lib/ocaml/coq/user-contrib $out/lib/coq/${coq.coq-version}/user-contrib
109+
''
110+
else null;
111+
112+
installFlags = if useDune then [] else [
71113
"COQLIB=$(out)/lib/coq/${coq.coq-version}/"
72114
"COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
73115
"COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
@@ -78,11 +120,19 @@
78120
env.env = pkgs.buildEnv { inherit name; paths = buildInputs; };
79121
passthru = {
80122
compatibleCoqVersions = v:
81-
builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" "8.20" ];
123+
builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" "8.20" "9.0" "9.1" ];
82124
};
83125
};
84126

85-
category-theory = coqPackages: with pkgs.${coqPackages}; pkgs.stdenv.mkDerivation rec {
127+
category-theory = coqPackages: with pkgs.${coqPackages};
128+
let
129+
isRocq = coqPackages == "coqPackages_9_0" || coqPackages == "coqPackages_9_1";
130+
rocqPackages = if coqPackages == "coqPackages_9_0" then "rocqPackages_9_0"
131+
else if coqPackages == "coqPackages_9_1" then "rocqPackages_9_1"
132+
else null;
133+
stdlib = if rocqPackages != null then pkgs.${rocqPackages}.stdlib else null;
134+
eqns = equations coqPackages;
135+
in pkgs.stdenv.mkDerivation rec {
86136
name = "coq${coq.coq-version}-category-theory-${version}";
87137
version = "1.0";
88138

@@ -91,13 +141,22 @@
91141
else ./.;
92142

93143
buildInputs = [
94-
coq coq.ocaml coq.findlib (equations coqPackages)
144+
coq coq.ocaml coq.findlib eqns
95145
] ++ pkgs.lib.optionals (coqPackages == "coqPackages_8_14" ||
96146
coqPackages == "coqPackages_8_15") [
97147
dpdgraph
148+
] ++ pkgs.lib.optionals (stdlib != null) [
149+
stdlib
98150
];
99151
enableParallelBuilding = true;
100152

153+
# Set path variables for finding Equations theories and plugins
154+
# For Rocq 9.x, use ROCQPATH; for older Coq, use COQPATH
155+
# OCAMLPATH allows findlib to locate the rocq-equations.plugin package (for Rocq 9.x)
156+
ROCQPATH = if isRocq then "${eqns}/lib/coq/${coq.coq-version}/user-contrib" else null;
157+
COQPATH = if isRocq then null else "${eqns}/lib/coq/${coq.coq-version}/user-contrib";
158+
OCAMLPATH = if isRocq then "${eqns}/lib/ocaml" else null;
159+
101160
configurePhase = "coq_makefile -f _CoqProject -o Makefile.coq";
102161

103162
installFlags = [
@@ -111,7 +170,7 @@
111170
env.env = pkgs.buildEnv { inherit name; paths = buildInputs; };
112171
passthru = {
113172
compatibleCoqVersions = v:
114-
builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" "8.20" ];
173+
builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" "8.20" "9.0" "9.1" ];
115174
};
116175
};
117176

@@ -122,8 +181,10 @@
122181
category-theory_8_18 = category-theory "coqPackages_8_18";
123182
category-theory_8_19 = category-theory "coqPackages_8_19";
124183
category-theory_8_20 = category-theory "coqPackages_8_20";
184+
category-theory_9_0 = category-theory "coqPackages_9_0";
185+
category-theory_9_1 = category-theory "coqPackages_9_1";
125186

126-
default = category-theory_8_20;
187+
default = category-theory_9_1;
127188
};
128189

129190
defaultPackage = packages.default;

0 commit comments

Comments
 (0)