The Coq mailing list

[Michael Soegtrop <MSoegtrop AT yahoo.de>]

Hello David

> Yes thank you but in fact it was after the coq-platform script failed 
that I tried to install flocq individually.

OK, then we should try to get this fixed - that's the point of alpha and 
beta releases. A few questions:

- I understand you are using macOS. Do you have XCode command line tools 
installed or do you use a different compiler?

- Do you use homebrew or MacPorts or some other method to install open 
source dependencies?

I attached the opam versions I end up with on my Mac after running the 
script. I am using XCode command line tools + MacPorts and installed 
opam via MacPorts (but this should not matter). opam also uses MacPorts 
to install system dependencies via depext, but as far as I can see the 
support for this should be better on homebrew.

I will look at the dependencies and build procedure of Flocq to see what 
this could be. Are you active on the Coq Zulip chat? I am not sure if 
everybody on this list is interested on all the details - as long as it 
gets fixed.

One more note: there is also a 8.11.2 branch of the coq platform. This 
is more stable because it does not drag in the development coq opam 
repos (which lead to the .dev versions below). The .dev versions might 
change every day. I hope I can soon release a beta version of the 8.12.0 
coq platform without dev repos. Right now the time is still too close to 
the 8.12.0 Coq release - package maintainers are still working on the 
8.12.0 ports of their packages, so things are a bit rough for the next 2 
to 4 weeks. Nevertheless I encourage people to try the Coq platform 
8.12.0 alpha release so that we can fix issues.

Best regards,

Michael

*base-bigarray* base
*base-threads* base
*base-unix* base
*cairo2* 0.6.1                          Binding to Cairo, a 2D Vector 
Graphics Library
*conf-cairo* 1Virtual package relying on a Cairo system installation
*conf-findutils* 1Virtual package relying on findutils
*conf-g++* 1.0Virtual package relying on the g++ compiler (for C++)
*conf-gnome-icon-theme3* 0Virtual package relying on gnome-icon-theme
*conf-gtk3* 18Virtual package relying on GTK+ 3
*conf-gtksourceview3* 0+2Virtual package relying on a GtkSourceView-3 
system installation
*conf-m4* 1Virtual package relying on m4
*conf-pkg-config* 1.3Virtual package relying on pkg-config installation
*coq**8.12.0*                        pinned to version *8.12.0*
*coq-aac-tactics*8.12.0                        This Coq plugin provides 
tactics for rewriting universally quantified equations, modulo 
associative (and possibly co
*coq-bignums*8.12.dev                      Bignums, the Coq library of 
arbitrary large numbers
*coq-compcert*3.7+8.12~coq_platform~open_sourceThe CompCert C compiler 
(only open source files + using coq-platform)
*coq-compcert-64*3.7+8.12~coq_platform~open_sourceThe CompCert C 
compiler (64 bit, only open source files + using coq-platform)
*coq-coquelicot*3.1.0                          A Coq formalization of 
real analysis compatible with the standard library
*coq-equations*1.2.3+8.12                    A function definition 
package for Coq
*coq-ext-lib*dev                            a library of Coq 
definitions, theorems, and tactics
*coq-flocq*3.3.1                          A formalization of 
floating-point arithmetic for the Coq system
*coq-interval*4.0.0                          A Coq tactic for proving 
bounds on real-valued expressions automatically
*coq-mathcomp-algebra*1.11.0                        Mathematical 
Components Library on Algebra
*coq-mathcomp-bigenough*1.0.0                          A small library 
to do epsilon - N reasonning
*coq-mathcomp-character*1.11.0                        Mathematical 
Components Library on character theory
*coq-mathcomp-field*1.11.0                        Mathematical 
Components Library on Fields
*coq-mathcomp-fingroup*1.11.0                        Mathematical 
Components Library on finite groups
*coq-mathcomp-finmap*dev                            Finite sets, finite 
maps, finitely supported functions, orders
*coq-mathcomp-real-closed*1.1.1                          Mathematical 
Components Library on real closed fields
*coq-mathcomp-solvable*1.11.0                        Mathematical 
Components Library on finite groups (II)
*coq-mathcomp-ssreflect* *1.11.0*                        pinned to 
version *1.11.0*
*coq-menhirlib**20200624*                      pinned to version *20200624*
*coq-quickchick*8.12.dev                      Randomized Property-Based 
Testing Plugin for Coq
*coq-simple-io* dev                              IO monad for Coq
*coq-vst*2.6                            Verified Software Toolchain
*coq-vst-64*2.6                            Verified Software Toolchain
*coqide*8.12.0                        IDE of the Coq formal proof 
management system
*depext*transition                    opam-depext transition package
*dune* 2.6.2                          Fast, portable, and opinionated 
build system
*dune-configurator* 2.6.2                          Helper library for 
gathering system configuration
*dune-private-libs* 2.6.2                          Private libraries of Dune
*lablgtk3**3.0.beta5*                      pinned to version *3.0.beta5*
*lablgtk3-sourceview3* 3.0.beta6                      OCaml interface to 
GTK+ gtksourceview library
*menhir*20200624                      An LR(1) parser generator
*menhirLib* 20200624                      Runtime support library for 
parsers generated by Menhir
*menhirSdk* 20200624                      Compile-time library for 
auxiliary tools related to Menhir
*num* 1.3                              The legacy Num library for 
arbitrary-precision integer and rational arithmetic
*ocaml* 4.07.1                        The OCaml compiler (virtual package)
*ocaml-base-compiler*4.07.1                        Official release 4.07.1
*ocaml-config* 1OCaml Switch Configuration
*ocamlbuild* 0.14.0                        OCamlbuild is a build system 
with builtin rules to easily build most OCaml projects.
*ocamlfind* 1.8.1                          A library manager for OCaml
*opam-depext* 1.1.3                          Query and install external 
dependencies of OPAM packages