8000 In Ltac, interpret constr arguments of an Ltac definition by default as open constr (with type classes inference) by herbelin · Pull Request #17087 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

In Ltac, interpret constr arguments of an Ltac definition by default as open constr (with type classes inference) #17087

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
wants to merge 1 commit into from
Closed

In Ltac, interpret constr arguments of an Ltac definition by default as open constr (with type classes inference) #17087

wants to merge 1 commit into from

Conversation

herbelin
Copy link
Member
@herbelin herbelin commented Jan 7, 2023

This is an experience, initially suggested by the compatibility in #17084.

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.

@herbelin herbelin added part: ltac Issues and PRs related to the Ltac tactic language. request: full CI Use this label when you want your next push to trigger a full CI. labels Jan 7, 2023
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 7, 2023
@coqbot-app
Copy link
Contributor
coqbot-app bot commented Jan 7, 2023

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

@coqbot-app
Copy link
Contributor
coqbot-app bot commented Jan 8, 2023

🔴 CI failures at commit 194bfb1 without any failure in the test-suite

✔️ Corresponding jobs for the base commit d2dabb6 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-mtac2, ci-sf, ci-tlc
  • You can also pass me a specific list of targets to minimize as arguments.

@herbelin herbelin mentioned this pull request Jan 8, 2023
Closed
2 tasks
@herbelin
Copy link
Member Author
herbelin commented Jan 8, 2023
8000

The failures in tlc and sf are both related to tlc's rapply which is "broken" since refine changed in 2015 (new proof engine), and which the PR makes working again (up to unwanted extra shelving). To evaluate if the impact of the PR on the rapply behavior is ok or not, the status of rapply should first be clarified.

The code failing in Mtac2 is associated to a comment (** One tricky thing about our nice notation [!] is that it doesn't work for open terms: *). I don't know how to interpret the comment, that is: whether it is a good failure or not.

So, shortly, it is unclear at the current time whether the change is expected or not.

@JasonGross
Copy link
Member

the status of rapply should first be clarified.

Is this the same rapply as in the Coq stdlib? I think the desired/ideal behavior of rapply is to interpret its arguments uconstr

@herbelin
Copy link
Member Author

I did not know the rapply in the standard library. This actually seems worth to be moved from Program to Init.

The rapply of tlc is the same idea except that it is broken (it does not add _).

@herbelin herbelin mentioned this pull request Feb 4, 2023
Closed
@ppedrot
Copy link
Member
ppedrot commented Nov 6, 2023

Closing this as it's explicitly branded as an experiment.

@ppedrot ppedrot closed this Nov 6, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
part: ltac Issues and PRs related to the Ltac tactic language.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@herbelin @JasonGross @ppedrot
0