The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Abhishek,

I did get the opam installation of metacoq to work with the help of the
zulip metacoq group.  Here's a link to the thread:
https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/error.20from.20opam

Hope that helps,
Jonathan

On Tue, 16 Feb 2021 09:58:05 -0800
Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

> 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>.
> 
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
> 
> 
> 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
> > there  
> >> a 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
> >>  
> >
> >