Hi Daniel, math/coq also can work with camlp4. I have a working port of it at https://github.com/jasperla/openbsd-wip/tree/master/math/coq
Christopher On Mon, 13 Aug 2012 00:44:44 -0400 (EDT) Daniel Dickman <[email protected]> wrote: > Here's a new port for camlp5 which is needed to fix BROKEN math/coq. > > I have a working update for coq as well but need to clean it up a bit to > make it suitable for submission. > > Note I am targeting coq 8.3 since it will some time for dependencies to > support 8.4 (which isn't released yet). To use this latest version of > camlp5 with coq 8.3, I'm using the below in my coq 8.3 Makefile to work > around a small issue: > > -------------------------------------------------------------------- > # back-port a fix to allow coq 8.3 to work with camlp5 > 6.04. See: > # http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2728 > post-patch: > find ${WRKSRC} -name "*.ml" -o -name "*.ml4" \ > -exec perl -pi -e 's/Stdpp.Exc_located/Compat.Exc_located/g' {} \; > -------------------------------------------------------------------- > > I've had this in my tree for a while but I believe my version started with > work from Nima Hoda back in 2010. > http://archives.neohapsis.com/archives/openbsd/2010-01/2212.html > > - Daniel > > # pkg_info camlp5 > Information for inst:camlp5-6.06 > > Comment: > OCaml preprocessor and pretty-printer > > Description: > Camlp5 is a preprocessor and pretty-printer for OCaml programs. > > As a preprocessor, it can: > * extend the syntax of OCaml, > * redefine the syntax of the language. > > As a pretty printer, it can: > * display OCaml programs in an elegant way, > * convert from one syntax to another, > * check the results of syntax extensions. > > Camlp5 also provides some parsing and pretty printing tools, namely: > * extensible grammars > * extensible printers > * stream parsers and lexers > * pretty print module > > Maintainer: The OpenBSD ports mailing-list <[email protected]> > > WWW: http://pauillac.inria.fr/~ddr/camlp5/
