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.

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

Fix auto minimizer to download all dependencies #333

Merged
merged 2 commits into from
Jan 27, 2025

Conversation

SkySkimmer
Copy link
Contributor

No description provided.

@SkySkimmer
Copy link
Contributor Author

Do we not have CI to check that it compiles? I don't have the bot dependencies installed right now so I was coding without compiling.

@Zimmi48
Copy link
Member

Zimmi48 commented Jan 22, 2025

Indeed, we don't. We could certainly adapt the current CI for master to also run on branch, but by making the final deploy step require a specific click on a button. It would be better than the current setup, where I push to my fork to test-deploy PRs.

I have pushed a commit fixing blindly the compilation. Please review my changes, and if you are happy with them, I can test-deploy the PR for further debugging.

@SkySkimmer
Copy link
Contributor Author

Updated, should be ready to test

@Zimmi48
Copy link
Member

Zimmi48 commented Jan 22, 2025

@SkySkimmer
Copy link
Contributor Author

SkySkimmer commented Jan 22, 2025

I guess we won't be able to test the minimizer immediately since it needs a master pipeline with the updated message in checks.

EDIT: or does it? I'm not sure.

@SkySkimmer
Copy link
Contributor Author

@SkySkimmer
Copy link
Contributor Author

I don't think you pushed the right commit, the actions link you gave says "Zimmi48 pushed fba784b"

@Zimmi48
Copy link
Member

Zimmi48 commented Jan 22, 2025

Arf, really sorry about that. It looks like I'm forgetting how to use git 😆
New pipeline started at https://github.com/Zimmi48/bot/actions/runs/12907217721.

@SkySkimmer
Copy link
Contributor Author

The regex was incorrect, please redeploy

@SkySkimmer
Copy link
Contributor Author

@SkySkimmer
Copy link
Contributor Author

This part seems to work, there are more fixes needed for unrelated reasons but this PR should be good to merge.

@Zimmi48 Zimmi48 merged commit e838d62 into rocq-prover:master Jan 27, 2025
@SkySkimmer SkySkimmer deleted the fix-minim branch March 3, 2025 13:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants