Michael Soegtrop (May 12 2021 at 15:13): Michael Soegtrop (May 12 2021 at 15:13):@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?
Pierre-Marie Pédrot (May 12 2021 at 16:36):It was not merged yet.
Pierre-Marie Pédrot (May 12 2021 at 16:36):There are legitimate concerns about the fact that it can be surprising w.r.t. to global effects.
Michael Soegtrop (May 12 2021 at 18:18):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?
Pierre-Marie Pédrot (May 12 2021 at 19:53):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
Michael Soegtrop (May 13 2021 at 07:10):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?
Michael Soegtrop (May 13 2021 at 07:18):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