Loading the default translations from a file to avoid heavy list operations

[akirak]

I am submitting this PR to address the following error which is commented at MELPA (melpa/melpa#8106):

lean4-input.el:185:1: Error: Lisp nesting exceeds `max-lisp-eval-depth'

My suggestion here is to read the data from an external JSON file, instead of hard-coding it in Emacs Lisp. Using json-parse-buffer which is built-in since Emacs 27, you can deserialize the file into a hash table where values are vectors. I assume the data is static, so it doesn't have to be customizable.

I used the following snippet to serialize the data:

(with-temp-buffer
  (let ((table (make-hash-table :test #'equal)))
    (unwind-protect
        (progn
          (map-do (lambda (key values)
                    (puthash key
                             (apply #'vector values)
                             table))
                  lean4-input-translations)
          (insert (json-serialize table)))
      (clrhash table)))
  (json-pretty-print (point-min) (point-max))
  (append-to-file (point-min) (point-max) "translations.json"))

The limitation of this solution is that you cannot add comments or organize the translation entries into groups. It's a limitation of JSON. Alternatively, you could dump the data into an elisp data file using prin1.

If you merge this PR, you have to update the MELPA recipe as follows. Otherwise, the data file won't become part of artifacts, so the input method won't work:

(lean4-mode :fetcher github :repo "leanprover/lean4-mode"
            :files (:defaults ("data" "data/*.json")))

Hope this PR helps and lean4-mode will become available from MELPA!

[Kha]

Thanks, this is great! We should use this opportunity to sync up with the main "source of truth", which is https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/src/abbreviation/abbreviations.json. Could you adapt your code to that format? I think just copying the file into this repo is fine.

[akirak]

Could you adapt your code to that format?

It is possible to adopt the code, but some entries have {$CURSOR}, which apparently are snippets and unsuitable for support with the input method. Is it okay to drop them?

[Kha]

Yes, dropping them sounds good.

[akirak]

Okay, I will work on it from now.

[akirak]

I have made a change to use the data for the vscode extension.

[Kha]

Thanks!