While I'm not sure of the best way to go forward, let me explain why set.mm and the metamath program are currently in the same directory.
A significant number of people are completely unfamiliar with command line interfaces on Windows and don't know how to specify directory paths. Even worse, there are multiple ways to specify directory paths depending on the platform, the compiler, and (on Windows) whether or not you are using Cygwin. While the program directory can be added to the Windows "Path", it involves going into advanced system settings to alter the Path environmental variable (an awkward and dangerous edit with the crude editing facility provided). Putting both into one directory allows an unsophisticated Windows user to click on metamath.exe and type "read set.mm". This goes back to the days before the Metamath site existed, when the only access to set.mm was via the program, so it was important to make getting started as simple and quick as possible for such users. Norm On Sunday, May 3, 2020 at 1:16:07 PM UTC-4, David A. Wheeler wrote: > > I want to clarify a key point in my earlier post, > "[Metamath] Proposed installation conventions so things will be easier to > install". > > To make it easier to install mmj2 and other tools, I want to change the > conventions > so that "set.mm" is by default stored in its *own* directory > (I recommend ~/set.mm for non-Windows, C:\set.mm for Windows). > Separating code from data, when they're not updated at the same time, > makes > updates & many other operations much simpler. > > If you really want to, you can continue to do things the old way. I just > want to change > the instructions & scripts so this is the *default*. > > --- David A. Wheeler > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f8d3d98a-a7f2-4a28-b186-2114be645aa9%40googlegroups.com.
