Trunk+abstracting injection flags by maximedenes · Pull Request #677 · rocq-prover/rocq

maximedenes · 2017-05-24T19:14:20Z

This replaces #420 as discussed during the WG.

maximedenes · 2017-05-28T16:31:48Z

@herbelin would you mind rebasing this? Thanks!

herbelin · 2017-06-09T10:18:00Z

Rebased done. (It is actually more than a bugfix, it is the beginning of a proposal for adding a static control of tactic flags on top of the current dynamic control.)

maximedenes · 2017-06-19T07:40:36Z

@herbelin It seems there was a failure in formal-topology. Could you have a look?

herbelin · 2017-07-13T17:32:19Z

Overlay added for formal-topology (decide equality had become stronger).

maximedenes · 2017-07-26T09:49:59Z

+(* [keep_proofs] is relevant for types in Prop with elimination in Type *)
+(* In particular, it is relevant for injection but not for discriminate *)
+
+let find_positions keep_proofs env sigma ~no_discr t1 t2 =


keep_proofs should be a label here.

I agree that a label better documents itself (and be consistent with the use of a label for no_discr).

maximedenes · 2017-07-26T09:50:57Z


-let injectable env sigma t1 t2 =
-    match find_positions env sigma ~no_discr:true t1 t2 with
+let injectable keep_proofs env sigma t1 t2 =


Same here, should be a label.

Finally, I changed this to support a Boolean option so as to have better compatibility. Now, plugin writers have to make a conscious decision of whether they want to use the API with a statically-defined behavior or with a behavior which varies depending on the value of global flags.

maximedenes · 2017-07-26T09:52:51Z

 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
-		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite]  g
+		     else if Equality.injectable false(*?*) (pf_env g) (project g) t1 t2


Is there something that shoud be checked, as indicated by the comment?

Previously, this behavior was dynamically decided by the Keep Proof Equalities flag. In principle, it should be @forestjulien and @Matafou to know what they want here, but I don't think it matters a lot.

I committed a new version which preserves the former dynamic behavior.

maximedenes · 2017-07-26T09:53:23Z

+  | None -> !keep_proof_equalities_for_injection
+  | Some b -> b
+
+let dEqThen keep_proofs with_evars ntac = function


There are pros and cons. For instance, here, there is also an issue of uniformity of style. The with_evars flag is used pervasively without being a label.

maximedenes · 2017-07-26T09:55:36Z

-  !injection_in_context
-  && Flags.version_strictly_greater Flags.V8_5
+let use_injection_in_context = function
+  | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5


What is this option and why do flags have priority over it? I'm not saying anything is wrong, just trying to understand.

The Boolean injection_in_context is the dynamic value of the Structural Injection option.

The flags is the static configuration, defaulting to the dynamic configuration when None. If Some, the static configuration takes priority. See discussion at ceps #29.

maximedenes · 2017-07-28T08:15:36Z

@herbelin Is the topology fix backward compatible? If yes, can you make a PR upstream so that we can remove the overlay?

herbelin · 2017-07-28T12:41:43Z

It is not. We could make one of course but to the price of an uglier code or of getting rid of decide equality.

maximedenes · 2017-07-31T13:19:38Z

@herbelin Can you integrate the fix in topology?

herbelin · 2017-08-01T08:51:34Z

Sorry, I failed to understand the policy with fixes to contributor packages. We don't have control on topology besides overlays, do we? What do you want me to do exactly?

maximedenes · 2017-08-01T09:00:14Z

If you can make a pull request on topology, it would be ideal. But of course, if they don't ship a version of topology for each version of Coq, the fix should be backward compatible.

herbelin · 2017-08-01T12:08:36Z

@maximedenes: I don't know if you are a subscriber to topology. So, just to be sure you know, I made a PR, letting them decide what they think is best for them.

maximedenes · 2017-08-01T12:11:26Z

Indeed, I'm not, so thanks for the update.

Zimmi48 · 2017-08-02T14:41:44Z

@herbelin if you give the link to the PR in the thread, it can help track its status.

herbelin · 2017-08-02T15:26:35Z

PR on topology here.

Zimmi48 · 2017-08-09T10:20:42Z

It seems that this PR creates warnings which make the Travis build fail (and in passing there is also a trivial merge conflict).

