coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] is there a metacoq email list?
- Date: Tue, 16 Feb 2021 09:58:05 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f172.google.com
- Ironport-phdr: 9a23:8a/57BGigTwsVfYNvXSdi51GYnF86YWxBRYc798ds5kLTJ7ypMqwAkXT6L1XgUPTWs2DsrQY0ruQ7PirCDRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLd/IA+0oAnNucUbhZduIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFog61brhCuqRxxzYDXfY+bKuZxc7jHct8GX2dMRNpdWzBDD466coABD/ABPeFdr4Tlu1YBthu+BQi3BOPv1DBIhWL90LE80+s7FwHJwRErEtUUv3vPrNX1NbwSUeCrw6nL1znMdfVW1i376IfVaBwhoPCMXa5/ccfKxkkvEhnKjlSUqYD/IzyV0eENvnGd4uF9Wu2hl3QppBttojiz2MgskI/Ji5oLx17E6Cl0wYg7K9OmRUJmfNOpHpVeuj+HOoV2X88vQ3xktik1xLEapJO2eCgHxZYlyhDRavGKc5aE7B3iWeuNJzpzmXxreLW6hxmo8EigzPXxVsa10FZWripFj8LDumoR2BzU78iLUvR9/kG82TqV0ADT8O5ELVgomqrcMZ4hxKA/lp4XsUjZACD5hVj2gamLfUsn4uil8/rrbqniq5OGNIJ5ihvyPrkvl8G+G+g0LwoDU3ad9O+hzrPs51f5T69PjvAukqnWrpTaJcMDq668GQBV04Ij5w++DzeizdgUhHcHIE9HdR6ZlYTpNFbOIPf3Dfe7nVugiitkx/fDPrH5A5XNKGbMkKv5cLpj90JRzBA/wNNf6p5OF70MIfP+VlXsuNHaEBM1Kwm0zPzmCNV52IMeQ2WPAqqBPazIqlCI5uMvI/KMZIALuzbxMeIq5/j0gn8/hFARZ6ip3ZoLaHC3BflmLECZbmDtgtcFC2sFog0+TOnyhF2YTTFTf2qyX7475jwjFI2mCp7DSpmxj7yFwSe0BYZbZntGC1CJCXfnbZ+IW/YKaCKII89uiCYIVba7S9xp6Rb7vwjjjrFjM+CcriYfrNfo0MV/z+zVjxA7szJuWZezyWaIGkh+nmITRzI1lIl5qEpxggOK26h5mPxVFppa4fpPXkE7NILT5+N/AtH2HAnGe4HaGx6dXty6DGRpHZoKyNgUbhMlQojwvlX4xyOvRoQtufmLCZgzqPyO2nHwI4N8zy+D2vB+1R8pRcxAMWDgjal6pVCKVtz51n6BnqPvTpwymSvE9WON122L5RgKXwt5UKGDVncaNBKP8YbJo3jaRrrrMowJdxNbwJfbeKRPY9zty15BQaW7NQ==
I got the same error while installing metacoq (version https://github.com/MetaCoq/metacoq/commit/1591d9c5d8f62ae4ccc3b030d9c5c1817c76ef91) on the latest Manjaro. Was there a resolution?
[abhishek@optiplex ~]$ gsed
-bash: gsed: command not found
[abhishek@optiplex ~]$ sed --version
sed (GNU sed) 4.8
Copyright (C) 2020 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <https://gnu.org/licenses/gpl.html>.
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Written by Jay Fenlason, Tom Lord, Ken Pizzini,
Paolo Bonzini, Jim Meyering, and Assaf Gordon.
This sed program was built without SELinux support.
GNU sed home page: <https://www.gnu.org/software/sed/>.
General help using GNU software: <https://www.gnu.org/gethelp/>.
E-mail bug reports to: <bug-sed AT gnu.org>.
-bash: gsed: command not found
[abhishek@optiplex ~]$ sed --version
sed (GNU sed) 4.8
Copyright (C) 2020 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <https://gnu.org/licenses/gpl.html>.
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Written by Jay Fenlason, Tom Lord, Ken Pizzini,
Paolo Bonzini, Jim Meyering, and Assaf Gordon.
This sed program was built without SELinux support.
GNU sed home page: <https://www.gnu.org/software/sed/>.
General help using GNU software: <https://www.gnu.org/gethelp/>.
E-mail bug reports to: <bug-sed AT gnu.org>.
On Fri, Jan 8, 2021 at 10:31 PM Yannick Forster <yannick AT yforster.de> wrote:
There's a MetaCoq Zulip stream, where we try to help new and old users. You can come over and ask there, but we're also happy to answer questions via Coq-Club.Regarding the error: Are you on Windows? This error usually stems from a problem with sed/gsed, so the exact OS and exact package version you're trying to install matters.On 9 January 2021 00:11:57 "jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:I'm getting some errors trying to install metacoq from opam. Is therea metacoq email list I can request help from?# Error: The implementation gen-src/cRelationClasses.ml# [...]# val eq_equivalence : ('a1, __) coq_Equivalence# File "gen-src/cRelationClasses.mli", line 107, characters 0-46:# Expected declaration# File "gen-src/cRelationClasses.ml", line 204, characters 4-18:# Actual declaration# make[3]: *** [Makefile.plugin:664: gen-src/cRelationClasses.cmx]Error 2 # make[2]: *** [Makefile.plugin:339: all] Error 2
- Re: [Coq-Club] is there a metacoq email list?, Abhishek Anand, 02/16/2021
- Re: [Coq-Club] is there a metacoq email list?, jonikelee AT gmail.com, 02/16/2021
Archive powered by MHonArc 2.6.19+.