Here are some brainstorming questions and thoughts: Would it make sense to have "search path" variables for metamath and mmj2?
The FHS describes /var/lib and /var/local/lib as places for "variable data" associated with programs in /usr and /usr/local, respectively. Ostensibly, the purpose of /var is so that /usr can be make read-only. In this respect, it makes sense to me for the set.mm repo to be checked out in a directory like /var/lib/metamath. What about mmj2? I haven't tried out mmj2 yet, but would the above apply there too? My eyes are certainly Linux-tinted, but is there some sort of analogue to the above for Windows? There also seems to be some tension about installation expectations. Some people like the fact that metamath Just Works by downloading and extracting an archive to wherever. Others, like myself, seem to prefer that metamath Just Works by installing it like any other program on your platform. Upstream build and distribution burden notwithstanding, it seems like both of these installation methods are mutually compatible. 2020年5月6日水曜日 5時25分48秒 UTC+9 Norman Megill: > > -------- Forwarded Message -------- > Subject: Current problem > Date: Tue, 5 May 2020 20:19:24 +0200 (CEST) > From: fl > To: Megill Norman > > Hi Norm, > > Can you post this. > > I don't know how you do, but my own version of mmj2 has no problems to > find set.mm in the current directory. > > -- > FL > > On Tuesday, May 5, 2020 at 10:44:18 AM UTC-4, David A. Wheeler wrote: >> >> FL: >> > For me it's not "/usr/bin" it's "/usr/local/bin" >> >> That's true for many people. Metamath-exe actually already supports this, >> just use "make install" with autoconf (as always that's the default). >> If you want /usr/bin (as is common for packages installed with a >> package manager), use "PREFIX=/usr/bin make install" >> >> ... >> >> > and set.mm is not a library it's a file of data. >> > You have to be able to browse it and modify it with an editor. >> >> Agreed. >> >> > And the applications must look for it in the current directory "." not >> in $HOME. >> >> The bigger problem is mmj2. >> GUIs don't really have the concept of "current directory", and mmj2 >> needs to know where its current database is. >> >> --- 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/1f36efa8-a57f-4186-ab97-176fa92b31a5%40googlegroups.com.
