Stream: Nix toolbox devs & users

Topic: mathcomp-analysis outdated in Nix repo


view this post on Zulip Sebastian Ertel (Jan 31 2024 at 09:24):

Hi,

I'm trying to load mathcomp-2.X with mathcomp-analysis via Nix.

I was unable to load mathcomp-2.0.0 and received the following error:

error: builder for '/nix/store/akhd7kg8x9wqq3hapiys04wv9z2vb6cj-coq8.18-mathcomp-ssreflect-2.0.0.drv' failed with exit code 2;
       last 10 log lines:
       > Use attribute #[clearbody] to get the current behaviour of clearing the body
       > at the start of proofs in a forward compatible way.
       > [opaque-let,deprecated-since-8.18,deprecated,default]
       > File "./order.v", line 4806, characters 0-138:
       > Error: Attribute infer.T is not supported
       >
       > make[2]: *** [Makefile.coq:838: order.vo] Error 1
       > make[2]: *** [order.vo] Deleting file 'order.glob'
       > make[1]: *** [Makefile.coq:409: all] Error 2
       > make: *** [../Makefile.common:99: this-build] Error 2
       For full logs, run 'nix-store -l /nix/store/akhd7kg8x9wqq3hapiys04wv9z2vb6cj-coq8.18-mathcomp-ssreflect-2.0.0.drv'.

So I switched to mathcomp-2.1.0 and that worked.
But mathcomp-analysis seems to not be up-to-date in the nixpkgs:

error: Package coq8.18-mathcomp2.1-mathcomp-analysis-broken in /nix/store/8pfd2imn5vkhwb1m7yqx3g2250nh3lip-source/pkgs/development/coq-modules/mathcomp-analysis/default.nix:67 is marked as broken, refusing to evaluate.

The mathcomp-analysis repository though supports mathcomp-2.X and has an updated nix setup.

Is there anything that I can do to help fix this problem?

view this post on Zulip Cyril Cohen (Jan 31 2024 at 09:30):

Mathcomp analysis 1 (for mathcomp 2) was released last week, I'm not sure anyone updated it in nixpkgs so far. @Pierre Roux do you know about that?

view this post on Zulip Pierre Roux (Jan 31 2024 at 09:31):

Could you share your .nix file? Analysis master is tested with Nix in CI and releases are tested on the CI of the nix toolbox, so I would at least expect some setting to work. WOuld be interesting to compare to your own setting.

view this post on Zulip Pierre Roux (Jan 31 2024 at 09:33):

Cyril Cohen said:

Mathcomp analysis 1 (for mathcomp 2) was released last week, I'm not sure anyone updated it in nixpkgs so far. Pierre Roux do you know about that?

Indeed, 1.0 is not yet in nixpkgs

view this post on Zulip Cyril Cohen (Jan 31 2024 at 09:34):

AFAICT nixpkgs master was not updated. @Sebastian Ertel if you have some time and want to contribute, you can add the few lines there that will make it compile.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 09:35):

(Should you accept, I can help with the process)

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 10:10):

I'm happy to do that also to get some more experience to be of better help in the future.
What are the steps?
(Fork nix-pkgs, do the update there and then ...? )

view this post on Zulip Cyril Cohen (Jan 31 2024 at 10:24):

Sure:

  1. Fork nixpkgs
  2. Make a PR including the new version descriptions
  3. You should test your change against all coq packages for serveral versions of coq using the coq-nix-toolbox. https://github.com/coq-community/coq-nix-toolbox?tab=readme-ov-file#testing-coqpackages-updates-in-nixpkgs
    you should make a reference to your nixpkgs PR in the coq-nix-toolbox one.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 10:48):

Which branch of the nix-pkgs repo do I use?
master or unstable?

view this post on Zulip Pierre Roux (Jan 31 2024 at 10:49):

I always used master.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 11:08):

Where does the sha hash for the according release come from?
(It does not seem to be the commit hash.)

view this post on Zulip Pierre Roux (Jan 31 2024 at 11:09):

The only way I ever managed to get it is let it empty, then run nix-build -A coqPackages.foo and fill it with the result of the error message.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 13:14):

I'm trying
nix-build --arg mathcomp '{ version = "2.0.0";}' -A coqPackages.mathcomp-analysis
to get the nix script to choose a specific version but that does not work.
Is that the proper way to do this?

view this post on Zulip Pierre Roux (Jan 31 2024 at 13:15):

Honestly I don't really know how to do it, usually, I temporarily edit mathcomp/default.nix so that mathcomp 2.0.0 is the default mathcomp (copy the line on top of the switch) and it works.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 13:17):

Sebastian Ertel said:

