Has opam been updated wrt to PR 230 (https://github.com/math-comp/analysis/pull/230) ? @Théo Vignon is working on Banach-Steinhauss Theorem from the opam distribution of MathComp Analaysis and may have encountered a problem related to that.
I would say no because it was merged 22 days ago and the last release is 28 days ago.
Why isn't he working in math-comp/analysis?
He installed mathcomp-analysis through opam, what is the issue with that ? I'm not using opam so I would probably create errors while updating it.
if he wants a bleeding edge coq-mathcomp-analysis
via opam, he needs to add the extra-dev
opam repo and install coq-mathcomp-analysis.dev
. Otherwise, the content will be limited to the last release. With the dev
version, it builds from the GitHub repo, which will have all changes at the time of the build.
thanks @Karl Palmskog !
ah, it looks like the dev
OPAM version is not fully up to date: https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.dev/opam - perhaps you can refresh it from the one in the analysis repo @affeldt-aist ?
in the meantime, it's also a possibility to install the opam package that lives in the analysis repo:
git checkout <mathcomp/analysis>
cd analysis
opam pin add coq-mathcomp-analysis . -k path
Marie Kerjean said:
He installed mathcomp-analysis through opam, what is the issue with that ? I'm not using opam so I would probably create errors while updating it.
If he is going to contribute with classic analysis results, I'd rather see it integrated more tightly to mathcomp analysis, rather than depending in it. Moreover it would be more practical if his work requires extending the library.
Thanks for your help, I have been able to install the last version of mathcomp-analysis. I just needed to adapt the command a little bit. I didn't need the first one, I thinks this is because I only download nathcomp-analysis and not mathcomp. And in the opam command, the path
was't working for me, but with the auto
option the command work.
Last updated: Feb 05 2023 at 07:03 UTC