Re: [Fwd: Résumé discussion licence de Coq]
On Tuesday 18 May 2004 18:12, Samuel Mimram wrote:
> Is any one volunteering to begin COQ's packaging (I cannot do that
> myself before at least two weeks because I only have a modem
> connection)? This can be done on the current distribution and there
> should be only very few modifications (if any) to have it working
> with the new COQ source code.
> It would be a good thing to have it done quickly in order to be
> sure that COQ 8.0 will be part of sarge.
I've had a quick look at this today. I'm not a maintainer, but I
might be able to offer some help if it'll speed things up.
Notable changes, and some thoughts:
- the patch for 3.07 compatibility now seems redundant.
(doesn't apply + builds without, but haven't looked carefully)
- configure should be called with "--reals all"
- you can use "--reals" to get basic reals theory, but some (4?)
of the tests fail.
- test-suite/success seems to fail anyway, as there are no .v8 files
in that directory (I just added an empty one, in preference to
removing the "for ... in *.v8" code that checks them) - worked
fine.
- the CoqIDE, which would pull in some more build-depends,
(presumably liblablgtk-ocaml-dev, at least) but I haven't tried to
build this yet. Maybe this ought to go into a separate package.
It doesn't build at the moment as configure doesn't find library,
even if it's installed.
- Oh, and it's twice the size of the old one even without the IDE.
(Do the theories7, states7 and contrib7 directories really need to be
there for users working on new theories? Should they go in a
separate package? coqtop bombs if called with the -translate option
if they don't exist. _Seems_ to work otherwise. OTOH, its only
5.5Mb)
On Tuesday 18 May 2004 18:31, Claudio Sacerdoti Coen wrote:
> Thus my question is: what will be linked into the Debian package
> and what license will it have?
According to the bablefish translation of the french(!), it looks like
it would be GPL. I don't think that it would be hard to remove
things to make it LGPL - but I'm not sure whether that would make
much difference to Debian.
Don't know if the bit about pcoq contradicts this - it didn't
translate very well :o(
Presumably just liblablgtk-ocaml + dependencies from other packages?
Regards
Martin
Reply to: