Age | Commit message (Collapse) | Author | Files | Lines |
|
RECOMMENDED is removed. It becomes ABI_DEPENDS.
BUILDLINK_RECOMMENDED.foo becomes BUILDLINK_ABI_DEPENDS.foo.
BUILDLINK_DEPENDS.foo becomes BUILDLINK_API_DEPENDS.foo.
BUILDLINK_DEPENDS does not change.
IGNORE_RECOMMENDED (which defaulted to "no") becomes USE_ABI_DEPENDS
which defaults to "yes".
Added to obsolete.mk checking for IGNORE_RECOMMENDED.
I did not manually go through and fix any aesthetic tab/spacing issues.
I have tested the above patch on DragonFly building and packaging
subversion and pkglint and their many dependencies.
I have also tested USE_ABI_DEPENDS=no on my NetBSD workstation (where I
have used IGNORE_RECOMMENDED for a long time). I have been an active user
of IGNORE_RECOMMENDED since it was available.
As suggested, I removed the documentation sentences suggesting bumping for
"security" issues.
As discussed on tech-pkg.
I will commit to revbump, pkglint, pkg_install, createbuildlink separately.
Note that if you use wip, it will fail! I will commit to pkgsrc-wip
later (within day).
|
|
|
|
Changelog:
- Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0.
- The search depth argument of auto can be parameterised in the Ltac language
- Added entry constr_may_eval for tactic extensions (new syntax)
- A couple of lemmas of ZArith were renamed: O -> 0
- many bugfixes, for extraction, Ltac, tactics...
|
|
by applying the patch distributed by the coq team
Bump PKGREVISION, and require ocaml >= 3.09
|
|
USE_GNU_TOOLS -> USE_TOOLS
awk -> gawk
m4 -> gm4
make -> gmake
sed -> gsed
yacc -> bison
|
|
|
|
|
|
- Initial patches supplied by Antoine Reilles, thanks !
- Lots of changes/fixes/updates, see: CHANGES
|
|
packages: ocaml, ocaml-graphics and labltk. Bump PKGREVISION.
|
|
Suggested by Roland Illig, ok'd by various.
|
|
in the process. (More information on tech-pkg.)
Bump PKGREVISION and BUILDLINK_DEPENDS of all packages using libtool and
installing .la files.
Bump PKGREVISION (only) of all packages depending directly on the above
via a buildlink3 include.
|
|
|
|
|
|
which now includes powerpc and sparc.
Bump PKGREVISION.
|
|
with prior art (e.g. lang/twelf).
Coq is a Proof Assistant for a Logical Framework known as the
Calculus of Inductive Constructions. It allows the interactive
construction of formal proofs, and also the manipulation of
functional programs consistently with their specifications.
|