Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adapt w.r.t. coq/coq#19313. #802

Merged
merged 1 commit into from
Jul 7, 2024
Merged

Adapt w.r.t. coq/coq#19313. #802

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions coq/loader.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,10 @@ let map_serlib fl_pkg =
let supported = match fl_pkg with
(* Supported by serlib *) (* directory *)
| "coq-core.plugins.btauto" (* btauto *)
| "coq-core.plugins.cc_core" (* cc_core *)
| "coq-core.plugins.cc" (* cc *)
| "coq-core.plugins.extraction" (* extraction *)
| "coq-core.plugins.firstorder_core" (* firstorder_core *)
| "coq-core.plugins.firstorder" (* firstorder *)
| "coq-core.plugins.funind" (* funind *)
| "coq-core.plugins.ltac" (* ltac *)
Expand Down
12 changes: 12 additions & 0 deletions serlib/plugins/cc_core/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
(library
(name serlib_cc_core)
(public_name coq-lsp.serlib.cc_core)
(synopsis "Serialization Library for Coq Cc_core Plugin")
(preprocess
(staged_pps
ppx_import
ppx_sexp_conv
ppx_deriving_yojson
ppx_hash
ppx_compare))
(libraries coq-core.plugins.cc_core serlib sexplib))
12 changes: 12 additions & 0 deletions serlib/plugins/firstorder_core/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
(library
(name serlib_firstorder_core)
(public_name coq-lsp.serlib.firstorder_core)
(synopsis "Serialization Library for Coq Firstorder_core Plugin")
(preprocess
(staged_pps
ppx_import
ppx_sexp_conv
ppx_deriving_yojson
ppx_hash
ppx_compare))
(libraries coq-core.plugins.firstorder_core serlib sexplib))
12 changes: 12 additions & 0 deletions serlib/plugins/nsatz_core/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
(library
(name serlib_nsatz_core)
(public_name coq-lsp.serlib.nsatz_core)
(synopsis "Serialization Library for Coq Nsatz_core Plugin")
(preprocess
(staged_pps
ppx_import
ppx_sexp_conv
ppx_deriving_yojson
ppx_hash
ppx_compare))
(libraries coq-core.plugins.nsatz_core serlib sexplib))
26 changes: 13 additions & 13 deletions test/compiler/basic/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ Describe the project
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -18,7 +18,7 @@ Compile a single file, don't generate a `.vo` file:
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -34,7 +34,7 @@ Compile a single file, generate a .vo file
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -54,7 +54,7 @@ Compile a dependent file
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -74,7 +74,7 @@ Compile both files
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -95,7 +95,7 @@ Compile a dependent file without the dep being built
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand Down Expand Up @@ -132,7 +132,7 @@ Compile a file with all messages:
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -143,7 +143,7 @@ Compile a file with all messages:
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand Down Expand Up @@ -173,15 +173,15 @@ Use two workspaces
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
[message] Configuration loaded from Command-line arguments
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -198,7 +198,7 @@ Load the example plugin
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -211,7 +211,7 @@ Load the astdump plugin
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand All @@ -236,7 +236,7 @@ We do the same for the goaldump plugin:
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand Down
2 changes: 1 addition & 1 deletion test/compiler/exit_code/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Describe the environment:
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 3 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 3 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand Down
2 changes: 1 addition & 1 deletion test/compiler/long_file/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ We now compile the challenging file:
- coqlib is at: [TEST_PATH]
+ coqcorelib is at: [TEST_PATH]
- Modules [Coq.Init.Prelude] will be loaded by default
- 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
- 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
- ocamlpath wasn't overriden
+ findlib config: [TEST_PATH]
+ findlib default location: [TEST_PATH]
Expand Down
2 changes: 1 addition & 1 deletion vendor/coq
Open in desktop
Submodule coq updated 166 files
Loading