mailing-list for TeXmacs Users

[Joris van der Hoeven <address@hidden>]

On Mon, Aug 07, 2006 at 02:39:32PM +0200, Lionel Elie Mamane wrote:
> > That looks very interesting. Is there a place where the plug-in can
> > be downloaded?
> 
> There is a public mirror of my GNU Arch development repository at
> http://www.cs.ru.nl/fnds-arch/lmamane/science/; the tmegg--mainline
> branch is it. There is exactly zero documentation, though.

Thanks.

> > Can we include it inside TeXmacs? Or is it (or Coq) still too
> > unstable?
> 
> Including it with TeXmacs is premature.

OK, so please tell me when the project gets more stable; then I will test it.

> It is a prototype (not feature-complete), needs a beta version of Coq
> and will soon need my own development branch (fork) of Coq. At some
> point in the future, I'll merge my changes back into the mainline
> Coq. Then, we can start talking about adding my plug-in to TeXmacs. Or
> maybe when a new version of Coq (with my changes) is released.

Are the Coq people willing to accept your changes? I ask this,
because I remember that Philippe Audebaud was facing a similar problem.
I would very much like to have at least one interface for a proof system
working inside TeXmacs, so that other people can take example on it.
So I thank you for your efforts and very much hope that your tentative
will be successfull.

Best wishes, Joris