Thibaut Pérami (Sep 11 2023 at 15:25): Thibaut Pérami (Sep 11 2023 at 15:25):I have a long section (800LoC), that creates a new type and proves lots of lemmas about it, and put some of them into specific hint databases (both normal and rewrite). The proof of later lemmas in the section use both databases in their proof scripts. Then I close the section and the databases disappear. Is there a way to export that database outside the section so that user of the type can use the associated databases, or do I need to copy all the hint commands outside the section?
Paolo Giarrusso (Sep 11 2023 at 16:27):sadly for now you need to copy the hints — or split the section. You want #[export] Hint Resolve/#[global] Hint Resolve, but this is still pending last I checked
Paolo Giarrusso (Sep 11 2023 at 16:29):where "split the section" means
End your_section.
#[export] Hint Resolve ....
Section your_section.
(* abstract again over everything — hoping all assumptions can be auto-inferred when applying hints, but otherwise you'd have bigger problems *)
...
and yeah, I agree this isn't great when you use hints to prove more hints :-|
Meven Lennon-Bertrand (Sep 11 2023 at 16:29):To be sure, the difficulty is that hints can contain arbitrary tactic code, and that the section-closing mechanism cannot handle tactics, right?
Paolo Giarrusso (Sep 11 2023 at 16:30):Hint Resolve can't use tactics
Paolo Giarrusso (Sep 11 2023 at 16:31):and each Hint command gives semantics to attributes separately — you're talking of Hint Extern, which is orthogonal to Hint Resolve.
Gaëtan Gilbert (Sep 11 2023 at 16:31):no, the difficulty is that nobody has written the section closing for Hint Resolve
also not clear we want to do it when the hint is an arbitrary term
Paolo Giarrusso (Sep 11 2023 at 16:32):even having it just for constants would be very nice, especially since using arbitrary terms is somewhat discouraged already (I forget how officially beyond "PMP wants to drop that")
Paolo Giarrusso (Sep 11 2023 at 16:32):existing issue https://github.com/coq/coq/issues/16048
Gaëtan Gilbert (Sep 11 2023 at 16:36):ping @Pierre-Marie Pédrot
Last updated: Oct 13 2024 at 01:02 UTC