mailing-list for TeXmacs Users

[Lionel Elie Mamane <address@hidden>]

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.

>> 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.

> 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.

> 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.

 - 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.

But, well, we'll see.

> So I thank you for your efforts

My pleasure :)

> and very much hope that your tentative will be successfull.

Thanks.



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.

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.


Best Regards,

-- 
Lionel