Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP agda: Add libraries semi-automatically from package-index #87903

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

turion
Copy link
Contributor

@turion turion commented May 15, 2020

Motivation for this change

We don't want to keep a manual list of agda packages. This already exists in the form of https://github.com/agda/package-index/, and should be reused as far as automatically possible

This is work in progress. Further things to be done:

  • Find a good way to select the best revisions for each library. Either we fix a rev here in nixpkgs, or there has to be an automatic way to get the newest recorded revision from package-index.
  • Try to build all libraries and mark
  • Metadata
    • Add myself (and @alexarice ?) as maintainers for each package
    • Descriptions and URL
  • Overwrite mechanisms per library
    • Choose a different rev
    • add more maintainers
    • dependencies (those that cannot easily be parsed)
    • Custom files or build phases
Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
  • Built on platform(s)
    • NixOS
    • macOS
    • other Linux distributions
  • Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Determined the impact on package closure size (by running nix path-info -S before and after)
  • Ensured that relevant documentation is up to date
  • Fits CONTRIBUTING.md.

@alexarice

@turion turion mentioned this pull request May 15, 2020
@alexarice
Copy link
Contributor

My intuition is that a separate script like cabal2nix would be easier. i.e. a script you run that generates a load of nix files

@veprbl
Copy link
Member

veprbl commented May 15, 2020

@turion This is an interesting approach, but it is not Hydra-friendly as you can see.

@alexarice
Copy link
Contributor

I am still not sure how often the package index is updated either, I still think it is better to maintain our own package versions

@turion
Copy link
Contributor Author

turion commented May 16, 2020

@veprbl What is the error? I have no idea how to debug this.

@emilazy
Copy link
Member

emilazy commented May 16, 2020

You can't import, readFile, readDir, ... the result of a derivation (such as fetchTarball) in nixpkgs; that's called (somewhat inaccurately) import-from-derivation and Hydra forbids it. It leads to builds happening at evaluation time, whereas otherwise in the Nix model they're separate: Nix code is evaluated to produce a derivation which is then built.

Basically, you'll have to adopt the approach @alexarice suggested: write a script (possibly in Nix) to fetch the tarball and process its contents, but check the generated code into nixpkgs.

@turion
Copy link
Contributor Author

turion commented May 16, 2020

@emilazy I see, thanks for the explanation. I guess that's the reason why Haskell on nixpkgs has its complicated workflow. Is there any documentation or discussion of this restriction?

@emilazy
Copy link
Member

emilazy commented May 16, 2020

It's avoided because it means that the build graph cannot be determined statically, and you can't answer questions like "what attributes are available in agdaPackages?" without doing arbitrary fetches/builds. Practical implications include not working well with --dry-run and nix-env(1). I'm afraid I don't know a pointer to a specific central discussion on this, but see e.g. #24590 (comment), #11319 (comment), #87592 (comment).

The approach I would suggest is to have a script (in Nix itself, or Python, or even just a bash script if you really want) that downloads the package index and extracts the package names, URLs and hashes to a JSON file; then you can construct agdaPackages from the underlying data with builtins.fromJSON (builtins.readFile ./packages.json).

@turion
Copy link
Contributor Author

turion commented May 16, 2020

@emilazy Thanks again for your advice!

@alexarice Ok, then I guess it's a script. Maybe agda-pkg can be used for that somehow..?

I am still not sure how often the package index is updated either, I still think it is better to maintain our own package versions

Hmmm, package-index seems to be a one-person project run by @jonaprieto, but still it's in the agda organisation, and it seems to receive updates every odd months. Also, since it's open, we can as well send PRs there. Then the non-Nix-using (part of the) Agda community can also profit.

And we in turn profit from the listings of new and updated packages there. I wouldn't underestimate that. If we run our own library set here, we can quickly get out of sync with the rest of the community, and I would very much like to avoid that, because it would mean losing any adoption that nix might win very quickly.

I asked the maintainer of package-index for collaboration here: agda/package-index#20

@alexarice If we mainly pull packages from package-index and add mechanisms for overrides, is that an acceptable solution for you?

@alexarice
Copy link
Contributor

