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
).
E.g. the doc of analysis is here: https://math-comp.github.io/analysis/
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.
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?
Sure for the numbering. I was planning to follow the same organization of directory.
\
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
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/.
The main developer is @YOSHIHIRO Imai
if you plan to make this into a "real" tool, maybe a good idea to rename it to distinguish from coq2html, e.g., ssr2html?
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
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?
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.
You need to regenerate the actions after the update by doing nix-shell --arg do-nothing true --run "genNixActions"
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
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
Which PR are you using?
Cyril Cohen said:
Which PR are you using?
https://github.com/math-comp/Coq-Combi/pull/8
yes you should commit the new github actions files and remove the old ones
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.
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 ?
Yes, because you removed: .nix/coq-overlays/coq-combi/default.nix
as well, which was describing the dependencies
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.
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 ?
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.
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.
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...
@Cyril Cohen I mistakely asked you to review my pull request on github. Sorry !
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 ?
You forgot to regenerate the github actions after the last fix I suggested
Cyril Cohen said:
Thanks ! I just did. Hopefully this will work now !
Florent Hivert said:
Cyril Cohen said:
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.
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
Which version of mathcomp are you running?
Cyril Cohen said:
Which version of mathcomp are you running?
2.1.0
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
I'm not sure what I need to write. Is it just hierarchy-builder
?
You should also make sure mathcomp 2.1.0 is used by adding an override here:
coqPackages.mathcomp.override.version = "2.1.0";
The test are now properly running !!! Thanks.
Florent Hivert said:
The test are now properly running !!! Thanks.
Thanks a lot and good night !
Last updated: Oct 13 2024 at 01:02 UTC