coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Guillaume Claret <guillaume AT claret.me>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] MathClasses compilation with 8.4pl5
- Date: Thu, 04 Dec 2014 12:26:33 +0100
You can use my fork on https://github.com/clarus/math-classes which works with the pl5.
By the way, you can also directly install MathClasses with OPAM:
opam repo add coq-stable https://github.com/coq/repo-stable.git
opam install --jobs=4 coq:math-classes
The 12/04/2014 10:02, Cedric Auger wrote:
Seing the file on the git repository, I guess that changing (φ c d) into
(@φ c d) should do the trick. Didn’t tried it though.
2014-12-04 1:01 GMT+01:00 Vadim Zaliva
<vzaliva AT cmu.edu
<mailto:vzaliva AT cmu.edu>>:
After upgrading to 8.4pl5 I am no longer able to compile MathClasses.
coqc -R . CoRN -R math-classes/src MathClasses -q
math-classes/src/theory/adjunctions.v
File "/Volumes/CORN/corn/math-classes/src/theory/adjunctions.v",
line 192, characters 32-38:
Error: Illegal application (Non-functional construction):
The expression "φ c" of type "?1062 ⟶ G ?1063"
cannot be applied to the term
"d" : "?1057"
I am not up to the task of fixing it myself. Does somebody have a
workaround?
To make things worse, one could no longer used the version compiled
with with
previous version:
Error: Compiled library MathClasses.interfaces.abstract_algebra.vo makes
inconsistent assumptions over library Coq.Init.Datatypes
The only course of action I see is to downgrade to 8.4pl4.
Sincerely,
Vadim Zaliva
--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva
--
.../Sedrikov\...
- [Coq-Club] MathClasses compilation with 8.4pl5, Vadim Zaliva, 12/04/2014
- Re: [Coq-Club] MathClasses compilation with 8.4pl5, Cedric Auger, 12/04/2014
- Re: [Coq-Club] MathClasses compilation with 8.4pl5, Guillaume Claret, 12/04/2014
- Re: [Coq-Club] MathClasses compilation with 8.4pl5, Cedric Auger, 12/04/2014
Archive powered by MHonArc 2.6.18.