branch: elpa/proof-general
commit 175af3f18bec914bcd028d56187bac18662915a5
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
CI: new tests for 3-pane mode for small frame heights
These tests are for #760 and some of them fail because of this
problem.
---
ci/simple-tests/README.md | 3 +
ci/simple-tests/coq-test-three-window.el | 121 +++++++++++++++++++++++++++++++
2 files changed, 124 insertions(+)
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
index c949d58d73..523975c6ef 100644
--- a/ci/simple-tests/README.md
+++ b/ci/simple-tests/README.md
@@ -15,6 +15,9 @@ coq-test-prelude-correct
coq-test-goals-present
: test that Proof General shows goals correctly in various
situations
+coq-test-three-window.el
+: Test three-pane mode for different frame sizes, including ones that
+ are too small for three windows.
# Overview of existing tests for qRHL
diff --git a/ci/simple-tests/coq-test-three-window.el
b/ci/simple-tests/coq-test-three-window.el
new file mode 100644
index 0000000000..972bb1f68f
--- /dev/null
+++ b/ci/simple-tests/coq-test-three-window.el
@@ -0,0 +1,121 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2024 Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hend...@askra.de>
+;;
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Starting Proof General in three-pane mode
+;; (`proof-three-window-enable' is t and
+;; `proof-three-window-mode-policy' is 'smart) used to fail with
+;; "window ... too small for splitting" for frame heights less then
+;; three times `window-min-height' (which defaults to 4). The problem
+;; was relevant for Emacs 26.3, 27.1, and 27.2 running in batch mode
+;; in docker containers, because they set their frame height to 9 (and
+;; their width to 10). For this reason most Proof General CI tests
+;; disable three pane mode in one or the other way.
+;;
+;; This file tests the internal function `proof-select-three-b' that
+;; contains the bug and one user command affected by the bug
+;; (`proof-toggle-active-scripting') with three different frame sizes:
+;; too small for 3 windows, just big enough for 3 windows, and the
+;; default frame size.
+
+(require 'pg-response)
+
+(defun reset-coq ()
+ "Reset Coq and Proof General.
+Do `proof-shell-exit' to kill Coq and reset the locked region and
+a lot of other internal state of Proof General. Used at the
+beginning of the test when several tests work on the same Coq
+source file."
+ (when (and (boundp 'proof-shell-buffer)
+ (buffer-live-p proof-shell-buffer))
+ (proof-shell-exit t)
+ (message "Coq and Proof General reseted")))
+
+
+(defun test-proof-select-three-b-for-height (height)
+ "Test `proof-select-three-b' in 3-pane mode for HEIGHT.
+The function should not signal an error and set up 3 windows."
+ (let ((b1 (get-buffer-create "test-b1"))
+ (b2 (get-buffer-create "test-b2"))
+ (b3 (get-buffer-create "test-b3"))
+ ;; the following is set to its default value
+ (proof-three-window-enable t))
+ (reset-coq)
+ (message "Check test-proof-select-three-b for height %d" height)
+ (set-frame-height (selected-frame) height)
+ (proof-select-three-b b1 b2 b3 'smart)
+ (message "Apparently no error signaled in proof-select-three-b")
+ (message "Check that there are 3 windows")
+ (should (eq (length (window-list)) 3))))
+
+(ert-deftest test-proof-select-three-b-too-small ()
+ "Test `proof-select-three-b' for a frame height too small for 3 windows."
+ :expected-result :failed
+ (test-proof-select-three-b-for-height (- (* 3 window-min-height) 1)))
+
+(ert-deftest test-proof-select-three-b-just-big-enough ()
+ "Test `proof-select-three-b' for a frame height just big enough for 3
windows."
+ (test-proof-select-three-b-for-height (* 3 window-min-height)))
+
+(ert-deftest test-proof-select-three-b-default-height ()
+ "Test `proof-select-three-b' for the default frame height.
+Note that for Emacs 26.3, 27.1, and 27.2, the default frame
+height is 9 when running in a docker container."
+ :expected-result (if (and
+ ;; >= 26.3
+ (or (> emacs-major-version 26)
+ (and (eq emacs-major-version 26)
+ (>= emacs-minor-version 3)))
+ ;; < 28
+ (< emacs-major-version 28))
+ :failed
+ :passed)
+ (test-proof-select-three-b-for-height (frame-height)))
+
+
+(defun test-activate-scripting-for-height (height)
+ "Test `proof-toggle-active-scripting' in 3-pane mode for HEIGHT.
+The function should not signal an error and there should be 3
+windows afterwards."
+ (let ((proof-three-window-enable t)
+ (proof-three-window-mode-policy 'smart))
+ (reset-coq)
+ (message "Check proof-toggle-active-scripting for height %d" height)
+ (set-frame-height (selected-frame) height)
+ (find-file "some_file.v")
+ (proof-toggle-active-scripting)
+ (message "Apparently no error signaled in proof-toggle-active-scripting")
+ (message "Check that there are 3 windows")
+ (should (eq (length (window-list)) 3))))
+
+
+(ert-deftest test-proof-toggle-active-scripting-too-small ()
+ "Test `proof-toggle-active-scripting' in a frame too small for 3 windows."
+ :expected-result :failed
+ (test-activate-scripting-for-height (- (* 3 window-min-height) 1)))
+
+(ert-deftest test-proof-toggle-active-scripting-just-big-enough ()
+ "Test `proof-toggle-active-scripting' in a frame just enough for 3 windows."
+ (test-activate-scripting-for-height (* 3 window-min-height)))
+
+(ert-deftest test-proof-toggle-active-scripting-default-height ()
+ "Test `proof-toggle-active-scripting' with the default frame size.
+Note that for Emacs 26.3, 27.1, and 27.2, the default frame
+height is 9 when running in a docker container."
+ :expected-result (if (and
+ ;; >= 26.3
+ (or (> emacs-major-version 26)
+ (and (eq emacs-major-version 26)
+ (>= emacs-minor-version 3)))
+ ;; < 28
+ (< emacs-major-version 28))
+ :failed
+ :passed)
+ (test-activate-scripting-for-height (frame-height)))
