Stream: Ltac2

Topic: Ltac2 library, typeclasses


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

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

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

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

view this post on Zulip Ali Caglayan (Oct 19 2022 at 11:35):

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.

view this post on Zulip Ali Caglayan (Oct 19 2022 at 11:35):

So it might be that it is created in HoTT and then recreated in the stdlib.

view this post on Zulip Ali Caglayan (Oct 19 2022 at 11:36):

I think typeclass_instances is created on the ocaml side however, though I am not sure.

view this post on Zulip Gaëtan Gilbert (Oct 19 2022 at 11:36):

it's created in Init/Tactics.v

view this post on Zulip Ali Caglayan (Oct 19 2022 at 11:37):

Ok then problem solved, we have a copy of that in HoTT too.

view this post on Zulip Ali Caglayan (Oct 19 2022 at 11:37):

So the HintDb is being recreated here.

view this post on Zulip Ali Caglayan (Oct 19 2022 at 11:39):

Ideally Ltac2 should not load any of the stdlib so that the database is not recreated.

view this post on Zulip Ali Caglayan (Oct 19 2022 at 11:40):

However this is not so easy to do.

view this post on Zulip Paolo Giarrusso (Oct 19 2022 at 17:29):

is it expected that Create HintDb clears it?

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

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 17:34):

It all boils down to hint databases having an absolute name...

view this post on Zulip Paolo Giarrusso (Oct 19 2022 at 17:39):

that doesn't mandate _clearing_ the existing database, does it?

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Patrick Nicodemus (Dec 03 2022 at 20:56):

I created an issue on github for this

view this post on Zulip Patrick Nicodemus (Dec 03 2022 at 20:56):

https://github.com/coq/coq/issues/16934


Last updated: Jan 31 2023 at 11:01 UTC