Unable to build Coq-Equations

[davidlazar]

We're having trouble building Coq-Equations:

$ ocaml -version The Objective Caml toplevel, version 3.12.1

$ camlp4 -version 3.12.1

$ camlp5 -v Camlp5 version 6.05 (ocaml 3.12.1)

$ make -version GNU Make 3.82 Built for x86_64-unknown-linux-gnu

$ coqc -v The Coq Proof Assistant, version 8.3pl4 (April 2012) compiled on Apr 10 2012 22:08:24 with OCaml 3.12.1

On branch master:

$ make ... * Warning: in file theories/Init.v, declared ML module equations_plugin has not been found ! ocamlopt.opt -c -rectypes -I src -I /usr/lib/coq/kernel -I /usr/lib/coq/lib -I /usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/groebner -I /usr/lib/coq/plugins/interface -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml -I /usr/lib/ocaml/camlp5 -pp ""camlp5"o -I /usr/lib/ocaml -I . -I /usr/lib/coq/kernel -I /usr/lib/coq/lib -I /usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/groebner -I /usr/lib/coq/plugins/interface -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl" src/equations_common.ml File "src/equations_common.ml", line 78, characters 54-55: Error: This expression has type Term.constr option but an expression was expected of type Term.constr make: * [src/equations_common.cmx] Error 2

On branch 8.3:

$ make ... * Warning: in file theories/Init.v, declared ML module equations_plugin has not been found ! ocamlopt.opt -c -rectypes -I src -I /usr/lib/coq/kernel -I /usr/lib/coq/lib -I /usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/groebner -I /usr/lib/coq/plugins/interface -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml -I /usr/lib/ocaml/camlp5 -pp ""camlp5"o -I /usr/lib/ocaml -I . -I /usr/lib/coq/kernel -I /usr/lib/coq/lib -I /usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/groebner -I /usr/lib/coq/plugins/interface -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl" src/equations_common.ml File "src/equationscommon.ml", line 77, characters 6-15: Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: (None, ) File "src/equations_common.ml", line 353, characters 0-299: Error: Unbound value globwit_hintbases make: * [src/equations_common.cmx] Error 2

On branch coq-trunk:

$ make src/equations_common.ml4:2: *\ missing separator. Stop.

It seems there is a problem with files ending in a number being treated as Makefiles.

[mattam82]

Hi, the coq-trunk branch is the one following the trunk version of Coq. It is now up-to-date, and hopefully the Makefile issue has been resolved as well.

[davidlazar]

Hi, we're still having issues building Coq-Equations on coq-trunk (commit 6d2f8c6014cca012e3e6b847392a4eba4a129103):

$ make src/equations_common.ml4:2: *\ missing separator. Stop.

Here is the fragment of the generated Makefile that is problematic:

MLFILES:=src/equations_common.ml4\ src/sigma.ml4\ src/subterm.ml4\ src/eqdec.ml4\ src/depelim.ml4\ src/equations.ml4\ src/equations_plugin_mod.ml

Does it match your Makefile?

[mattam82]

Hi David,

that's strange, I got:

ML4FILES:=src/equations.ml4\ src/depelim.ml4\ src/eqdec.ml4\ src/subterm.ml4\ src/sigma.ml4\ src/equations_common.ml4

-include $(addsuffix .d,$(ML4FILES)) .SECONDARY: $(addsuffix .d,$(ML4FILES))

MLFILES:=src/equations_plugin_mod.ml

Did you correctly regenerate the Makefile (coq_makefile -f Make -o Makefile should do it). -- Matthieu

Le 15 avr. 2012 à 06:40, David Lazar a écrit :

Hi, we're still having issues building Coq-Equations on coq-trunk (commit 6d2f8c6014cca012e3e6b847392a4eba4a129103):

$ make src/equations_common.ml4:2: *\ missing separator. Stop.

Here is the fragment of the generated Makefile that is problematic:

MLFILES:=src/equations_common.ml4\ src/sigma.ml4\ src/subterm.ml4\ src/eqdec.ml4\ src/depelim.ml4\ src/equations.ml4\ src/equations_plugin_mod.ml

Does it match your Makefile?

---

Reply to this email directly or view it on GitHub: https://github.com/mattam82/Coq-Equations/issues/16#issuecomment-5136892

[fotanus]

I'm having the same problems, with the same versions from David (apart from make, mine is 3.81), but can't figure out what the problem is.

@mattam82, what is the coq and ocaml version you are using to test your coq-trunk branch?

[fotanus]

Moving to branch 8.3, I got the following error:

/usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl" src/equations_common.ml
File "src/equations_common.ml", line 77, characters 6-15:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(None, _)
File "src/equations_common.ml", line 353, characters 0-299:
Error: Unbound value globwit_hintbases
make: *** [src/equations_common.cmx] Error 2

I was only able to compile commenting the following function (path bellow)

diff --git a/src/equations_common.ml b/src/equations_common.ml
index 59d3fba..490502a 100644
--- a/src/equations_common.ml
+++ b/src/equations_common.ml
@@ -350,9 +350,11 @@ let autounfold_first db cl gl =
 open Extraargs
 open Eauto

+(*
 TACTIC EXTEND autounfold_first
 | [ "autounfold_first" hintbases(db) "in" hyp(id) ] ->
     [ autounfold_first (match db with None -> ["core"] | Some x -> x) (Some (id, InHyp)) ]
 | [ "autounfold_first" hintbases(db) ] ->
     [ autounfold_first (match db with None -> ["core"] | Some x -> x) None ]
 END
+*)

Is this problematic?

Environment: Ubuntu 12.04 with lastest updates coqc --version The Coq Proof Assistant, version 8.3pl4 (April 2012) compiled on Apr 03 2012 10:32:56 with OCaml 3.12.1

ocaml -vnum 3.12.1

[mattam82]

Hmm, currently I've been maintaining the 8.4 branch only, which is to be released officially when people have moved to 8.4, so that might explain your difficulties with 8.3 (I need things that are absent from its API, hence the dire state of this branch).

[mattam82]

I tried to update the coq-trunk branch as well but its taking me too much time right now. Will finish later.

[ntc2]

I was getting a <some file>.ml4: *** missing separator. Stop. error when running make for a different Coq library. I was able to resolve it by regenerating the corresponding Makefile.coq, using the coq_makefile <...> command after the # This Makefile was generated by the command line : comment in the Makefile.coq.

No idea if this helps with the specific missing separator error you guys are having, but this page is the first Google result for related searches.

[sp-hacks]

Hi, I am trying to build Coq-Equations-8.4. My system is running Ubuntu 12.04. I have: ocaml 3.12.1 camlp4 3.12.1 camlp5 6.02.3 make 3.81 coqc 8.4pl2 (I upgraded to this from 8.3pl4 to make sure the build was not because of an older coqc version).

I am getting this error: File "src/equations.ml4", line 2814, characters 3-9: Parse error: ':' expected after [name](in [entry]) File "src/equations.ml4", line 1, characters 0-1: Error: Preprocessor error make: *\ [src/equations.cmo] Error 2

Is there a solution to this yet? Or is there a Readme that lists the exact tool versions used to successfully build any other version of Coq-Equations?

[mattam82]

The latest revision of the branch should compile with pl2.