Attribute #[clearbody] useful instead of Let ... Qed by SkySkimmer · Pull Request #17544 · rocq-prover/rocq

SkySkimmer · 2023-04-27T13:05:35Z

cf discussion in #17205

ejgallego · 2023-04-27T15:32:31Z

      ?hook ?typing_flags () =
-    { poly; inline; kind; udecl; scope; hook; typing_flags }
+    let () = match scope, clearbody with
+      | Discharge, true ->


Can't we just put clearbody in the Discharge constructor? IMHO that's better it doesn't make sense for Global.

We could put it in the Discharge, although that type is also used for variables (ie no body) so I wasn't sure it would make much sense.
OTOH passing clearbody alongside it isn't better for that

Yeah maybe it has to go in the SectionLocalDef constructor? Would be good if we can find a way to avoid the assert etc... in the end the clearbody flag is used in a very very specific place.

I put it in SectionLocalDef, although it's still also in Info.t as SectionLocalDef is created late.
I moved this check to the attribute handling (synterp.ml defattributes)

ejgallego

It seems to me that the clearbody flag should be attached to maybe the SectionLocalDef constructor as it is the only place where it makes sense.

proux01 · 2023-04-28T13:50:00Z

Nice, but in mathcomp we would still prefer having Let lema. Proof. <proof> Qed act as Let lemma. Proof. abstract(<proof>). Defined. (if that is not overly broken) rather than having to put verbose #[clearbody] ... Defined everywhere.

SkySkimmer · 2023-04-28T14:01:54Z

That seems not broken, but the change of behaviour definitely would need a deprecation phase.

proux01 · 2023-04-28T14:57:46Z

Do you have it anywhere so that I could try it on mathcomp?

SkySkimmer · 2023-04-28T15:07:21Z

If you mean having abstract I haven't coded it.
It's equivalent to translating Let foo : T. proof. Qed. into Lemma foo_subproof : T. proof. Qed. Let foo := foo_subproof. so there shouldn't be major issues.

proux01 · 2023-04-28T15:20:33Z

Ok, I'll give it a try. For the deprecation phase, we could have an attribute #[abstract] for Let that will be deprecated right away and the current warning message for Let Qed offering to try it. Then, after deprecation phase, #[abstract] will become the default and be removed a few versions later.

SkySkimmer · 2023-04-28T15:35:33Z

We could also do an option eg Let Qed Is Abstract and deprecate unsetting it.

SkySkimmer · 2023-04-28T15:39:41Z

#17553

ejgallego

Declare parts look Ok, would be nice to do some more cleanup in another PR w.r.t. section handling etc...

SkySkimmer · 2023-05-03T15:30:06Z

I tried something like that too but Discharge is also used for Variable and I liked having clearbody in those paths less

jfehrle

Some suggestions and questions

ejgallego · 2023-05-03T20:46:04Z

I tried something like that too but Discharge is also used for Variable and I liked having clearbody in those paths less

Yes, it seems to me the current setup is a good compromise. How to improve it I have no idea, it could require having some more static typing for sections (as we do for interactive proofs now)

SkySkimmer · 2023-05-05T12:37:25Z

updated doc

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer · 2023-05-05T14:50:43Z

#17576 to experiment with Qed behaving like abstract

ejgallego · 2023-05-09T14:35:58Z

@SkySkimmer should we merge this? @silene are you OK with this?

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer · 2023-05-22T15:43:06Z

This is ready IMO

ejgallego · 2023-05-22T16:04:30Z

Will leave one day in case anyone wants to comment.

In light of #17576 I still think that maybe a better path forward could be to actually have a #[proof_env] attribute that would instead add stuff to the named environment , I get the feeling that this could make the code more orthogonal, so Let would become implemented as other things that run a hook after a declaration.

That could also be combined with some sort of "inline" attribute for section defs.

ejgallego · 2023-05-24T12:34:17Z

@coqbot: merge now

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer requested review from a team as code owners April 27, 2023 13:05

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 27, 2023

Zimmi48 approved these changes Apr 27, 2023

View reviewed changes

Comment thread doc/sphinx/language/core/sections.rst Outdated

Comment thread doc/sphinx/language/core/sections.rst Outdated

ejgallego reviewed Apr 27, 2023

View reviewed changes

Comment thread vernac/declare.ml Outdated

ejgallego reviewed Apr 27, 2023

View reviewed changes

Comment thread vernac/declare.ml Outdated

ejgallego reviewed Apr 27, 2023

View reviewed changes

SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Apr 27, 2023

