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

Replace use of omega with lia for Coq 8.14 #13741 #110

Closed jfehrle closed 3 years ago

jfehrle commented 3 years ago

For https://github.com/coq/coq/pull/13741

jfehrle commented 3 years ago

The checks are still not complete after 12+ hours. They all look like this:

image

Is some human intervention needed?

liyishuai commented 3 years ago

Seems like CircleCI wasn't enabled on your fork.

liyishuai commented 3 years ago

Tests passed on my fork; merged.

jfehrle commented 3 years ago

Thanks for your help. I had 2 jobs fail in the coqdoc stage with different errors. I guess those were transient errors?

Example:

Error:
/home/coq/project/theories/Data/HList.vo: premature end of file. Try to rebuild it
liyishuai commented 3 years ago

Those errors happen occasionally, and usually turn green upon rerun.