sorry to cross post here again:
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.
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.
_however_, if all you need to run on the command line is
coqc, creating a switch should not be necessary
I suspect the
coqc binary you need is hidden in the
Coq_Platform_2022.01.0.app folder (or such) inside
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
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
thx. that makes sense. it seems that there are packages in Coq platform that are newer than opam, how come that is the case?
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
BTW, the readme you linked is from the previous release to the one you're installing, that might affect some details
hmm... I see. then maybe I should try to live with opam at the moment until I fully understand how coq platform works.
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)
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).
the "system dependencies" are installed via opam too these days I believe (opam-depext, now built into opam)
Last updated: Oct 01 2023 at 18:01 UTC