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

FYI: compilation error revealed by apery's CI #95

Open
affeldt-aist opened this issue Nov 16, 2024 · 2 comments
Open

FYI: compilation error revealed by apery's CI #95

affeldt-aist opened this issue Nov 16, 2024 · 2 comments

Comments

@affeldt-aist
Copy link

This is just to let you know about a compilation error that we have observed
on Apery's CI: coq-community/apery@18a6456

The error messages reads as follows:

 # File "./refinements/param.v", line 59, characters 0-23:
 # Error: Unsatisfied constraints: simpl_pred.u0 <= simpl_fun.u0
 # (maybe a bugged tactic).
@proux01
Copy link
Collaborator

proux01 commented Nov 16, 2024

On which version of what?

@affeldt-aist
Copy link
Author

It looks like an error message about dev versions:

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
  +- The following actions failed
  | - build coq-coqeal dev
  +- 
  +- The following changes have been performed
  | - install coq-mathcomp-algebra-tactics dev
  | - install coq-mathcomp-bigenough       dev
  | - install coq-mathcomp-finmap          dev
  | - install coq-mathcomp-multinomials    dev
  | - install coq-mathcomp-real-closed     dev
  | - install coq-mathcomp-zify            dev
  | - install coq-paramcoq                 dev
  +- 

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants