Correctly run tests with opam

I have no clue how to get it to work with dune so I call make
directly.

We make test suite get BIN from configure.
(COQLIB was already found that way)
We also use this in CI test-suite-template instead of passing them
through the command line.

Close coq#17923

Might be worth adding `--with-test` in the CI `pkg:opam` script?

.gitlab-ci.yml

@@ -147,11 +147,8 @@ before_script:
   script:
     - cd test-suite
     - make clean
-    # careful with the ending /
-    - BIN=$(readlink -f ../_install_ci/bin)/
-    - LIB=$(readlink -f ../_install_ci/lib/coq)/
     - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
-    - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" all
+    - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" all
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure

coq.opam

@@ -26,8 +26,15 @@ depends: [
   "coqide-server" {= version}
   "odoc" {with-doc}
 ]
+dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
+  [ "./configure"
+    "-prefix" prefix
+    "-mandir" man
+    "-libdir" "%{lib}%/coq"
+    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+  ] {with-test}
   [
     "dune"
     "build"
@@ -37,9 +44,8 @@ build: [
     jobs
     "--promote-install-files=false"
     "@install"
-    "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  [ make "-C" "test-suite" "-j" jobs "COQ_INSTALLED=1" "PRINT_LOGS=1" ] {with-test}
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
-dev-repo: "git+https://github.com/coq/coq.git"

coq.opam.template

@@ -0,0 +1,22 @@
+build: [
+  ["dune" "subst"] {dev}
+  [ "./configure"
+    "-prefix" prefix
+    "-mandir" man
+    "-libdir" "%{lib}%/coq"
+    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+  ] {with-test}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@doc" {with-doc}
+  ]
+  [ make "-C" "test-suite" "-j" jobs "COQ_INSTALLED=1" "PRINT_LOGS=1" ] {with-test}
+  ["dune" "install" "-p" name "--create-install-files" name]
+]

dune

@@ -57,7 +57,7 @@
 ; Use summary.log as the target
 (alias
  (name runtest)
- (package coqide-server)
+ (package coq)
  (deps test-suite/summary.log))
 
 ; For make compat

test-suite/Makefile

@@ -37,11 +37,9 @@ endif
 # Variables
 #######################################################################
 
-# Using quotes to anticipate the possibility of spaces in the directory name
+# COQPREFIX is quoted to anticipate the possibility of spaces in the directory name
 # Note that this will later need an eval in shell to interpret the quotes
-ROOT='$(shell cd ..; pwd)'
-
-BIN:=$(ROOT)/_build/install/default/bin/
+BIN:=$(COQPREFIX)/bin/
 
 # An alternative is ifeq ($(OS),Windows_NT) using make's own variable.
 ifeq ($(ARCH),win32)