search

knowsys / Formale-Systeme-in-LEAN

LEAN4 formalization of the undergraduate lecture "Formale Systeme" at TU Dresden (WIP)
Apache License 2.0
8 stars 0 forks source link

setup ci #14

Closed matzemathics closed 11 months ago

mmarx commented 11 months ago

Also, having a devShells.default = pkgs.mkShell { buildInputs = [ leanPkgs.lean ]; }; would be nice.

matzemathics commented 11 months ago

I just noticed, that there is no way for me to get the dependencies, because the leanBuildPackage does not integrate with lake, but needs all dependencies as flakes (which for example mathlib4 is not). No idea how to work around this.

mmarx commented 11 months ago

I just noticed, that there is no way for me to get the dependencies, because the leanBuildPackage does not integrate with lake, but needs all dependencies as flakes (which for example mathlib4 is not). No idea how to work around this.

It looks like the lake-manifest.json has enough information to fetch the appropriate versions of the dependencies: it pins to a specific git commit, which should be enough to do a builtins.fetchGit. It would be better to use fetchgit from nixpkgs to get the dependencies (since that happens at build time instead of evaluation time), but then you would need to provide the output hashes as well, which is probably overkill. A problem might still be dealing with transitive dependencies, but I guess that this could in principle be automated. It might be illuminating to see how the rust support in nixpkgs deals with this: https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/rust/import-cargo-lock.nix.

Alternatively, you could just add each dependency as a package to the flake, and then just provide those as buildInputs. This is easier to do, but might be more work in the long term if dependencies change frequently.

monsterkrampe commented 11 months ago

Thanks for the effort!

Should I be able to use lean and lake within a nix develop shell (so far I cannot) or is the flake really only meant for builds in the CI? (I would be fine with that.)

mmarx commented 11 months ago

Should I be able to use lean and lake within a nix develop shell (so far I cannot) or is the flake really only meant for builds in the CI? (I would be fine with that.)

I thought so, but apparently that's not included in the devShell generated by buildLeanPackage, so I've added that manually.

mmarx commented 11 months ago

This should probably also use a concurrency group … ;)

mmarx commented 11 months ago

Also the magic nix cache action is not of much use here, since it runs into the rate limits of the free-tier GitHub actions caching API. We should probably set up a cachix store instead and just use that, with lean4 as an extra substituter.