Marie Kerjean (Jul 09 2020 at 08:52): Marie Kerjean (Jul 09 2020 at 08:52):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.
Reynald Affeldt (Jul 09 2020 at 10:13):I would say no because it was merged 22 days ago and the last release is 28 days ago.
Cyril Cohen (Jul 09 2020 at 11:37):Why isn't he working in math-comp/analysis?
Marie Kerjean (Jul 09 2020 at 12:39):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.
Karl Palmskog (Jul 09 2020 at 12:41):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.
Marie Kerjean (Jul 09 2020 at 13:11):thanks @Karl Palmskog !
Karl Palmskog (Jul 09 2020 at 13:13):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 ?
Karl Palmskog (Jul 09 2020 at 13:16):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.
Théo Vignon (Jul 10 2020 at 15:10):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