Skip to content
New issue

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

#

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

Already on GitHub? # to your account

Jump to bottom

Add Hint Mode to Functor, Applicative, Monad #126

Merged
merged 1 commit into from
Jan 26, 2024
Merged

Add Hint Mode to Functor, Applicative, Monad #126

merged 1 commit into from
Jan 26, 2024

Conversation

Lysxia
Copy link
Contributor

@Lysxia Lysxia commented Mar 22, 2022

Not sure why the definition of sequence breaks...

@liyishuai
Copy link
Member

Now ITree is broken 🙃

@liyishuai
Copy link
Member

liyishuai commented Mar 31, 2022 •
edited
Loading

Breaks MonadLaws on Coq 8.8 ~ 8.11; breaks ITree on Coq 8.12 ~ 8.15. Any fix for MonadLaws?

@Lysxia
Copy link
Contributor Author

Lysxia commented Mar 31, 2022

coq-itree 4.0.0 is broken but dev is fixed.

@Lysxia
Copy link
Contributor Author

Lysxia commented Mar 31, 2022

And I can't reproduce the weird CI failure on 8.9

@github-actions github-actions bot added the Stale label Sep 20, 2023
@liyishuai liyishuai removed the Stale label Jan 4, 2024
@liyishuai
Copy link
Member

Any idea with the CertiCoq breakage?

@Lysxia Lysxia mentioned this pull request Jan 9, 2024
Merged
@Lysxia
Copy link
Contributor Author

Lysxia commented Jan 9, 2024

To be fixed in CertiCoq/certicoq#86

@Lysxia Lysxia marked this pull request as ready for review January 10, 2024 15:10
@Lysxia
Copy link
Contributor Author

Lysxia commented Jan 10, 2024

For reference I asked about this practice of Hint Mode on Zulip, and learned that this is common practice in stdpp and iris.

@liyishuai
Copy link
Member

liyishuai commented Jan 11, 2024 •
edited
Loading

Schedule:

  1. Add coq-certicoq.dev coq/opam#2893
  2. Package coq-ext-lib.1.2.1 coq/opam#2934
  3. CertiCoq 0.9 ExtLib upper bound coq/opam#2894

@liyishuai liyishuai enabled auto-merge (squash) January 24, 2024 16:26
@liyishuai liyishuai mentioned this pull request Jan 26, 2024
Closed
@liyishuai liyishuai disabled auto-merge January 26, 2024 06:24
@liyishuai liyishuai merged commit d47e472 into rocq-community:master Jan 26, 2024
@Lysxia Lysxia deleted the mode branch January 27, 2024 13:16
# for free to join this conversation on GitHub. Already have an account? # to comment
Reviewers

@liyishuai liyishuai

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Lysxia @liyishuai