Skip to Content.
Sympa Menu

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

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?


Chronological Thread 
  • From: Mandy Martino <tesleft AT hotmail.com>
  • To: John Wiegley <johnw AT newartisans.com>
  • Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] how to run this program to verify a simple function?
  • Date: Sat, 23 Jan 2016 10:56:13 +0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tesleft AT hotmail.com; spf=Pass smtp.mailfrom=tesleft AT hotmail.com; spf=None smtp.helo=postmaster AT BLU004-OMC4S2.hotmail.com
  • Importance: Normal
  • Ironport-phdr: 9a23:UpSPTR+J419KZv9uRHKM819IXTAuvvDOBiVQ1KB91OMcTK2v8tzYMVDF4r011RmSDdudsqoawLeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU1pzpnL3qs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+lx7DS0Ow53YTVmgH2k5KBAjD8zn8U4j4qDf7reN7w2+ROsigHp4uXjH3yq5tRA6grS4dKz8/9ymDlsFriK9VvDqhoAB6yo/QJoqSMawtLevmYdoGSD8ZDY5qXCtbD9b5NtNXAg==

Hi  ,

it  use  version 8.0

after downloaded,  i  discover  that  in ubuntu 12  i installed  version  8.4  before,  i do not  know  how to uninstall  this  which  using configure to install

i  continue to  configure  8.0  and  make world, got  error

martin@ubuntu:~/hilbertreborn/coq-8.0pl3$ make world
OCAMLC    config/coq_config.mli
OCAMLC    config/coq_config.ml
ECHO... > scripts/tolink.ml
OCAMLC    scripts/tolink.ml
OCAMLC    scripts/coqmktop.ml
File "scripts/coqmktop.ml", line 233, characters 8-11:
Warning 26: unused variable stg.
OCAMLC -o bin/coqmktop
OCAMLOPT  config/coq_config.ml
OCAMLC    lib/pp_control.mli
OCAMLOPT  lib/pp_control.ml
OCAMLC    lib/pp.mli
OCAMLOPT4 lib/pp.ml4
Camlp4: Uncaught exception: DynLoader.Error ("pa_ifdef.cmo", "file not found in path")

File "lib/pp.ml4", line 1, characters 0-1:
Error: Preprocessor error
make: *** [lib/pp.cmx] Error 2
martin@ubuntu:~/hilbertreborn/coq-8.0pl3$ 

Regards,

Martin 


> From: johnw AT newartisans.com
> To: tesleft AT hotmail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] how to run this program to verify a simple function?
> Date: Fri, 22 Jan 2016 18:16:18 -0800
>
> >>>>> Mandy Martino <tesleft AT hotmail.com> writes:
>
> > is_empty_correct < destruct s; simpl; intuition.
> > inversion_clear H0.
> > elim H with z; auto.
> > Error: Attempt to save an incomplete proof
>
> Are you using the right version of Coq for this material? There seem to be a
> lot of things going on, and I'm not sure what the underlying problem is from
> this distance..
>
> --
> John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2



Archive powered by MHonArc 2.6.18.

Top of Page