Jason Hu (Jul 07 2022 at 18:59): Jason Hu (Jul 07 2022 at 18:59):sorry to cross post here again:
Hi,
I follow the steps here https://github.com/coq/platform/blob/2022.01.0/doc/README_macOS.md to install 8.15.2022.04 release on my Mac Pro M1. I am now able to launch CoqIDE on applications.
However, I am not able to run coqc on command line. The doc says that I need to add a path to PATH, but I expect that Coq platform somehow manages to hook up with opam and create a switch, but it is not happening. I see in the README file, https://github.com/coq/platform, it seems that indeed we can manage packages using opam. What am I missing here? opam at this moment still only contains the switches I created.
Paolo Giarrusso (Jul 07 2022 at 20:11):TLDR: if you install the Coq platform using the command-line instructions, a switch will be created. If you use the installer, it will not.
Paolo Giarrusso (Jul 07 2022 at 20:12):_however_, if all you need to run on the command line is coqc, creating a switch should not be necessary
Paolo Giarrusso (Jul 07 2022 at 20:13):I suspect the coqc binary you need is hidden in the CoqIDE-8.15.appCoq_Platform_2022.01.0.app folder (or such) inside /Applications/
Paolo Giarrusso (Jul 07 2022 at 20:13):Indeed, if you used the installer, the appropriate instructions say:
In case you want to use the installed coqc from the command line, please add the folder
/Applications/Coq_Platform_2022.01.0.app/Contents/Resources/binto yourPATH.
Paolo Giarrusso (Jul 07 2022 at 20:19):however, if you need to install extra packages with opam, you cannot use the dmg _and_ you need to use the advanced instructions (https://github.com/coq/platform/blob/2022.01.0/doc/README_macOS.md#installation-by-compiling-from-sources-using-opam). A full build with all packages should take around 30 minutes
Jason Hu (Jul 07 2022 at 21:41):thx. that makes sense. it seems that there are packages in Coq platform that are newer than opam, how come that is the case?
Paolo Giarrusso (Jul 07 2022 at 21:51):Maybe you've found a package that the platform customized? Like Linux distros, sometimes they patch packages as needed, while trying to then upstream everything. But everything is still an opam package, just on a custom repository
Paolo Giarrusso (Jul 07 2022 at 21:52):BTW, the readme you linked is from the previous release to the one you're installing, that might affect some details
Jason Hu (Jul 07 2022 at 23:34):hmm... I see. then maybe I should try to live with opam at the moment until I fully understand how coq platform works.
Karl Palmskog (Jul 07 2022 at 23:38):the set of packages and their versions in the Coq opam archive is constantly in flux. We try our best to mark compatibility for each package version, but as soon as a Platform package version is changed/upgraded, most guarantees go out the window (i.e., you will be running some combination of packages that did not receive a lot of testing)
Paolo Giarrusso (Jul 07 2022 at 23:40):IIUC, the platform installs system dependencies, creates an opam switch (with a special extra opam repo) and installs a blessed set of versions that work together (and gets them released promptly in the first place).
Karl Palmskog (Jul 07 2022 at 23:41):the "system dependencies" are installed via opam too these days I believe (opam-depext, now built into opam)
Last updated: Oct 13 2024 at 01:02 UTC