[declare] Allow custom typing flags when declaring constants.

[ejgallego]

We use the new Declare.Info structure to uniformly add properties to
the handling of constants. In this case, per-constant typing flags.

The internal code may want to see some further refactoring, including
pushing the flags down to Safe_typing.add_constant , but the changes
in the interface should be definitive.

By request, we also implement attributes to specify the typing flags, they have the form
#[typing($ATT=$ENABLE)] where:

• ATT is one of guarded, universes, positive
• ENABLE is one of on / off

This replaces #12539 and finishes #9004 .

[ejgallego]

Not sure I'm happy with the current setup, but requesting review.

[coqbot]

For your complete information, the following job in allow failure mode has failed: test-suite:4.12+trunk+dune

[coqbot]

For your complete information, the following job in allow failure mode has failed: test-suite:4.12+trunk+dune

[SkySkimmer]

This isn't hooked up to anything.

[ejgallego]

This isn't hooked up to anything

@SkySkimmer indeed I provide here the core API and defer to #12539 and #9004 the implementation using attributes + the test cases. Do you think it is a bad idea?

How should @lthms proceed?

[SkySkimmer]

I think having an unused API is a bad idea, we should just merge this PR and its first user.

[ejgallego]

Ok , @lthms , please include this PR in your branch then.

[lthms]

Ack. I will try to give it a try later this week.

[ejgallego]

I did some progress, but still the parsing is broken.

[lthms]

Am I correct to guess your three last commits implements what I tried to do in my PR, @ejgallego? (it’s fine by me, I just want to be sure I understood correctly)

[ejgallego]

Am I correct to guess your three last commits implements what I tried to do in my PR, @ejgallego? (it’s fine by me, I just want to be sure I understood correctly)

They are just a try, I didn't finish them; feel free to ignore them / update them.

[ejgallego]

@lthms actually only the last commit has overlap with your PR, the rest are the base infrastructure that couldn't be implemented before #12372

[gares]

More concretely, in the objective of a discussion at the next call, is there a summary of all propositions, together with an indication of which are the closest to be adopted and why?

Given all the valid (as in correct in English) options, I'd say we pick the ones we like the most and find less confusing for a user.
I don't think involving the community as a whole is needed in this case, but more than a few devs and users may be beneficial.
The weekly call seemed to fit both the time frame I hope for (that is very soon) and the number of participants (about 10 usually).

I can sum up all the proposals given here, as well as all the preferences, if you like.

[gares]

terminaison(admit)

If there were many ways to pass the termination check, I'd probably like termination(structutal)...termination(lexicographic).
But we already have a syntax, for both toplevel and inner fixpoints, to express that. Here it seems we talk about a bunch of booleans (see also the other spin off PR), so I would not flip the object with the action.

[ejgallego]

Updated to bypass_check which is IMHO clear and scary enough; for the naming of the flags themselves, I've chosen to keep the same name used in the Set global options, for consistency. Renaming / deprecation is much welcome if you feel like doing it, but IMHO they should be kept in sync.

[ejgallego]

Actually after looking a bit more to the global Set flags, it could make sense to just use #[check(guarded=no)] , etc... instead of bypass_check. WDYT folks?

[herbelin]

As far as I'm concerned, both bypass_check(guard) and check(guarded=no) are ok to me.

[gares]

The the sea of comments, there were these two, by myself and @mattam82:

W.r.t. the terminology, both in the attributes and refman, I'd frankly pick termination and productivity rather than guardedness (by destructor/constructor), since at least the most common one (termination) is clear even without a PhD in TT.

I agree guard_check is a bit technical.

[Zimmi48]

@gares: This was answered:

for the naming of the flags themselves, I've chosen to keep the same name used in the Set global options, for consistency. Renaming / deprecation is much welcome if you feel like doing it, but IMHO they should be kept in sync.

[Zimmi48]

I like bypass_check. Quite scary indeed 👻

[gares]

This was answered:

for the naming of the flags themselves, I've chosen to keep the same name used in the Set global options

fair enough, but I'm not so sure the deprecation plan makes sense. I mean, if we agree that termination is better than guarded, maybe we can deprecate it right now, and provide the new name as an attribute from the start. (in another PR)

[Zimmi48]

Agreed. Making the change in a separate (but 8.13) PR is also a good idea to make the process more efficient.

[gares]

@herbelin this seems all good to me. If you see no other problems, the sooner its merged the better

[herbelin]

So, if I understand correctly, the current proposal is:

bypass_check(positivity)
bypass_check(universe)
bypass_check(guard)

Are the plans clear regarding guard vs termination?

Concretely, my question is whether there is a risk of having to backtrack if I merge now?

[ejgallego]

Concretely, my question is whether there is a risk of having to backtrack if I merge now?

I think we could refine more; my point is indeed what @Zimmi48 said, IMHO we should keep the attributes and the Set flags in sync, otherwise seems a bit inconsistent (that's also a point for moving towards check vs bypass_check IMO)

[Zimmi48]

Concretely, my question is whether there is a risk of having to backtrack if I merge now?

The plan is indeed to change the guard into termination but as part of a separate PR (that would still go into 8.13).

[herbelin]

OK, you then think that enough feedback has been given and we could now safely merge?

If so, will do around 8PM Paris time.

[Zimmi48]

Yes, because this was discussed during the Coq Call and it corresponds more or less to the conclusion.

[herbelin]

@coqbot: merge now

[ejgallego]

Thanks to all!

[jfehrle]

Though the train has left the station, skip_check might be a good alternative to bypass_check.

[ejgallego]

Though the train has left the station, skip_check might be a good alternative to bypass_check.

There is still time until the final release. I still like just check more, see:

Set Positivity Checking.
#[check(positivity=no)] Inductive foo := ...
#[skip_check(positivity=yes] Inductive foo := ...
#[bypass_check(positivity=no)] ...

I don't like the double negation in the last example. That alone, should be a reason to go with check; if on top, we add the current semantics for Set, IMHO the case is strong. WDYT @jfehrle ?

[jfehrle]

I've not followed the details of the PR. I don't care for the double negative in the last example, either.

check(positivity=yes) and skip_check(positivity=no) seem pretty clear. check(positivity=no) is a little vague--does it mean to actively check that positivity is false or does it mean not to check that positivity is true? One would have to know/learn that. check(positivity) and skip_check(positivity) would be pretty clear, but I don't if that's sufficient for your use case.

On the other hand, check or skip_check seem to be rather general terms that might be used for other attributes, for example, hypothetically, check(transitivity)--would attributes allow/support that?

No wording is perfect and no code lasts forever. We can change this relatively easily if we come up with a better idea in the future. We may come up with better ideas as more attributes are created over time.