-
Notifications
You must be signed in to change notification settings - Fork 409
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add reproduction test-case for dune#11012.
Signed-off-by: Rodolphe Lepigre <[email protected]>
- Loading branch information
Rodolphe Lepigre
committed
Nov 4, 2024
1 parent
b409963
commit 7f57d8c
Showing
14 changed files
with
33 additions
and
0 deletions.
There are no files selected for viewing
Empty file.
Empty file.
3 changes: 3 additions & 0 deletions
3
test/blackbox-tests/test-cases/coq/plugin-deps.t/coqlib/dune-project
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
(lang dune 3.8) | ||
(using coq 0.8) | ||
(name coqlib) |
Empty file.
4 changes: 4 additions & 0 deletions
4
test/blackbox-tests/test-cases/coq/plugin-deps.t/coqlib/plugin/dune
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
(library | ||
(name coqlib_plugin) | ||
(public_name coqlib-plugin.plugin) | ||
(libraries somelib)) |
Empty file.
9 changes: 9 additions & 0 deletions
9
test/blackbox-tests/test-cases/coq/plugin-deps.t/coqlib/theories/dune
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
(coq.theory | ||
(name coqlib) | ||
(package coqlib) | ||
(plugins coqlib-plugin.plugin)) | ||
|
||
;(rule | ||
; (targets dummy.v) | ||
; (deps (package coqlib-plugin)) | ||
; (action (with-stdout-to %{targets} (echo "(* dummy file *)")))) |
1 change: 1 addition & 0 deletions
1
test/blackbox-tests/test-cases/coq/plugin-deps.t/coqlib/theories/plugin.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Declare ML Module "coqlib-plugin.plugin". |
1 change: 1 addition & 0 deletions
1
test/blackbox-tests/test-cases/coq/plugin-deps.t/dune-workspace
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
(lang dune 3.8) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
The following should succeed. | ||
|
||
$ dune build coqlib/theories/plugin.vo | ||
Warning: Cannot open directory ../../somelib/src | ||
[cannot-open-dir,filesystem,default] | ||
File "./coqlib/theories/plugin.v", line 1, characters 0-41: | ||
Error: | ||
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"$TESTCASE_ROOT/_build/install/default/lib/somelib/somelib.cmxs: cannot open shared object file: No such file or directory\")") | ||
|
||
[1] |
2 changes: 2 additions & 0 deletions
2
test/blackbox-tests/test-cases/coq/plugin-deps.t/somelib/dune-project
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
(lang dune 3.8) | ||
(name somelib) |
Empty file.
2 changes: 2 additions & 0 deletions
2
test/blackbox-tests/test-cases/coq/plugin-deps.t/somelib/src/dune
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
(library | ||
(public_name somelib)) |
1 change: 1 addition & 0 deletions
1
test/blackbox-tests/test-cases/coq/plugin-deps.t/somelib/src/version.ml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
let version = "dev" |