coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] make error for geocoq

From: Julien Narboux <jnarboux AT narboux.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] make error for geocoq
Date: Sat, 12 Dec 2015 22:40:04 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jnarboux AT narboux.fr; spf=None smtp.mailfrom=jnarboux AT narboux.fr; spf=None smtp.helo=postmaster AT mail-vk0-f45.google.com
Ironport-phdr: 9a23:DFstaBKn3tQ50wo4l9mcpTZWNBhigK39O0sv0rFitYgULPjxwZ3uMQTl6Ol3ixeRBMOAu6wC07KempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRMiK14ye7KObxd76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtLYqySlbuuog+shcSu26Ov1gFf0LRAghZksy/YXAsQTJBV+E4WJZWWELmDJJBRLE5Vf0RMGinDH9s79fxS2bMMu+a7kuUzO//+8/Shnhki0AKi4R9mjNgMttnORVukTy9FRE34fIbdTNZ7JFdaTHcIZfHDIZUw==

Hi Martin,

Currently we test GeoCoq only with Coq version 8.4 pl6, I will try to port to 8.5 beta soon, but we don't plan to support 8.3 version you are using.

Regards,

Julien Narboux

2015-12-11 12:08 GMT+01:00 Mandy Martino <tesleft AT hotmail.com>:

Hi

martin@ubuntu:~/geo/GeoCoq$ git clone https://github.com/GeoCoq/GeoCoq
martin@ubuntu:~/geo/GeoCoq$ ./configure.sh
martin@ubuntu:~/geo/GeoCoq$ make
make: ocamlc.opt: Command not found
coqc -q -R . GeoCoq Tarski_dev/Ch02_cong
File "/home/martin/geo/GeoCoq/Tarski_dev/Ch02_cong.v", line 90, characters 13-31:
Error: Cannot infer the implicit parameter M of
cong_commutativity.
Could not find an instance for "Tarski_neutral_dimensionless".

make: *** [Tarski_dev/Ch02_cong.vo] Error 1

Regards,

Martin

[Coq-Club] make error for geocoq, Mandy Martino, 12/11/2015
- Re: [Coq-Club] make error for geocoq, Julien Narboux, 12/12/2015
  - [Coq-Club] Add Load Path however still can not find library, Mandy Martino, 12/20/2015
    - Re: [Coq-Club] Add Load Path however still can not find library, Abhishek Anand, 12/20/2015