coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to run this program to verify a simple function?

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to run this program to verify a simple function?
Date: Sun, 24 Jan 2016 05:41:43 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing.csail.mit.edu
Ironport-phdr: 9a23:E/orVxR6WoTVVag7THcSw23rVtpsv+yvbD5Q0YIujvd0So/mwa64ZxyN2/xhgRfzUJnB7Loc0qyN4/6mADRQqs/Q+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8OVOl0Yz2PsKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxzNECg2NxxH+X4/4tiKy4uNx0SyRFcbtRLEwHzGj8+FmRAK+23RPDCIw7GyC0p84t6lcuh/0/xE=

Again, Mandy, regardless of what response you've gotten on this mailing list so far, I'd ask that you please take this kind of installation discussion off this mailing list. The #coq IRC channel is a better place.

On 01/23/2016 09:29 PM, Mandy Martino wrote:

Hi John,

in ubuntu 12 virtual machine using ocqml 3.12.1 but install coq 8.0 got error
as stated before.

in ubuntu 14, have 8.4pl6 , have error , so i change to ubuntu 12 machine ,
then have installation error for coq 8.0.
martin@ubuntu:~$ ocaml -version
The OCaml toplevel, version 4.01.0
martin@ubuntu:~$ coqc -version
coqc: -version: no such file or directory
martin@ubuntu:~$ coqc --version
The Coq Proof Assistant, version 8.4pl6 (December 2015)
compiled on Dec 18 2015 23:12:11 with OCaml 4.01.0
martin@ubuntu:~$

Error: In environment
x : Z
y : Z
The term "x" has type "Z" while it is expected to have type
"nat".

is_empty_correct < is_empty_correct < Toplevel input, characters 13-25:

generalize (compare_spec x z); destruct (compare x z).
^^^^^^^^^^^^

Error: The reference compare_spec was not found in the current environment.

is_empty_correct <

Regards,

Martin

________________________________________
寄件者: John Wiegley
<jwiegley AT gmail.com>
代表 John Wiegley
<johnw AT newartisans.com>
寄件日期: 2016年1月24日 3:58
收件者: Mandy Martino
副本:
coq-club AT inria.fr
主旨: Re: [Coq-Club] how to run this program to verify a simple function?

Mandy Martino
<tesleft AT hotmail.com>
writes:

i have already been using 3.12.1, why still have error?

I'm not sure, but 3.12 and Coq 8.0 are very old versions. Is there any way to
upgrade to OCaml 4 and Coq 8.4pl6? Then I could try your code here, if it is
available online anywhere.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
- Re: [Coq-Club] how to run this program to verify a simple function?, John Wiegley, 01/23/2016
  - RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
    - RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
      - Re: [Coq-Club] how to run this program to verify a simple function?, John Wiegley, 01/23/2016
        
        RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
        
        RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/23/2016
        
        Re: [Coq-Club] how to run this program to verify a simple function?, John Wiegley, 01/23/2016
        RE: [Coq-Club] how to run this program to verify a simple function?, Mandy Martino, 01/24/2016
        Re: [Coq-Club] how to run this program to verify a simple function?, Adam Chlipala, 01/24/2016