The Coq mailing list

[Evgeny Makarov <emakarov AT gmail.com>]

Hello,

I successfully installed Coq trunk 12874 except for several library
files (output of make -k is below). I went through the files in
ProofGeneral, and it turns out the error occurs during the invocation
of tactics ring and ring_simplify. The rest of Coq seems to work fine
after make -k. Any help is appreciated.

I have Ubuntu 8.04, OCaml 3.10.1 and Camlp5 5.07.

Evgeny

make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
...
COQC      theories/ZArith/Zcomplements.v
make[1]: *** [theories/ZArith/Zcomplements.vo] Segmentation fault
make[1]: *** [theories/ZArith/Zcomplements.vo] Deleting file
`theories/ZArith/Zcomplements.glob'
COQC      theories/ZArith/Zsqrt.v
make[1]: *** [theories/ZArith/Zsqrt.vo] Segmentation fault
make[1]: *** [theories/ZArith/Zsqrt.vo] Deleting file
`theories/ZArith/Zsqrt.glob'
COQC      plugins/setoid_ring/Field_theory.v
make[1]: *** [plugins/setoid_ring/Field_theory.vo] Segmentation fault
make[1]: *** [plugins/setoid_ring/Field_theory.vo] Deleting file
`plugins/setoid_ring/Field_theory.glob'
COQC      plugins/micromega/OrderedRing.v
make[1]: *** [plugins/micromega/OrderedRing.vo] Segmentation fault
make[1]: *** [plugins/micromega/OrderedRing.vo] Deleting file
`plugins/micromega/OrderedRing.glob'
OCAMLOPT  tools/coqdep_lexer.ml
OCAMLOPT  tools/coqdep_common.ml
OCAMLOPT  tools/coqdep.ml
OCAMLBEST -o bin/coqdep
make[1]: Target `world' not remade because of errors.
make[1]: Leaving directory `/home/emakarov/coq/trunk'
make: *** [world] Error 2
make: Target `NOARG' not remade because of errors.