search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Experiment with parallel checking using make #1057

Open felixwellen opened 11 months ago

felixwellen commented 11 months ago

This is just an experiment other people might be interested in, don't know if it is really something we want to merge. The PR deletes a couple of files which do not type check (they were manually excluded from the CI).

On my machine, checking with a generated makefile:

./generate-make.sh  > generated_makefile && cat GNUmakefile_head generated_makefile > GNUmakefile
time make -j9 check

checks everything in about 17m instead of the usual 30m. It does use all of my 32GB of RAM though. This approach could also be used to check everything without Everything.agdas or similar, to actually check using less RAM.

I also wondered about clustering/reducing the dependency graph, but didn't really get started on that (there is a python script for that).

gallais commented 11 months ago

I also wondered about clustering/reducing the dependency graph, but didn't really get started on that (there is a python script for that).

We have been doing something like that lately in the stdlib. I have an experiment using very basic metrics to identify sus looking modules: https://github.com/gallais/dot-analysis

It would be nice to get insights from people who actually know some graph theory as to what good metrics might be.

mortberg commented 11 months ago

This would be nice if I could easily control how many cores to use (I only have 8GB of RAM on my old laptop and don't like to run out...)

Another feature request I have wrt the build system is to be able to just check a single package instead of the whole library, for example if I'm working on a particular package I don't want to be forced build some completely unrelated part of the library when checking that my changes doesn't destroy something downstream in the package I'm working on.

felixwellen commented 11 months ago

This would be nice if I could easily control how many cores to use (I only have 8GB of RAM on my old laptop and don't like to run out...)

This is easy to control right now with the stuff in this PR, you can just say make -jN check, where N is the number of cores.

felixwellen commented 11 months ago

Another feature request I have wrt the build system is to be able to just check a single package instead of the whole library, for example if I'm working on a particular package I don't want to be forced build some completely unrelated part of the library when checking that my changes doesn't destroy something downstream in the package I'm working on.

That should automatically be the case with the stuff in this PR and also with the usual make, if you already built the library once. But I guess you are thinking about the situation where you haven't already built the whole library in the past. I guess in that case, we would have to decide on a source of truth for file changes. Maybe git? If you use that when jumping around between branches, time of change should be pretty useless.

felixwellen commented 11 months ago

... assuming you want to know, if your changes really only affect the package you are working on.