Set Default Proof Mode is ignored in 8.20

[Engreyight]

I am working in a project that uses a mixture of ltac1 and ltac2 tactics, with ltac1 wrappers for the latter. Because of this, we often use Set Default Proof Mode "Classic". at the top of files and use the ltac1 tactics and wrappers, which worked fine so far on 8.18 and the latest version of the plugin. However, since upgrading to 8.20 (and not touching the plugin version), it seems that this plugin ignores that line, breaking all the scripts, while coqide handles it as usual. Here is a simple example to demonstrate the problem:

From Ltac2 Require Import Ltac2 Message.

Ltac2 test () := print (of_string "test").
Ltac test := ltac2:(test ()).

Set Default Proof Mode "Classic".
Test Default Proof Mode.

Goal True.
Proof.
  test.
  split.
Qed.

Running this in vim with the plugin gives Default Proof Mode: Some(val='Ltac2') for line 7, immediately showing that the setting didn't persist, but continuing further, I get This expression should have type unit but has type unit -> unit. [not-unit,ltac2,default] for line 11, so it indeed doesn't work. Running the same script in coqide, line 7 gives Current value of Default Proof Mode is "Classic", and line 11 gives the expected test. Piping the script to coqtop gives the same result as coqide, so the issue is not there.

While the usual workarounds, such as starting the proof with Proof Mode "Classic"., or using ltac1:(test). or test (). work, it would be nice to have this issue fixed, so I don't need special scripts compared to the rest of the team.

[whonore]

Interesting, this seems to be specific to Default Proof Mode because other options that take a string argument work fine on 8.18-8.20:

Test Mangle Names Prefix. (* Mangle Names Prefix: Some(val='_') *)
Set Mangle Names Prefix "a".
Test Mangle Names Prefix. (* Mangle Names Prefix: Some(val='a') *)

Test Loose Hint Behavior. (* Loose Hint Behavior: Some(val='Lax') *)
Set Loose Hint Behavior "Warn".
Test Loose Hint Behavior. (* Loose Hint Behavior: Some(val='Warn') *)

I don't have any ideas as to what's going wrong and the debug logs aren't revealing anything useful, so I'm trying to track down when exactly it broke using git bisect. From what I've seen so far, it stopped working somewhere between 8.18+alpha and 8.18.0.

[whonore]

This is the commit where it stopped working. It seems to have something to do with a change to how and when certain vernacular statements get executed. I'll have to dig into this more, but I probably won't be able to get to it until January.

Possibly related: #345.

[Engreyight]

Thank you very much!