← → ↑
Wims calls interfaces to other programs by a command exec. This command accepts also parameters which will be sent to the interface as standard input to the program. The standard output of the interface is put into the return value of exec. Apart from this standard communication channel, variables can also be used to communicate with background programs in both ways. On the one hand, all Wims variables are visible by child programs as environmen t variables. On the other hand, child programs can define variables for Wims by writing their definition in a special file named exec.var in the session directory.
For security reasons, only interfaced programs can be called by Wims. The following interfaces are currently available.
The header of PARI/GP output is automatically stripped off by the interface. For the rest, each line of the output corresponds to a line in the calling parameter.
Often it is desired to put preliminary definitions or computations to PARI/GP before output is required. If the preliminary material is so long as to create difficulty or reliability to the computation of the output line numbers, this preliminary material can be put into a variable pari_header. The content of this variable will be executed by PARI/GP when it is called, but its output is stripped off.
The functioning of the interface is similar to that of PARI/GP.
This program is relatively slow to load. Whenever possible, we prefer PARI/GP which is much faster.
Several incompatibilities concerning mathematical expressions are fixed by the interface: for exponentials, `^' is translated to `**'. For divisions, integer fractions like `1/2' are translated to `1/2.0' (otherwise Gnuplot applies integer division on 1/2 and gives out 0).
The interface includes adaptation making it possible to plot animated sequences, by adding a few extra parameters. This is done by asking Gnuplot to plot images of the animation one by one, then using convert to put these images together into an animated gif file. Performance is reasonably good, as animations with acceptable quality can be generated within a few seconds.
This program is included in standard Linux distributions. But the Wims interface assumes that it is recompiled with gif support enabled.
Wims does not have a command like insray. So Povray should be called via the command exec. On successful execution, the interface returns the complete html syntax for addressing the resulting image file.
Povray has native support for animation, but rendering is usually too slow to permit efficient animation within the execution time limit allowed to the program, unless the system is installed on a super-fast hardware.
The application Polyray makes use of this package. As it seems that there is no danger allowing direct user-supplied source for Povray, Polyray has included a text field which allows the user to do so.
The program is designed for interactive use. At each proof step, a status is printed including new goals to prove as well as hypotheses for the principal goal.
A Wims module using this package should support step by step operations. It should store the whole command history in a variable, and at each step, the last command is appended to the command history, then the latter is fed to the interface for Coq.
The interface captures the last status printed by Coq, and splits this status into two return data, one for the goals remaining to be proven, and the other for the hypotheses for the principal goal.
One of the problems which occurs when several programs are called in a single process is that each program has its particular syntax for mathematical expressions. For example, Gnuplot uses x**3 to denote x3, which is not recognized neither by PARI/GP nor by MuPAD. In order to make the mathematical expressions directly chainable from program to program, in the respective filters, routines have been inserted which translates syntaxes used unambiguously by other programs into the syntax proper to the interfaced program. Similarly, function names or constant names which are commonly used but not recognized by the interfaced programs are defined in the interfaces (such as sh, ch, sec, tg).
← → ↑