Fix option setting removal to avoid multiple timing info warning

[Copilot]

Problem

When splitting definitions with options tracking enabled, the tool was emitting warnings about finding multiple timing info entries in the same prompt from coqtop:

Warning: found multiple timing info in 'Chars 78290 - 78364 [Set~Warnings~"-funind-cannot-b...] 0. secs (0.u,0.s)\nChars 78381 - 78389 [Defined.] 0.06 secs (0.06u,0.s)\n\n

This occurred because Print Options. statements were being injected before Set/Unset commands, causing both statements to be grouped together in coqtop's response, resulting in multiple timing entries in a single prompt.

Solution

Modified split_statements_to_definitions_with_options to skip injecting Print Options. before Set/Unset statements, since these are option-setting commands themselves. The fix:

1. Adds a regex pattern to detect Set/Unset statements (including variants with Local, Global, Polymorphic, Monomorphic, and attributes)
2. Only injects Print Options. before statements that are NOT Set/Unset commands (and not Proof (...) statements, which were already handled)
3. Maintains the Print Options. injection after each statement to properly track option changes

The regex pattern used is consistent with the SET_REG pattern already used in find_bug.py.

Example

Before:

Print Options.
Set Warnings "-funind-cannot-b..."
Print Options.
Definition foo := 1.
Print Options.

→ Print Options. and Set Warnings might be grouped together, causing multiple timing entries

After:

Set Warnings "-funind-cannot-b..."
Print Options.
Definition foo := 1.
Print Options.

→ Set Warnings has its own timing entry, Print Options. has its own, no grouping issue

This eliminates the spurious warning while maintaining correct option tracking functionality.

Fixes the issue described in the title "Fix option setting removal".

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Fix option setting removal</issue_title> <issue_description>In order to efficiently manipulate the file, I have to break it into definitions. I will now attempt to do this. Sending statements to coqtop... Done. Splitting to definitions... Warning: found multiple timing info in 'Chars 78290 - 78364 [Set~Warnings~"-funind-cannot-b...] 0. secs (0.u,0.s)\nChars 78381 - 78389 [Defined.] 0.06 secs (0.06u,0.s)\n\nCoq < 2119 || 0 < ': [('78290', '78364'), ('78381', '78389')]

Non-fatal error: Failed to split file to definitions and preserve the error.
The new error was: Warning: Cannot open /Users/bcpierce/tmp/VST/compcert [cannot-open-path,filesystem] Warning: Cannot open /Users/bcpierce/tmp/VST/msl [cannot-open-path,filesystem] Warning: Cannot open /Users/bcpierce/tmp/VST/sepcomp [cannot-open-path,filesystem] Warning: Cannot open /Users/bcpierce/tmp/VST/veric [cannot-open-path,filesystem] Warning: Cannot open /Users/bcpierce/tmp/VST/floyd [cannot-open-path,filesystem] File "/tmp/tmp74xmcokl/VC/EverythingVCRequires.v", line 520, characters 30-42: Warning: Notation Lt.lt_irrefl is deprecated since 8.16. The Arith.Lt file is obsolete. Use Nat.lt_irrefl instead. [deprecated-syntactic-definition,deprecated] File "/tmp/tmp74xmcokl/VC/EverythingVCRequires.v", line 520, characters 30-42: Warning: Notation Lt.lt_irrefl is deprecated since 8.16. The Arith.Lt file is obsolete. Use Nat.lt_irrefl instead. [deprecated-syntactic-definition,deprecated] File "/tmp/tmp74xmcokl/VC/EverythingVCRequires.v", line 520, characters 30-42: Warning: Notation Lt.lt_irrefl is deprecated since 8.16. The Arith.Lt file is obsolete. Use Nat.lt_irrefl instead. [deprecated-syntactic-definition,deprecated] File "/tmp/tmp74xmcokl/VC/EverythingVCRequires.v", line 4996, characters 0-1: Error: Syntax error: illegal begin of vernac.

Split not saved. Splitting to definitions with options settings failed, skipping useless option settings removal Sending statements to coqtop... Done. Splitting to definitions... Warning: found multiple timing info in 'Chars 62435 - 62509 [Set~Warnings~"-funind-cannot-b...] 0. secs (0.u,0.s)\nChars 62511 - 62519 [Defined.] 0.059 secs (0.059u,0.s)\n\nCoq < 1061 || 0 < ': [('62435', '62509'), ('62511', '62519')]

Presumably the code inserts option settings in the middle of proofs is bugging out or something</issue_description>

Comments on the Issue (you are @copilot in this section)

Fixes JasonGross/coq-tools#372

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.