mailing-list for TeXmacs Users

[Joris van der Hoeven <address@hidden>]

On Tue, Aug 08, 2006 at 09:22:16AM +0200, Lionel Elie Mamane wrote:
> On Mon, Aug 07, 2006 at 03:54:55PM +0200, Joris van der Hoeven wrote:
> > On Mon, Aug 07, 2006 at 02:39:32PM +0200, Lionel Elie Mamane wrote:
> 
> >>> 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.
> 
> Also be aware that my plugin contains OCaml code, and uses a Guile
> library or two. You may not want to add dependencies on these things
> for TeXmacs just for a plugin.

This does not bother me. Plug-ins that don't compile are automatically 
ignored.
People who build official static binaries may install Ocaml if they want
to ship your plug-in (of course, the size of binaries should remain 
reasonable;
otherwise, a separate project becomes more adequate).

> >> 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?
> 
> They know I'm doing it, and haven't expressed particular "réticences" to it.

OK.

> > I ask this, because I remember that Philippe Audebaud was facing a
> > similar problem.
> 
> There are several tactical differences:
> 
>  - I work on the Coq trunk (equivalent of CVS HEAD), while
>    Audebaud-Rideau were working on a stable released version of Coq,
>    while Coq was undergoing major changes (the whole syntax was
>    changed). This makes merges easier.
> 
>  - I don't add anything TeXmacs-specific to Coq. The TeXmacs-specific
>    parts are in a separate wrapper binary that is in the plugin
>    (similarly, I presume, to tm_axiom). At the Coq level, I'm taking a
>    protocol that Coq already can speak (the one used by the PCoq
>    interface) and I'm extending it to support newer features in Coq
>    and make it a bit more generic, so that it can serve the needs of
>    several interfaces.

OK.

> > 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.
> 
> Looking forward a bit, I'm not sure it will be a straightforward
> example for many other proof assistant:
> 
>  - The central concept of tmEgg relies critically on the fact that Coq
>    can go backwards in time (roughly, multiple undo) to a state it was
>    in before.

This can always be simulated by re-executing everything, even if that
quickly becomes impracticable. But this strategy can be used in order
to mimick some existing code.

>  - I don't see it being an "example" for e.g. Agda; they have a
>    different interfacing model: Coq is LCF-style (you give it commands
>    which change the state and construct the proof (the lambda-term)
>    indirectly), with Agda you write the lambda-term directly on
>    screen.

Sure, there are many types of proof systems.
Some other systems basically prove one single statement
in a command line fashion, etc.

> But, well, we'll see.

Exactly. Some interface should be the first.

> While I have your attention:
> 
>  I'd like my code to get notified (and be able to do stuff) when text
>  in an <input> of a Coq session is modified / deleted, as well as when
>  a whole <input> or a whole Coq <session> is deleted (or cut) or
>  pasted. Is there any way to do this in TeXmacs currently, or would it
>  be rather straightforward to add (as in, you can roughly delineate
>  how to do it, and I could do it without being intimate with the
>  TeXmacs internals)? What I'd like is to be able to register a "hook"
>  (a scheme function) that gets called when the described event
>  happens.

In that case, a client-server protocol is probably better than using
a hacked computer algebra session. In that case you would basically
create a tmEgg mode and redefine (tm-define) any function you need to
in this specific mode.

As to the client-server stuff, you might want to look at what Henri
sent you. Notice also that I started to develop the TeXmacs server project
(see the server directory on CVS). New modules can easily be added.
The project is still at a rudimentary stage, but that might actually
be good for you. Any improvements would be appreciated.
One of the major current drawbacks is that the connections are
not persistent: we re-open a socket at each request.

> The reason I want this is:
> 
>  tmEgg tries to enforce that, were one to save the document, exit
>  TeXmacs, start a new TeXmacs and reopen the same document, one would
>  get the same results by executing the Coq commands in the document.
> 
>  I'll take the axiom plugin to make an example of what I want to
>  avoid. I execute these two axiom commands in separate input fields:
> 
>  a:=5
> 
>  a
> 
>  The second command answers "5". Now, if I the first <input>, and
>  replace the text in the second one by:
> 
>  b:=a^2
> 
>  and add another input:
> 
>  b
> 
>  which will answer 25. Now, the whole document looks like:
> 
>  b:=a^2
> 
>  b
> 
>   25
> 
>  But were I to save that and open it in a new TeXmacs, it wouldn't
>  work! The first command would give an error, because "a" is not
>  defined. So, were the user to do a similar thing with my plugin, I'd
>  like my plugin to take notice that the input field containing "a:=5"
>  has just been deleted and remove "a" from the Coq environment at this
>  time.
> 
> I hope this was understandable.

Sure, I understand this problem, but it might require you to hack
quite a lot of editing stuff. I'll think a bit about it and be back later.

Best wishes, Joris