Many changes, among them: - Many bugs have been fixed (cf coq-bugs web page) - changed parsing precedence of let/in and fun constructions of Ltac: let x := t in e1; e2 is now parsed as let x := t in (e1;e2). - New primitive "external" for communication with tool external to Coq. - Omega now handles arbitrary precision integers. - Haskell extraction: types of functions are now printed, better unsafeCoerce mechanism, both for hugs and ghc. - Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme. - New notation "exists! x:A, P" for unique existence. - New library on String and Ascii characters (contributed by L. Thery). - New library FSets+FMaps of finite sets and maps. - New library QArith on rational numbers. - Few improvements in ZArith potentially exceptionally breaking the compatibility (useless hypothesys of Zgt_square_simpl and Zlt_square_simpl removed; fixed names mentioning letter O instead of digit 0; weaken premises in Z_lt_induction).
167 lines
5.9 KiB
Text
167 lines
5.9 KiB
Text
$NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
|
|
|
|
--- Makefile.orig 2007-02-07 13:21:01.000000000 +0100
|
|
+++ Makefile
|
|
@@ -697,22 +697,22 @@ install-coqide:: install-ide-$(HASCOQIDE
|
|
install-ide-no:
|
|
|
|
install-ide-byte:
|
|
- $(MKDIR) $(FULLBINDIR)
|
|
- cp $(COQIDEBYTE) $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_SCRIPT} $(COQIDEBYTE) $(FULLBINDIR)
|
|
cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE)
|
|
|
|
install-ide-opt:
|
|
- $(MKDIR) $(FULLBINDIR)
|
|
- cp $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_SCRIPT} $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR)
|
|
cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE)
|
|
|
|
install-ide-files:
|
|
- $(MKDIR) $(FULLIDELIB)
|
|
- cp $(IDEFILES) $(FULLIDELIB)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLIDELIB)
|
|
+ ${BSD_INSTALL_DATA} $(IDEFILES) $(FULLIDELIB)
|
|
|
|
install-ide-info:
|
|
- $(MKDIR) $(FULLIDELIB)
|
|
- cp ide/FAQ $(FULLIDELIB)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLIDELIB)
|
|
+ ${BSD_INSTALL_DATA} ide/FAQ $(FULLIDELIB)
|
|
|
|
###########################################################################
|
|
# Pcoq: special binaries for debugging (coq-interface, parser)
|
|
@@ -782,18 +782,18 @@ clean::
|
|
install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages
|
|
|
|
install-pcoq-binaries::
|
|
- $(MKDIR) $(FULLBINDIR)
|
|
- cp $(COQINTERFACE) $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_PROGRAM} $(COQINTERFACE) $(FULLBINDIR)
|
|
|
|
install-pcoq-files::
|
|
- $(MKDIR) $(FULLCOQLIB)/contrib/interface
|
|
- cp $(INTERFACERC) $(FULLCOQLIB)/contrib/interface
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/contrib/interface
|
|
+ ${BSD_INSTALL_DATA} $(INTERFACERC) $(FULLCOQLIB)/contrib/interface
|
|
|
|
PCOQMANPAGES=man/coq-interface.1 man/parser.1
|
|
|
|
install-pcoq-manpages:
|
|
- $(MKDIR) $(FULLMANDIR)/man1
|
|
- cp $(PCOQMANPAGES) $(FULLMANDIR)/man1
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLMANDIR)/man1
|
|
+ ${BSD_INSTALL_MAN} $(PCOQMANPAGES) $(FULLMANDIR)/man1
|
|
|
|
###########################################################################
|
|
# tests
|
|
@@ -1248,21 +1248,21 @@ install-coqlight: install-binaries insta
|
|
install-binaries:: install-$(BEST) install-tools
|
|
|
|
install-byte::
|
|
- $(MKDIR) $(FULLBINDIR)
|
|
- cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_SCRIPT} $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
|
|
cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE)
|
|
|
|
install-opt::
|
|
- $(MKDIR) $(FULLBINDIR)
|
|
- cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_SCRIPT} $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
|
|
cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE)
|
|
|
|
install-tools::
|
|
- $(MKDIR) $(FULLBINDIR)
|
|
# recopie des fichiers de style pour coqide
|
|
- $(MKDIR) $(FULLCOQLIB)/tools/coqdoc
|
|
- cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
|
|
- cp $(TOOLS) $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_SCRIPT} $(TOOLS) $(FULLBINDIR)
|
|
+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLCOQLIB)/tools/coqdoc
|
|
+ ${BSD_INSTALL_DATA} tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
|
|
|
|
LIBFILES=$(THEORIESVO) $(CONTRIBVO)
|
|
LIBFILESLIGHT=$(THEORIESLIGHTVO)
|
|
@@ -1275,52 +1275,55 @@ OBJECTCMA=lib/lib.cma kernel/kernel.cma
|
|
OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
|
|
|
|
install-library:
|
|
- $(MKDIR) $(FULLCOQLIB)
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)
|
|
for f in $(LIBFILES); do \
|
|
- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
|
|
- cp $$f $(FULLCOQLIB)/`dirname $$f`; \
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \
|
|
+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \
|
|
done
|
|
- $(MKDIR) $(FULLCOQLIB)/states
|
|
- cp states/*.coq $(FULLCOQLIB)/states
|
|
- $(MKDIR) $(FULLCOQLIB)/user-contrib
|
|
- cp $(OBJECTCMA) $(OBJECTCMXA) $(FULLCOQLIB)
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states
|
|
+ ${BSD_INSTALL_DATA} states/*.coq $(FULLCOQLIB)/states
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/user-contrib
|
|
+ ${BSD_INSTALL_DATA} $(OBJECTCMA) $(OBJECTCMXA) $(FULLCOQLIB)/states
|
|
|
|
install-library-light:
|
|
- $(MKDIR) $(FULLCOQLIB)
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)
|
|
for f in $(LIBFILESLIGHT); do \
|
|
- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
|
|
- cp $$f $(FULLCOQLIB)/`dirname $$f`; \
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \
|
|
+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \
|
|
done
|
|
- $(MKDIR) $(FULLCOQLIB)/states
|
|
- cp states/*.coq $(FULLCOQLIB)/states
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states
|
|
+ ${BSD_INSTALL_DATA} states/*.coq $(FULLCOQLIB)/states
|
|
|
|
install-allreals::
|
|
for f in $(ALLREALS); do \
|
|
- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
|
|
- cp $$f $(FULLCOQLIB)/`dirname $$f`; \
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \
|
|
+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \
|
|
done
|
|
|
|
install-coq-info: install-coq-manpages install-emacs install-latex
|
|
|
|
MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
|
|
- man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
|
|
+ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 \
|
|
man/coqwc.1 man/coqdoc.1 \
|
|
man/coq_makefile.1 man/coqmktop.1
|
|
+ ifeq ($(BEST),opt)
|
|
+ MANPAGES+=man/coqtop.opt.1
|
|
+ endif
|
|
|
|
install-coq-manpages:
|
|
- $(MKDIR) $(FULLMANDIR)/man1
|
|
- cp $(MANPAGES) $(FULLMANDIR)/man1
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLMANDIR)/man1
|
|
+ ${BSD_INSTALL_MAN} $(MANPAGES) $(FULLMANDIR)/man1
|
|
|
|
install-emacs:
|
|
- $(MKDIR) $(FULLEMACSLIB)
|
|
- cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLEMACSLIB)
|
|
+ ${BSD_INSTALL_DATA} tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
|
|
|
|
# command to update TeX' kpathsea database
|
|
#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
|
|
|
|
install-latex:
|
|
- $(MKDIR) $(FULLCOQDOCDIR)
|
|
- cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
|
|
+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQDOCDIR)
|
|
+ ${BSD_INSTALL_DATA} tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
|
|
# -$(UPDATETEX)
|
|
|
|
###########################################################################
|