On 2012/12/23 11:15, Stuart Henderson wrote:
> > Yet another diff.
> > - The xdg file is now installed in
> > ${PREFIX}/share/examples/coq/ and /etc/xdg/coq/
>
> The reason for me saying "lets get the huge diff with added files
> out of the way and committed first" is that it's hard to review th
On 2012/12/22 23:11, Christopher Zimmermann wrote:
> On Sat, 22 Dec 2012 10:30:15 +
> Stuart Henderson wrote:
>
> > ===> Building package for coq-8.4
> > Create /data/packages/powerpc/all/coq-8.4.tgz
> > Error: duplicate item in packing-list /usr/local/bin/coqtop
> > Error: duplicate item in
On 2012/12/21 19:30, Christopher Zimmermann wrote:
> Here's a diff which installs the the coqchk.byte, too. Works on amd64
> and sparc64 (not native, no native-dynlink).
===> Building package for coq-8.4
Create /data/packages/powerpc/all/coq-8.4.tgz
Error: duplicate item in packing-list /usr/loca
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA512
thank you for checking the coq port, and sorry that I couldn't respond promptly.
> Well it does work on sparc64 and I would guess that it will genarally
> work on (!ocaml_native || ocaml_native_dynlink)
>
> Have you tried -byte-only or -natdynlink
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA512
> completes without errors. Coq 8.4 has just been released, so it
> would be good if we could update to that directly (although older
looking at https://github.com/jasperla/openbsd-wip/tree/master/math/coq,
it is already updated to use Coq 8.4. G
On 15 Aug 2012, at 12:40, Yozo TODA wrote:
> -BEGIN PGP SIGNED MESSAGE-
> Hash: SHA512
>
>> 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
>
> good news!
> I'll try Chris port later.
> anyway, I expect m
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA512
> 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
good news!
I'll try Chris port later.
anyway, I expect math/coq getting un-broken soon.
-- yozo.
-BEGIN PGP SI
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 wrote:
> Here's a new port for camlp5 which is needed to fix BROKEN math/coq.
>
> I h
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 t
