Fix byte-compilation problems

[dominique-unruh]

The current MELPA version does not work properly:

• error byte-code: Symbol’s function definition is void: proof-easy-config-check-setup Seems solved by 124db99
• Byte compiling gives errors when compiling qrhl-input-25.el in Emacs 26+ (and vice verse for qrhl-input.el) even though will never be included.

[dominique-unruh]

One idea for solving the compilation errors would be to merge the Emacs 25 & 26 files into a single .el file.
Upon second thoughts, I don't think this works:
Even if we make the Emacs 26-incompatible code conditional in that file, it will still be compiled.
What we need is a way to conditionally exclude a file or a code block from compilation in the first place.
I don't know a way for that.

The only solution I can see at the moment is to disable the compilation of the code completely (wrapping everything in Emacs macro dont-compile). But that means that we do not get byte-compilation advantages for that file (even in the file that is actually loaded).

@erikmd mentions (eval-when-compile …) but I don't understand how this can be used here.

[erikmd]

To suggest a slightly different idea using eval-when-compile,
I'm wondering whether some global #ifdef-like elisp form would be possible to address item 2?

cf. https://www.gnu.org/software/emacs/manual/html_node/elisp/Eval-During-Compile.html

(eval-when-compile
  (unless (fboundp 'some-new-thing)
    (defmacro 'some-new-thing ()
      (compatibility code))))

"This is often good for code that’s only a fallback for compatibility with other versions of Emacs. "

So my suggestion would be to:

Enclose the forms of qrhl-input-25.el in:

(eval-when-compile
  (when (version< emacs-version "26")
  
    (require 'quail)
    (quail-define-package
    … etc.
))

and enclose the forms of qrhl-input.el in:

(eval-when-compile
  (unless (version< emacs-version "26")

    (require 'quail)
    (quail-define-package
    … etc.
))

@monnier @Matafou @hendriktews do you think that this could work without breaking other things?

[dominique-unruh]

@erikmd mentions (eval-when-compile …) but I don't understand how this can be used here.

I just realized what @erikmd means. There is already an eval-when-compile in the source file! (Since I just copied this from the Emacs dist, I didn't really know what's in there.) So I think the solution is to make the code inside eval-when-compile conditional, and that might well work. Will try to do so later.

EDIT: This was written before seeing the preceding message by @erikmd. So "@erikmd means" refers to #636 (comment)

[dominique-unruh]

• I tried @erikmd 's suggestion, it didn't work. (I put the whole code within (eval-when-compile (when false ...)) and still got the compilation error.)
• I tried removing the existing eval-when-compile (under the assumption that I get a compile-time listp error only in code that is actually executed during compilation). Still I get the compilation error.
• I put the whole file into dont-compile. That works. But it means the code will be interpreted each time it is loaded.

Any ideas? Otherwise I will go with the dont-compile approach. @erikmd @monnier @Matafou @hendriktews

[dominique-unruh]

Slightly related: I saw this in proof-general.el:

  (let ((byte-compile-directories
         '("generic" "lib"
           "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"
           )))
    (dolist (dir byte-compile-directories)
      (add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))

Here qrhl is not included. I assume it should be but I thought I'd check just in case. (After all, the error shows that the qrhl code is actually byte compiled, so I don't understand what this fragment does.)

[erikmd]

I tried @erikmd 's #643 (comment), it didn't work. (I put the whole code within (eval-when-compile (when false ...)) and still got the compilation error.)

could you try again with something like (eval-when-compile (when nil … )) ?

because just to recall, false is a truthy value (everything ≠ nil does so actually)

[erikmd]

Slightly related: I saw this in proof-general.el:

  (let ((byte-compile-directories
         '("generic" "lib"
           "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"
           )))
    (dolist (dir byte-compile-directories)
      (add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))

Here qrhl is not included. I assume it should be but I thought I'd check just in case. (After all, the error shows that the qrhl code is actually byte compiled, so I don't understand what this fragment does.)

Good question. Actually this code had been devised by @cpitclaudel so he'd certainly summarize this much better than me
(IIRC, this code was intended to workaround a flaw of MELPA and/or package.el when some files are not in toplevel folder)

But in any case, "qrhl" should definitely be listed there…

[dominique-unruh]

@erikmd

could you try again with something like (eval-when-compile (when nil … )) ?
Sorry. nil was what I used. I wrote false in the comment accidentally.

[erikmd]

@dominique-unruh you may want to test and integrate the patch suggested in the other PR:

#636 (comment)

Thanks a lot @monnier for your input ! 👍

[dominique-unruh]

Checks fail after 6cf7d1d but this is positive: It means the qrhl-input compilation issue is now detected by the CI.

[dominique-unruh]

Question: Where should I add my test case? @erikmd

I created a test case to see whether qrhl-input loads correctly on all Emacses (especially because I don't have an Emacs 25 instance). I put it in ci/simple-tests because that sounded logical. But in CI, simple-tests are only tested with a single Emacs (but with many coqs). It seems the tests in test-indent are tested with all Emacses, but the directory name indicates that it's not the right place. So how should I include test-qrhl.el so that it is tested with all Emacses?

PS: The test case is currently intentionally broken to check whether testing occurs.

[erikmd]

Hi @dominique-unruh, thanks for your question!

I created a test case to see whether qrhl-input loads correctly on all Emacses (especially because I don't have an Emacs 25 instance). I put it in ci/simple-tests because that sounded logical. But in CI, simple-tests are only tested with a single Emacs (but with many coqs). It seems the tests in test-indent are tested with all Emacses, but the directory name indicates that it's not the right place. So how should I include test-qrhl.el so that it is tested with all Emacses?

You precisely pinpointed a limitation of the current CI that we are currently working on with @hendriktews;
Namely, it is easy to test test-indent with several Emacsen because indentation does not depend on Coq,
while the tests involved in folders that possibly require Coq use a debian-based Docker image where there is currently only one version of emacs.
it's not an issue if the test you add now is not "comprehensive" because we have a PG maintainers telco next week
where we'll be able to start doing further CI tweaks.

So I'd suggest that:

• either you just put the test in ci/simple-tests, and if the Ci is green, I'll merge it today (the sooner, the better)
• or you try to do something more involved if you have some time (because I suspect that the test you'll add don't use Coq :) and thereby should be separated from simple-tests where Coq is needed)

[dominique-unruh]

@erikmd
Your message exactly coincided with my push right now.

Just adding to simple-tests is not enough because this specific issue needs testing in different Emacs versions (because the code is different in Emacs 25 and Emacs 26.) And I don't have Emacs 25 available for testing locally.

So what I did as a stopgap is to include the test in simple-tests, but to add it in test test-indent job in test.yml. (See 876629e) A bit untidy, but until you decide how to structure the tests, it will do.

Now I can continue to fix the issues in this pull request.

[erikmd]

@dominique-unruh OK, LGTM! thank you

[dominique-unruh]

@monnier
I incorporated your patch from #636 (comment) for the files qrhl.el and qrhl-input-25.el and those parts work fine.

I have not included the patch for proof-easy-config.el because I am not sure what it does (the problem related to easy-config was resolved by (require proof-easy-config)) and because it also got corrupted by copy-and-pasting it into the comment. (The line containing ***@***.***) I think we can leave it out at least from the pull request.

My main problem is qrhl-input.el: I also incorporated your patch there (b1e3780) but it does not work. Compilation on Emacs 25 still fails (see the CI). I do not understand enough Elisp-magic to figure out what needs to be done to make it work the same as in qrhl-input-25.el. Can you help with this one?

[monnier]

My main problem is `qrhl-input.el`: I also incorporated your patch there (b1e3780) but it does not work. Compilation on Emacs 25 still fails (see the CI). I do not understand enough Elisp-magic to figure out what needs to be done to make it work the same as in `qrhl-input-25.el`. Can you help with this one?

The patch below seems like a better option, tho: it doesn't just make it so `qrhl-input.el` can be uselessly compiled on Emacs-25, but makes `qrhl-input.el` actually work correctly under Emacs-25, so we can get rid of `qrhl-input-25.el`. Stefan diff --git a/qrhl/qrhl-input.el b/qrhl/qrhl-input.el index 8cc520425c..49c16d4880 100644 --- a/qrhl/qrhl-input.el +++ b/qrhl/qrhl-input.el @@ -1,8 +1,7 @@ -;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in ProofGeneral -*-coding: utf-8;-*- +;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in ProofGeneral -*- lexical-binding: t -*- -;; Copyright (C) 2001-2018 Free Software Foundation, Inc. -;; Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, -;; 2010, 2011 +;; Copyright (C) 2001-2022 Free Software Foundation, Inc. +;; Copyright (C) 2001-2011 ;; National Institute of Advanced Industrial Science and Technology (AIST) ;; Registration Number H14PRO021 ;; Copyright (C) 2017-2022 University of Tartu @@ -28,9 +27,6 @@ ;;; Code: -(if (version< emacs-version "26") - (error "Emacs version >= 26 required")) - (require 'quail) (quail-define-package @@ -71,22 +71,28 @@ (pcase rule (`(,_ ,(pred characterp)) (push rule newrules)) ;; Normal quail rule. (`(,seq ,re) - (let ((count 0) - (re (eval re t))) - (maphash + (let* ((count 0) + (re (eval re t)) + (ucs-names (ucs-names)) + (process-one-entry (lambda (name char) (when (and (characterp char) ;; Ignore char-ranges. (string-match re name)) (let ((keys (if (stringp seq) (replace-match seq nil nil name) - (funcall seq name char)))) + (funcall (eval seq t) name char)))) (if (listp keys) (dolist (x keys) (setq count (1+ count)) (push (list x char) newrules)) (setq count (1+ count)) - (push (list keys char) newrules))))) - (ucs-names)) + (push (list keys char) newrules))))))) + ;; Emacs-25's `ucs-names' returned an alist rather than a hash + ;; table and that changed to a hash-table in Emacs-26. + (if (hash-table-p ucs-names) + (maphash process-one-entry ucs-names) + (dolist (pair ucs-names) + (funcall process-one-entry (car pair) (cdr pair)))) ;; (message "qrhl-input: %d mappings for %S" count re) )))) (setq newrules (delete-dups newrules))

