3 files changed, 49 insertions, 0 deletions
diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile
new file mode 100644
index 00000000..dc5c8e73
--- /dev/null
+++ b/ci/simple-tests/Makefile
@@ -0,0 +1,23 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2021  Hendrik Tews
+# 
+# Authors: Hendrik Tews
+# Maintainer: Hendrik Tews <hendrik@askra.de>
+# 
+# License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+
+TESTS:=$(wildcard test-*.el)
+SUCCESS:=$(TESTS:.el=.success)
+
+all: $(SUCCESS)
+
+test-%.success: test-%.el
+	emacs -batch -l ../../generic/proof-site.el -l $< \
+		-f ert-run-tests-batch-and-exit \
+	&& touch $@
+
+.PHONY: clean
+clean:
+	rm -f *.vo *.glob *.vio *.vos *.vok .*.aux *.success
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
new file mode 100644
index 00000000..618a9f3f
--- /dev/null
+++ b/ci/simple-tests/README.md
@@ -0,0 +1,2 @@
+This directory contains a number of more simple tests, that can
+all run in the same directory.
diff --git a/ci/simple-tests/test-coqtop-unavailable.el b/ci/simple-tests/test-coqtop-unavailable.el
new file mode 100644
index 00000000..8d16bf4e
--- /dev/null
+++ b/ci/simple-tests/test-coqtop-unavailable.el
@@ -0,0 +1,24 @@
+;; This file is part of Proof General.
+;; 
+;; © Copyright 2021  Hendrik Tews
+;; 
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hendrik@askra.de>
+;; 
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Test that Proof General can open Coq files even when coqtop is
+;; unavailable.
+
+
+(ert-deftest coqtop-unavailable ()
+  "Proof General can open Coq files even when coqtop is unavailable.."
+  (setq coq-prog-name "unavailable-program")
+
+  ;; ensure coq-prog-name cannot be found
+  (should (not (locate-file coq-prog-name exec-path)))
+
+  (find-file "simple.v")
+  (coq-prog-args))