Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problem installing flocq using opam

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem installing flocq using opam


Chronological Thread 
    < Chronological >      < Thread >
  • From: David Naumann <dnaumann AT stevens.edu>
  • To: Michael Soegtrop <MSoegtrop AT yahoo.de>, "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] problem installing flocq using opam
  • Date: Fri, 7 Aug 2020 17:09:12 +0000
  • Accept-language: en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=stevens.edu; dmarc=pass action=none header.from=stevens.edu; dkim=pass header.d=stevens.edu; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=zKj9ZTy0EA5BmmR2kPgKXtX9gYOsm5o9qDiww4H2FTY=; b=ORwo6mSRfnoYCZRTUXm/Y120d7h1J4FgZ1kfYHKq9xFtEHL2hkSI0CQR79LpjgzbkNJ3bns+oFTZcjpYM1nhsFnCQk+/JHuQ1eLKOEUe+YGA+UuwCvWWDofn81au8L5wFcPjiNstboy8BSDIPCtOdRxXL35WtxW91FiQTkjewm8CXCO/YbXAHJYrQLYFO0FcggGDilq8GxM7J75tCx4AcFX4WgoIoRMAlZ/b8sU1HsrrXsGlpaCGNgOA+TQ3UvGLt92YoUEDayQxWwzlsqgDdLahe5o6VYBWERBGARICLd/3YLQBRQsIEMnUireXi5P0gKy9nSJyF+PZxu22GgDxRA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=VHlWPtqLTq2OU1WoBnuAxw7xujYzT41166EdAFRN0GH9iZ0VeUuOOKtbM+3ho2gP/U90b02uV7u8L6R0N6WsFpRkWAOUWXB/IUuowAnugholiJCqE/HU1IIjCJKm4En6Zo2Oe1nbHFxuH5BK6qJIOUw6iMHzhhQCFSDlFOFy7a1mTM7Q37E83+wltLj7EaKh7wgf1d3S/MPQQtJS417Z86tFVNrZpauM8EeDI+JLtvIKDWAia58n14PzlLorJ4RsCAZ8kMwhoAQOL8FyukRxvQnZW1UqOboJUraowmXN4aFoDrFWmVOAdUhmTNHOR1TDJFBDVHVwCbvvFNTgwEnzMg==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dnaumann AT stevens.edu; spf=Pass smtp.mailfrom=dnaumann AT stevens.edu; spf=Pass smtp.helo=postmaster AT NAM12-MW2-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:xU9r0Bao92NmXV/FT9bEuWb/LSx+4OfEezUN459isYplN5qZpsyyYB7h7PlgxGXEQZ/co6odzbaP7eawAydZucrJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRS7oR/Su8UIjoduN7o9xxTUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMCZ6+YYQSFeoMJeZWoZfgqVsSoxWwBgesC+HhxT9JmnD40qI13v89EQ7d2QwsA84CvW7WodjzKawcUfq1zK7NzTjbYf1Zwyn96InVfRs8uf+DR69wcc/LxkkpEQPOk1KdppHjPzyPy+QNtnKU7+xmVe+0kG4ntx9+oiaxyccqkYnFnJwaxU3Z9Shgxos+ONK3RlJhb9G+DJtQqz+VN5FwQs46X21luik3x70It5OnciYG1poqygPQZfKIb4WF4hztWeaMLTl4in9oer2yiwqu/EW+xODyWMi53lhUoydZndfBsnYA3AHd5MiAT/ty5Eah2TCX2gDU9+FEPUQ0la3cK54i2LI/ip0TsUHbEi/5mUX2kK+Wdlg/9eSy9+vnZbDmq5mBPIF3kgHzKqsjltClDeglLgQDXXKX9fqz2bDs50H0QLVHguUrnqXFrJzWP8cWqrSnDwNIzIov8QizAym43NgAg3UKLU5JdRyCgoT0J13BO/H1APKhj1iwkzpmwu3KMqP/DpjIK3XOnqvtcLBg4EBG0gUz18pQ55dMB7EBPv3zXkjxucTAABIlNAK43vjrBMx62IweR26DG6iZP7jMvlOS4eIvPvWMa5QSuDbgLfgq+uTijWcjmV8aYammw4cYaGy5HvRhJUWVe33sgsodEWcOuQo+S+/qhEeeXj5UYna+R6M85jclB4K6FYrOSZyhjKac0CunHJBafH5KB1+DHHvyd4iJW+8AaCeILc9gljwEW6KhS4gk1Ry2qQD6zaBoLvfR+iICs5Lj0sN45/bPlR4s6zx7EcKd03qXQ25qg2wIWic63Lpjrkxl1leDza94juREGtxU/vNFSxs1NZrBz+NhEN3yQQLAftKRSFm8WNmmADcxTsgww9AUeUp9Fc+i3Vj/2H+PArQVnrGPTKcz/63AxX/pb5JY8HHL27U7iEEOU8JPMmrgiqMps0CZDInQ1k6diqyCdKIG3SeL+n3JhT6Fu1gdWwptW43EW2oebw3Yt4KqyFnFSuqCAKomPkNnwNOHI61MIonli1xbQf7lPvzFf2+vlmGrQxuE2+XfP8LRZ2wB0XCFWwA/mAcJ8CPDbFBmX3rzkyflFDVrUGnXTQbs/O159CzpaGYRllvPSnI7kr2/91gSmOCWTO4V0vQcoiA9pj5oHVG7mdXLF96HoAknd6JZM4pksQV3kFnBvgk4BaSOaqVrh1oQaQNy5hi8zAl6FIhGio4noG54lVMue5Ld60tIcnaj5b61IqfeczKg5wyidaPQwRfT3MvEoqo=
Yes thank you but in fact it was after the coq-platform script failed that I
tried to install flocq individually.

-----Original Message-----
From: Michael Soegtrop <MSoegtrop AT yahoo.de>
Date: Friday, August 7, 2020 at 12:33 PM
To: David Naumann <dnaumann AT stevens.edu>, "coq-club AT inria.fr"
<coq-club AT inria.fr>
Subject: Re: [Coq-Club] problem installing flocq using opam

Hello David,

this is exactly the kind of problem I try to solve with the Coq platform
project.


https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FMSoegtropIMC%2Fcoq-platform&amp;data=02%7C01%7Cdnaumann%40stevens.edu%7Cb992ed0550e84a9642a708d83aef8ca6%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C1%7C637324147813948525&amp;sdata=Bh6%2FhopaYM4ZtaEdjJ%2FolGTyQ4GeNaftblRB93Zya8g%3D&amp;reserved=0

This is essentially a script and a set of opam patches which installs a
well known version of Coq and various packages on a wide range of
platforms. It is currently in alpha, but it should work on Mac with
homebrew and Macports as long as opam is already installed. I mostly
test on Mac with Macports.

Usage is:

clone the above git repo (master is fine if you want Coq 8.12.0)

run coq_platform_make.sh

You might want to review the opam install commands at the end of the
script and remove things you don't need.

Running the script will always create a new opam switch, so it should
not mess up anything in your existing work environment. See the ReadMe
in the above repo.

It does install Flocq successfully on Mac and Windows (for me and a few
other testers). I will release the Ubuntu version tomorrow.

If you have any issues with this, please create an issue at the above
Git repo and/or ping me on Zulip.

Best regards,

Michael



Archive powered by MHonArc 2.6.19+.

Top of Page