Stream: Coq users

Topic: Side effects in Functors

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.

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

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

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!

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

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?

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

Paolo Giarrusso (Jun 22 2023 at 11:57):

Module Abort, with or without a name?

Gaëtan Gilbert (Jun 22 2023 at 12:10):

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

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?

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)

Rodolphe Lepigre (Jun 23 2023 at 11:49):

An alternative could be Abort Module foo I guess.

Emilio Jesús Gallego Arias (Jun 23 2023 at 13:08):

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

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.

Gaëtan Gilbert (Jun 23 2023 at 13:11):

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

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: Oct 13 2024 at 01:02 UTC