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

Put lemma-overloading back to CI #1290

Open
pi8027 opened this issue Nov 13, 2024 · 3 comments
Open

Put lemma-overloading back to CI #1290

pi8027 opened this issue Nov 13, 2024 · 3 comments
Labels
kind: CI Issue or PR about the CI. (Gitlab CI or CI of dependencies problems linked with math-comp)

Comments

@pi8027
Copy link
Member

pi8027 commented Nov 13, 2024

I ported it to recent versions of Coq and MathComp: coq-community/lemma-overloading#74
@pi8027 pi8027 added the kind: CI Issue or PR about the CI. (Gitlab CI or CI of dependencies problems linked with math-comp) label Nov 13, 2024
@pi8027
Copy link
Member Author

pi8027 commented Nov 13, 2024

@proux01 @CohenCyril Can you help me with this? I wanted to make sure that coq/coq#19611 does not break lemma-overloading, and thus, I need to put it back to the CI of Coq (and MathComp).

@CohenCyril
Copy link
Member

The first step is to add lemma-overloading to nixpkgs.
You can take inspiration from this: https://github.com/NixOS/nixpkgs/pull/122450/files

@pi8027
Copy link
Member Author

pi8027 commented Nov 14, 2024

NixOS/nixpkgs#355908

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: CI Issue or PR about the CI. (Gitlab CI or CI of dependencies problems linked with math-comp)
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@pi8027 @CohenCyril