16 files changed, 74 insertions, 28 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index e15094ccfa..5ab4cacdaf 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -169,9 +169,7 @@ summary.log:
 # local build, and downloadable on GitLab)
 report: summary.log
 	$(HIDE)./save-logs.sh
-	$(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:start:coq.logs'; fi
-	$(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec cat '{}' ';'; fi
-	$(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:end:coq.logs'; fi
+	$(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi
 	$(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi
 
 #######################################################################
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index d6bb52bb4a..e8291c89da 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp"
 sort -u > desired <<EOT
 .
 ./test
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.glob
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index d6bb52bb4a..e8291c89da 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp"
 sort -u > desired <<EOT
 .
 ./test
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.glob
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index f6fb3bcb42..10a200ddee 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -15,9 +15,7 @@ sort > desired <<EOT
 .
 ./test
 ./test/test.glob
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index f6fb3bcb42..10a200ddee 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -15,9 +15,7 @@ sort > desired <<EOT
 .
 ./test
 ./test/test.glob
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
index 863c39f500..3cd1ac305f 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -19,12 +19,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index f079662631..9f6295d644 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -18,9 +18,7 @@ sort > desired <<EOT
 .
 ./test
 ./test/test.glob
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
new file mode 100755
index 0000000000..6301aa03c0
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+if make VERBOSE=1; then
+  # make command should have failed (but didn't)
+  exit 1
+else
+  # make command should have failed (and it indeed did)
+  exit 0
+fi
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
new file mode 100755
index 0000000000..991fb4a61d
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-bypass-API
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+make VERBOSE=1
diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh
index 24ef8c891b..c2d47166fe 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -17,12 +17,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index 24ef8c891b..c2d47166fe 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -17,12 +17,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index 24ef8c891b..c2d47166fe 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -17,12 +17,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4
index 72765abe04..e7d0bfe1f8 100644
--- a/test-suite/coq-makefile/template/src/test.ml4
+++ b/test-suite/coq-makefile/template/src/test.ml4
@@ -1,3 +1,4 @@
+open API
 open Ltac_plugin
 DECLARE PLUGIN "test_plugin"
 let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml
index a01d0865a8..e134abd840 100644
--- a/test-suite/coq-makefile/template/src/test_aux.ml
+++ b/test-suite/coq-makefile/template/src/test_aux.ml
@@ -1 +1 @@
-let tac = Proofview.tclUNIT ()
+let tac = API.Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli
index 10020f27de..2e7ad1529f 100644
--- a/test-suite/coq-makefile/template/src/test_aux.mli
+++ b/test-suite/coq-makefile/template/src/test_aux.mli
@@ -1 +1 @@
-val tac : unit Proofview.tactic
+val tac : unit API.Proofview.tactic
diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh
index fb8a1c1b0a..b613621085 100755
--- a/test-suite/save-logs.sh
+++ b/test-suite/save-logs.sh
@@ -9,7 +9,7 @@ mkdir "$SAVEDIR"
 # keep this synced with test-suite/Makefile
 FAILMARK="==========> FAILURE <=========="
 
-FAILED=$(mktemp)
+FAILED=$(mktemp /tmp/coq-check-XXXXX)
 find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED"
 
 rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR"