Stream: math-comp devs

Topic: Port of Coq-Combi to mathcomp 2


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

Florent Hivert said:

Hi there ! I'm happy to report that I finished porting Coq-Combi to MathComp 2 ! I realized that since the repo was transfered to the Math-Comp organization, the documentation is broken. I'd like to fix it before making a release.

My question is the following: It seem to me natural to have the doc hosted in a subdirectory of https://math-comp.github.io/ If this is Ok with you, I can draft a pull request. I can also host it in my personal github.io if you prefer.
Is there a Math-Comp organization policy for that ?

Sure all mathcomp projects are welcome to have their doc in the main math-comp.github.io website.
However before a doc is posted, I would root for a release (with tag with format x.y.z, prefixed or not by v).

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

E.g. the doc of analysis is here: https://math-comp.github.io/analysis/

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

Note that @Reynald Affeldt and his coworkers are working on an alternative documentation tool that is currently beta(?)-tested on analysis, you might be interested if you are either of an early adopter or if you are interested in contributing.

view this post on Zulip Cyril Cohen (Jan 05 2024 at 15:17):

Florent Hivert said:

I've also a problem with the nix packaging:

'''
coq
Action failed with error: Error: Unable to locate executable file: cachix.
'''
But I know nothing about nix. Any pointer or help fixing this CI problem ? By the way, if not too complicated, I'd like to revive the CI which used to work a few years ago... Thanks for any help !

How can I reproduce this?

view this post on Zulip Florent Hivert (Jan 06 2024 at 03:52):

Sure for the numbering. I was planning to follow the same organization of directory.

view this post on Zulip Florent Hivert (Jan 06 2024 at 03:55):

\

Cyril Cohen said:

Florent Hivert said:

I've also a problem with the nix packaging:

'''
coq
Action failed with error: Error: Unable to locate executable file: cachix.
'''
But I know nothing about nix. Any pointer or help fixing this CI problem ? By the way, if not too complicated, I'd like to revive the CI which used to work a few years ago... Thanks for any help !

How can I reproduce this?

I got the error message when pushing to master. See https://github.com/math-comp/Coq-Combi/actions

view this post on Zulip Reynald Affeldt (Jan 09 2024 at 12:25):

Cyril Cohen said:

Note that Reynald Affeldt and his coworkers are working on an alternative documentation tool that is currently beta(?)-tested on analysis, you might be interested if you are either of an early adopter or if you are interested in contributing.

This is just a fork of coq2html that can be found here https://github.com/affeldt-aist/coq2html.
The result of processing MathComp-Analysis files can be seen here https://math-comp.github.io/analysis/htmldoc_0_6_7/.

view this post on Zulip Reynald Affeldt (Jan 09 2024 at 12:25):

The main developer is @YOSHIHIRO Imai

view this post on Zulip Karl Palmskog (Jan 09 2024 at 12:34):

if you plan to make this into a "real" tool, maybe a good idea to rename it to distinguish from coq2html, e.g., ssr2html?

view this post on Zulip Cyril Cohen (Jan 09 2024 at 12:39):

Florent Hivert said:

\

Cyril Cohen said:

Florent Hivert said:

I've also a problem with the nix packaging:

'''
coq
Action failed with error: Error: Unable to locate executable file: cachix.
'''
But I know nothing about nix. Any pointer or help fixing this CI problem ? By the way, if not too complicated, I'd like to revive the CI which used to work a few years ago... Thanks for any help !

How can I reproduce this?

I got the error message when pushing to master. See https://github.com/math-comp/Coq-Combi/actions

I think you just nee to update the toolbox:

Cf end of the "how to use" section https://github.com/coq-community/coq-nix-toolbox?tab=readme-ov-file#how-to-use

view this post on Zulip Karl Palmskog (Jan 09 2024 at 13:25):

see also https://github.com/coq/platform/issues/17 where we didn't manage to convince Xavier that adding coq2html to the Platform was a good idea, but maybe this could an option eventually for the fork?

view this post on Zulip Florent Hivert (Jan 19 2024 at 18:57):

Cyril Cohen said:

I think you just nee to update the toolbox:

Cf end of the "how to use" section https://github.com/coq-community/coq-nix-toolbox?tab=readme-ov-file#how-to-use

I tried to follow the instruction but it is still failing:

Run cachix/cachix-action@v10
  with:
    extraPullNames: coq-community, math-comp
    name: coq
  env:
    tested_commit: 9b2ca0fe70623cbe9ac36ad3b3792b4fe1e90d1b
    NIX_PATH: nixpkgs=channel:nixpkgs-unstable
Warning: The `save-state` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/
Cachix: installing
  /usr/bin/bash -c nix-env --quiet -j8 -iA cachix -f https://cachix.org/api/v1/install
Cachix: using cache coq
  Error: Action failed with error: Error: Unable to locate executable file: cachix. Please verify either the file path exists or the file can be found within a directory specified by the PATH environment variable. Also check the file mode to verify the file is executable.

view this post on Zulip Cyril Cohen (Jan 22 2024 at 09:06):

You need to regenerate the actions after the update by doing nix-shell --arg do-nothing true --run "genNixActions"

view this post on Zulip Cyril Cohen (Jan 22 2024 at 09:08):

I guess that if you ran nix-shell --arg do-nothing true --run "updateNixToolBox & genNixActions" it ran updateNixToolBox and genNixActions in parallel, didn't it? We should fix the doc

view this post on Zulip Florent Hivert (Jan 22 2024 at 09:12):

Cyril Cohen said:

You need to regenerate the actions after the update by doing nix-shell --arg do-nothing true --run "genNixActions"

I did and it didn't work. I'm reoing it. I get:

this derivation will be built:
  /nix/store/c9d3xsk43xaav6vjkd37nvnlc45vb8jk-jsonAction.drv
building '/nix/store/c9d3xsk43xaav6vjkd37nvnlc45vb8jk-jsonAction.drv'...
bash: warning: setlocale: LC_ALL: cannot change locale (fr_FR.utf8)
generating /home/florent/src/Coq/Combi/.github/workflows/nix-action-8.18.yml
bash: warning: setlocale: LC_ALL: cannot change locale (fr_FR.utf8)
/nix/store/9vafkkic27k7m4934fpawl6yip3a6k4h-bash-5.2-p21/bin/bash: warning: setlocale: LC_ALL: cannot change locale (fr_FR.utf8)

Nothing changes but I notice that 'git diff' report an untracked files named .github/workflows/nix-action-8.18.yml should I add it ?

I'm trying with it on https://github.com/math-comp/Coq-Combi/tree/Nix

view this post on Zulip Cyril Cohen (Jan 22 2024 at 09:14):

Which PR are you using?

view this post on Zulip Florent Hivert (Jan 22 2024 at 09:14):

Cyril Cohen said:

Which PR are you using?

https://github.com/math-comp/Coq-Combi/pull/8

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

yes you should commit the new github actions files and remove the old ones

view this post on Zulip Florent Hivert (Jan 22 2024 at 09:16):

Cyril Cohen said:

yes you should commit the new github actions files and remove the old ones

And apparently delete the old one ;-) Nix CI for bundle 8.15 is failling but Nix CI for bundle 8.18 is succesful on Coq and Coq-Combi is running ... Let's wait.

view this post on Zulip Florent Hivert (Jan 22 2024 at 09:18):

I now got a lot of error like

Error: Cannot find a physical path bound to logical path
mathcomp.ssreflect.ssreflect.

I guess mathcomp is not properly installed. Could you point me where an example showing me how to have it installed ?

view this post on Zulip Cyril Cohen (Jan 22 2024 at 09:20):

Yes, because you removed: .nix/coq-overlays/coq-combi/default.nix as well, which was describing the dependencies

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

Florent Hivert said:

Nix CI for bundle 8.15 is failling

Mathcomp 2 requires Coq >= 8.16 so that's expected, it should work with Coq 8.16, 8.17, 8.18 and 8.19.

view this post on Zulip Florent Hivert (Jan 22 2024 at 09:30):

Pierre Roux said:

Florent Hivert said:

Nix CI for bundle 8.15 is failling

Mathcomp 2 requires Coq >= 8.16 so that's expected, it should work with Coq 8.16, 8.17, 8.18 and 8.19.

I deleted .github/workflows/nix-action-8.15.yml but it is still lauching the checks for 8.15. How do I remove it ?

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

It's expected to still be launched as "pull_request_target" (for some security reasons) but not as "pull_request". Once the pull request will be merged it will actually disappear from subsequent pull requests. So it should just be ignored.

view this post on Zulip Florent Hivert (Jan 22 2024 at 09:35):

Pierre Roux said:

It's expected to still be launched as "pull_request_target" (for some security reasons) but not as "pull_request". Once the pull request will be merged it will actually disappear from subsequent pull requests. So it should just be ignored.

Ok thanks for the explanation.

view this post on Zulip Florent Hivert (Jan 22 2024 at 09:37):

Cyril Cohen said:

Yes, because you removed: .nix/coq-overlays/coq-combi/default.nix as well, which was describing the dependencies

I tried to re-add it (I'm not sure why it was deleted). But it doesn't fixes the problem...

view this post on Zulip Florent Hivert (Jan 22 2024 at 09:39):

@Cyril Cohen I mistakely asked you to review my pull request on github. Sorry !

view this post on Zulip Florent Hivert (Jan 22 2024 at 21:49):

Florent Hivert said:

Cyril Cohen I mistakely asked you to review my pull request on github. Sorry !

Thanks to you, nix is now working, but no test is performed. My last stupid commit https://github.com/math-comp/Coq-Combi/commit/389926250c65b0eb74257aaf0ba1a6bb5747e400 didn't raise any error. Can someone please check my Nix/CI config ?

view this post on Zulip Cyril Cohen (Jan 22 2024 at 22:36):

You forgot to regenerate the github actions after the last fix I suggested

view this post on Zulip Cyril Cohen (Jan 22 2024 at 22:38):

math-comp/Coq-Combi#10

view this post on Zulip Florent Hivert (Jan 22 2024 at 22:39):

Cyril Cohen said:

math-comp/Coq-Combi#10

Thanks ! I just did. Hopefully this will work now !

view this post on Zulip Florent Hivert (Jan 22 2024 at 22:45):

Florent Hivert said:

Cyril Cohen said:

math-comp/Coq-Combi#10

Thanks ! I just did. Hopefully this will work now !

There is still a problem : Hierachy Builder is not installed... I'm trying to fix it.

view this post on Zulip Cyril Cohen (Jan 22 2024 at 22:46):

You should add it here:
https://github.com/math-comp/Coq-Combi/blob/136f692ac92ef66c5c5b5b1ea898d0e29dbc6599/.nix/coq-overlays/coq-combi/default.nix#L12
and there:
https://github.com/math-comp/Coq-Combi/blob/136f692ac92ef66c5c5b5b1ea898d0e29dbc6599/.nix/coq-overlays/coq-combi/default.nix#L48

view this post on Zulip Cyril Cohen (Jan 22 2024 at 22:47):

Which version of mathcomp are you running?

view this post on Zulip Florent Hivert (Jan 22 2024 at 22:48):

Cyril Cohen said:

Which version of mathcomp are you running?

2.1.0

view this post on Zulip Cyril Cohen (Jan 22 2024 at 22:49):

As you can see here, https://github.com/math-comp/Coq-Combi/actions/runs/7618279276/job/20749132144?pr=10#step:10:10 mathcomp 1.18 is installed

view this post on Zulip Florent Hivert (Jan 22 2024 at 22:49):

I'm not sure what I need to write. Is it just hierarchy-builder ?

view this post on Zulip Cyril Cohen (Jan 22 2024 at 22:49):

You should also make sure mathcomp 2.1.0 is used by adding an override here:

view this post on Zulip Cyril Cohen (Jan 22 2024 at 22:50):

https://github.com/math-comp/Coq-Combi/blob/136f692ac92ef66c5c5b5b1ea898d0e29dbc6599/.nix/config.nix#L46

coqPackages.mathcomp.override.version = "2.1.0";

view this post on Zulip Florent Hivert (Jan 22 2024 at 23:07):

The test are now properly running !!! Thanks.

view this post on Zulip Florent Hivert (Jan 22 2024 at 23:08):

Florent Hivert said:

The test are now properly running !!! Thanks.

Thanks a lot and good night !


Last updated: Jul 23 2024 at 21:01 UTC