Patrick Nicodemus (Oct 19 2022 at 02:15): Patrick Nicodemus (Oct 19 2022 at 02:15):I understand that the order of Require statements matters in general but I don't understand exactly what's going on in this case.
If I 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?
Jason Gross (Oct 19 2022 at 06:11):This sounds like a bug that should be reported on the issue tracker. (I don't know what's going on, though)
Ali Caglayan (Oct 19 2022 at 11:29):@Patrick Nicodemus Do you have an example we can have a look at? I am unable to reproduce locally from your description.
Patrick Nicodemus (Oct 19 2022 at 11:32):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.
Ali Caglayan (Oct 19 2022 at 11:35):So it might be that it is created in HoTT and then recreated in the stdlib.
Ali Caglayan (Oct 19 2022 at 11:36):I think typeclass_instances is created on the ocaml side however, though I am not sure.
Gaëtan Gilbert (Oct 19 2022 at 11:36):it's created in Init/Tactics.v
Ali Caglayan (Oct 19 2022 at 11:37):Ok then problem solved, we have a copy of that in HoTT too.
Ali Caglayan (Oct 19 2022 at 11:37):So the HintDb is being recreated here.
Ali Caglayan (Oct 19 2022 at 11:39):Ideally Ltac2 should not load any of the stdlib so that the database is not recreated.
Ali Caglayan (Oct 19 2022 at 11:40):However this is not so easy to do.
Paolo Giarrusso (Oct 19 2022 at 17:29):is it expected that Create HintDb clears it?
Paolo Giarrusso (Oct 19 2022 at 17:31):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.
Pierre-Marie Pédrot (Oct 19 2022 at 17:34):It all boils down to hint databases having an absolute name...
Paolo Giarrusso (Oct 19 2022 at 17:39):that doesn't mandate _clearing_ the existing database, does it?
Pierre-Marie Pédrot (Oct 19 2022 at 17:44):It's hard, because what do you do when you import two unrelated modules defining the same base?
Janno (Oct 19 2022 at 17:47):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.
Paolo Giarrusso (Oct 19 2022 at 18:50):it should certainly be a warning/error, and then we can talk of what to do when warnings are disabled
Paolo Giarrusso (Oct 19 2022 at 18:52):merging the DBs seems likely to create fewer problems — you need a shared typeclass/constant with non-composable instances/hints to get them
Paolo Giarrusso (Oct 19 2022 at 18:54):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:
Pierre-Marie Pédrot (Oct 19 2022 at 20:52):scoping dbs is hard, I've tried implementing it several times and it's a can of worms
Paolo Giarrusso (Oct 20 2022 at 01:43):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:
Gaëtan Gilbert (Oct 20 2022 at 09:19):there is nothing to merge when you have an existing db and then call create db
Paolo Giarrusso (Oct 22 2022 at 01:22):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.
Paolo Giarrusso (Oct 22 2022 at 01:25):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...
Patrick Nicodemus (Dec 03 2022 at 20:56):I created an issue on github for this
Patrick Nicodemus (Dec 03 2022 at 20:56):https://github.com/coq/coq/issues/16934
Last updated: Oct 13 2024 at 01:02 UTC