verus-lang / verus-mode.el

Support for Verus programming in Emacs
BSD 3-Clause "New" or "Revised" License
5 stars 0 forks source link

TOML parser fails with Rust quick fixes, leading to opaque errors. Includes solution. #9

Open CleveGreen opened 4 hours ago

CleveGreen commented 4 hours ago

Problem

The TOML parser used by verus-mode.el does not support single-quoted strings, which causes issues when using Rust's built-in quick fixes and code suggestions. These often generate TOML with single quotes, leading to an opaque error message (Bad readable value).

Why This Matters

  1. Breaks the workflow when following Rust's own tooling suggestions
  2. The error message is not user-friendly or actionable
  3. Users might waste time debugging what appears to be a problem with their TOML when it's actually a parser limitation

Steps to Reproduce

  1. Use latest Rust compiler, have some cfg(flag) it does not recognize.
  2. Apply the suggestion (which uses single quotes)
  3. Try to use verus-mode.el

Example problematic TOML:

[lints.rust]
# (I was migrating from prusti to verus, this was copied and pasted from the warning rust gave me)
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(prusti)'] } 

Solution

I simply added support for single quote strings in the TOML library with these following changes:

First, I wrote a simple macro to generate a string reading function. A higher order function would also be a fine alternative:

(defmacro toml:define-read-string (name quote-char)
  "Define a string reader function named NAME that reads strings enclosed by QUOTE-CHAR."
  `(defun ,name ()
     (unless (eq ,quote-char (toml:get-char-at-point))
       (signal 'toml-string-error (list (point))))
     (let ((characters '())
           (char (toml:read-char)))
       (while (not (eq char ,quote-char))
         (when (toml:end-of-line-p)
           (signal 'toml-string-error (list (point))))
         (push (if (eq char ?\\)
                   (toml:read-escaped-char)
                 (toml:read-char))
               characters)
         (setq char (toml:get-char-at-point)))
       (forward-char)
       (apply 'concat (nreverse characters)))))

(toml:define-read-string toml:read-double-quoted-string ?\")
(toml:define-read-string toml:read-single-quoted-string ?\')

Added these to the read-table:

(defconst toml->read-table
  (let ((table
         '((?t  . toml:read-boolean)
           (?f  . toml:read-boolean)
           (?\[ . toml:read-array)
           (?{  . toml:read-inline-table)
           (?\' . toml:read-single-quoted-string)
           (?\" . toml:read-double-quoted-string))))
    (mapc (lambda (char)
            (push (cons char 'toml:read-start-with-number) table))
          '(?- ?0 ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9))
    table))

Adjusted the special-escape-characters constant to include single quotes:

(defconst toml->special-escape-characters
  '(?b ?t ?n ?f ?r ?\" ?\' ?\/ ?\\)
  "Characters which are escaped in TOML.

\\b     - backspace       (U+0008)
\\t     - tab             (U+0009)
\\n     - linefeed        (U+000A)
\\f     - form feed       (U+000C)
\\r     - carriage return (U+000D)
\\\"     - quote           (U+0022)
\\\'     - single-quote    (U+0027)
\\\/     - slash           (U+002F)
\\\\     - backslash       (U+005C)

notes:

 Excluded four hex (\\uXXXX).  Do check in `toml:read-escaped-char'")

This is the solution I am currently using, which works and passes the toml library's tests. My chain is quite minimal, so I have not performed a great deal of testing, however it does fix the issue.

The toml library has not seen much maintenance, and users have been annoyed by this, so I am not sure what the best way of integrating this fix is.