search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
204 stars 51 forks source link

Don't use `core` hint database? #222

Closed Lysxia closed 2 years ago

Lysxia commented 2 years ago

Dumping our hints in core seems unhygienic but I'm actually not sure what the drawbacks are, like whether it does slow things down for non-itree users.

YaZko commented 2 years ago

I agree that it's a bad idea and should be fixed if possible.

I do not know of the specific induced overhead here, but I had in the past issues with math-classes's core hints leading to a drastic (>10x) slow-down of itree-related rewrites despite none of these additional hints being used in the resolution. And the hints would leak through transitive imports even if no math-classes module was explicitly imported in the file of interest.

So definitely in general we should be in the habit of not polluting other development unless explicitly requested I believe.