Stream: Coq users

Topic: Side effects in Functors


view this post on Zulip Janno (Jun 22 2023 at 11:18):

I often put test cases in trivial functors to avoid their side effects from leaking. This is useful in particular when Succeed Qed. Abort doesn't cut it, e.g. when test cases build on each other. However, it seems like functors actually do not properly prevent side effects from leaking. Specifically, universe constraints on monomorphic universes are applied globally even when the functor is never instantiated. Is this know? Is it intended? If so, what is a better alternative? Module Type prohibits Ltac2 definitions and thus cannot always be used.

view this post on Zulip Gaëtan Gilbert (Jun 22 2023 at 11:20):

It's known and intended
Module Type also produces universe constraints so wouldn't help anyway

view this post on Zulip Gaëtan Gilbert (Jun 22 2023 at 11:22):

the only thing that doesn't produce global universe constraints and isn't Succeed-like is universe polymorphism

view this post on Zulip Janno (Jun 22 2023 at 11:26):

I had no idea that Module Type had the same problem. Thanks for making me aware of that!

view this post on Zulip Gaëtan Gilbert (Jun 22 2023 at 11:28):

I think at some point there was a feature request for Abort for modules, but it never got implemented
some syntax would have to be picked since Abort already exists ofc

view this post on Zulip Rodolphe Lepigre (Jun 22 2023 at 11:30):

For syntax, I guess Abort ModuleName in the place of End ModuleName would do it. Or would there be a problem with that?

view this post on Zulip Gaëtan Gilbert (Jun 22 2023 at 11:34):

I don't like controlling whether it aborts a proof vs a module based on the presence of a name

view this post on Zulip Paolo Giarrusso (Jun 22 2023 at 11:57):

Module Abort, with or without a name?

view this post on Zulip Gaëtan Gilbert (Jun 22 2023 at 12:10):

Module Abort means starting a module called Abort currently
we could do #[abort] End name

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:28):

Gaëtan Gilbert said:

I don't like controlling whether it aborts a proof vs a module based on the presence of a name

What's the problem you see with that?

view this post on Zulip Gaëtan Gilbert (Jun 23 2023 at 11:39):

With Abort meaning abort the current proof, it feels confusing that

Lemma foo : T.
Abort foo.

fails (or aborts a foo module)

view this post on Zulip Rodolphe Lepigre (Jun 23 2023 at 11:49):

An alternative could be Abort Module foo I guess.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 13:08):

Oh indeed I forgot that Abort doesn't take any names now.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 13:09):

Anyways for the original test case, I think we could support test cases that are only run under some conditions. That was discussed in the past, however it needs to be implemented properly.

view this post on Zulip Gaëtan Gilbert (Jun 23 2023 at 13:11):

there's also Succeed Load as an option, not nice to edit though

view this post on Zulip Paolo Giarrusso (Jun 23 2023 at 17:58):

conditional testcases demand that any code after would be built twice — Abort seems a better semantics and some "Test Module" command such that "End" aborts the module might be a more declarative interface


Last updated: Jun 22 2024 at 15:01 UTC