search

agda / cubical

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

Release v0.6 for agda 2.6.4 #1050

Closed felixwellen closed 10 months ago

felixwellen commented 11 months ago

Just one fix from #1048

felixwellen commented 10 months ago

If there is something to do nix-wise can someone do it? (Ping @MatthiasHu @jpoiret ) I cannot check this on my machine: image

felixwellen commented 10 months ago

If there is something to do nix-wise can someone do it? (Ping @MatthiasHu @jpoiret ) I cannot check this on my machine: image

Or @ncfavier ?

ncfavier commented 10 months ago

Agda build runs out of memory.

felixwellen commented 10 months ago

If I get it right, the flake for agda is used to build agda, which means it is built with a lot of optimization. So it is no surprise it runs out of memory. Is there a way to prevent this? Can we use a build of agda?

ncfavier commented 10 months ago

AFAICT we have three options:

  1. set up a Cachix cache for the agda organisation and push builds of released versions there, either manually or via CI
  2. wait for Agda 2.6.4 to land in nixpkgs and use that, since the build will be cached on cache.nixos.org (https://github.com/NixOS/nixpkgs/issues/259572)
  3. remove optimise-heavily using an overlay and see if that builds
ncfavier commented 10 months ago

In case we want to go with 1, I've created a Cachix cache (https://agda.cachix.org). Members of the agda GitHub organisation should have write access (if they log into Cachix via their GitHub account?).

felixwellen commented 10 months ago

Thanks! But I actually tend somewhat towards deactivating the nix-workflow. It seems a bit like it is mostly testing if the flake (and the agda flake) still works on github's machines. Shouldn't it be enough if someone tests it locally, which you probably did today when you produced the flake.lock? I'll of course wait a bit if someone solves the problem, but this is my default plan (which is not yet discussed with other maintainers).

felixwellen commented 10 months ago

Just to be clear: I am happy about the nix-workflow as long as it doesn't block the release. So if someone implements an easy solution (the "overlay" suggestion sounds like one) that's perfectly fine from my point of view.

phijor commented 10 months ago

I built 82aa301f6fed8896cfd2aa11a3dc5f441635843a locally with nix on the updated flake. I can confirm that it succeeds without errors/warnings.

In general I'm in favor of caching build artifacts via Cachix. Not only does it reduce build time, but people downstream would benefit from the caching, too.

AFAICT we have three options:

What about a fourth option: Provide two outputs in the flake:

  1. one depending on stable Agda (found in nixpkgs). This wouldn't have to build Agda from source and would break whenever changes depending on an unreleased Agda are introduced (which isn't necessarily bad)
  2. one depending on an unreleased version of agda, as it's done right now. One could tweak it to build a non-optimized Agda, if the point is to catch breaking changes. If the cache is shared across the entire organization it might not even be necessary to rebuild at all.

In any case, I'm willing to help out tweaking the nix workflow so that it doesn't block future releases.

ncfavier commented 10 months ago

I'm on board with removing the Nix workflow.

ncfavier commented 10 months ago

Note that 0.5 compiles with agda 2.6.4. Maybe that should be noted in the README.

felixwellen commented 10 months ago

I removed the ci-nix.yml, just because commenting out the whole file didn't work and I don't want to spend time on this. I also added 2.6.4 as an additional agda-version you can use with v0.5

mortberg commented 10 months ago

Looks good to me! Thanks for preparing this

felixwellen commented 10 months ago

Ok - will do.