@Pierre-Marie Pédrot : I believe to remember that a few weeks back you did a change such that one can have the effect of Set
as a tactic rather than a vernacular command. But somehow I can't find it in the master docs and code or the commit list. Did I just dream of it?
It was not merged yet.
There are legitimate concerns about the fact that it can be surprising w.r.t. to global effects.
Ah, that explains it - I was looking for closed PRs ... (FTR, it is https://github.com/coq/coq/pull/13982)
I guess this won't do for the use case I have in mind. I am more after a comfortable way to maintain a hint database, which essentially requires to set a mutable global to the result of an Ltac2 function call, e.g. to put some hints into some hash tables or so - essentially a combination of Set and Eval. Would this be possible?
You can already do that, can't you? Just wrap the mutable value in a closure and modify it in place with the as
binder
Won't this evaluate it every time I use it then? Imagine I have a complicated database structure (say a balanced tree) with hints and want to add a hint. I want to compute the new data structure and assign the computed result to the mutable field, because it wouldn't be efficient to redo the computation each time the data structure is used, especially not over a number of incremental changes. Is this possible as is?
Hmm, thinking about it, I guess I spent too much time writing gallina code with all its half evaluated terms. As far as I understand this, in Ltac2 ground terms are always fully evaluated, so the scenario I described above should just work.
Last updated: Jan 31 2023 at 10:01 UTC