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

[CleveGreen]

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.

[jaybosamiya]

Thanks for pointing this out. I will have to give some thought as to how to integrate this into verus-mode.el.

For maintenance reasons, I do not wish to maintain a fork of toml, but indeed this is something that should be solved somewhere. I have some ideas on how I might be able to maintain a patching shim, but I need to think about it a bit more before I can add it in. The code you've provided is already helpful to suggest places we need to (ideally, programatically) insert the patches, so just want to also say thanks for that.

Current simplest workaround is to just use double-quotes. I'm sure you're aware of this, but noting it here for anyone else who hits the same issue until we have a fix.

Interestingly, this suggests an alternate strategy for implementation within verus-mode.el, where we can pre-transform the Cargo.toml to perform a single-quote to double-quote transformation (making sure to translate relevant escapes, since single quotes behave kinda like raw strings in TOML), before passing it to toml.

Again, will give some more thought before I implement the fix in the next release; thanks for bringing this to my attention.

[jaybosamiya-ms]

Quick note that I added an error message that should at least help users understand what is happening (until a proper fix is done), rather than get an inscrutable toml error: 42c5160

I don't have much bandwidth to attempt this change, but I think having had time to think, the approach I would like to go for is the alternate strategy I mentioned above:

pre-transform the Cargo.toml to perform a single-quote to double-quote transformation (making sure to translate relevant escapes, since single quotes behave kinda like raw strings in TOML), before passing it to toml.

[CleveGreen]

Nice, this should save others significant time in debugging. However, single-quotes are valid in some contexts (e.g., within strings), so perhaps this should be a warning instead of an error? This is also something to consider when implementing the transformation from single-quotes to double-quotes.

[jaybosamiya-ms]

Good point; for now I am going to leave it as an error; the error itself is captured via a with-demoted-errors which merely prevents automatically running Verus on the file, rather than completely causing a full blown backtrace, so the user should still have a semi-usable state with the message.

Thanks for pointing out that the quoting transformation needing to deal with this though. Hopefully I'll have a few spare cycles for this soon!