I'm trying
nix-build --arg mathcomp '{ version = "2.0.0";}' -A coqPackages.mathcomp-analysis
to get the nix script to choose a specific version but that does not work.
Is that the proper way to do this?

Looks good to me.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 13:30):

Pierre Roux schrieb:

Honestly I don't really know how to do it, usually, I temporarily edit mathcomp/default.nix so that mathcomp 2.0.0 is the default mathcomp (copy the line on top of the switch) and it works.

Indeed that did work.
(The command sadly did not.)

view this post on Zulip Cyril Cohen (Jan 31 2024 at 13:35):

right...
it would rather be:

nix-build -E 'with import ./. { }; with coqPackages_8_18.overrideScope (self: super: { mathcomp = super.mathcomp.override {version = "2.0.0";};}); mathcomp-analysis'

view this post on Zulip Cyril Cohen (Jan 31 2024 at 13:37):

well... @Pierre Roux the point of the coq-nix-toolbox ci is that you should not make this up by hand...

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 13:48):

The coq-nix-toolbox repo states a more convenient way of writing this:
--arg override '{mathcomp="2.0.0"}'
Is this by means of the coq-nix-toolbox itself or this just a hint?

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 13:50):

I opened the nixpkgs PR here: https://github.com/NixOS/nixpkgs/pull/285276

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 13:52):

And sorry for the typo in the commit message. Of course this updates to mathcomp-analysis 1.0.0

view this post on Zulip Théo Zimmermann (Jan 31 2024 at 14:38):

The shorter and convenient way indeed requires going through the Coq Nix Toolbox.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 14:47):

On the coq-nix-toolbox website, I have trouble to find the information of just how I would use it.
Can you give me a pointer?

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:09):

Cyril Cohen said:

  1. You should test your change against all coq packages for serveral versions of coq using the coq-nix-toolbox. https://github.com/coq-community/coq-nix-toolbox?tab=readme-ov-file#testing-coqpackages-updates-in-nixpkgs
    you should make a reference to your nixpkgs PR in the coq-nix-toolbox one.

:up: could you make feedback on how this does not help you?

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:11):

BTW concerning NixOS/nixpkgs#285276 please never put a merge commit in your PRs, do rebase (e.g. git pull -r upstream master) instead.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 15:11):

I created the draft pull request on coq-nix-toolbox: https://github.com/coq-community/coq-nix-toolbox/pull/200

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:14):

Sebastian Ertel said:

I created the draft pull request on coq-nix-toolbox: https://github.com/coq-community/coq-nix-toolbox/pull/200

You probably forgot to commit the generated new .github/workflowsstuff in the latter PR.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 15:14):

Cyril Cohen schrieb:

Cyril Cohen said:

  1. You should test your change against all coq packages for serveral versions of coq using the coq-nix-toolbox. https://github.com/coq-community/coq-nix-toolbox?tab=readme-ov-file#testing-coqpackages-updates-in-nixpkgs
    you should make a reference to your nixpkgs PR in the coq-nix-toolbox one.

:up: could you make feedback on how this does not help you?

I was actually referring to what @Théo Zimmermann said.
To make this more precise: I do not understand how to use/install(?) the coq-nix-toolbox such that I can issue
nix-build --arg override '{mathcomp="2.0.0"}' -A coqPackages.mathcomp-analysis
at the command line.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:16):

Sebastian Ertel said:

Cyril Cohen schrieb:

Cyril Cohen said:

  1. You should test your change against all coq packages for serveral versions of coq using the coq-nix-toolbox. https://github.com/coq-community/coq-nix-toolbox?tab=readme-ov-file#testing-coqpackages-updates-in-nixpkgs
    you should make a reference to your nixpkgs PR in the coq-nix-toolbox one.

:up: could you make feedback on how this does not help you?

I was actually referring to what Théo Zimmermann said.
To make this more precise: I do not understand how to use/install(?) the coq-nix-toolbox such that I can issue
nix-build --arg override '{mathcomp="2.0.0"}' -A coqPackages.mathcomp-analysis
at the command line.

Ah right! You can do it from any worktree containing a checkout of the coq-nix-toolbox and from any worktree that uses the toolbox (e.g. via the initialization command)

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:16):

For example from your own PR coq-community/coq-nix-toolbox#200 you can do it.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 15:17):

I see. Thanks a lot for clarifying this.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 15:19):

Cyril Cohen schrieb:

Sebastian Ertel said:

I created the draft pull request on coq-nix-toolbox: https://github.com/coq-community/coq-nix-toolbox/pull/200

You probably forgot to commit the generated new .github/workflowsstuff in the latter PR.

That I do not understand. The commit has the changes to the .github/workflows folder as far as I can see. Can you please clarify?

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:20):

Nevermind I was looking at the wrong PR... It's fine.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:21):

