Skip to content

Commit da6ea45

Browse files
ejgallegoejgallego
authored
Merge pull request #892 from ejgallego/nits_rocq
[misc] [ci] [windows] Some more nits form Rocq / Coq migration
2 parents bf828d3 + d3ed164 commit da6ea45

File tree

12 files changed

+50
-26
lines changed

12 files changed

+50
-26
lines changed

‎.github/workflows/build.yml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,11 @@ jobs:
6969

7070
- name: 🐛 Special Windows Config [only on Win CI]
7171
if: matrix.os == 'windows-latest'
72-
run: opam exec -- make winconfig
72+
run: |
73+
# Waiting on ocamlfind 1.9.8
74+
# c.f. https://github.com/ocaml/opam-repository/pull/27253
75+
opam pin add --dev ocamlfind
76+
opam exec -- make winconfig
7377
7478
- name: 🧱 Build coq-lsp
7579
run: opam exec -- make build

‎Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -147,7 +147,8 @@ make-fmt: build fmt
147147
.PHONY: opam-update-and-reinstall
148148
opam-update-and-reinstall:
149149
git pull --recurse-submodules
150-
for pkg in rocq-runtime coq-core rocq-core stdlib/coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done
150+
for pkg in rocq-runtime coq-core rocq-core coqide-server rocq coq; do opam install -y vendor/coq/$$pkg.opam; done
151+
for pkg in rocq-stdlib coq-stdlib; do opam install -y vendor/coq-stdlib/$$pkg.opam; done
151152
opam install .
152153

153154
.PHONY: patch-for-js

‎coq/workspace.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -172,7 +172,7 @@ let make ~cmdline ~implicit ~kind ~debug =
172172
in
173173
let require_libs =
174174
let rq_list =
175-
if init then ((None, "Stdlib.Init.Prelude") :: require_libraries) @ libs
175+
if init then ((None, "Corelib.Init.Prelude") :: require_libraries) @ libs
176176
else require_libraries @ libs
177177
in
178178
List.map mk_require_from rq_list

‎petanque/README.md

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,8 +40,7 @@ $ opam install coq-lsp
4040

4141
```
4242
$ git clone ... coq-lsp && cd coq-lsp
43-
$ opam install vendor/coq/coq{-core,-stdlib,ide-server,}.opam
44-
$ opam install .
43+
$ make opam-update-and-reinstall
4544
$ opam install coq-mathcomp-ssreflect # etc...
4645
```
4746

‎petanque/test/dune

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,32 @@
11
(test
22
(name basic_api)
33
(modules basic_api)
4-
(deps test.v)
4+
(deps
5+
(package rocq-stdlib)
6+
(package coq-lsp)
7+
test.v)
58
(libraries petanque_shell))
69

710
(test
811
(name json_api)
912
(modules json_api)
10-
(deps test.v %{bin:pet})
13+
(deps
14+
(package rocq-stdlib)
15+
(package coq-lsp)
16+
test.v
17+
%{bin:pet})
1118
(enabled_if
1219
(<> %{os_type} "Win32"))
1320
(libraries petanque petanque_shell lsp))
1421

1522
(test
1623
(name json_api_failure)
1724
(modules json_api_failure)
18-
(deps test.v %{bin:pet})
25+
(deps
26+
(package rocq-stdlib)
27+
(package coq-lsp)
28+
test.v
29+
%{bin:pet})
1930
(enabled_if
2031
(<> %{os_type} "Win32"))
2132
(libraries petanque petanque_shell lsp))

‎test/compiler/basic/dune

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33
(source_tree proj1)
44
(source_tree proj2)
55
(source_tree tests)
6-
; For the plugins to be built
6+
; For the Coq prelude to be built
7+
(package rocq-core)
8+
; For the serlib plugins to be built
79
(package coq-lsp)
810
%{bin:fcc}))

