The Coq mailing list

[Mandy Martino <tesleft AT hotmail.com>]

Hi John,

martin@ubuntu:~/hilbertreborn$ ocaml -version

The Objective Caml toplevel, version 3.12.1

http://stackoverflow.com/questions/18798614/installing-old-active-networking-language-plan

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

Regards,

Martin 

---

From: tesleft AT hotmail.com
To: johnw AT newartisans.com
CC: 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

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