jfehrle reviewed Apr 27, 2023

View reviewed changes

Comment thread doc/sphinx/language/core/sections.rst Outdated

SkySkimmer force-pushed the clearbody-att branch from 7ef9be9 to 30560b4 Compare April 28, 2023 11:19

SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: progress Work in progress: awaiting action from the author. labels Apr 28, 2023

SkySkimmer force-pushed the clearbody-att branch from 30560b4 to d3295eb Compare April 28, 2023 13:26

coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Apr 28, 2023

SkySkimmer mentioned this pull request Apr 28, 2023

Let .. Qed should produce an opaque subproof instead of doing clearbody #17553

Closed

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 1, 2023

SkySkimmer force-pushed the clearbody-att branch from d3295eb to cb010de Compare May 2, 2023 11:05

coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels May 2, 2023

SkySkimmer requested a review from a team May 3, 2023 13:43

ejgallego approved these changes May 3, 2023

View reviewed changes

jfehrle reviewed May 3, 2023

View reviewed changes

Comment thread doc/changelog/08-vernac-commands-and-options/17544-clearbody-att.rst Outdated

Comment thread doc/changelog/08-vernac-commands-and-options/17544-clearbody-att.rst Outdated

Comment thread doc/sphinx/language/core/sections.rst

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label May 5, 2023

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label May 5, 2023

SkySkimmer force-pushed the clearbody-att branch from 63951fd to b57c4bd Compare May 5, 2023 12:37

coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels May 5, 2023

SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request May 5, 2023

Let with Qed: produce really-Qed side definition

d185ff1

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer mentioned this pull request May 5, 2023

Let with Qed: produce really-Qed side definition #17576

Merged

SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request May 10, 2023

Let with Qed: produce really-Qed side definition

bb019f4

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request May 12, 2023

Let with Qed: produce really-Qed side definition

f77e8a2

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

Attribute #[clearbody] useful instead of Let ... Qed

6049407

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label May 15, 2023

SkySkimmer force-pushed the clearbody-att branch from b57c4bd to 6049407 Compare May 15, 2023 11:12

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 15, 2023

coqbot-app Bot merged commit cabc945 into rocq-prover:master May 24, 2023

SkySkimmer deleted the clearbody-att branch May 24, 2023 12:54

proux01 pushed a commit to SkySkimmer/rocq that referenced this pull request Sep 22, 2023

Let with Qed: produce really-Qed side definition

3fd15ff

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

proux01 pushed a commit to SkySkimmer/rocq that referenced this pull request Sep 25, 2023

Let with Qed: produce really-Qed side definition

b814c67

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request Nov 2, 2023

Let with Qed: produce really-Qed side definition

43d58cc

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request Nov 2, 2023

Let with Qed: produce really-Qed side definition

edd9f76

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request Nov 2, 2023

Let with Qed: produce really-Qed side definition

a945053

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request Nov 2, 2023

Let with Qed: produce really-Qed side definition

95341cf

cf discussion in rocq-prover#17544 This does have a tradeoff as the side definition still exists after the section is closed unlike usual.

Uh oh!

Conversation

SkySkimmer commented Apr 27, 2023

Uh oh!

Uh oh!

Uh oh!

ejgallego Apr 27, 2023

Choose a reason for hiding this comment

Uh oh!

SkySkimmer Apr 27, 2023

Choose a reason for hiding this comment

Uh oh!

ejgallego Apr 27, 2023

Choose a reason for hiding this comment

Uh oh!

SkySkimmer Apr 28, 2023

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

ejgallego left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

proux01 commented Apr 28, 2023

Uh oh!

SkySkimmer commented Apr 28, 2023

Uh oh!

proux01 commented Apr 28, 2023

Uh oh!

SkySkimmer commented Apr 28, 2023

Uh oh!

proux01 commented Apr 28, 2023

Uh oh!

SkySkimmer commented Apr 28, 2023

Uh oh!

SkySkimmer commented Apr 28, 2023

Uh oh!

ejgallego left a comment

Choose a reason for hiding this comment

Uh oh!

SkySkimmer commented May 3, 2023

Uh oh!

jfehrle left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ejgallego commented May 3, 2023

Uh oh!

SkySkimmer commented May 5, 2023

Uh oh!

SkySkimmer commented May 5, 2023

Uh oh!

ejgallego commented May 9, 2023

Uh oh!

SkySkimmer commented May 22, 2023

Uh oh!

ejgallego commented May 22, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented May 24, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

ejgallego commented May 22, 2023 •

edited

Loading