I personally don't see how agda-pkg will help, as I believe the main purpose of it is to download the git repos, which nix will do for us

@jonaprieto
Copy link

jonaprieto commented May 16, 2020

I am still not sure how often the package index is updated either, I still think it is better to maintain our own package versions

I update the package-index every once in a while, without any periodicity. Unfortunately, some packages do not have any release, so we keep the last commit seen as their version.

One may think to have one script to keep the package-index updated. It can not take longer. However, I have not found time to do that, to be honest.

It's avoided because it means that the build graph cannot be determined statically, and you can't answer questions like "what attributes are available in agdaPackages?" without doing arbitrary fetches/builds. Practical implications include not working well with --dry-run and nix-env(1). I'm afraid I don't know a pointer to a specific central discussion on this, but see e.g. #24590 (comment), #11319 (comment), #87592 (comment).

The approach I would suggest is to have a script (in Nix itself, or Python, or even just a bash script if you really want) that downloads the package index and extracts the package names, URLs and hashes to a JSON file; then you can construct agdaPackages from the underlying data with builtins.fromJSON (builtins.readFile ./packages.json).

Agda-pkg may help you with that. Run the following commands, each command have their own flags, so check them with --help.

$ pip3 install agda-pkg
$ apkg init
$ apkg list
Library name         Latest version  URL
---------------------------------------------------------------------------------------------------------
agda-base            v0.2            https://github.com/pcapriotti/agda-base.git
agda-categories      v0.1            https://github.com/agda/agda-categories.git.
...
$ apkg info standard-library
{ 'cached': False,
  'default': True,
  'depend': [],
  'description': None,
  'editable': False,
  'fromGit': True,
  'fromIndex': True,
  'fromUrl': False,
  'include': 'src/',
  'index_path': PosixPath('/Users/jonaprieto/.apkg@agda-2.6.1/package-index/src/standard-library/versions/v1.3'),
  'installed': False,
  'keywords': [],
  'library': 'standard-library',
  'license': '',
  'origin': 'https://github.com/agda/agda-stdlib.git',
  'sha': '9f929b4fe28bb7ba74b6b95d01ed0958343f3451',
  'source_path': PosixPath('/Users/jonaprieto/.apkg@agda-2.6.1/package-sources/standard-library@v1.3'),
  'testedWith': [],
  'version': 'v1.3'}

Hmmm, package-index seems to be a one-person project run by @jonaprieto, but still it's in the agda organisation, and it seems to receive updates every odd months. Also, since it's open, we can as well send PRs there. Then the non-Nix-using (part of the) Agda community can also profit.

Indeed.

I personally don't see how agda-pkg will help, as I believe the main purpose of it is to download the git repos, which nix will do for us

Download git repos is one thing. Agda-pkg has more usages. See the documentation https://agda.github.io/agda-pkg/#/?id=usage-manual
If there is something you want to add, please add an issue, or PR.

BTW, someone a few weeks ago added something related to NixOS, you might be interested.

https://agda.github.io/agda-pkg/#/?id=using-with-nix-or-nixos

@alexarice
Copy link
Contributor

Ah i did not realise there were more commands, I expect the JSON output could be used

@alexarice alexarice mentioned this pull request May 17, 2020
10 tasks
@alexarice
Copy link
Contributor

alexarice commented May 17, 2020

I've had more of a look at agda-pkg. It does a lot more than I thought it did, and the json output would be very useful, though I am not sure how you would plan on generating build instructions based on the data. For example, there is no information anywhere that ial should be built with make (that needs a patchShebangs according to our current package) and standard-library needs you to run a haskell script.

@turion
Copy link
Contributor Author

turion commented May 17, 2020

though I am not sure how you would plan on generating build instructions based on the data

I can see three ways:

  1. PR to the library itself that gets rid of the make script. Gives the cleanest solution, but is the most effort, may yield friction with the library maintainers, and is often not feasible.
  2. That information needs to be encoded by hand in package-index, but I don't know how. @jonaprieto how would you deal with that situation?
  3. Allow to override the buildPhase in nixpkgs.

I think there are not enough Agda libraries out there in order to try and detect the build strategy automatically. Probably it's going to be option 3., since it's easiest and also quite stable and versatile.

