search

UniMath / Schools

77 stars 21 forks source link

Make CI work for the coq files #52

Closed arnoudvanderleer closed 2 months ago

arnoudvanderleer commented 2 months ago

This is based on the setup in the SetHITs repository.

arnoudvanderleer commented 2 months ago

@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 commented 2 months ago

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 commented 2 months ago

@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 commented 2 months ago

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

arnoudvanderleer commented 2 months ago

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 commented 2 months ago

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