Stream: Coq users

Topic: Hint databases

Hugo Herbelin (May 30 2020 at 12:31):

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 auto?

By the way, would it be worth to provide a way to add databases to what auto uses by default?

Ralf Jung (Jun 06 2020 at 09:37):

when we did that migration for iris, we didn't have to patch auto uses... strange

Ralf Jung (Jun 06 2020 at 09:38):

@Hugo Herbelin

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.

Simon Hudon (Jun 14 2020 at 14:27):

It's possible to use Create HintDb to create a hind database but how does one read from it?

Donald Sebastian Leung (Jun 14 2020 at 14:44):

auto with HintDb (source)

Simon Hudon (Jun 14 2020 at 14:58):

What if you don't want the behavior of auto, you want to write your own tactic customizable with a hint database?

Donald Sebastian Leung (Jun 14 2020 at 15:07):

Hmmm ... not sure about that but I found this

Simon Hudon (Jun 14 2020 at 15:16):

Ok, that's an interesting applications. So I take it that autorewrite, auto, eauto and autounfold are the only tactics with access to databases. That's too bad but I think I can do something with that.

Kenji Maillard (Jun 14 2020 at 15:21):

beware that autorewrite access different databases from the others (at least acoording to this part of the doc)

Simon Hudon (Jun 14 2020 at 15:25):

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 Rewrite hints

Pierre-Marie Pédrot (Jun 14 2020 at 15:28):

Implementation-wise there are two different types...

Simon Hudon (Jun 14 2020 at 15:30):

So when you create a database, is their a way to make it either a rewrite database or an auto database?

Kenji Maillard (Jun 14 2020 at 15:30):

It is automatically an auto database I think

Pierre-Marie Pédrot (Jun 14 2020 at 15:30):

I think that they're just two different namespaces

Pierre-Marie Pédrot (Jun 14 2020 at 15:31):

Create HintDb is just for auto / eauto / typeclasses eauto

Pierre-Marie Pédrot (Jun 14 2020 at 15:31):

Rewrite database follow the previous behaviour, i.e. implicit declaration at hint definition time

Kenji Maillard (Jun 14 2020 at 15:32):

for instance

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

Simon Hudon (Jun 14 2020 at 15:36):

Oh that's good to know! Thanks!

Simon Hudon (Jun 14 2020 at 15:37):

Just to confirm, beside the tactics auto, autorewrite, etc, there's no way to query those databases, am I correct?

Kenji Maillard (Jun 14 2020 at 15:37):

Conversely, you won't get any error from autorewrite if you have a typo in your db name...

Kenji Maillard (Jun 14 2020 at 15:37):

Print HintDb ?

Simon Hudon (Jun 14 2020 at 15:38):

You can't put that in an Ltac script, can you?

Kenji Maillard (Jun 14 2020 at 15:39):

I don't think so

Simon Hudon (Jun 14 2020 at 15:59):

Thanks :) That helps

Paolo Giarrusso (Jun 14 2020 at 17:19):

@Simon Hudon you seem to want https://github.com/gmalecha/coq-ltac-iter

Paolo Giarrusso (Jun 14 2020 at 17:20):

(Not tried myself, but relevant)

Simon Hudon (Jun 14 2020 at 17:32):

Nice! Thanks!

Ezra elias kilty Cooper (Aug 07 2021 at 02:41):

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?

Théo Zimmermann (Aug 07 2021 at 10:36):

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.

Paolo Giarrusso (Aug 08 2021 at 12:45):

@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.

Paolo Giarrusso (Aug 08 2021 at 12:45):

Then you could Import A.core_hints in B.

Ezra elias kilty Cooper (Aug 08 2021 at 19:11):

@Paolo Giarrusso That's a great workaround, thanks!

Notification Bot (Nov 10 2021 at 10:32):

This topic was moved by Karl Palmskog to #math-comp users > Hint databases for finishing tactic

Last updated: Sep 23 2023 at 15:01 UTC