Maybe a mention should be added in the compatibility file (I'm not sure what's the rule concerning when to update this file).

Finally, following your PR on topology, a commit was added to the master branch for backward-forward compatibility. Maybe this branch can be tested as a temporary overlay to confirm this commit does the job?

Zimmi48 · 2017-08-15T12:49:31Z

@herbelin Would you mind fixing the conflict and the warnings? Otherwise, this is going to miss 8.7+beta.

bmsherman · 2017-09-03T23:10:55Z

@Zimmi48 I have also now pushed that commit to the ci branch of the bmsherman/topology library, which is the one that I believe you are following. It took me a while because I wanted to be able to confirm that it was working on Travis, but have been having other difficulties with Travis so it wasn't building for some other reason.

herbelin · 2017-09-04T10:45:42Z

@Zimmi48: I rebased. I cannot reproduced the warning, so I suspect it resulted from a temporary failure of master.

Zimmi48 · 2017-09-04T12:43:21Z

@herbelin Did you try to compile with the -warn-error configure option? Travis still reports some fatal warnings.

Zimmi48 · 2017-09-04T12:44:09Z

Also note that you should normally be able to drop the overlay (commit 2c1c901) now.

herbelin · 2017-09-04T13:28:52Z

@Zimmi48: Ah, sorry, I did not see the funind warning (I generally don't use the -warn-error configuration flag because I generally prefer to skip warnings while in work-in-progress phase; I should eventually find a more robust light way to check them before pushing though, other than my eyes jumping over the non-filtered tacentries.ml warning).

Warning now fixed, and overlay removed.

Zimmi48 · 2017-09-04T13:29:55Z

I generally don't use the -warn-error configuration flag because I generally prefer to skip warnings while in work-in-progress phase; I should eventually find a more robust light way to check them before pushing though

Same here.

maximedenes · 2017-09-15T07:35:16Z

A travis run on my repo seemed to indicate a failure in formal-topology, but maybe unrelated. A quick rebase would help figuring out.

Zimmi48 · 2017-09-15T07:43:39Z

If we believe the Travis output before the conflict, the failure on formal-topology is real. This is also consistent with the history of this PR that has highlighted that formal-topology uses a lot of decide equality.
The conflicts come only from the CHANGES file and this is really annoying (this file is a large source of merge conflicts). We should probably come up with a strategy for generating the CHANGES file at the time of the release instead, but with formatted descriptions left in the commit messages (or PR messages). In the meantime, in the case of this PR, the CHANGES mention should go in the section "Changes beyond 8.7" (since it is too late at this point in the release cycle to backport a fix that affects the behavior of a tactic).

bmsherman · 2017-09-15T17:09:29Z

I'm sorry, for some reason I thought that I had pushed the change to stop using the decide equality tactic in the formal-topology library (ci branch of bmsherman/topology), but I just checked it now and apparently that change had not been incorporated. I've just made the change now.

(@Zimmi48 formal-topology actually only used decide equality once, and all that used to solve was decidable equality of the empty type anyway, so I removed the use of the decide equality tactic and just manually created the decidable equality instance.)

…n time.

ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug rocq-prover#5281.

herbelin · 2017-10-26T13:45:03Z

It seems this branch has been forgotten because of a needs:rebase tag which was not relevant at that time and which noone checked the relevance about.

A property of such tag is of course that it eventually spontaneously becomes relevant again, so I rebased.

Anything preventing this fix to be merged? (I guess now in 8.8 since it changes the ML API?)

Zimmi48 · 2017-10-26T14:51:22Z

A property of such tag is of course that it eventually spontaneously becomes relevant again, so I rebased.

If you mean: "I rebased today", then you forgot to push. Not a big deal though because the only conflicts are in the change-log files.

herbelin · 2017-10-26T14:53:28Z

Indeed (I forgot the -f).

herbelin mentioned this pull request May 26, 2017

Adding eassert, eset, epose, etc. #248

Merged

maximedenes added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 28, 2017

maximedenes added this to the 8.7 milestone Jun 1, 2017

maximedenes added the kind: fix This fixes a bug or incorrect documentation. label Jun 1, 2017

herbelin removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 9, 2017

herbelin force-pushed the trunk+abstracting-injection-flags branch from 37ea1ca to ff32694 Compare June 9, 2017 10:17

maximedenes added the needs: fixing The proposed code change is broken. label Jun 19, 2017

herbelin force-pushed the trunk+abstracting-injection-flags branch from ff32694 to 82d0aa2 Compare July 13, 2017 17:31

herbelin changed the base branch from trunk to master July 13, 2017 17:31

herbelin force-pushed the trunk+abstracting-injection-flags branch from 82d0aa2 to 4dd9ac1 Compare July 13, 2017 21:32

Zimmi48 removed the needs: fixing The proposed code change is broken. label Jul 19, 2017

herbelin mentioned this pull request Jul 23, 2017

Fix rewrite in * side conditions #915

Merged

maximedenes commented Jul 26, 2017

View reviewed changes

herbelin force-pushed the trunk+abstracting-injection-flags branch 2 times, most recently from a3c1b60 to ada2c38 Compare July 26, 2017 11:16

Zimmi48 added needs: fixing The proposed code change is broken. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Aug 9, 2017

maximedenes modified the milestones: 8.8, 8.7+beta Aug 17, 2017

herbelin force-pushed the trunk+abstracting-injection-flags branch from ada2c38 to 2c1c901 Compare September 4, 2017 10:44

Zimmi48 removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 4, 2017

herbelin force-pushed the trunk+abstracting-injection-flags branch 2 times, most recently from 6059756 to 630ef94 Compare September 4, 2017 13:16

Zimmi48 removed the needs: fixing The proposed code change is broken. label Sep 4, 2017

maximedenes added a commit to maximedenes/coq that referenced this pull request Sep 11, 2017

Merge PR rocq-prover#677: Trunk+abstracting injection flags

b11faa6

maximedenes added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 15, 2017

coqbot mentioned this pull request Oct 18, 2017

[Set Keep Proof Equalities.] should not be needed to make [Scheme Equality] succeed #5281

Closed

herbelin added 2 commits October 26, 2017 15:33

Delay use of flag "Discriminate Introduction" from interp to executio…

925c434

…n time.

Passing around the flag for injection so that tactics calling inj at

91e9e1c

ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug rocq-prover#5281.

herbelin removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 26, 2017

herbelin force-pushed the trunk+abstracting-injection-flags branch from 630ef94 to 91e9e1c Compare October 26, 2017 14:52

coqbot merged commit 91e9e1c into rocq-prover:master Oct 27, 2017

coqbot pushed a commit that referenced this pull request Oct 27, 2017

Merge PR #677: Trunk+abstracting injection flags

bb383ae

Conversation

maximedenes commented May 24, 2017

Uh oh!

maximedenes commented May 28, 2017

Uh oh!

herbelin commented Jun 9, 2017

Uh oh!

maximedenes commented Jun 19, 2017

Uh oh!

herbelin commented Jul 13, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maximedenes commented Jul 28, 2017

Uh oh!

herbelin commented Jul 28, 2017

Uh oh!

maximedenes commented Jul 31, 2017

Uh oh!

herbelin commented Aug 1, 2017

Uh oh!

maximedenes commented Aug 1, 2017

Uh oh!

herbelin commented Aug 1, 2017

Uh oh!

maximedenes commented Aug 1, 2017

Uh oh!

Zimmi48 commented Aug 2, 2017

Uh oh!

herbelin commented Aug 2, 2017

Uh oh!

Zimmi48 commented Aug 9, 2017

Uh oh!

Zimmi48 commented Aug 15, 2017

Uh oh!

bmsherman commented Sep 3, 2017

Uh oh!

herbelin commented Sep 4, 2017

Uh oh!

Zimmi48 commented Sep 4, 2017

Uh oh!

Zimmi48 commented Sep 4, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

herbelin commented Sep 4, 2017

Uh oh!

Zimmi48 commented Sep 4, 2017

Uh oh!

maximedenes commented Sep 15, 2017

Uh oh!

Zimmi48 commented Sep 15, 2017

Uh oh!

bmsherman commented Sep 15, 2017

Uh oh!

herbelin commented Oct 26, 2017

Uh oh!

Zimmi48 commented Oct 26, 2017

Uh oh!

herbelin commented Oct 26, 2017

Uh oh!

Zimmi48 commented Sep 4, 2017 •

edited

Loading