Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] MathClasses compilation with 8.4pl5

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] MathClasses compilation with 8.4pl5


Chronological Thread 
  • 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\...



Archive powered by MHonArc 2.6.18.

Top of Page