[dominique-unruh]

Thanks @monnier, your patch seems to work fine. (I tested in my local Emacs, and the CI checks at least whether loading the input methods raises any error on all supported Emacses)

I rebased everything on master, and the CI passes. @erikmd

From my side, this fix is ready for merging.

[erikmd]

👍 Many thanks @dominique-unruh for this very tidy fixup PR.

[dominique-unruh]

@erikmd The new version is already on MELPA and I verified that it now installs fine (in Emacs 27.1). :)

[monnier]

Dominique Unruh [2022-03-10 07:41:19] wrote:

@erikmd The new version is already on MELPA and I verified that it now installs fine (in Emacs 27.1). :)

Yay! Thanks!

[monnier]

I have not included the patch for `proof-easy-config.el` because I am not sure what it does (the problem related to easy-config was resolved by `(require proof-easy-config)`) and because it also got corrupted by copy-and-pasting it into the comment. (The line containing `***@***.***`)

`proof-easy-config` is an autoloaded macro, so it is obviously intended to be used without having to `require` first. But it expands to code which calls functions from that same file and those functions aren't autoloaded, so currently if you take advantage of the autoload (like you did) you have a bug. We can either decide that users of `proof-easy-config` need to explicitly `require`, and then we can stop autoloading the macro (the best option, in my opinion), or we can change `proof-easy-config` so it makes sure the functions used in the expansion will be available (either by including a `require` in the output, like my patch does, or by additionally autoloading those functions).

