Skip to content
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

Warn when automatically lowering an inductive declared with : Type to Prop #18989

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Warn when automatically lowering an inductive declared with : Type to Prop #18989

wants to merge 9 commits into from
+171 −72

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Apr 29, 2024 •
edited

  • option to disable the lowering and option to default declare dependent eliminators for inductives with explicit Prop (for compat when fixing the warning by putting explicit Prop)

Inductives with no explicit type (eg Inductive foo := C.) can still get silently put in Prop.

Maybe it would make sense to support _ as "pick Prop or Type as needed" to make it easier to port indexed inductives? eg Inductive foo : nat -> Type := . would become Inductive foo : nat -> _ := . (currently it fails saying "not an arity"). But it doesn't look that nice so probably not worth doing.

Funind behaviour is slightly changed as we now force its inductives in Type instead of letting them be lowered (forward compatible way to disable the warning).

Overlays:

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2024
@SkySkimmer SkySkimmer requested review from a team as code owners April 29, 2024 15:10
@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 Apr 29, 2024
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Apr 30, 2024
@SkySkimmer
Adapt to coq/coq#18989 (warn when auto lowering inductive to Prop)
6c3e68f
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2024
@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 Apr 30, 2024
@SkySkimmer SkySkimmer added the needs: changelog entry This should be documented in doc/changelog. label Apr 30, 2024
@SkySkimmer
Copy link
Contributor Author

Maybe the options should be attributes instead, not sure.

@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: changelog entry This should be documented in doc/changelog. labels Apr 30, 2024
@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 Apr 30, 2024
@SkySkimmer SkySkimmer added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: inductives Inductive types, fixpoints, etc. labels May 2, 2024
@SkySkimmer SkySkimmer added this to the 8.20+rc1 milestone May 2, 2024
jfehrle
jfehrle reviewed May 3, 2024
View reviewed changes
doc/sphinx/language/core/inductive.rst Outdated Show resolved Hide resolved
doc/sphinx/language/core/inductive.rst Outdated Show resolved Hide resolved
@github-actions 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 5, 2024
@coqbot-app 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 7, 2024
@github-actions 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 16, 2024
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 16, 2024
@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 16, 2024
@github-actions 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 17, 2024
@coqbot-app 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 21, 2024
@ppedrot ppedrot self-assigned this May 21, 2024
@ppedrot
Copy link
Member

ppedrot commented May 22, 2024

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 22, 2024
@SkySkimmer
Copy link
Contributor Author

category theory failure is spurious

@coqbot-app 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 23, 2024
@SkySkimmer SkySkimmer removed 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 23, 2024
@github-actions 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 26, 2024
SkySkimmer and others added 9 commits May 27, 2024 14:11
@SkySkimmer
Add "Dependent Proposition Eliminators" option
3452d4d 
simulates what we do when automatically lowering inductives to Prop
for inductives explicitly put in Prop.
@SkySkimmer
Warn when automatically lowering inductives to Prop
585dd80
@SkySkimmer
Add Automatic Proposition Inductives to control automatic Prop lowering
285dd1e
@SkySkimmer
Fix small doc incorrectness after SProp
af08d12 
Note that with sort poly even foo_sind may be impossible to derive.
@SkySkimmer
Funind force automatic prop lowering off
55ee0c9
@SkySkimmer
Fix most tests which are incompatible with automatic Prop lowering di…
4aab758 
…sabled

except for those which appear to be testing the automatic prop lowering
@SkySkimmer
Doc: drop "accessing the type level" subsection and identity mention
ffbe31d 
`identity` is currently a notation for eq in Datatypes deprecated
since 8.16. `Logic_Type`  was deleted and `notT` moved to Logic at the
same time (coq#15256).
@SkySkimmer
Overlay for warn on auto Prop lowering
37aadbc
@SkySkimmer @jfehrle
Apply suggestions from code review (doc)
cd9b1e7 
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
@coqbot-app 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 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle jfehrle left review comments

At least 1 approving review is required to merge this pull request.

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: inductives Inductive types, fixpoints, etc.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@SkySkimmer @ppedrot @jfehrle