‎test/compiler/basic/run.t

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Describe the project
66
[message] Configuration loaded from Command-line arguments
77
- coqlib is at: [TEST_PATH]
88
+ coqcorelib is at: [TEST_PATH]
9-
- Modules [Stdlib.Init.Prelude] will be loaded by default
9+
- Modules [Corelib.Init.Prelude] will be loaded by default
1010
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
1111
- ocamlpath added paths: []
1212
+ findlib config: [TEST_PATH]
@@ -17,7 +17,7 @@ Compile a single file, don't generate a `.vo` file:
1717
[message] Configuration loaded from Command-line arguments
1818
- coqlib is at: [TEST_PATH]
1919
+ coqcorelib is at: [TEST_PATH]
20-
- Modules [Stdlib.Init.Prelude] will be loaded by default
20+
- Modules [Corelib.Init.Prelude] will be loaded by default
2121
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
2222
- ocamlpath added paths: []
2323
+ findlib config: [TEST_PATH]
@@ -33,7 +33,7 @@ Compile a single file, generate a .vo file
3333
[message] Configuration loaded from Command-line arguments
3434
- coqlib is at: [TEST_PATH]
3535
+ coqcorelib is at: [TEST_PATH]
36-
- Modules [Stdlib.Init.Prelude] will be loaded by default
36+
- Modules [Corelib.Init.Prelude] will be loaded by default
3737
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
3838
- ocamlpath added paths: []
3939
+ findlib config: [TEST_PATH]
@@ -53,7 +53,7 @@ Compile a dependent file
5353
[message] Configuration loaded from Command-line arguments
5454
- coqlib is at: [TEST_PATH]
5555
+ coqcorelib is at: [TEST_PATH]
56-
- Modules [Stdlib.Init.Prelude] will be loaded by default
56+
- Modules [Corelib.Init.Prelude] will be loaded by default
5757
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
5858
- ocamlpath added paths: []
5959
+ findlib config: [TEST_PATH]
@@ -73,7 +73,7 @@ Compile both files
7373
[message] Configuration loaded from Command-line arguments
7474
- coqlib is at: [TEST_PATH]
7575
+ coqcorelib is at: [TEST_PATH]
76-
- Modules [Stdlib.Init.Prelude] will be loaded by default
76+
- Modules [Corelib.Init.Prelude] will be loaded by default
7777
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
7878
- ocamlpath added paths: []
7979
+ findlib config: [TEST_PATH]
@@ -94,7 +94,7 @@ Compile a dependent file without the dep being built
9494
[message] Configuration loaded from Command-line arguments
9595
- coqlib is at: [TEST_PATH]
9696
+ coqcorelib is at: [TEST_PATH]
97-
- Modules [Stdlib.Init.Prelude] will be loaded by default
97+
- Modules [Corelib.Init.Prelude] will be loaded by default
9898
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
9999
- ocamlpath added paths: []
100100
+ findlib config: [TEST_PATH]
@@ -131,7 +131,7 @@ Compile a file with all messages:
131131
[message] Configuration loaded from Command-line arguments
132132
- coqlib is at: [TEST_PATH]
133133
+ coqcorelib is at: [TEST_PATH]
134-
- Modules [Stdlib.Init.Prelude] will be loaded by default
134+
- Modules [Corelib.Init.Prelude] will be loaded by default
135135
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
136136
- ocamlpath added paths: []
137137
+ findlib config: [TEST_PATH]
@@ -142,7 +142,7 @@ Compile a file with all messages:
142142
[message] Configuration loaded from Command-line arguments
143143
- coqlib is at: [TEST_PATH]
144144
+ coqcorelib is at: [TEST_PATH]
145-
- Modules [Stdlib.Init.Prelude] will be loaded by default
145+
- Modules [Corelib.Init.Prelude] will be loaded by default
146146
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
147147
- ocamlpath added paths: []
148148
+ findlib config: [TEST_PATH]
@@ -172,15 +172,15 @@ Use two workspaces
172172
[message] Configuration loaded from Command-line arguments
173173
- coqlib is at: [TEST_PATH]
174174
+ coqcorelib is at: [TEST_PATH]
175-
- Modules [Stdlib.Init.Prelude] will be loaded by default
175+
- Modules [Corelib.Init.Prelude] will be loaded by default
176176
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
177177
- ocamlpath added paths: []
178178
+ findlib config: [TEST_PATH]
179179
+ findlib default location: [TEST_PATH]
180180
[message] Configuration loaded from Command-line arguments
181181
- coqlib is at: [TEST_PATH]
182182
+ coqcorelib is at: [TEST_PATH]
183-
- Modules [Stdlib.Init.Prelude] will be loaded by default
183+
- Modules [Corelib.Init.Prelude] will be loaded by default
184184
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
185185
- ocamlpath added paths: []
186186
+ findlib config: [TEST_PATH]
@@ -197,7 +197,7 @@ Load the example plugin
197197
[message] Configuration loaded from Command-line arguments
198198
- coqlib is at: [TEST_PATH]
199199
+ coqcorelib is at: [TEST_PATH]
200-
- Modules [Stdlib.Init.Prelude] will be loaded by default
200+
- Modules [Corelib.Init.Prelude] will be loaded by default
201201
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
202202
- ocamlpath added paths: []
203203
+ findlib config: [TEST_PATH]
@@ -210,7 +210,7 @@ Load the astdump plugin
210210
[message] Configuration loaded from Command-line arguments
211211
- coqlib is at: [TEST_PATH]
212212
+ coqcorelib is at: [TEST_PATH]
213-
- Modules [Stdlib.Init.Prelude] will be loaded by default
213+
- Modules [Corelib.Init.Prelude] will be loaded by default
214214
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
215215
- ocamlpath added paths: []
216216
+ findlib config: [TEST_PATH]
@@ -235,7 +235,7 @@ We do the same for the goaldump plugin:
235235
[message] Configuration loaded from Command-line arguments
236236
- coqlib is at: [TEST_PATH]
237237
+ coqcorelib is at: [TEST_PATH]
238-
- Modules [Stdlib.Init.Prelude] will be loaded by default
238+
- Modules [Corelib.Init.Prelude] will be loaded by default
239239
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
240240
- ocamlpath added paths: []
241241
+ findlib config: [TEST_PATH]

