INSTALLATION ============ BINARY SNAPSHOT --------------- Untar the downloaded tarball to /some/place of your choosing, and symlink it into your TeXmacs's plugin directory: cd /some/place; tar -x --bzip2 -f tmEgg--mainline--0--patch-NNN--i386.tar.bz2 mkdir -p ~/.TeXmacs/plugins || mkdirhier ~/.TeXmacs/plugins cd ~/.TeXmacs/plugins ln -s /some/place/fat_tmEgg--mainline--0--patch-NNN coq SOURCE ------ Debian packages necessary for building/running the plugin: - ocaml (upstream: http://caml.inria.fr/) - libregexp-pp-ocaml-dev (upstream: http://web.yl.is.s.u-tokyo.ac.jp/~oiwa/caml/#regexp-pp) If installing from upstream sources, note that they do not compile out of the box; you need Debian's 10_pp patch, available from the tmEgg website. - ocaml-findlib (upstream: http://www.ocaml-programming.de/programming/findlib.html) - guile-library (upstream: http://yi.org/rotty/GuileLib) - GNU make Install the plugin in ~/.TeXmacs/plugins/coq/, cd there and type "make". You can get the sources either as a tarball from http://www.cs.ru.nl/~lionelm/tmEgg/ or from my GNU Arch (tla) archive: tla register-archive http://www.fnds.cs.ru.nl/fnds-arch/lmamane/science/ mkdir -p ~/.TeXmacs/plugins cd ~/.TeXmacs/plugins tla get lionel@mamane.lu--science/tmegg--mainline coq cd coq make # and then, use "tla replay" from that directory to update to newer versions. USE === One-time configuration ---------------------- You need to purge TeXmacs's system cache, or it won't notice you installed tmEgg: rm ~/.TeXmacs/system/cache/* If TeXmacs notices you installed (and built) tmEgg, you will get an additional top-level menu entry "Coq" and an entry "Coq" in "Insert / Session", after you answer TeXmacs's customary question "load autosave file?". (You need to start a fresh TeXmacs _after_ finishing all installation steps and _after_ puring the system cache.) tmEgg will by default use the first "coq-interface" in your PATH; select another one with menu "Edit / Preferences / Coq executable" in TeXmacs and restart TeXmacs. You need an SVN trunk checkout of Coq (or Lionel's fork). If you want to pass arguments (e.g. -R, -I or -impredicative-set) to Coq, write a wrapper script and configure tmEgg to use the wrapper script. E.g.: mkdir -p ~/bin cat > ~/bin/mycoq << END #! /bin/sh exec /path/to/coq/bin/coq-interface -I /home/user/coq/private_lib/ "$@" END chmod +x ~/bin/mycoq Basics ------ Insert a Coq session into the document with menu Coq/Coq session, type a Coq command into the input area, press enter to execute (shift-enter in multiline mode). Don't use Coq commands "Backtrack", "Back", "Suspend", "Resume", "Reset", "BackTo", they will confuse tmEgg. Pressing enter always means "reexecute this command", even if it is known that the result will be the same as in the previous execution. The Coq command "Quit" is not available. Interrupting Coq (with the "Stop sign" button) works when supported by Coq and killing Coq (with the scissors button) sorta-works (see BUGS). You can insert multiple Coq sessions, they will all be linked together into a consistent continuous stream of Coq commands, executed in the order they appear in the document. You can jump to (that is, put the cursor in) any Coq input field, change its content or not, and have it reexecuted, and it will "just work", independently of the state the Coq process is in. You do not need to explicitly reexecute commands you modify, they well automatically be reexecuted when necessary when you ask for (re)execution of another command. Note that execution of Coq commands stops at the first error. Similarly, you can insert a new Coq session, or new input fields (A-up and A-down) within a Coq session anywhere at any time, type any command in them, they will be taken in account the next time you execute a command. You can also delete or cut/paste entire Coq sessions, etc. Copy/pasting individual input fields (or a group of them) is possible with utmost care; you need to ensure they land in a Coq session again, that you cut the whole input field, etc. You probably want to do that in the "View source" mode of TeXmacs. Copy-pasting text between input fields is naturally not a problem. If you wish to copy/paste a Coq command from another application into a tmEgg input field, make sure you paste it as verbatim ("Edit / Paste From / verbatim" or "Tools / Selections / Import / Verbatim"). If you wish to copy-paste multiple Coq commands from another application so that each command lands into its own input field, use "Paste from / Coq vernacular" with the cursor _outside_ of any Coq session. This will create a new Coq session, which you can then split and move as desired. The empty / full circle next to results and sessions is to show / hide them. Prompt Colours -------------- The prompt is: * grey for command that have already been executed * red for commands you modified since their execution * black for non-executed commands * pink for commands that were not modified since execution, but a command before them was * green for the current Coq execution point * orange for the current Coq execution point when already executed commands were modified * magenta in unknown circumstances; please contact me if you get ever get a magenta prompt The prompt colouring is lazy; not all commands that should turn pink will do so until refreshed by TeXmacs. Use menu "Coq / Refresh all Coq prompts" to force refreshing all prompts. The colouring does not detect deletions and insertions as such; it will see it as a series of modifications (the commands after the insertion should be pink, but are red). The colouring is quadratic in time, you may want to turn it off (Edit / Preferences / Coq / Colour prompts) for slow machines or long documents. Theorems -------- If you want to create a document that contains a piece of mathematics both in TeXmacs and Coq format, the entries in menu "Coq / new statement" will create an empty template to fill in. tmEgg documents in VCS systems ------------------------------ You may want to purge all outputs (menu "Coq / purge all outputs") before committing a tmEgg document to a version control system, in order to avoid spurious changes. BUGS ==== See http://www.fnds.cs.ru.nl/fndswiki/tmEgg_bugs ; you can file new bugs or comment on existing ones with the login tmEgg, password tmEgg. When you kill Coq, the prompts should all turn black, but don't.