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

Make CI work for the coq files #52

Merged
merged 6 commits into from
Aug 20, 2024
Merged

Conversation

arnoudvanderleer
Copy link
Contributor

This is based on the setup in the SetHITs repository.

@arnoudvanderleer
Copy link
Contributor Author

@rmatthes I do not have a lot of experience with CI, but I based this on SetHITs. Can you maybe take a look at this to check that it should work as expected?

@arnoudvanderleer
Copy link
Contributor Author

All right, since the CI failed for commit 9f46247 with the same errors that I got locally, and succeeded for commit f507d9b, so the CI setup is at least somewhat correct. Note that both the CI here, and my local setup compile all files, but give a couple of warnings that xyz relies on an unsafe universe hierarchy.

@benediktahrens
Copy link
Member

@arnoudvanderleer : thanks for preparing this, it's great.

Some small comments:

  1. The version of Coq seems to be fixed to 8.19. Is there a way to always test with the current release?
  2. The Check commands are of pedagogical value. I am not sure it is a good idea to comment them out, even though I agree that they produce a lot of output.

@benediktahrens
Copy link
Member

I am merging this, but let's discuss the questions I raise above.

@benediktahrens benediktahrens merged commit 47a11d2 into UniMath:master Aug 20, 2024
1 check passed
@arnoudvanderleer
Copy link
Contributor Author

All right

  1. Good point, I think we may be able to set it to latest, but I am not sure. I will try in a next PR
  2. And good point. Note by the way that I let the Check commands intact. I only commented out the Search commands. Of course, these also may be of pedagogical value, although anyone is able to uncomment them in their local installation of coq. I commented them out because it made it very hard to see where compilation failed, although I now realize that that is fixed with the --error-reporting=twice flag.

@benediktahrens
Copy link
Member

@arnoudvanderleer : sorry, I meant Search, not Check.

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