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
base: master
Are you sure you want to change the base?
Conversation
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 |
@turion This is an interesting approach, but it is not Hydra-friendly as you can see. |
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 |
@veprbl What is the error? I have no idea how to debug this. |
You can't 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. |
@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? |
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 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 |
@emilazy Thanks again for your advice! @alexarice Ok, then I guess it's a script. Maybe agda-pkg can be used for that somehow..?
Hmmm, 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 @alexarice If we mainly pull packages from |
I personally don't see how |
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.
Agda-pkg may help you with that. Run the following commands, each command have their own flags, so check them with $ 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'}
Indeed.
Download git repos is one thing. Agda-pkg has more usages. See the documentation https://agda.github.io/agda-pkg/#/?id=usage-manual 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 |
Ah i did not realise there were more commands, I expect the JSON output could be used |
I've had more of a look at |
I can see three ways:
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. |
Once you do option 3 I don't see the point of having automatic package generation |
I'll choose this approach. |
The point is that we don't have to updated releases and hashes by hand. |
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. |
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 |
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
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:
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. |
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. |
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. |
@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
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 |
I think there are two points in the design space here:
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. |
To be honest I'm not exactly sure what your points mean here but the things I have noticed are:
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) |
Ok, that makes listing the dependency easy. We need only one version.
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.
You mean, potentially? Often Agda libraries will still compile with a newer Agda.
Good point. I somehow thought there is a reverse dependency on agda-categories somewhere, but at least there is none in nixpkgs.
We can still have older versions of Agda around. But it becomes a burden to maintain them all.
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. |
I know for a fact that |
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. |
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 think it is with some effort. Either in |
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
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 |
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)?
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. |
I marked this as stale due to inactivity. → More info |
Ok, to make this work I have to make an update script. |
I marked this as stale due to inactivity. → More info |
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:
package-index
.Things done
sandbox
innix.conf
on non-NixOS linux)nix-shell -p nixpkgs-review --run "nixpkgs-review wip"
./result/bin/
)nix path-info -S
before and after)@alexarice