"Back"/"Undo" don't undo syntax extensions #12575
Comments
|
Excellent, thanks for putting this into an issue @jfehrle! |
|
Stack trace, partly annotated, using 8.12 beta. Not sure it tells us much. |
|
Interestingly, I believe this used to be an issue with |
|
The CoqIDE behavior is confusing. If I CTRL-up to the beginning of the file after the first try of executing the If I instead move the cursor to the beginning of the buffer and comment out the The command entry for I see the same problem with the @JasonGross Any ideas on what to look at next or where the |
|
cc @coq/parsing-maintainers |
jfehrle
added
the
part: parser
|
@gares or @maximedenes: I verified with a FWIW, another example that probably has the same root cause. The following gets a syntax error on the |
|
IIRC set parsing state is called after each step, and the code seems to do that. This should be the line reached on commands such as Require: https://github.com/coq/coq/blob/master/stm/stm.ml#L2999 (since VernacRequire is classified as a Sideff with VtNow https://github.com/coq/coq/blob/master/stm/vernac_classifier.ml#L182). I don't know if this is problem, but ML code cannot be unloaded and I'm pretty sure Ltac2 defines some parsing rules in ML (it must really). I'm pretty sure the "undoing" a regular notation works. |
|
With gramlib in the archive, its state could be registered to the global summary and I suspect this would solve the problem. |
|
@gares That line is not executed for
I don't see how that would be a problem for this use case.
Yes, I tried undoing both regular notations and Ltac2 notations and it seemed to work correctly. The Ltac2 code path looks a bit different from regular notations but I didn't investigate since it seems to work. |
@herbelin even so that's a bit bizarre that pcoq already is not capturing this; the vernacular extension point already pushed to the internal undo/redo table. Maybe we could have a look at it in person some day? |
|
@ejgallego: you're right, these syntax extensions goes through |
…ktracking mechanism. In particular, we remove the "ByEXTEND" mechanism.
|
For reproducibility in The point is that |
|
See also #5234 |
|
@jfehrle : this appears to be fixed in CoqIDE 8.15, but not in VsCoq. Do you remember how this has been fixed? |
|
@MSoegtropIMC You mean the anomaly is gone or that this is completely fixed? I haven't made any code changes to address this. I think the fix would be entirely on the server side, so I don't see why VsCoq would behave any differently. Note my comments above:
Perhaps you're spawning a new process on CoqIDE but not on VsCoq? |
|
Actually my older issue (#11793) is fixed, but this one appears to be not fixed. |
|
More specifically what is fixed that stepping hence and forth over valid code including the Ltac2 require did not work in the past, but now it does. I find this more important than the error messages one gets when stepping over code which got invalid cause the Ltac2 require was removed. |
|
I am positive we still have problems handling the state in the parsing engine, this should be IMHO a top priority in terms of engineering power. |
Can't reproduce since 89ad33f |
|
@SkySkimmer there is an easy reproduction case:
Coq will fail to parse it. Can be tested very easily with coq-lsp for example. |
Require Import ssreflect.
Goal True.
unfold idProp in |- *.parses for me with whatever combination of executing then backtracking that I tried. |
|
Actually this seems quite tricky to reproduce / minimize indeed, let me research a bit more, as it seems the bug only happens with a very particular sequence of plugin loading / I see the bug always in coq-lsp when I open |
|
The problem is pretty hard to debug due to all the hack in So starting with a state with the ssrplugin loaded, then switching to a state before it was loaded, somehow the keywords and grammar rules are affected. So this bug may be specific to ssreflect actually. |
|
cc @artagnon , here is the error you've been suffering. |
|
Hmm, isn't the fix just to wrap the keyword declaration through |
|
Thanks @ppedrot , I hope that works, the bug is very subtle and is giving me a headache (the dance done with the lexer and ssr_is_loaded is not very, ehem, pleasant) I think the only way we can hope to have a reasonably maintainable setup is to do require writers to parsing and lexing state to grab a handle so they can update it functionally. |
|
This may be related to calling |
|
See also #10146 |
I think you may be into something @SkySkimmer , thanks; I can reproduce this better, and without involving ssreflect (still not a simple repro case yet). So indeed, that happens with regular Coq plugins so seems like a core issue. |
|
Definitely related as if I remove the redo code and test Reserved Notation "& $ k" (at level 300).
Require Import Ltac2.Ltac2.
Ltac2 Eval ().run everything, backtrack to before the Reserved Notation, run just Ltac2 Eval Turning this info into a fix is harder though. |
ie to fix rocq-prover#12575 This is in a hacky state currently, mostly because coqpp is not adapted (so the g_ltac2.ml file was manually modified for the proof of concept) and because GRAMMAR EXTEND is not properly treated but was just hacked up (but the same method should be applicable). This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) g_ltac2.ml was generated by unmodified coqpp then manually edited in 2 ways: - vernac_extend calls have an added `~plugin:__coq_plugin_name` argument - the code generated from ~~~ GRAMMAR EXTEND Gram GLOBAL: tac2mode; tac2mode: TOP [ [ tac = G_vernac.query_command -> { tac None } ] ]; END ~~~ was wrapped in Mltop.add_init_function and uses `Pcoq.grammar_extend ~redo:false` (without this it complains about mssing levels because it executes before the vernac extensions) This is just a hack and grammar_extend should not have the redo argument once this is in a mergeable state. The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. To summarize TODOs: - use some similar create_command_grammar mechanism to avoid raw grammar_extend calls from GRAMMAR EXTEND (?, not sure I fully understand GRAMMAR EXTEND) - adapt coqpp to use the new mechanism instead of manually editing g_ltac2 - remove hack "redo" argument of grammar_extend
ie to fix rocq-prover#12575 This is in a hacky state currently, mostly because coqpp is not adapted (so the g_ltac2.ml file was manually modified for the proof of concept) and because GRAMMAR EXTEND is not properly treated but was just hacked up (but the same method should be applicable). This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) g_ltac2.ml was generated by unmodified coqpp then manually edited in 2 ways: - vernac_extend calls have an added `~plugin:__coq_plugin_name` argument - the code generated from ~~~ GRAMMAR EXTEND Gram GLOBAL: tac2mode; tac2mode: TOP [ [ tac = G_vernac.query_command -> { tac None } ] ]; END ~~~ was wrapped in Mltop.add_init_function and uses `Pcoq.grammar_extend ~redo:false` (without this it complains about mssing levels because it executes before the vernac extensions) This is just a hack and grammar_extend should not have the redo argument once this is in a mergeable state. The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. To summarize TODOs: - use some similar create_command_grammar mechanism to avoid raw grammar_extend calls from GRAMMAR EXTEND (?, not sure I fully understand GRAMMAR EXTEND) - adapt coqpp to use the new mechanism instead of manually editing g_ltac2 - remove hack "redo" argument of grammar_extend
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Fix rocq-prover#12575 This was hand tested using ~~~coq Require Import Ltac2.Ltac2. Ltac2 Eval (). ~~~ we must correctly handle - eval all, backtrack before the Require, eval just Ltac2 Eval: should parsing error illegal begin etc - eval all, backtrack before the Require, eval all again: should work (ie the parsing rules must be re-applied) The interesting part is what happens in vernac_extend and the associated egramml functions: - an indirection is added from the command name (Foo in `VERNAC COMMAND EXTEND Foo`) to the extension data (which contains a closure: not marshallable). This is non-backtracking, and there is no use to making it backtrack since we can't unlink plugins. - vernac_extend calls `Egramml.extend_vernac_command` with `undoable:false` when there is no `plugin` argument, this is the old non backtrackable behaviour. Typically for non-plugin callers like g_obligations. Eventually we will clean up so that rules added this way produce an error when backtracked over instead of having the redo code in pcoq, until then it's also available for plugin hacks which don't mind the backtrack bug I guess. - when there is a `plugin` argument, vernac_extend wraps the call to `Egramml.extend_vernac_command` in `Mltop.add_init_function` and uses `undoable:true`. In undoable mode, egramml uses the Pcoq.create_grammar_command system which backtracks properly. Because this system puts its input in the grammar_stack which ends up in the summary, we need the indirection mentioned above to keep the input marshallable. For GRAMMAR EXTEND there is no user-given name so we produce a uid from DECLARE PLUGIN, the file name and the number of occurences of GRAMMAR EXTEND in the file (we end up with eg `coq.plugins.ltac:coretactics.mlg:42`). In the future we will probably try to replace the redo code of ByEXTEND with an error and make the users in plugins switch to the new mechanism. For now it is too much work, when a plugin is modifying its own entries it doesn't matter if backtrack is undone.
Uh oh!
There was an error while loading. Please reload this page.
If you load a plugin such as, say, Ltac2 and then backtrack in CoqIDE, the syntax extensions from the plugin are not undone. This causes unexpected and confusing errors when you try to redo those lines.
I ran into this while experimenting with Ltac2 Notation. Here's an example in 8.12 from @tchajed:
If you do the
Ltac2 Eval ()in a fresh buffer, you getSyntax error: illegal begin of vernac.From @ppedrot #11549 (comment):
UPDATE: Backtracking seems to work correctly for both
NotationandLtac2 Notation, so apparently some things are being backtracked.The text was updated successfully, but these errors were encountered: