Stream: Coq users

Topic: Hint databases


view this post on Zulip 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?

view this post on Zulip Ralf Jung (Jun 06 2020 at 09:37):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Donald Sebastian Leung (Jun 14 2020 at 14:44):

auto with HintDb (source)

view this post on Zulip 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?

view this post on Zulip Donald Sebastian Leung (Jun 14 2020 at 15:07):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 14 2020 at 15:28):

Implementation-wise there are two different types...

view this post on Zulip 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?

view this post on Zulip Kenji Maillard (Jun 14 2020 at 15:30):

It is automatically an auto database I think

view this post on Zulip Pierre-Marie Pédrot (Jun 14 2020 at 15:30):

I think that they're just two different namespaces

view this post on Zulip Pierre-Marie Pédrot (Jun 14 2020 at 15:31):

Create HintDb is just for auto / eauto / typeclasses eauto

view this post on Zulip Pierre-Marie Pédrot (Jun 14 2020 at 15:31):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jun 14 2020 at 15:36):

Oh that's good to know! Thanks!

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Kenji Maillard (Jun 14 2020 at 15:37):

Print HintDb ?

view this post on Zulip Simon Hudon (Jun 14 2020 at 15:38):

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

view this post on Zulip Kenji Maillard (Jun 14 2020 at 15:39):

I don't think so

view this post on Zulip Simon Hudon (Jun 14 2020 at 15:59):

Thanks :) That helps

view this post on Zulip Paolo Giarrusso (Jun 14 2020 at 17:19):

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

view this post on Zulip Paolo Giarrusso (Jun 14 2020 at 17:20):

(Not tried myself, but relevant)

view this post on Zulip Simon Hudon (Jun 14 2020 at 17:32):

Nice! Thanks!

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 08 2021 at 12:45):

Then you could Import A.core_hints in B.

view this post on Zulip Ezra elias kilty Cooper (Aug 08 2021 at 19:11):

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

view this post on Zulip 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: Jan 28 2023 at 07:30 UTC