I'm migrating a development from 8.9 to 8.11 and I need to provide each
Hint with a database name. Has someone somewhere a script to automatically do such migration, including automatically adding a database name to the calls to
By the way, would it be worth to provide a way to add databases to what
auto uses by default?
when we did that migration for iris, we didn't have to patch
auto uses... strange
By the way, would it be worth to provide a way to add databases to what auto uses by default?
I think that way exists: it's the
core hint db.
It's possible to use
Create HintDb to create a hind database but how does one read from it?
auto with HintDb (source)
What if you don't want the behavior of
auto, you want to write your own tactic customizable with a hint database?
Hmmm ... not sure about that but I found this
Ok, that's an interesting applications. So I take it that
autounfold are the only tactics with access to databases. That's too bad but I think I can do something with that.
autorewrite access different databases from the others (at least acoording to this part of the doc)
You seem to be able to create those with
Create HintDb too so I'm wondering if that part of the doc doesn't mean that each database has a separate table of for
Implementation-wise there are two different types...
So when you create a database, is their a way to make it either a rewrite database or an auto database?
It is automatically an auto database I think
I think that they're just two different namespaces
Create HintDb is just for auto / eauto / typeclasses eauto
Rewrite database follow the previous behaviour, i.e. implicit declaration at hint definition time
Section Foo. Context (A B : Type) (e : A = B). Hint Rewrite e : myfoo. Goal A = B. Proof. autorewrite with myfoo. reflexivity. Qed. End Foo.
you don't need to declare the rewrite db
Oh that's good to know! Thanks!
Just to confirm, beside the tactics
autorewrite, etc, there's no way to query those databases, am I correct?
Conversely, you won't get any error from
autorewrite if you have a typo in your db name...
Print HintDb ?
You can't put that in an Ltac script, can you?
I don't think so
Thanks :) That helps
@Simon Hudon you seem to want https://github.com/gmalecha/coq-ltac-iter
(Not tried myself, but relevant)
I have the same question as the OP, for a "default hint database." I would like to be able to put my hints in a database of my own, but within a given file or section I'd like to "open" that hint database. So my hints would not be searched for everyone importing file A.v, but just in certain files: B.v and C.v might both import A, bu only B.v wants to search that hint database on every
auto, and without mentioning the DB. Any advice for this situation?
This feature has indeed been discussed before, but no one has volunteered yet to implement it. See https://github.com/coq/coq/issues/10559 for the initial discussion and https://github.com/coq/coq/issues/14752 for the more specific proposal.
@Ezra elias kilty Cooper not exactly what you want, but you could have inside A a Module core_hints. that uses #[export] Hint Resolve foo bar : core.
Then you could Import A.core_hints in B.
@Paolo Giarrusso That's a great workaround, thanks!
This topic was moved by Karl Palmskog to #math-comp users > Hint databases for finishing tactic
Last updated: Jan 28 2023 at 07:30 UTC