search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
26 stars 5 forks source link

Set up some CI #26

Closed maxsnew closed 1 year ago

maxsnew commented 1 year ago

Things that would be nice to have:

  1. Automatically checking the whole repo to see if it compiles
  2. Linters like checking we don't go over 80 chars (this is the style in the cubical stdlib)
stschaef commented 1 year ago

On my fork I'm attempting to set up some CI based on what is currently used in Cubical

This seems like it'll work well if I can get the caching to reliably work

A few questions

  1. Do we want to reject broken builds, or just flag them as broken?
  2. It seems like the Cubical CI checks if all the code there compiles. If we implement something like this, I imagine that some of the more WIP files, or things that haven't been touched for a while, might not build. If that is the case, I'm not sure where those fall on our list of priorities
  3. Are there any Agda linters out there? After searching a bit I couldn't find any, but we could use a very barebones linter if we're only worrying about things like 80char width
maxsnew commented 1 year ago
  1. What do you mean by reject broken builds? Will it actually stop you from pushing to a branch until it passes? Or is this just for PRs?
  2. Check if all code compiles, yes. Broken/incomplete code can go in branches
  3. No clue
stschaef commented 1 year ago

Right now, whatever code the user pushes will be on the desired branch. If it passes all the tests you get a green check, if it fails a red X.

I think there are rules that can be added to enforce that you must pass all the tests before the code change is accepted. I currently don't have any of these, but I was asking if we want this sort of functionality on either PRs or when pushing to a branch?

This could be somewhat "safer" but might be a little annoying/overkill. In any case, I think I can get the non-rejecting version of this setup on main later today

stschaef commented 1 year ago

27 sets this up

there may be opportunities for better caching, but cloning from github takes ~30s-1min for cubical + stdlib, so this isn't prohibitively slow. But if agda itself isn't cached, it'll take around 20 minutes. If it is cached, the run takes 3-5 minutes

we still need to fix some line lengths, and there is existing non-compiling code on main. Over the next few days, we can gradually fix these and move the broken code into development branches.

At this moment, I'm unsure which files still have lines that are too long but I'm finding them one at a time with find . -type f -name "*.agda" -print0 | xargs -0 awk 'length($0) > 80 { print FILENAME ":" FNR ": line too long"; exit 1 }'

and the files that do not compile are

We can find these by reading the output of make test-and-report which compiles all files and lists which failed.

stschaef commented 1 year ago

This is NOW finally set up. Sorry for the PR spam

Will close this issue when there is finally a green checkmark after fixing the above

stschaef commented 1 year ago

Finally passing checks on my fork. So I'm pushing the changes to line lengths/commenting out broken code

I think that the CI can be more efficient, but I'm having some issues correctly caching the agdai files