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.
Patrick Nicodemus (Mar 03 2023 at 22:46):@Michael Soegtrop Sorry for the thread necro. Did you indeed go on to develop a hint database in Ltac2? Do you have any code on github i can look at? I am interested in this and have been looking for existing models to emulate.
Patrick Nicodemus (Mar 03 2023 at 22:48):I would be generally interested in advice from somebody who has had to implement data structures in Ltac2 and how they efficiently retrieved terms or tactics., what kind of keys or queries did your data structure support?
Michael Soegtrop (Mar 04 2023 at 08:34):@Patrick Nicodemus : for tactics which require databases of terms I would consider using Elpi rather than Ltac2. I currently use a mix of Ltac2, Elpi and reflexive (Gallina) tactics with approximately equal share. My preference is reflexive for performance, correctness and maintainability reasons in cases where this is an issue. For the rest I would say about half of the tactics one could write equally well in Ltac2 or Elpi - for the other half one or the other language has advantages. Databases is a case where the advantages of Elpi are obvious.
Patrick Nicodemus (Mar 06 2023 at 15:11):@Michael Soegtrop Is it realistic for somebody to design their own discriminated tree indexing structure or something like that for hint databases? or for the general coq user is it more appropriate to just take advantage of the interface provided by Elpi
Enrico Tassi (Mar 06 2023 at 16:13):Coq has dnets in the code base, it is a matter of exposing them.
Soonish Elpi may get something similar for its clauses, since sometimes its internal index is too shallow. Like in 1 to 2 years, proviso benchmarks agree
Patrick Nicodemus (Mar 07 2023 at 23:47):Enrico Tassi said:
Coq has dnets in the code base, it is a matter of exposing them.
Soonish Elpi may get something similar for its clauses, since sometimes its internal index is too shallow. Like in 1 to 2 years, proviso benchmarks agree
How doable would it be for me to write an Ocaml plugin that interfaced with the existing dnets? Like, say I want to query it with a term and it returns an Ltac2 list of applicable theorems or Ltac2 tactics stored as hint externs?
Enrico Tassi (Mar 08 2023 at 07:34):IMO the need it so common that it should go in ltac2 proper. I've little experience with adding APIs to ltac2, I'll let the others estimate its cost.
Michael Soegtrop (Mar 08 2023 at 08:17):@Enrico Tassi : what is your view on Elpi vs Ltac2 for this application? Since we now have both languages, we should discuss advantages and disadvantages.
Enrico Tassi (Mar 08 2023 at 08:59):It is not so clear to me what "this application" means. Storing terms, or maps on terms, in a state and look things up is a bit too vague to me. It is useful for many things, but the kind of quotienting on terms (up to alpha equivalence, up to conversion, up to unification) changes a lot, as well as the speed requirements (e.g. if you write an automatic prover the indexing data structure is the key, should scale to billions... if you are reifying a goal you are more in the hundreds ballpark).
So I'm not so sure I can give a satisfying answer without more constraints on the table.
Yes, since day one Elpi had this ability to store terms in a data base, since the programming language is "like that", made of rules, able to synthesize and accumulate rules. This is in the spirit of the language. But as I was saying the indexing Elpi does today is likely not appropriate for fast lookups on Coq terms (some doc here), but I think I (or a student of mine) will improve on this in the coming years. So the answer to the question is also depending on when ;-)
Michael Soegtrop (Mar 08 2023 at 09:30):@Enrico Tassi : thanks for the details!
@Patrick Nicodemus : my "educated guess" on this is that as is today Elpi is faster than or about en par (a small constant I expect to be likely <3) with something one could write directly in Ltac2 (without OCaml) for any kind of term database / term indexing application. This is of course not true for something one could write in OCaml. I am thinking about implementing support for hashing Coq terms in Ltac2 and believe that this would already change the picture for some applications. If implementing something which is substantially faster than Elpi in OCaml is feasible mostly depends on the time you want to invest , and as Enrico pointed out, how specialised your application is.
Last updated: Sep 25 2023 at 12:01 UTC