protect uses of coq-callcoq

Uses of coq-callcoq need to correctly handle nil as result for
the case that coq-callcoq fails.

Additionally, add a regression test.

Fixes #551

6 files changed, 104 insertions, 1 deletions

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 199c3539..74191a97 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -131,6 +131,7 @@ jobs:
     runs-on: ubuntu-latest
 
     strategy:
+      # change to selected versions of coq-emacs docker containers
       matrix:
         coq_version:
           - '8.9'
@@ -174,3 +175,50 @@ jobs:
             sudo chown -R coq:coq ./ci
             make -C ci/compile-tests test
           endGroup
+
+  simple-tests:
+    runs-on: ubuntu-latest
+
+    strategy:
+      # change to selected versions of coq-emacs docker containers
+      matrix:
+        coq_version:
+          - '8.9'
+          - '8.10'
+          - '8.11'
+        ocaml_version:
+          - minimal
+      max-parallel: 6
+      # don't cancel all in-progress jobs if one matrix job fails:
+      fail-fast: false
+
+    steps:
+    - uses: actions/checkout@v2
+
+    - name: Add ert problem matcher
+      run: echo "::add-matcher::.github/ert.json"
+      
+    - uses: coq-community/docker-coq-action@v1
+      id: docker-coq-action
+      with:
+        opam_file: 'dummy.opam'
+        coq_version: ${{ matrix.coq_version }}
+        ocaml_version: ${{ matrix.ocaml_version }}
+        custom_script: |
+          startGroup Print opam config
+            opam config list; opam repo list; opam list
+          endGroup
+          startGroup Install emacs
+            sudo apt-get update -y -q
+            sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends emacs
+          endGroup
+          startGroup other relevant configuration
+            getconf _NPROCESSORS_ONLN
+            emacs --version
+            coqc --version
+            ocaml --version
+          endGroup
+          startGroup Run tests
+            sudo chown -R coq:coq ./ci
+            make -C ci/simple-tests all
+          endGroup
diff --git a/ci/compile-tests/README.md b/ci/compile-tests/README.md
index 3b0364e2..08491125 100644
--- a/ci/compile-tests/README.md
+++ b/ci/compile-tests/README.md
@@ -5,6 +5,9 @@ compilation feature for Coq. The test check that
   are compiled
 - files are locked and registered in the right require commands.
 
+Each test comes with a hand-crafted set of Coq source files that
+implement a particular dependency tree. Therefore, most of the
+tests have a subdirectory on their own.
 
 Tests currently missing:
 - unlock checks for ancestors of failed jobs in different cases
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))
diff --git a/coq/coq-system.el b/coq/coq-system.el
index c090cecb..01b9b1d5 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -140,7 +140,10 @@ Interactively (with INTERACTIVE-P), show that number."
 (defun coq-autodetect-help (&optional interactive-p)
   "Record the output of coqotp -help in `coq-autodetected-help'."
   (interactive '(t))
-  (setq coq-autodetected-help (coq-callcoq "-help")))
+  (let ((coq-output (coq-callcoq "-help")))
+    (if coq-output
+        (setq coq-autodetected-help coq-output)
+      (setq coq-autodetected-help ""))))
 
 
 (defun coq--version< (v1 v2)