Skip to content

Commit 2d2d144

Browse files
ejgallegoejgallego
committed
[rocq] Replace COQLIB and COQPATH by ROCQLIB and ROCQPATH versions.
Beware both `rocq c --config` and `coqc --config` still output `COQ*` variable names. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
1 parent 902a269 commit 2d2d144

File tree

14 files changed

+45
-150
lines changed

14 files changed

+45
-150
lines changed

‎doc/rocq.rst‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -345,6 +345,7 @@ The supported Rocq language versions (not the version of Rocq) are:
345345
- ``0.11``: Support for the Rocq Prover; most important changes are:
346346
+ all deprecated features in ``(lang coq 0.10)`` have been removed.
347347
+ ``(mode native)`` is not allowed anymore. It is the default it Rocq was configured with native compute enabled.
348+
+ ``COQPATH`` is not recognized anymore, use ``ROCQPATH``.
348349

349350
.. _rocq-lang-1.0:
350351

‎src/dune_rules/rocq/rocq_config.ml‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -236,9 +236,10 @@ let make ~(coqc : Action.Prog.t) =
236236
let* config_output = config_output in
237237
match Vars.of_lines config_output with
238238
| Ok vars ->
239+
(* EJGA: Note, this is still COQLIB and
240+
COQ_NATIVE_COMPILER_DEFAULT in both [coqc --config] and [rocq c
241+
--config] ; so BEWARE ! *)
239242
let rocqlib = Vars.get_path vars "COQLIB" in
240-
(* this is not available in Coq < 8.14 *)
241-
(* this is not available in Coq < 8.13 *)
242243
let rocq_native_compiler_default = Vars.get_opt vars "COQ_NATIVE_COMPILER_DEFAULT" in
243244
Ok { rocqlib; rocq_native_compiler_default }
244245
| Error msg ->

‎src/dune_rules/rocq/rocq_path.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -196,7 +196,7 @@ let of_env env =
196196
let coqpath =
197197
(* windows uses ';' *)
198198
let coqpath_sep = if Sys.cygwin then ';' else Bin.path_sep in
199-
Env.get env "COQPATH"
199+
Env.get env "ROCQPATH"
200200
|> function
201201
| None -> []
202202
| Some coqpath -> Bin.parse_path ~sep:coqpath_sep coqpath

‎src/dune_rules/rocq/rocq_path.mli‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414
open Import
1515

1616
(** A Rocq Path is a non-dune source of Rocq theories, these can come from Rocq's
17-
stdlib and user-contrib location, and [COQPATH] environment variable. *)
17+
stdlib and user-contrib location, and [ROCQPATH] environment variable. *)
1818

1919
(** This module is similar to [Dir_contents] but for globally installed libs *)
2020

