CI simple-tests: separate github action job for qRHL

[hendriktews]

Separate qRHL tests in ci/simple-tests from Coq tests such that they can run in a separate action. Before, the qRHL test was running twice, as part of simple-tests and additionally in test-indent.

[hendriktews]

Hi @dominique-unruh, is this PR fine with you?

In your qRHL test you write, you would like to check keypress translations. Can you give an example?

[dominique-unruh]

@hendriktews

Hi @dominique-unruh, is this PR fine with you?

Yes.

In your qRHL test you write, you would like to check keypress translations. Can you give an example?

For example, I might want to check that, if I press the sequence *\subC, the buffer contains *⇩C afterwards. Currently, the test only checks whether the input method loads without errors, but not whether it does anything.

[monnier]

For example, I might want to check that, if I press the sequence *\subC, the buffer contains *⇩C afterwards. Currently, the test only checks whether the input method loads without errors, but not whether it does anything.

You should be able to cobble something up using unread-command-event, but it's messy. E.g. something like:

(ert-deftest my-test ()
  (with-temp-buffer
    ...enable-the-input-method-and-stuff...
    (catch 'my-exit
      (let ((unread-command-events (append "*\\subC" nil)))
        ;; To avoid the actual wait when the test is successful,
        ;; you can (in addition to the timer) setup a key-binding
        ;; that does the `throw` and add the corresponding key to
        ;; the `unread-command-events`.
        (run-with-timer 1 nil (lambda () (throw 'my-exit nil)))
        (recursive-edit)))
    (should (equal (buffer-string) "*⇩C"))))

-- Stefan

[dominique-unruh]

You should be able to cobble something up using unread-command-event, but it's messy.

If it's complicated, maybe best to leave those things untested instead. If it's brittle, we might end up spending time fixing or debugging the tests down the line.

[hendriktews]

merging now, continuing the discussion later

[hendriktews]

I ended up with

  ;; To simulate typing, we put the keys into `unread-command-events'.
  ;; To process them normally, we enter a recursive edit. To abort the
  ;; recursive edit, we add \C-\M-c, the binding of
  ;; `exit-recursive-edit' to the simulated keys.
  (setq unread-command-events (listify-key-sequence "*\\subC\C-\M-c"))
  (recursive-edit)
  (should (equal "*⇩C" (buffer-substring 1 (point))))

which seems to run relatively stable, see PR #714