Admitted does not emit univ constraints from the proof

[SkySkimmer]

Fix #19566

Reverts part 3b4cf49

[herbelin]

I would call it restoring of a previous behavior more than fix, but ok.

[ejgallego]

@herbelin I indeed agree with your point, this is actually a kind of choice that is hard to make at the level of Qed / Admitted. , but IMHO belong more to the document-manager that is scheduling.

For example, in Flèche we try to ensure to run Admitted (or Qed , if failing) in the proof initial environment, as this helps us avoid recomputing the parts of the document after. But indeed, there are cases where the document manager may prefer (dynamically) to actually present the environment after the partial proof execution.

So this is IMO more of layering issue.

[herbelin]

Do you mean that save_admitted (i.e. Admitted) should take an option telling to cancel or not the current effects?

Or that save_admitted should always take the effects into account but that the UI may decide to implement Admitted as a combination of Abort and Admitted?

[SkySkimmer]

I don't think the semantics of a coq script should be up to the document manager. That sounds rather difficult to debug when someone gets a problem with one manager and can't be reproduced with another.

[SkySkimmer]

ie there should be 1 language "coq" not a bunch of variants "coq-coqc" "coq-fleche" "coq-coqide"...

[ejgallego]

I don't think the semantics of a coq script should be up to the document manager. That sounds rather difficult to debug when someone gets a problem with one manager and can't be reproduced with another.

I don't see a way to sentence-level commands to control document-level semantics, so IMHO what you ask is impossible with the current design of Coq.

For example, what to do on error, etc... There are multiple other cases, for example proof delegation, interaction with externals tools, etc... I don't see how different document models can yield the same semantics in this case, that is to say, documents with incomplete proofs.

Maybe document managers could agree on the semantics of error-free and admit-free documents. But once you have incomplete stuff, there are just different valid approaches. In fact, coq-lsp can be configured to give very different semantics to errors etc...

Do you mean that save_admitted (i.e. Admitted) should take an option telling to cancel or not the current effects?

Or that save_admitted should always take the effects into account but that the UI may decide to implement Admitted as a combination of Abort and Admitted?

@herbelin I guess several options are valid, I was pointing out that indeed IMHO Admitted is a command that actually take roles that don't belong to this layer. As a user, it seems a mis-feature: if I break something, now I have to replace all the Qeds. by Admitted to keep working?

That seems like very annoying, and to me a workflow-killer.

coq-lsp doesn't require users to replace failing Qed by Admitted in order to keep interacting with other parts of the document, so indeed, if you use coq-lsp you never need to use Admitted., unless you activate the flags to recover old semantics.

[SkySkimmer]

For example, what to do on error, etc... There are multiple other cases, for example proof delegation, interaction with externals tools, etc... I don't see how different document models can yield the same semantics in this case, that is to say, documents with incomplete proofs.

I agree that document managers can do different things with errors.
But Admitted is not an error.

[ejgallego]

But Admitted is not an error.

Admitted is however a very dubious command, and IMHO it admits different valid interpretations, so this is why the discussion happens.

Hence, IMHO, it should not be a command, note that Coq did fine not having Admitted. until 8.5.

[SkySkimmer]

@herbelin IDK what any of that means

[ejgallego]

IMHO we should remove Admitted and let the DMs handle failing Qeds. in the way they want.

[SkySkimmer]

Admitted is used significantly by the bug minimizer so removing it would take some work there

[ejgallego]

Admitted is used significantly by the bug minimizer so removing it would take some work there

Yes, I don't think removing Admitted is feasible as of today.

Also the bug minimizer could see big improvement by using coq-lsp and its caching / error recovery system / code slicing caps, and wouldn't need Admitted, but that's a different story.

I didn't mean to hijack this PR, I'm sorry, just wanted to give some more perspective on Admitted and how it is a bit of a special command.

IMHO it is best is to merge this PR for now, and maybe backport. As of today we all grew used to Admitted semantics this PR re-implements, and in general I think the ones we had in 8.19 are preferable.

[ejgallego]

See discussion as to why this is subtle.

IMHO the 8.20 semantics are widely expected, and the change was not intentional. I suggest we merge and backport.

Will merge soonish if nobody opposes.

[ejgallego]

@SkySkimmer maybe you could update the commit message to indicate this reverts a particular change if you feel like it?

I did update the PR description.

[ejgallego]

I wonder if this requires some kind of change entry tho?

[SkySkimmer]

I wonder if this requires some kind of change entry tho?

The back and forth is internal to 8.21 AFAICT so no

[SkySkimmer]

only changed the commit message, shouldn't need another full ci

[ejgallego]

Oh indeed this is 8.21 only, my bad cc: #19091

I should have done git branch --contains 3b4cf49e39ccb506aeb317aab818dc2fdc828175 to double-check.

[herbelin]

@SkySkimmer: my message was indeed un grand n'importe quoi. I canceled it. What I wanted to say is that we could have two words to reflect whether side-effects are expected or not. These words could be:

• Admitted which does the same as Restart. Admitted (whatever original semantics Admitted has).
• Suspended which does the same as Admitted before this PR.

At least, that would clarify why Admitted has sometimes side-effect and sometimes not.

(The current situation is probably not so much a big deal in practice though.)

[ejgallego]

@herbelin IMHO these kind of setups tend to be annoying for the user. Having to edit your document to get a change of behavior can get heavy, so IMHO these options live better at the level of user-config.

[ejgallego]

@SkySkimmer dunno what happened but test suite is failing :(

[SkySkimmer]

Indeed if we don't use the state at the end of the proof it's not possible to admit at https://github.com/coq/coq/blob/cd066bd59731fc878aa368aa9cb5ad488d9031ba/test-suite/bugs/bug_18951.v#L13

[SkySkimmer]

@coqbot run full ci

[ejgallego]

@coqbot: merge now