Closed brando90 closed 2 years ago
Zimmi48
commented
2 years ago For the record, the relevant part from the Platform issue tracker is the last one (which shows the result of running the Platform scripts). I expect the previous attempts (without the Platform) should have not any impact on the results of running the Platform scripts.
MSoegtropIMC
commented
2 years ago Indeed Coq Platform creates a new switch, so whatever you did before doesn't (or shouldn't) matter.
The "dev" variant of Coq Platform is for obvious reasons not guaranteed to work. This is "best effort" and I would say you get a reasonable collection of dev packages. That coq-interval.dev doesn't work is known. Please report on results for one of the supported release variants.
Also note that M1 is not fully supported as yet - as it looks z3 does not compile on M1. We will do our best to work with you getting this fixed, but dues to lack of CI support this can't be guaranteed either.
brando90
commented
2 years ago seems this fixed it?
(base) brandomiranda~/Downloads/platform-2022.01.0 β― eval $(opam env)
(base) brandomiranda~/Downloads/platform-2022.01.0 β― coqc -v
The Coq Proof Assistant, version 8.16+alpha
compiled with OCaml 4.10.2Indeed Coq Platform creates a new switch, so whatever you did before doesn't (or shouldn't) matter.
The "dev" variant of Coq Platform is for obvious reasons not guaranteed to work. This is "best effort" and I would say you get a reasonable collection of dev packages. That coq-interval.dev doesn't work is known. Please report on results for one of the supported release variants.
Also note that M1 is not fully supported as yet - as it looks z3 does not compile on M1. We will do our best to work with you getting this fixed, but dues to lack of CI support this can't be guaranteed either.
how do I install a non dev version? wonder why a dev installed in the first place...
Zimmi48
commented
2 years ago how do I install a non dev version? wonder why a dev installed in the first place...
The script is supposed to be interactive and is supposed to ask you what version you want at some point. The default is supposed to be 8.14.
MSoegtropIMC
commented
2 years ago Well there is not really a default. The second screen of coq_platform_make.sh is:
The Coq Platform allows to install the latest release version of Coq, but also
older or development versions of Coq. Besides the Coq version, you can choose
a 'package pick', that is a selection of specific versions of Coq libraries,
plugins and tools. For some versions of Coq several package picks are available.
Package picks with the same release date for different Coq versions are made
as compatible as possible.
You can install several versions of Coq in parallel, which simplifies porting of
developments. You can use "opam switch" to switch between Coq versions.
The following Coq versions and package picks are available:
(1): Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022
(2): Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022
(3): Coq 8.13.2 (released Apr 2021) with an extended package pick from Sep 2021
(4): Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
(5): Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
(6): Coq 8.15.0 (released Jan 2022) with a beta package pick
(7): Coq dev (latest master of all packages)
Please select a package pick by entering the number shown at the begin of a line.
========================= SELECT PACKAGE_PICK VERSION ==========================
Select package list (number in 1..7, c=cancel)You did select 7 here, but you should select 1 (or maybe 6).
MSoegtropIMC
commented
2 years ago I guess I should change the (dev) line to:
(7): Coq dev (latest master of all packages - frequently does not fully compile)Can we also separate more clearly the recommended package sets from the compatibility ones and the preview ones (like we do in the release notes)?
Another idea is that maybe it shouldn't be as easy to select a preview set than it is to select a recommended set (e.g., require the user to confirm afterward).
brando90
commented
2 years ago I suppose I did select 7. I didn't know it was going to bring issues (not sure why it is or if thats the issue). Will try option 1 right now. I do suggest to make it as automatic to the user and friendly as possible :)
brando90
commented
2 years ago I am basing my actions on this btw: https://github.com/coq/platform/blob/main/doc/README_macOS.md
Zimmi48
commented
2 years ago So the issue with dev is twofold: for you as a user, you get a version that's less stable, and this is why interval has failed. Trying option 1 is indeed a good idea to get a more stable version and fewer errors.
Unfortunately, it's likely that you will still get errors in the build of z3 and cairo because these are unrelated to the choice of option. They are probably related to the M1 platform.
This comment was saying that the Platform was working on M1 though, was this before adding the z3 package somehow? What could be different between @brando90's environment and @k4rtik's previous tests?
brando90
commented
2 years ago So the issue with dev is twofold: for you as a user, you get a version that's less stable, and this is why interval has failed. Trying option 1 is indeed a good idea to get a more stable version and fewer errors.
Unfortunately, it's likely that you will still get errors in the build of z3 and cairo because these are unrelated to the choice of option. They are probably related to the M1 platform.
This comment was saying that the Platform was working on M1 though, was this before adding the z3 package somehow? What could be different between @brando90's environment and @k4rtik's previous tests?
the install worked but I am unable to use coqide (or the coq plataform did not install it for me). See output:
(base) brandomiranda~/Downloads/platform-2022.01.0 β― coqc -v
The Coq Proof Assistant, version 8.14.1
compiled with OCaml 4.10.2
(base) brandomiranda~/Downloads/platform-2022.01.0 β― coqide
zsh: command not found: coqidehow do I proceed?
brando90
commented
2 years ago ok it does fail:
(base) brandomiranda~/Downloads/platform-2022.01.0 β― opam pin coqide 8.14.1
coqide is now pinned to version 8.14.1
[WARNING] Opam package conf-python-3.9.0.0 depends on the following system package that can no longer be found: python@3
The following actions will be performed:
β install cairo2 0.6.2 [required by lablgtk3]
β install lablgtk3 3.1.2 [required by lablgtk3-sourceview3]
β install lablgtk3-sourceview3 3.1.2 [required by coqide]
β install coqide 8.14.1*
===== β 4 =====
Do you want to continue? [Y/n] y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> π«
β¬ retrieved cairo2.0.6.2 (cached)
Processing 4/12:
β¬ retrieved lablgtk3-sourceview3.3.1.2 (cached)
β¬ retrieved lablgtk3.3.1.2 (cached)
β¬ retrieved coqide.8.14.1 (cached)
[ERROR] The compilation of cairo2.0.6.2 failed at "dune build -p cairo2 -j 16".
#=== ERROR while compiling cairo2.0.6.2 =======================================#
# context 2.1.2 | macos/arm64 | ocaml-base-compiler.4.10.2 | https://opam.ocaml.org#ae76a8bc
# path ~/.opam/__coq-platform.2022.01.0~8.14~2022.01/.opam-switch/build/cairo2.0.6.2
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p cairo2 -j 16
# exit-code 1
# env-file ~/.opam/log/cairo2-50542-6e01f7.env
# output-file ~/.opam/log/cairo2-50542-6e01f7.out
### output ###
# ocamlmklib src/dllcairo_stubs.so,src/libcairo_stubs.a (exit 2)
# (cd _build/default && /Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.14~2022.01/bin/ocamlmklib.opt -g -o src/cairo_stubs src/cairo_stubs.o -L/opt/homebrew/opt/freetype/lib -lfreetype -L/opt/homebrew/Cellar/fontconfig/2.13.1/lib -L/opt/homebrew/opt/freetype/lib -lfontconfig -lfreetype -L/opt/homebrew/Cellar/cairo/1.16.0_5/lib -lcairo)
# ld: in '/usr/local/lib/libpng16.16.dylib', building for macOS-arm64 but attempting to link with file built for macOS-x86_64
# clang: error: linker command failed with exit code 1 (use -v to see invocation)
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> π«
ββ The following actions failed
β Ξ» build cairo2 0.6.2
ββ
βΆβ No changes have been performed
<><> cairo2.0.6.2 troubleshooting <><><><><><><><><><><><><><><><><><><><><> π«
=> Try to re-run the install command with PKG_CONFIG_PATH pointing a pkg-config path including libffi, e.g. if you use homebrew you can try
PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig
[NOTE] Pinning command successful, but your installed packages may be out of sync.I was previously able to use the coqide by installing the dmg but then there were two version of coq going on and the coqide seemed to bechave strangely...afaik...so dorcing it via the dmg and the coq plataform at the same time seems like a bad idea...
MSoegtropIMC
commented
2 years ago @brando90 : do you use Homebrew or Macports?
brando90
commented
2 years ago yes, brew
MSoegtropIMC
commented
2 years ago Try Macports. The issue building for macOS-arm64 but attempting to link with file built for macOS-x86_64 you see is definitely an issue of the system package manager you use.
brando90
commented
2 years ago Try Macports. The issue
building for macOS-arm64 but attempting to link with file built for macOS-x86_64you see is definitely an issue of the system package manager you use.
what do I try? Do you have a command?
MSoegtropIMC
commented
2 years ago Uninstall Homebrew (or somehow hide it) and install MacPorts.
brando90
commented
2 years ago I'm confused, do you want me to try this: https://github.com/coq/platform/blob/main/doc/README_macOS.md#installing
Installing For MacPorts installation follow the instructions at (https://www.macports.org/install.php) - that is download the installer package matching our OS version and double click on the downloaded package.
For homebrew installation instructions see (https://brew.sh/index) - we followed the recommended approach /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)" using the default location - see the next section on a discussion if this is safe.
MSoegtropIMC
commented
2 years ago Having both will likely result in quite a mess unless you know exactly what you are doing, so I would uninstall Homebrew.
brando90
commented
2 years ago Having both will likely result in quite a mess unless you know exactly what you are doing, so I would uninstall Homebrew.
but I use brew all the time. I don't really want to uninstall it...
brando90
commented
2 years ago even if I did I am unsure what the goal is. Is what we are trying to install is coq or the coqide? or both?
I'm also happy to return using my emacs setup or vscode...
Zimmi48
commented
2 years ago If you are happy with Emacs or VsCode, this is indeed a simpler and safer option for you.
MSoegtropIMC
commented
2 years ago Well then you have to fix it. It apparently installs Intel binaries on yor ARM machine which is no good.
Coqide needs much more dependencies than coq itself. If you don't need CoqIDE, you can just ignore the errors you get from installing it. Nothing else in the Coq Platform depends on it.
brando90
commented
2 years ago Thank you! I appreciate the help :)
Will try this later and report what I did (in case it's useful for folks in the future that come across this issue)
brando90
commented
2 years ago Well then you have to fix it. It apparently installs Intel binaries on yor ARM machine which is no good.
Out of curiosity, what does brew have to do with this? I've never ran a brew command in this entire discussion. Unless the coq plataform binaries run it for me. I did run:
bash coq_platform_make.shCoqide needs much more dependencies than coq itself. If you don't need CoqIDE, you can just ignore the errors you get from installing it. Nothing else in the Coq Platform depends on it.
@MSoegtropIMC
brando90
commented
2 years ago @Zimmi48 btw, I am puzzled. There is a Rossetta thing that translates between intel and m1 binaries. Why is coq or coqide inable to use them? Or the installation process? Should that not be supported by coq? My guess is that it shouldn't be to hard.
MSoegtropIMC
commented
2 years ago @brando90 : CoqPlatform uses opam and opam uses either Homebrew or MacPorts to install its system packages. You can see these when you run opam list. The packages which install Homebrew or Macports packages start with conf-.
It is a feature that you don't have to take care of this - it is actually quite complicated and it is a great feature of opam to handle this in a system independent way. It was a good part of the work of implementing Coq Platform to fix opam conf packages on all supported platforms.
You should see the system package installation in your first run of coq_platform_make.sh in a section where it says it is running depext. You won't see much of this in consecutive runs since the packages are then already installed.
And as I said, homebrew obviously installs bad packages - which is the source of your problems.
MSoegtropIMC
commented
2 years ago There is a Rossetta thing that translates between intel and m1 binaries. Why is coq or coqide inable to use them?
This works for complete executables, but not for libraries.
You could install an x86 opam and compile everything for x86, but then everything will be much slower.
MSoegtropIMC
commented
2 years ago It shouldn't be that difficult to fix the broken brew file, btw., but as MacPorts user I can't help much with that. M1 is quite new and I think it is normal that not all brew files work properly on M1 as yet.
MSoegtropIMC
commented
2 years ago MacPorts has btw. a declarative package file format - similar to opam - which makes it easier to handle such things. Afaik brew packages can contain unrestricted python (?) code, which makes it much harder to so something like a x86 to arm migration.
MSoegtropIMC
commented
2 years ago @brando90 : Are there any news about this? Did you manage to get things running? Can you give some hints for future M1 users?
brando90
commented
2 years ago @brando90 : Are there any news about this? Did you manage to get things running? Can you give some hints for future M1 users?
Hi @MSoegtropIMC, I'm not sure what to say. I can't remember right now what I did exactly. But from memory I just followed the coq plataform install scripts and I think it worked. Let me print the current versions of coq and opam switches I have in case it is useful for future m1 users:
(meta_learning) brandomiranda~β― coqc -v
The Coq Proof Assistant, version 8.15.0
compiled with OCaml 4.10.2
(meta_learning) brandomiranda~ β― opam switch list
# switch compiler description
4.05.0 ocaml-base-compiler.4.05.0 4.05.0
4.06.0 ocaml-base-compiler.4.06.0 4.06.0
4.07.0 4.07.0
4.12.0 ocaml-base-compiler.4.12.0 4.12.0
__coq-platform.2022.01.0~8.14~2022.01 ocaml-base-compiler.4.10.2 __coq-platform.2022.01.0~8.14~2022.01
β __coq-platform.2022.01.0~8.15~beta1 ocaml-base-compiler.4.10.2 __coq-platform.2022.01.0~8.15~beta1
__coq-platform.2022.01.0~dev ocaml-base-compiler.4.10.2 __coq-platform.2022.01.0~dev
default ocaml-system.4.07.0 default
hammer_switch ocaml-base-compiler.4.12.0 hammer_switchActually I just saw my answer in stack overflow, let me copy the link to it:
https://stackoverflow.com/a/71146080/1601580
I think that is what people should use as a reference. Happy to re-open it if there is something worth discussing but since the answer I wrote there worked for me now that should be a good answer for this too.
MSoegtropIMC
commented
2 years ago @brando90 : OK, if this information did help you and the official documentation did not, then we need to work on it.
Out of curiosity: did you come across this documentation:
https://github.com/coq/platform/blob/main/doc/README_Linux.md
If yes I guess the introductory lines stating that beginners should use snap got you on the wrong path (snap is way wrong on gentoo because afaik it does not officially support snap, so using the scripts is much easier than doing all the hacks required to get snap running on gentoo.
If no - can you recap what your documentation entry / reading path was?
My apologies that we obviously put you an an entirely wrong path.
MSoegtropIMC
commented
2 years ago P.S. I reopened this to make sure we update the docs.
Zimmi48
commented
2 years ago @MSoegtropIMC
If yes I guess the introductory lines stating that beginners should use snap got you on the wrong path (snap is way wrong on gentoo because afaik it does not officially support snap, so using the scripts is much easier than doing all the hacks required to get snap running on gentoo.
You seem to be confusing two different issues: this one is not about Gentoo, it is about macOS with M1 hardware.
From what I remember from this issue, the main problem was that when you switch macOS machines, Apple will sync your files for you, including your opam root, which may be a problem if you are switching from Intel to Apple processors. Once the opam root was removed, just following the documented scripts worked (and not forgetting about eval $(opam env)).
MSoegtropIMC
commented
2 years ago @Zimmi48 : ah yes, sorry - too much switching hence and forth between issues.
So I guess this can be solved by noting in the Mac docs that one switching between Intel/Apple silicon one has to be careful to not copy opam root.
brando90
commented
2 years ago Hi @MSoegtropIMC !
I think what got me in the wrong path is the terminal instructions is a rather long document + it says "source" but it doesn't feel it was from source from installing from source in other experiences I've had.
I do think ppl have to be careful with restoring from a time machine when moving to an m1 cuz the time machine doesn't know the cpu chip is new which causes a bunch of issues. Can't remember which were related with coq.
In my ideal mac install I'd run 1 command (like I do for pytorch) and it would just work.
Hope my feedback helps. :)
MSoegtropIMC
commented
2 years ago but it doesn't feel it was from source from installing from source in other experiences I've had.
I don't understand this statement. Opam does compile everything from sources - that's the reason it takes an hour. How does this not meet your expectations?
In my ideal mac install I'd run 1 command
Well isn't that how it is? OK the scripts asks a few questions, but it should hardly take more than 1 minute to answer them.
brando90
commented
2 years ago but it doesn't feel it was from source from installing from source in other experiences I've had.
I don't understand this statement. Opam does compile everything from sources - that's the reason it takes an hour. How does this not meet your expectations?
In my ideal mac install I'd run 1 command
Well isn't that how it is? OK the scripts asks a few questions, but it should hardly take more than 1 minute to answer them.
Like when I tried installing coq from homebrew which is the intuitive way to install things on mac -- it didn't work if I remember.
Finding the instruction to downloading the install script took some effort to do that I think I only found after other nice ppl (like yourself) helped me with.
I'd hate to lie accidentally, but it feels like I did try the single command in opam but my feeling is if that worked, then I likely wouldn't have resorted to the coq plataform install scripts.
Perhaps having a homebrew/opam run that plataform tool for us be the way to go?
I really hope my feedback helps. Not sure if it is but I'm happy to help if I can.
MSoegtropIMC
commented
2 years ago it feels like I did try the single command in opam
As @Zimmi48 said the issue here was that you got your .opam folder copied over from an Intel machine automatically. This is the reason for the obscure library errors. This killed opam on M1. I guess the best way to mitigate that is to have a sanity check in opam which detects this - I will create a ticket.
I think the docs we control are fine now: If I google "install Coq" the first hit brings me to:
which immediately links to here:
https://github.com/coq/platform
which for Mac links to here:
https://github.com/coq/platform/blob/main/doc/README_macOS.md
I updated these instructions to tell M1 useres to not try the installer and also put in a note that one should take care of the .opam folder.
Regarding a Coq Platform Homebrew package: this is likely infeasible for more than one reason. First it is much to big and would likely kill Homebrew's build servers, but then it would also be quite a bit of maintenance effort. But one could give it a try.
brando90
commented
2 years ago @Zimmi48 what is wrong with the following method of installation? (note I need to install it in an HPC automatically):
# - install opam
# brew install opam
# https://stackoverflow.com/questions/72522266/how-does-one-install-opam-with-conda-for-mac-apple-os-x
conda install -c conda-forge opam
opam init
# if doing local env? https://stackoverflow.com/questions/72522412/what-does-eval-opam-env-do-does-it-activate-a-opam-environment
#eval $(opam env)
# - install coq
# local install
#opam switch create . 4.12.1
#eval $(opam env)
#opam repo add coq-released https://coq.inria.fr/opam/released
#opam install coq
# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create 4.12.1
opam switch 4.12.1
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coqI am not quite sure why you are installing opam via conda - this looks like an unsupported detour. The recommended method for all systems is:
bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"(see https://opam.ocaml.org/doc/Install.html).
If this method and/or the system package manager methods recommended on the same page don't work, you should investigate why and fix it and/or report an issue at opam.
It might be that conda works better for you because then everything likely runs in a sanitized conda environment, but IMHO it would make more sense to find out what is wrong with your system(s) so that the recommended install methods don't work.
In my personal experience conda is nice as long as it works and quite a pain if it suddenly stops working - which is not that unlikely for a likely in the conda world rarely used package like opam.
And of course it is fine to use opam directly to install Coq especially in specialized environments and when you need only a small number of packages.
brando90
commented
1 year ago @MSoegtropIMC which compiler for ocaml do I need if I am running on m1 arm machine and want to use coq 8.10?
brando90
commented
1 year ago @Zimmi48 which compilers are available for mac m1 but when I try to instlal it fails
(iit_synthesis) brandomiranda~/proverbot9001 β― opam switch list-avialable
[ERROR] No switch list-avialable is currently installed. Did you mean 'opam switch create list-avialable'?
Installed switches are:
- coq-8.16.0
- coq-8.6.1
- __coq-platform.2022.01.0~8.15~beta1
- hammer_switch
- __coq-platform.2022.01.0~8.14~2022.01
- 4.12.0
- __coq-platform.2022.01.0~dev
- 4.07.0
- 4.06.0
- 4.05.0
- default@brando90 : Coq 8.10 is currently not supported by Coq Platform, so I don't know. I could support it, if there is a good reason, say porting an interesting package to current Coq. If you need support for Coq 8.10 or 8.11, please open an issue (with justification). It will likely take a week or 2.
I got a new machine (mac book m1, not sure if it matters) and I noticed I didn't have Coq:
So I went to the instructions to download coq (https://coq.inria.fr/opam-using.html). Some part of it seems to work:
but then when I go get and pin coq opam can't find it:
anyone know what is going on? Seems puzzling.
cross: https://coq.discourse.group/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found/1562
Getting this issue now:
also:
seems there was an error:
when running the coq plataform script:
cross: -https://coq.discourse.group/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/15 -https://stackoverflow.com/questions/71117837/how-does-one-install-a-new-version-of-coq-when-it-cannot-find-the-repositories-i
https://dependenttyp.es/classes/artifacts/6-languages.html#hack
INSTALLATION INSTRUCTIONS If you already have Coq 8.14.0 installed, you do not need to do anything. It is OK if you are on a different OCaml installation, or if you are using a different IDE for proof development. If you do not have Coq installed, though, please follow these instructions:
If you do not have opam, install it. Otherwise, if you do have opam, run opam update to fetch the latest versions of packages from the repository. Run opam switch create 4.12.0 to install OCaml 4.12.0 in a switch. Run eval $(opam env)$ to configure your environment to use that switch. Install Coq 8.14.0 by running opam pin add coq 8.14.0. Install CoqIDE---the default IDE for Coq---by running opam pin coqide 8.14.0. Run eval $(opam env)$ again to update the shell environment. Download Hello.v, the hello world file. Compile Hello.v (coqc Hello.v from the command line) to test your Coq setup. Open Hello.v in CoqIDE (coqide Hello.v from the command line), and step to the bottom to check your CoqIDE setup. Download this file, which we will work on in class.