search

coq-community / coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
https://coq-community.org/coq-ext-lib/
BSD 2-Clause "Simplified" License
129 stars 46 forks source link

Add Hint Mode to Functor, Applicative, Monad #126

Closed Lysxia closed 10 months ago

Lysxia commented 2 years ago

Not sure why the definition of sequence breaks...

liyishuai commented 2 years ago

Now ITree is broken 🙃

liyishuai commented 2 years ago

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

Lysxia commented 2 years ago

coq-itree 4.0.0 is broken but dev is fixed.

Lysxia commented 2 years ago

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

liyishuai commented 10 months ago

Any idea with the CertiCoq breakage?

Lysxia commented 10 months ago

To be fixed in https://github.com/CertiCoq/certicoq/pull/86

Lysxia commented 10 months ago

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

liyishuai commented 10 months ago

Schedule:

  1. [x] coq/opam#2893
  2. [x] coq/opam#2934
  3. [x] coq/opam#2894