@alexarice
Copy link
Contributor

Once you do option 3 I don't see the point of having automatic package generation

@jonaprieto
Copy link

3. Allow to override the buildPhase in nixpkgs.

I'll choose this approach.

@turion
Copy link
Contributor Author

turion commented Feb 5, 2021

Once you do option 3 I don't see the point of having automatic package generation

The point is that we don't have to updated releases and hashes by hand.

@turion
Copy link
Contributor Author

turion commented Feb 5, 2021

And also we would get new packages for free when they're added to the index. We only need to overwrite the build phase if it doesn't work out of the box.

@alexarice
Copy link
Contributor

Once you do option 3 I don't see the point of having automatic package generation

The point is that we don't have to updated releases and hashes by hand.

I actually tried quite hard to get this working recently here but was stopped by a few things that made it easier to just do manually. If I remember correctly the main issues were that it wasn't immediately clear what was the latest version for some packages and there also seemed to be no way to figure out what what packages worked with each versions. That said I was trying to do something that mapped versions of packages to the appropriate version of agda.

I did even try to hack around with the python code a bit but didn't get very far. If you have any ideas I'd be happy to hear about them

@turion
Copy link
Contributor Author

turion commented Feb 5, 2021

I actually tried quite hard to get this working recently here

That's really cool! When reading through it I was wondering why you've created your own index instead of reusing https://github.com/agda/package-index. Is there a particular reason? Maybe package-index has an impractical format?

If I remember correctly the main issues were that it wasn't immediately clear what was the latest version for some packages

Some packages have proper releases with tags. For those, it should be possible to figure out the latest version automatically by looking at the directory structure. But for those with no tags and just commit hashes, we can only fix a particular hash. That, or get our hands real dirty and do git hackery (i.e. looking up the date of the rev and compare that). I think fixing a particular hash is better for starters.

Like that it's not much better than doing it all by hand, but:

  1. It's still easier to e.g. roll back and forth between different versions (because the index lists them all)
  2. there is a single source of truth, i.e. the whole community agrees on which versions are relevant
  3. maybe with time and prodding, agda library devs will acknowledge the usefulness of releasing versions, and start doing it

and there also seemed to be no way to figure out what what packages worked with each versions.

I would have said, simply chose the latest (building) version of everything, and those packages that don't build with these dependencies are marked as broken, and an issue should be created upstream. Getting a compatible package set doesn't come for free, and we'll have to prod the community constantly to fight the bitrot. But I think it's a great service to the community because everyone is notified of breakages soon, and actively maintained packages stand out.

That means we have to have some mechanism that allows us to override the automatically generated nix files, similar to how it works in Haskell.

@alexarice
Copy link
Contributor

To be honest I can't exactly remember why I stopped trying to use the index but I spent a good half a day trying to get it to work before deciding to roll up my own thing.

I believe the main problem was the mapping between agda versions and package versions. Once this had to be manually specified, I had to manually do something each package anyway, and by that point typing in the (very low amount of) hashes was was far easier than trying to get the package index's data in the correct format.

Secondly, part of the reason for making my own repository was so that I could mess around with stuff without worrying whether it was the correct fit for nixpkgs and so that I could push whatever I wanted and pin whatever versions or commits of packages make sense (my main motivation was to get a development version of agda with a development version of cubical). Doing this and then tying myself to package-index seemed contradictory.

Hope this helps. If you are determined to use the package-index, my personal thought on the easiest way to do it is to add functionality to agda-pkg which prints out data in the exact format you want. This will almost certainly be easier than trying to work out where this data currently is in agda-pkg and trying to parse it.

@alexarice
Copy link
Contributor

Something else that would make this far easier is if you could convince people to use some standardised way to build an agda library, preferably with a standardised way of building of building html files as well.

@alexarice
Copy link
Contributor

@turion I have worked a bit more on https://github.com/alexarice/all-agda so that more stuff is now read from json files. If you look in the various versions.json files, you will see that the necessary things are:

  • version name
  • sha256
  • list of agda versions that the library works with
  • list of dependencies including their version