‎test/compiler/exit_code/dune

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
(deps
33
_CoqProject
44
Demo.v
5-
; For the plugins to be built
5+
; For the Coq prelude to be built
6+
(package rocq-core)
7+
; For the serlib plugins to be built
68
(package coq-lsp)
79
%{bin:fcc}))

‎test/compiler/exit_code/run.t

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Describe the environment:
77
[message] Configuration loaded from ./_CoqProject
88
- coqlib is at: [TEST_PATH]
99
+ coqcorelib is at: [TEST_PATH]
10-
- Modules [Stdlib.Init.Prelude] will be loaded by default
10+
- Modules [Corelib.Init.Prelude] will be loaded by default
1111
- 3 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
1212
- ocamlpath added paths: []
1313
+ findlib config: [TEST_PATH]

‎test/compiler/long_file/dune

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
(cram
22
(deps
3-
; For the plugins to be built
3+
; For the Coq prelude to be built
4+
(package rocq-core)
5+
; For the serlib plugins to be built
46
(package coq-lsp)
57
%{bin:fcc}))

‎test/compiler/long_file/run.t

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ We now compile the challenging file:
1010
[message] Configuration loaded from Command-line arguments
1111
- coqlib is at: [TEST_PATH]
1212
+ coqcorelib is at: [TEST_PATH]
13-
- Modules [Stdlib.Init.Prelude] will be loaded by default
13+
- Modules [Corelib.Init.Prelude] will be loaded by default
1414
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
1515
- ocamlpath added paths: []
1616
+ findlib config: [TEST_PATH]

‎test/serlib/genarg/dune

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@
44
(targets test_roundtrip)
55
(deps
66
(:input test_roundtrip.in)
7+
; For the Coq prelude to be built
8+
(package rocq-core)
9+
; For the serlib plugins to be built
710
(package coq-lsp))
811
(action
912
(progn

0 commit comments

Comments
 (0)