I understand that the order of
Require statements matters in general but I don't understand exactly what's going on in this case.
Require Import files that add hints to the typeclass resolution hint database and then
Require Ltac2, this latter line of code wipes out the whole typeclass database.
I have to start with requiring the Ltac2 and then import everything else to avoid this.
Why does this happen, is this to be expected or a bug or what?
This sounds like a bug that should be reported on the issue tracker. (I don't know what's going on, though)
@Patrick Nicodemus Do you have an example we can have a look at? I am unable to reproduce locally from your description.
I was using the HoTT library for this which is probably part of it.
Require Import HoTT.Basics. Print HintDb typeclass_instances. From Ltac2 Require Ltac2. Print HintDb typeclass_instances. (* Empty database *)
So HoTT works with -noinit. And if you do
Print HintDb typeclass_instances in an empty file with
-noinit you will see that the HintDb doesn't exist.
So it might be that it is created in HoTT and then recreated in the stdlib.
I think typeclass_instances is created on the ocaml side however, though I am not sure.
it's created in Init/Tactics.v
Ok then problem solved, we have a copy of that in HoTT too.
So the HintDb is being recreated here.
Ideally Ltac2 should not load any of the stdlib so that the database is not recreated.
However this is not so easy to do.
is it expected that
Create HintDb clears it?
at least not from reading https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#creating-hint-databases... this is still ambiguous enough:
Creates a new hint database named ident.
It all boils down to hint databases having an absolute name...
that doesn't mandate _clearing_ the existing database, does it?
It's hard, because what do you do when you import two unrelated modules defining the same base?
I would turn that into a warning that is treated as an error by default. If the files truly are unrelated It's almost always a recipe for disaster and people who want to do it on purpose can disable the warning.
it should certainly be a warning/error, and then we can talk of what to do when warnings are disabled
merging the DBs seems likely to create fewer problems — you need a shared typeclass/constant with non-composable instances/hints to get them
worst-case, one of the two libraries will have to rename their DB; that's less bad than having to agree on notations...
Of course, scoping DBs would be even better, but if it were easy/urgent you'd have done it, and there are more urgent things :sweat_smile:
scoping dbs is hard, I've tried implementing it several times and it's a can of worms
I imagined; I wasn't asking to spend effort on that, but to do something simpler to remove a footgun; the perfect can be the enemy of the good. Janno's idea is footgun-free, and merging DBs when the error is turned into a warning seems a smaller footgun :grinning:
there is nothing to merge when you have an existing db and then call create db
let me rephrase less ambiguously: if the warning is disabled,
Create HintDb could be a no-op. (I'd say that merges both DBs). If the DB settings are different, that could warrant an additional message.
especially if the warnings are loud enough (and errors-by-default counts), almost any behavior other than https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/Ltac2.20library.2C.20typeclasses/near/304932279 is much better...
I created an issue on github for this
Last updated: Jun 10 2023 at 06:31 UTC