I do not see opt in my config either:
jgross@ubuntu:~/Documents/foo$ coqtop -v
The Coq Proof Assistant, version 8.3pl4 (April 2012)
compiled on Apr 03 2012 10:41:42 with OCaml 3.12.1
jgross@ubuntu:~/Documents/foo$ coqtop -config
LOCAL=0
COQLIB=/usr/lib/coq/
COQSRC=/build/buildd/coq-8.3.pl4+dfsg/
CAMLBIN=/usr/bin/
CAMLLIB=/usr/lib/ocaml/
CAMLP4=camlp5
CAMLP4BIN=/usr/bin
CAMLP4LIB=+camlp5
But coq_makefile none-the-less uses .opt versions (note in particular the
CAMLC:=$(CAMLBIN)ocamlc.opt -c -rectypes
CAMLOPTC:=$(CAMLBIN)ocamlopt.opt -c -rectypes
CAMLLINK:=$(CAMLBIN)ocamlc.opt -rectypes
CAMLOPTLINK:=$(CAMLBIN)ocamlopt.opt -rectypes
)
$ coq_makefile A.v
#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.3pl4 ##
#############################################################################
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
#
# This Makefile was generated by the command line :
# coq_makefile A.v
#
#
# This Makefile may take 3 arguments passed as environment variables:
# - COQBIN to specify the directory where Coq binaries resides;
# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.
COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')"
ifndef CAMLP4BIN
CAMLP4BIN:=$(CAMLBIN)
endif
CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)
##########################
# #
# Libraries definitions. #
# #
##########################
OCAMLLIBS:=-I .
COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \
-I $(COQLIB)/library -I $(COQLIB)/parsing \
-I $(COQLIB)/pretyping -I $(COQLIB)/interp \
-I $(COQLIB)/proofs -I $(COQLIB)/tactics \
-I $(COQLIB)/toplevel \
-I $(COQLIB)/plugins/cc \
-I $(COQLIB)/plugins/dp \
-I $(COQLIB)/plugins/extraction \
-I $(COQLIB)/plugins/field \
-I $(COQLIB)/plugins/firstorder \
-I $(COQLIB)/plugins/fourier \
-I $(COQLIB)/plugins/funind \
-I $(COQLIB)/plugins/micromega \
-I $(COQLIB)/plugins/nsatz \
-I $(COQLIB)/plugins/omega \
-I $(COQLIB)/plugins/quote \
-I $(COQLIB)/plugins/ring \
-I $(COQLIB)/plugins/romega \
-I $(COQLIB)/plugins/rtauto \
-I $(COQLIB)/plugins/setoid_ring \
-I $(COQLIB)/plugins/subtac \
-I $(COQLIB)/plugins/subtac/test \
-I $(COQLIB)/plugins/syntax \
-I $(COQLIB)/plugins/xml
COQLIBS:=-I .
COQDOCLIBS:=
##########################
# #
# Variables definitions. #
# #
##########################
ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
OPT:=
COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
ifdef CAMLBIN
COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)
endif
COQC:=$(COQBIN)coqc
COQDEP:=$(COQBIN)coqdep -c
GALLINA:=$(COQBIN)gallina
COQDOC:=$(COQBIN)coqdoc
COQMKTOP:=$(COQBIN)coqmktop
CAMLLIB:=$(shell $(CAMLBIN)ocamlc.opt -where)
CAMLC:=$(CAMLBIN)ocamlc.opt -c -rectypes
CAMLOPTC:=$(CAMLBIN)ocamlopt.opt -c -rectypes
CAMLLINK:=$(CAMLBIN)ocamlc.opt -rectypes
CAMLOPTLINK:=$(CAMLBIN)ocamlopt.opt -rectypes
GRAMMARS:=grammar.cma
CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
CAMLP4OPTIONS:=
PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
###################################
# #
# Definition of the "all" target. #
# #
###################################
VFILES:=A.v
VOFILES:=$(VFILES:.v=.vo)
VOFILES0:=$(filter-out ,$(VOFILES))
GLOBFILES:=$(VFILES:.v=.glob)
VIFILES:=$(VFILES:.v=.vi)
GFILES:=$(VFILES:.v=.g)
HTMLFILES:=$(VFILES:.v=.html)
GHTMLFILES:=$(VFILES:.v=.g.html)
all: $(VOFILES)
spec: $(VIFILES)
gallina: $(GFILES)
html: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)
gallinahtml: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)
all.ps: $(VFILES)
$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
all-gal.ps: $(VFILES)
$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
all.pdf: $(VFILES)
$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
all-gal.pdf: $(VFILES)
$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
####################
# #
# Special targets. #
# #
####################
.PHONY: all opt byte archclean clean install depend html
%.vo %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $*
%.vi: %.v
$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
%.g: %.v
$(GALLINA) $<
%.tex: %.v
$(COQDOC) -latex $< -o $@
%.html: %.v %.glob
$(COQDOC) -html $< -o $@
%.g.tex: %.v
$(COQDOC) -latex -g $< -o $@
%.g.html: %.v %.glob
$(COQDOC) -html -g $< -o $@
%.v.d: %.v
$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
byte:
$(MAKE) all "OPT:=-byte"
opt:
$(MAKE) all "OPT:=-opt"
install:
mkdir -p $(COQLIB)/user-contrib
(for i in $(VOFILES0); do \
install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \
install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \
done)
clean:
rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~
rm -f
all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
- rm -rf html
archclean:
rm -f *.cmx *.o
printenv:
@echo CAMLC = $(CAMLC)
@echo CAMLOPTC = $(CAMLOPTC)
@echo CAMLP4LIB = $(CAMLP4LIB)
-include $(VFILES:.v=.v.d)
.SECONDARY: $(VFILES:.v=.v.d)
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
reportbug gives me the following template, which probably has the relevant info:
Package: coq
Version: 8.3.pl4+dfsg-1
Severity: normal
Dear Maintainer,
*** Please consider answering these questions, where appropriate ***
* What led up to the situation?
* What exactly did you do (or not do) that was effective (or
ineffective)?
* What was the outcome of this action?
* What outcome did you expect instead?
*** End of the template - remove these lines ***
-- System Information:
Debian Release: wheezy/sid
APT prefers precise-updates
APT policy: (500, 'precise-updates'), (500, 'precise-security'), (500, 'precise'), (100, 'precise-backports')
Architecture: amd64 (x86_64)
Kernel: Linux 3.8.0-34-generic (SMP w/1 CPU core)
Locale: LANG=en_US.UTF-8, LC_CTYPE=en_US.UTF-8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/dash
Versions of packages coq depends on:
ii coq-theories 8.3.pl4+dfsg-1
ii emacsen-common 1.4.22ubuntu1
ii libc6 2.15-0ubuntu10.5
ii libcoq-ocaml [libcoq-ocaml-k3dy8] 8.3.pl4+dfsg-1
ii ocaml-base-nox [ocaml-base-nox-3.12.1] 3.12.1-2ubuntu2
Versions of packages coq recommends:
ii coqide 8.3.pl4+dfsg-1
ii proofgeneral 3.7-4
Versions of packages coq suggests:
pn coq-doc <none>
pn ledit [readline-editor] 2.02.1-3build3
pn libcoq-ocaml-dev <none>
pn ocaml-nox 3.12.1-2ubuntu2
pn proofgeneral 3.7-4
pn why <none>
-- no debconf information