Cyril Cohen said:

Sebastian Ertel said:

Cyril Cohen schrieb:

Cyril Cohen said:

  1. You should test your change against all coq packages for serveral versions of coq using the coq-nix-toolbox. https://github.com/coq-community/coq-nix-toolbox?tab=readme-ov-file#testing-coqpackages-updates-in-nixpkgs
    you should make a reference to your nixpkgs PR in the coq-nix-toolbox one.

:up: could you make feedback on how this does not help you?

I was actually referring to what Théo Zimmermann said.
To make this more precise: I do not understand how to use/install(?) the coq-nix-toolbox such that I can issue
nix-build --arg override '{mathcomp="2.0.0"}' -A coqPackages.mathcomp-analysis
at the command line.

Ah right! You can do it from any worktree containing a checkout of the coq-nix-toolbox and from any worktree that uses the toolbox (e.g. via the initialization command)

In this instance, the command would be
nix-build --arg override '{mathcomp="2.0.0";}' --argstr job mathcomp-analysis

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:23):

Another "PR styling comment", it is a good practice not to push a new branch from your own fork's master branch, one should name the branch instead. (This leads to less accidental undesirable side effects in the middle to long run)

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 15:26):

With respect to the use of the coq-nix-toolbox, I see now.
One has to initialize the nix setup for the repo in the coq-nix-toolbox style. Got it.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 15:27):

In my case, I was running the command in the nixpkgs repo which would have not worked.
I suppose that is why it is good practice to have the default.nix to be populated in the nixpkgs repo also in the .nix folder of the local repo.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:28):

Sebastian Ertel said:

In my case, I was running the command in the nixpkgs repo which would have not worked.
I suppose that is why it is good practice to have the default.nix to be populated in the nixpkgs repo also in the .nix folder of the local repo.

Having a local copy of the default.nix from a package is not necessary if it does not require an update compared to the one in nixpkgs.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:29):

You can see it mostly as a staging area

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 15:30):

But then I would not be able to use the coq-nix-toolbox unless I clone into the repo.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 15:32):

Sebastian Ertel said:

But then I would not be able to use the coq-nix-toolbox unless I clone into the repo.

I am not sure I understand. The local packages' default.nix are useful while waiting for their integration in upstream nixpkgs.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 15:41):

I rephrase this then:
Say I have a local repo nixpkgs. In this repo on the command line, I would like to use the coq-nix-toolbox (for example to get the convenient command mentioned above).
What would I need to do?

view this post on Zulip Cyril Cohen (Jan 31 2024 at 16:02):

Ah ok... you can do exactly what you did: push a branch on github and do updateNixPkgs yourgithubuser yourbranch

view this post on Zulip Cyril Cohen (Jan 31 2024 at 16:03):

Actually knowing the internals you do not even need to push to github, but I did not advertize this... Maybe I could implement a shortcut for this exact usecase.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 16:03):

My priority is to switch to flakes and I do not even have the time for that though...

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 16:15):

I do use flakes for all my Coq projects and it would be great to have more flakes support.

view this post on Zulip Sebastian Ertel (Jan 31 2024 at 16:15):

Let me know if I can be of any help with this.

view this post on Zulip Cyril Cohen (Jan 31 2024 at 18:20):

That would be great! Let's discuss that in another thread though.

view this post on Zulip Sebastian Ertel (Feb 01 2024 at 08:23):

Sure.

view this post on Zulip Sebastian Ertel (Feb 01 2024 at 16:13):

I'm having trouble specifying the requirements for mathcomp-infotheo version 0.6.0. Starting from the version it requires an additional dependency for hierarchy-builder.

I have seen the patching pattern from mathcomp and used it there too but I get an error: infinite recursion encountered that I have trouble chasing down.

Also mathcomp-infotheo version 0.6.0 actually only works for hierarchy-builder version 1.5.0. So I need to specify this version as well in a patch I suppose.

view this post on Zulip Pierre Roux (Feb 01 2024 at 16:17):

hierarchy-builder is already a dependency of analysis so you shouldn't have to do anything specific about it I guess.
For the specific version of hierarchy-builder, I guess an argument can be added to the version switch, like for mathcomp 1/2.

view this post on Zulip Sebastian Ertel (Feb 01 2024 at 16:19):

But what version would I define for versions of mathcomp-infotheo that did not yet have that dependency? The first version of hb?

view this post on Zulip Sebastian Ertel (Feb 01 2024 at 16:20):

At least I do not see such a pattern being defined for mathcomp.

view this post on Zulip Sebastian Ertel (Feb 01 2024 at 16:23):

