Add repro for #7344.

Signed-off-by: Rodolphe Lepigre <[email protected]>

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/dune

@@ -0,0 +1,3 @@
+(include_subdirs qualified)
+(coq.theory
+ (name theory2))

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune

@@ -0,0 +1,2 @@
+(coq.theory
+ (name theory1))

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-workspace

@@ -0,0 +1 @@
+(lang dune 3.8)

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/dune

@@ -0,0 +1,3 @@
+(include_subdirs qualified)
+(coq.theory
+ (name theory4))

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune

@@ -0,0 +1,2 @@
+(coq.theory
+ (name theory3))

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/run.t

@@ -0,0 +1,120 @@
+Running "dune coq top" from different directories in a workspace. The setup is
+a workspace whose root is the root of a first project, and a second project is
+contained under directory "project".
+
+  $ unset INSIDE_DUNE
+  $ . ./util.sh
+
+Calling "dune coq top" from the workspace root.
+
+  $ coqtop_test file1.v
+  $ coqtop_test coq_dir1/file2.v
+  $ coqtop_test coq_dir1/dir1/file3.v
+  $ coqtop_test project/file4.v
+  $ coqtop_test project/coq_dir2/file5.v
+  $ coqtop_test project/coq_dir2/dir2/file6.v
+
+  $ check_build
+
+Calling "dune coq top" from the "coq_dir1" directory.
+
+  $ cd coq_dir1
+
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../coq_dir1/file2.v
+  $ coqtop_test ../coq_dir1/dir1/file3.v
+  $ coqtop_test ../project/file4.v
+  $ coqtop_test ../project/coq_dir2/file5.v
+  $ coqtop_test ../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test file2.v
+  $ coqtop_test dir1/file3.v
+
+  $ cd ..
+
+  $ check_build
+
+Calling "dune coq top" from the "coq_dir1/dir1" directory.
+
+  $ cd coq_dir1/dir1
+
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../coq_dir1/file2.v
+  $ coqtop_test ../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../project/file4.v
+  $ coqtop_test ../../project/coq_dir2/file5.v
+  $ coqtop_test ../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../file2.v
+  $ coqtop_test ../dir1/file3.v
+  $ coqtop_test file3.v
+
+  $ cd ../..
+
+  $ check_build
+
+Calling "dune coq top" from the "project" directory.
+
+  $ cd project
+
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../coq_dir1/file2.v
+  $ coqtop_test ../coq_dir1/dir1/file3.v
+  $ coqtop_test ../project/file4.v
+  $ coqtop_test ../project/coq_dir2/file5.v
+  $ coqtop_test ../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test file4.v
+  $ coqtop_test coq_dir2/file5.v
+  $ coqtop_test coq_dir2/dir2/file6.v
+
+  $ cd ..
+
+  $ check_build
+
+Calling "dune coq top" from the "project/coq_dir2" directory.
+
+  $ cd project/coq_dir2
+
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../coq_dir1/file2.v
+  $ coqtop_test ../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../project/file4.v
+  $ coqtop_test ../../project/coq_dir2/file5.v
+  $ coqtop_test ../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../file4.v
+  $ coqtop_test ../coq_dir2/file5.v
+  $ coqtop_test ../coq_dir2/dir2/file6.v
+  $ coqtop_test file5.v
+  $ coqtop_test dir2/file6.v
+
+  $ cd ../..
+
+  $ check_build
+
+Calling "dune coq top" from the "project/coq_dir2/dir2" directory.
+
+  $ cd project/coq_dir2/dir2
+
+  $ coqtop_test ../../../file1.v
+  $ coqtop_test ../../../file1.v
+  $ coqtop_test ../../../coq_dir1/file2.v
+  $ coqtop_test ../../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../../project/file4.v
+  $ coqtop_test ../../../project/coq_dir2/file5.v
+  $ coqtop_test ../../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../../file4.v
+  $ coqtop_test ../../coq_dir2/file5.v
+  $ coqtop_test ../../coq_dir2/dir2/file6.v
+  $ coqtop_test ../file5.v
+  $ coqtop_test ../dir2/file6.v
+  $ coqtop_test file6.v
+
+  $ cd ../../..
+
+  $ check_build

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/util.sh

@@ -0,0 +1,20 @@
+#!/bin/bash
+
+export OUTPUT="$PWD/coqtop_test.tmp"
+export PWD0="$PWD"
+
+function coqtop_test() {
+  (true | (dune coq top "$1" 1>$OUTPUT 2>&1)) || cat $OUTPUT
+}
+
+function check_build() {
+  if [[ ! -d "./_build" ]]; then
+    echo "No build directory found..."
+    exit 1
+  fi
+
+  if [[ $(find . -name _build -type d | wc -l) > 1 ]]; then
+    echo "More than one _build directory..."
+    exit 1
+  fi
+}