agdaPackages.generic: init at v0.1 #95059
Conversation
|
|
||
| preBuild = '' | ||
| echo "module Everything where" > Everything.agda | ||
| find src -name '*.agda' -and -not -name '*Lookup*' | sed -e 's/src\///;s/\//./g;s/\.agda$//;s/^/import /' >> Everything.agda |
There was a problem hiding this comment.
That's amazing. Maybe make this a function/option in the nixpkgs agda lib?
There was a problem hiding this comment.
It could also be a function that computes a new derivation, given an agda src. In that case, it's possible to patch the automatically generated Everything file.
There was a problem hiding this comment.
I shamelessly stole this from https://github.com/UlfNorell/agda-prelude/blob/master/test/Makefile but I agree it could be made to work in general
|
I could successfully build this. |
|
Just waiting on effectfully/Generic#4 I think |
Huh, so it doesn't build for you?? |
|
It does but only because I put in a hack to make sure no file containing the word |
alexarice
force-pushed
the
agda-generic
branch
from
9e3fae8
to
c63ece0
Compare
alexarice
changed the title
|
Should be ready for review |
| standard-library | ||
| ]; | ||
|
|
||
| preBuild = '' |
There was a problem hiding this comment.
It would be really cool if this could be abstracted into the agdaPackages lib. Either as simple option generateEverythingFile = true; or a transformation withEverythingFile (fetchFromGitHub { ... }) on the source.
There was a problem hiding this comment.
I agree but maybe this should a different PR. A potential problem with this is that you need a way to get where the source lives. This is given as the include field in the .agda-lib file but we don't currently extract it. This file could also contain multiple include sources
There was a problem hiding this comment.
This should potentially be in preConfigure instead of preBuild but as agda packages don't really have a configure stage, this doesn't really matter
There was a problem hiding this comment.
Ok, so let's touch this again when there is another library where this trick comes in handy.
|
Ok, so this still builds. Looking good to me then. |
|
If you want, you can speed the wait for merge by using https://github.com/apps/marvin-mk2 |
Motivation for this change
Fixes #94932
Things done
sandboxinnix.confon non-NixOS linux)nix-shell -p nixpkgs-review --run "nixpkgs-review wip"./result/bin/)nix path-info -Sbefore and after)@turion
There appears to be no
Everything.agdafile. There is aMain.agdabut I don't think it hits all the files usingfind(commented in code atm) takes a while and I think there might be some errors