mathcomp-analysis also does not state any specific version restrictions on hierarchy-builder. But mathcomp-infotheo does. That means mathcomp-infotheo does not only inherit the hb dependency from mathcomp-analysis but uses a dedicated version which is also stated in the release notes: https://github.com/affeldt-aist/infotheo/releases/tag/0.6.0

view this post on Zulip Pierre Roux (Feb 01 2024 at 16:33):

Here is an example https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix#L11 I guess one could replace mathcompalgebra with hierarchy-builder to enforce the constraint on HB version (of course the package will only be buildable when specifying that specific version for hierarchy-builder).

view this post on Zulip Pierre Roux (Feb 01 2024 at 16:34):

That being said, I'd tend to think that adding those versions of infotheo with very specific restrictions on HB is probably not worth it. Probably better wait for future versions without such constraints.

view this post on Zulip Sebastian Ertel (Feb 01 2024 at 17:26):

I second that.

view this post on Zulip Sebastian Ertel (Feb 02 2024 at 13:00):

So the CI for my PR still fails because of caching issues in github.
The workflow still contains the actions for infotheo:
https://github.com/coq-community/coq-nix-toolbox/actions/runs/7746994691/workflow?pr=200
But it also points to this latest commit where I clearly dropped them:
https://github.com/coq-community/coq-nix-toolbox/commit/ea4266ae9e0ad50a52ba5132a59fc1b666344992
I could not see that the workflow for coq-nix-toolbox uses any github caches. Is that so?

view this post on Zulip Pierre Roux (Feb 02 2024 at 13:36):

For some security reasons, there are two kind of jobs: pull_request and pull_request_target, when there is a pull_request, the corresponding pull_request_target should simply be ignored. Here the pull_request jobs were not run probably because of the conflict on the .nix/nixpkgs.nix file. I solved the conflict and force pushed (BTW, please don't name your PR branches master) and they seem to be running now.

view this post on Zulip Reynald Affeldt (Feb 04 2024 at 08:47):

Pierre Roux said:

That being said, I'd tend to think that adding those versions of infotheo with very specific restrictions on HB is probably not worth it. Probably better wait for future versions without such constraints.

We've tagged and released a 0.6.1 version that does not force HB to be 1.5.0 (only greater than or equal). It has been submitted to opam at the time of this writing.

view this post on Zulip Reynald Affeldt (Feb 04 2024 at 10:11):

(opam PR failing though: https://github.com/coq/opam/pull/2953...)

view this post on Zulip Sebastian Ertel (Feb 04 2024 at 13:32):

@Reynald Affeldt , that is great and I would happily add that to the current update.

Yet the relaxed constraints as requested by @Vincent Laporte do not work: https://github.com/coq-community/coq-nix-toolbox/actions/runs/7765932923/job/21182209019
Not having an upper bound on mathcomp-analysis is essentially saying that infotheo also compiles with mathcomp-analysis version 1.0.0. But mathcomp-analysis version 1.0.0 depends on mathcomp version 2.X which has breaking changes (here, the removal of EqMixin).
But the latest release 0.6.1 of infotheo does not have that support.

So really all that would work is to put the upper bound tomathcomp-analysis version 0.7.0 and output infotheo version 0.6.1.
(This worked: https://github.com/coq-community/coq-nix-toolbox/pull/200)
Would that be ok for you?

view this post on Zulip Reynald Affeldt (Feb 04 2024 at 13:38):

in the opam file of infotheo, we set the versions of mathcomp-analysis to be coq-mathcomp-analysis" { (>= "0.6.6") & (< "0.8~")} because maybe we'll have some 0.7.X versions of mathcomp-analysis with minimal changes in the near future

view this post on Zulip Reynald Affeldt (Feb 04 2024 at 13:39):

but yes setting the upper bound of mathcomp-analysis to be 0.7.X looks perfectly fine and even desirable

view this post on Zulip Sebastian Ertel (Feb 06 2024 at 20:29):

I'm trying to understand why the last CI run failed. In particular, I would like to understand why the scripts in coq-nix-toolbox decided to run infotheo with the mathcomp-2 bundles even though I specified no such version configuration. (mathcomp-analysis uses mathcomp-2 only starting with version 1.0.0.)

But I do have a hard time getting into all the scripts of the coq-nix-toolbox. Can somebody please point me to the place in the code where this decision is made?
(I assume it happens somewhere in deps.nix.)

view this post on Zulip Théo Zimmermann (Feb 22 2024 at 14:54):

Most of the logic for choosing which version is built is in nixpkgs, not in the Coq Nix Toolbox (cf. defaultVersion mechanisms). The Coq Nix Toolbox config files only contain a small amount of overrides (typically mostly the Coq version, and sometimes also the MathComp version, sometimes more if the defaults are not working).


Last updated: May 25 2024 at 21:01 UTC