I believe if the package-index was extended to contain this data (in particular I don't believe it currently contains the last 2) then it could be used. I'd also be willing to help upstream some of this data if this is the direction that is chosen

@turion
Copy link
Contributor Author

turion commented Feb 12, 2021

* list of agda versions that the library works with

* list of dependencies including their version

I think there are two points in the design space here:

  1. All libraries should be in sync and up to date with the latest Agda & dependency versions

  2. Every package can work with older versions of everything, but these versions need to be specified

  3. is more coherent, simpler, puts pressure on the ecosystem to always update, risks losing packages that aren't regularly maintained

  4. is more flexible, more complex, leaves the ecosystem in peace, harder to maintain

My impression is that I've been pursuing 1., but you prefer 2.?

One thing about 2. that is hard: It needs a dependency resolution mechanism. Assume you have a dependency triangle where A depends on B, B depends on C, and A also on C. Assume that some version of A needs a newer version of C than B can handle. Then this won't work in Agda because the module namespace is global. It's the same in Haskell. We would need to detect this and try to solve the constraints somehow. This is really complicated, and I believe nixpkgs is not the right place for that.

It can be simplified by saying that a dependency cannot have a version range, but must have a definite version. (Possibly, a right open interval might do as well.) Then the above case would be simply rejected. But then a lot of cases that would compile are rejected because the version bounds need to be maintained. If we maintain the version bounds then that could work. Optionally we can apply pressure on the ecosystem to increase the bounds.

So my impression is this can only work either with 1., or with 2. but really simple dependency version specifications.

@alexarice
Copy link
Contributor

To be honest I'm not exactly sure what your points mean here but the things I have noticed are:

  1. Packages tend to only work with one specific version of their dependencies.
  2. There is a lag between e.g. standard-library updating and things that depend on standard-library updating. This is unavoidable.
  3. When Agda updates, everything will break
  4. I do not know of a single package with multiple dependencies, so have not considered dependency triangles or anything. Ideally the library maintainer would have found versions of libraries that work together.

1 and 2 could be fixed by maintaining multiple versions of packages in nixpkgs. As far as I can tell (3) is unavoidable as Agda is tied into the haskell ecosystem.

Also I'm not really trying to push any method of doing things, I've just had a mess around and found that the data above is the necessary information you need (at least if you are maintaining multiple versions of packages)

@turion
Copy link
Contributor Author

turion commented Feb 12, 2021

1. Packages tend to only work with one specific version of their dependencies.

Ok, that makes listing the dependency easy. We need only one version.

2. There is a lag between e.g. standard-library updating and things that depend on standard-library updating. This is unavoidable.

Yes. With my scenario 1. this means that we would need to wait until the reverse dependencies of standard-library have updated, or mark them as broken.

3. When Agda updates, everything will break

You mean, potentially? Often Agda libraries will still compile with a newer Agda.

4. I do not know of a single package with multiple dependencies, so have not considered dependency triangles or anything. Ideally the library maintainer would have found versions of libraries that work together.

Good point. I somehow thought there is a reverse dependency on agda-categories somewhere, but at least there is none in nixpkgs.

1 and 2 could be fixed by maintaining multiple versions of packages in nixpkgs. As far as I can tell (3) is unavoidable as Agda is tied into the haskell ecosystem.

We can still have older versions of Agda around. But it becomes a burden to maintain them all.

Also I'm not really trying to push any method of doing things, I've just had a mess around and found that the data above is the necessary information you need (at least if you are maintaining multiple versions of packages)

Ah ok. I was just pointing out that we can either choose to maintain multiple versions, or stick with a single version. While multiple versions are nice, single versions are probably easier. But I'll support either decision.

@alexarice
Copy link
Contributor

You mean, potentially? Often Agda libraries will still compile with a newer Agda.

I know for a fact that standard-library-1.5 does not compile with current master agda for example. I would consider this quite a large breakage (I am referring to major versions, bug fix versions are fine)

@alexarice
Copy link
Contributor

And in reply to "We can still have older versions of Agda around", what I was trying to say is that precisely this is not possible in nixpkgs.

@turion
Copy link
Contributor Author

turion commented Feb 12, 2021

You mean, potentially? Often Agda libraries will still compile with a newer Agda.

I know for a fact that standard-library-1.5 does not compile with current master agda for example. I would consider this quite a large breakage (I am referring to major versions, bug fix versions are fine)

Yes that would be a huge breakage. But does it compile with the latest released (i.e on hackage) version? Those are the relevant ones for us, I think.

And in reply to "We can still have older versions of Agda around", what I was trying to say is that precisely this is not possible in nixpkgs.

I think it is with some effort. Either in nixpkgs/pkgs/development/haskell-modules/configuration-hackage2nix.yaml one can pin older versions for something, or we can just use haskellPackages.callHackage with some older version of Agda. In the latter case, those older versions are only visible for us.

@alexarice
Copy link
Contributor

You mean, potentially? Often Agda libraries will still compile with a newer Agda.

I know for a fact that standard-library-1.5 does not compile with current master agda for example. I would consider this quite a large breakage (I am referring to major versions, bug fix versions are fine)

Yes that would be a huge breakage. But does it compile with the latest released (i.e on hackage) version? Those are the relevant ones for us, I think.

I am making the point that at some point Agda 2.6.2 will be released, and whatever version of the standard-library that currently exists at that point will no longer work

And in reply to "We can still have older versions of Agda around", what I was trying to say is that precisely this is not possible in nixpkgs.

I think it is with some effort. Either in nixpkgs/pkgs/development/haskell-modules/configuration-hackage2nix.yaml one can pin older versions for something, or we can just use haskellPackages.callHackage with some older version of Agda. In the latter case, those older versions are only visible for us.

You will also have to maintain expressions for all the dependencies of Agda, or they will be updated to incompatible versions in the haskell infrastructure. At this point you would effectively be maintaining a parallel haskell distribution just for Agda. I don't think you'd have much luck getting this merged into nixpkgs

@turion
Copy link
Contributor Author

turion commented Feb 12, 2021

You mean, potentially? Often Agda libraries will still compile with a newer Agda.

I know for a fact that standard-library-1.5 does not compile with current master agda for example. I would consider this quite a large breakage (I am referring to major versions, bug fix versions are fine)

Yes that would be a huge breakage. But does it compile with the latest released (i.e on hackage) version? Those are the relevant ones for us, I think.

I am making the point that at some point Agda 2.6.2 will be released, and whatever version of the standard-library that currently exists at that point will no longer work

Fair point. How do we work around that then? If we don't want to maintain older versions of Agda, it seems like the only way is to mark it broken then until a fix is out (which will probably not take too long)?

And in reply to "We can still have older versions of Agda around", what I was trying to say is that precisely this is not possible in nixpkgs.

I think it is with some effort. Either in nixpkgs/pkgs/development/haskell-modules/configuration-hackage2nix.yaml one can pin older versions for something, or we can just use haskellPackages.callHackage with some older version of Agda. In the latter case, those older versions are only visible for us.

You will also have to maintain expressions for all the dependencies of Agda, or they will be updated to incompatible versions in the haskell infrastructure. At this point you would effectively be maintaining a parallel haskell distribution just for Agda. I don't think you'd have much luck getting this merged into nixpkgs

True, at least for those dependencies where Agda requires an older version. That's probably the latest point when the older Agda version needs to be dropped.

@stale
Copy link

stale bot commented Aug 29, 2021

I marked this as stale due to inactivity. → More info

@stale stale bot added the 2.status: stale https://github.com/NixOS/nixpkgs/blob/master/.github/STALE-BOT.md label Aug 29, 2021
@turion
Copy link
Contributor Author

turion commented Aug 30, 2021

Ok, to make this work I have to make an update script.

@stale stale bot removed the 2.status: stale https://github.com/NixOS/nixpkgs/blob/master/.github/STALE-BOT.md label Aug 30, 2021
@stale
Copy link

stale bot commented Apr 18, 2022

I marked this as stale due to inactivity. → More info

@stale stale bot added the 2.status: stale https://github.com/NixOS/nixpkgs/blob/master/.github/STALE-BOT.md label Apr 18, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
2.status: merge conflict 2.status: stale https://github.com/NixOS/nixpkgs/blob/master/.github/STALE-BOT.md 6.topic: agda
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

6 participants