My main problem is `qrhl-input.el`: I also incorporated your patch there (b1e3780) but it does not work. Compilation on Emacs 25 still fails (see the CI).

Oh, I didn't think about the case where we compile with Emacs-25. The patch below might fix it. Stefan diff --git a/qrhl/qrhl-input.el b/qrhl/qrhl-input.el index 8cc520425c..c051b09c93 100644 --- a/qrhl/qrhl-input.el +++ b/qrhl/qrhl-input.el @@ -1,8 +1,7 @@ -;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in ProofGeneral -*-coding: utf-8;-*- +;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in ProofGeneral -*- lexical-binding: t; -*- -;; Copyright (C) 2001-2018 Free Software Foundation, Inc. -;; Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, -;; 2010, 2011 +;; Copyright (C) 2001-2022 Free Software Foundation, Inc. +;; Copyright (C) 2001-2011 ;; National Institute of Advanced Industrial Science and Technology (AIST) ;; Registration Number H14PRO021 ;; Copyright (C) 2017-2022 University of Tartu @@ -72,21 +72,25 @@ (`(,_ ,(pred characterp)) (push rule newrules)) ;; Normal quail rule. (`(,seq ,re) (let ((count 0) - (re (eval re t))) + (re (eval re t)) + (ucs-names (ucs-names))) + ;; Emacs-25's `ucs-names' returned an alist rather than a hash + ;; table. + (when (hash-table-p ucs-names) (maphash (lambda (name char) (when (and (characterp char) ;; Ignore char-ranges. (string-match re name)) (let ((keys (if (stringp seq) (replace-match seq nil nil name) - (funcall seq name char)))) + (funcall (eval seq t) name char)))) (if (listp keys) (dolist (x keys) (setq count (1+ count)) (push (list x char) newrules)) (setq count (1+ count)) (push (list keys char) newrules))))) - (ucs-names)) + ucs-names)) ;; (message "qrhl-input: %d mappings for %S" count re) )))) (setq newrules (delete-dups newrules))

[dominique-unruh]

Oh, I didn't think about the case where we compile with Emacs-25. The patch below might fix it.

@monnier
I'm not sure there is an outstanding bug to fix here. Your earlier patch (#643 (comment)) seems to already address the issue (and is, I think, conflicting with your new patch).