I can help with Mathematica and some equations. I need help about Mizar at Debian.
Hello all. Usually I have a lot of problems with every new software I try to install. I use the Debian linux. Today I tried to deal with Mizar.
It does not seem to work, and I suspect, the error is because of my poor knowledge in linux. The installation protocol looked as follows: ~/Q/MIZAR>sudo sh install.sh Installation of Mizar System Version 7.11.05 (Linux/FPC) (MML 4.133.1080) Enter the path for installing Mizar executables [default is /usr/local/bin] Unpacking to /usr/local/bin Enter the path for installing Mizar shared files [default is /usr/local/share/mizar] Unpacking to /usr/local/share/mizar It may take some time... Enter the path for installing Mizar documentation [default is /usr/local/doc/mizar] Unpacking to /usr/local/doc/mizar The installation process of the Mizar system is completed. Note: The Mizar system requires a variable MIZFILES which should be set to /usr/local/share/mizar. If /usr/local/bin is not in your PATH please add it before running Mizar. With questions or comments contact mus@mizar.uwb.edu.pl ~/Q/MIZAR> (End of protocol) Which file should I edit to add line MIZFILE=/usr/local/share/mizar ? From my side, I could help about numerical evaluation of holomorphic solutions F of equation F(z+1)=H(F(z)); for several functions H, I have the efficient C++ implementations. |
All you have to do is type export MIZFILES=/usr/local/share/mizar. That will add the variable to your system. Then you also have to edit the path variable. Type echo $PATH, which will give you a long line of paths in your system. If you don't see /usr/local/bin in that, then type export PATH= then copy what was printed earlier, then at the end, add this:
Code:
:/usr/local/bin |
Quote:
export MIZFILES=/usr/local/share/mizar it seems to work; and no path should be modified. Perhaps, the path Code:
/usr/loca/bin So, since now, I have the Mizar; but I see, is not so easy to use as the Mathematica. |
Well, I'm glad I could help :) /usr/local/bin I think is supposed to be defined in the PATH variable by default, like you said, so I'm surprised their script said that. I'm even surprised that their script didn't define the first variable on its own.
|
All times are GMT -5. The time now is 10:29 AM. |