@@ -29,8 +29,8 @@ val vo : t -> Path.t list
2929
(** Does the path correspond to Rocq's [Corelib]? *)
3030
val corelib : t -> bool
3131

32-
(** Build list of Rocq paths from a Rocq install ([COQLIB] and [coqc -config]) *)
32+
(** Build list of Rocq paths from a Rocq install ([ROCQLIB] and [coqc -config]) *)
3333
val of_rocq_install : Context.t -> t list Memo.t
3434

35-
(** Build list of Rocq paths from [COQPATH] variable *)
35+
(** Build list of Rocq paths from [ROCQPATH] variable *)
3636
val of_env : Env.t -> t list Memo.t

‎test/blackbox-tests/test-cases/rocq-native/compose-installed-compat.t/run.t‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@ passed to Coq. This meant that we essentially have `-Q "" user-contrib` being
44
passed. In order to restore this behaviour for Coq lang < 0.8 we explicitly add
55
that flag. This PR makes sure that this is indeed the case.
66

7-
We configure COQLIB to be lib/coq. Coq will search for user-contrib from here.
7+
We configure ROCQLIB to be lib/coq. Coq will search for user-contrib from here.
88
We also need to set up a fake Coq install.
99

1010
$ mkdir -p lib/coq
11-
$ export COQLIB=$PWD/lib/coq
12-
$ echo $COQLIB
11+
$ export ROCQLIB=$PWD/lib/coq
12+
$ echo $ROCQLIB
1313
$TESTCASE_ROOT/lib/coq
1414

1515
$ mkdir -p lib/coq/theories/Init/

‎test/blackbox-tests/test-cases/rocq-native/compose-installed-rebuild.t/run.t‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
We test that installed Coq theories, when updated, prompt Dune to rebuild
22

33
$ mkdir -p lib/coq
4-
$ export COQLIB=$PWD/lib/coq
5-
$ echo $COQLIB
4+
$ export ROCQLIB=$PWD/lib/coq
5+
$ echo $ROCQLIB
66
$TESTCASE_ROOT/lib/coq
77

88
$ mkdir -p lib/coq/theories/Init/

‎test/blackbox-tests/test-cases/rocq-native/compose-installed-sub.t/run.t‎

Lines changed: 6 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ We test composing a project with an installed Coq theory. The installed theory
22
does *not* have to be a dune project. But for the purpose of this test, we use
33
the installation of a Dune project.
44

5-
We configure COQLIB to be lib/coq. Coq will search for user-contrib from here.
5+
We configure ROCQLIB to be lib/coq. Coq will search for user-contrib from here.
66
We also need to set up a fake Coq install.
77

88
$ mkdir -p lib/coq
9-
$ export COQLIB=$PWD/lib/coq
10-
$ echo $COQLIB
9+
$ export ROCQLIB=$PWD/lib/coq
10+
$ echo $ROCQLIB
1111
$TESTCASE_ROOT/lib/coq
1212

1313
$ mkdir -p lib/coq/theories/Init/
@@ -122,19 +122,16 @@ As expected, Dune can no longer build A:
122122
Leaving directory 'user'
123123
[1]
124124

125-
We therefore set a variable called COQPATH which allows for library install
125+
We therefore set a variable called ROCQPATH which allows for library install
126126
locations alternative to user-contrib.
127127

128-
$ export COQPATH=$PWD/another-place/lib/coq/user-contrib
128+
$ export ROCQPATH=$PWD/another-place/lib/coq/user-contrib
129129

130130
Now Dune should be able to build `user` again, since we scan both user-contrib and
131-
all the directories found in COQPATH.
131+
all the directories found in ROCQPATH.
132132

133133
$ dune build --root user
134134
Entering directory 'user'
135-
Warning, feedback message received but no listener to handle it!
136-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
137-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
138135
Inductive hello_alg : Set :=
139136
I : hello_alg
140137
| am : hello_alg
@@ -149,30 +146,12 @@ all the directories found in COQPATH.
149146
| install : hello_field
150147
| loc : hello_field
151148
| at_field : hello_field.
152-
Warning, feedback message received but no listener to handle it!
153-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
154-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
155149
Leaving directory 'user'
156150

157151
We test if having global in the workspace and in user-contrib will cause Dune
158152
any problems. It shouldn't do, as the workspace should take precedence.
159153

160154
$ dune build user
161-
Warning, feedback message received but no listener to handle it!
162-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
163-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
164-
Warning, feedback message received but no listener to handle it!
165-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
166-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
167-
Warning, feedback message received but no listener to handle it!
168-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
169-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
170-
Warning, feedback message received but no listener to handle it!
171-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
172-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
173-
Warning, feedback message received but no listener to handle it!
174-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
175-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
176155
Inductive hello_alg : Set :=
177156
I : hello_alg
178157
| am : hello_alg
@@ -187,9 +166,6 @@ any problems. It shouldn't do, as the workspace should take precedence.
187166
| install : hello_field
188167
| loc : hello_field
189168
| at_field : hello_field.
190-
Warning, feedback message received but no listener to handle it!
191-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
192-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
193169

194170
We test updating the dune file for user to use the super-theory works:
195171

@@ -200,9 +176,6 @@ We test updating the dune file for user to use the super-theory works:
200176
> EOF
201177
$ dune build --root user
202178
Entering directory 'user'
203-
Warning, feedback message received but no listener to handle it!
204-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
205-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
206179
Inductive hello_alg : Set :=
207180
I : hello_alg
208181
| am : hello_alg
@@ -217,9 +190,6 @@ We test updating the dune file for user to use the super-theory works:
217190
| install : hello_field
218191
| loc : hello_field
219192
| at_field : hello_field.
220-
Warning, feedback message received but no listener to handle it!
221-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
222-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
223193
Leaving directory 'user'
224194

225195
We test whether installing `global` again in user-contrib will cause Dune to reject the

‎test/blackbox-tests/test-cases/rocq-native/compose-installed.t/run.t‎

Lines changed: 6 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ We test composing a project with an installed Coq theory. The installed theory
22
does *not* have to be a dune project. But for the purpose of this test, we use
33
the installation of a Dune project.
44

5-
We configure COQLIB to be lib/coq. Coq will search for user-contrib from here.
5+
We configure ROCQLIB to be lib/coq. Coq will search for user-contrib from here.
66
We also need to set up a fake Coq install.
77

88
$ mkdir -p lib/coq
9-
$ export COQLIB=$PWD/lib/coq
10-
$ echo $COQLIB
9+
$ export ROCQLIB=$PWD/lib/coq
10+
$ echo $ROCQLIB
1111
$TESTCASE_ROOT/lib/coq
1212

1313
$ mkdir -p lib/coq/theories/Init/
@@ -84,44 +84,26 @@ As expected, Dune can no longer build A:
8484
Leaving directory 'A'
8585
[1]
8686

87-
We therefore set a variable called COQPATH which allows for library install
87+
We therefore set a variable called ROCQPATH which allows for library install
8888
locations alternative to user-contrib.
8989

90-
$ export COQPATH=$PWD/another-place/lib/coq/user-contrib
90+
$ export ROCQPATH=$PWD/another-place/lib/coq/user-contrib
9191

9292
Now Dune should be able to build A again, since we scan both user-contrib and
93-
all the directories found in COQPATH.
93+
all the directories found in ROCQPATH.
9494

9595
$ dune build --root A
9696
Entering directory 'A'
97-
Warning, feedback message received but no listener to handle it!
98-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
99-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
10097
Inductive hello : Set :=
10198
I : hello | am : hello | an : hello | install : hello | loc : hello.
102-
Warning, feedback message received but no listener to handle it!
103-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
104-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
10599
Leaving directory 'A'
106100

107101
We test if having B in the workspace and in user-contrib will cause Dune
108102
any problems. It shouldn't do, as the workspace should take precedence.
109103

110104
$ dune build A
111-
Warning, feedback message received but no listener to handle it!
112-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
113-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
114-
Warning, feedback message received but no listener to handle it!
115-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
116-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
117-
Warning, feedback message received but no listener to handle it!
118-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
119-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
120105
Inductive hello : Set :=
121106
I : hello | am : hello | an : hello | install : hello | loc : hello.
122-
Warning, feedback message received but no listener to handle it!
123-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
124-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
125107

126108
We test whether installing B again in user-contrib will cause Dune to reject the
127109
build. Currently this is not the case and the first theory is preferred inline

‎test/blackbox-tests/test-cases/rocq/compose-installed-compat.t/run.t‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@ passed to Coq. This meant that we essentially have `-Q "" user-contrib` being
44
passed. In order to restore this behaviour for Coq lang < 0.8 we explicitly add
55
that flag. This PR makes sure that this is indeed the case.
66

7-
We configure COQLIB to be lib/coq. Coq will search for user-contrib from here.
7+
We configure ROCQLIB to be lib/coq. Coq will search for user-contrib from here.
88
We also need to set up a fake Coq install.
99

1010
$ mkdir -p lib/coq
11-
$ export COQLIB=$PWD/lib/coq
12-
$ echo $COQLIB
11+
$ export ROCQLIB=$PWD/lib/coq
12+
$ echo $ROCQLIB
1313
$TESTCASE_ROOT/lib/coq
1414

1515
$ mkdir -p lib/coq/theories/Init/

‎test/blackbox-tests/test-cases/rocq/compose-installed-plugin.t/run.t‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,12 +10,7 @@ When using an installed theory with plugins, things should work fine.
1010
We now build the normal theory, and should work
1111

1212
$ OCAMLPATH=$PWD/lib/:$OCAMLPATH
13-
$ COQPATH=$PWD/lib/coq/user-contrib dune build --root user @all
13+
$ ROCQPATH=$PWD/lib/coq/user-contrib dune build --root user @all
1414
Entering directory 'user'
15-
Warning, feedback message received but no listener to handle it!
16-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
17-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
18-
Warning, feedback message received but no listener to handle it!
19-
Warning: Deprecated environment variable COQPATH, use ROCQPATH instead.
20-
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]Hello
15+
Hello
2116
Leaving directory 'user'

0 commit comments

Comments
 (0)