On Monday, January 27, 2020 at 1:32:19 PM UTC+1, vvs wrote: > > To have only one additional "Volume" instead of two may respect the >> concerns of vvs (see >> https://groups.google.com/d/msg/metamath/mnkBQV1_cXc/Xkrv9_9AAQAJ) a >> little bit... >> > > No, that wasn't my concern. My concern is that Metamath' s collection of > informal conventions and rules already goes way overboard. This looks > extremely weird for software which primary purpose is to formalize things. > > Instead of adding yet another informal agreement why not just split > database into several files and put them into different name spaces? AFAIK > there already is rudimentary support for including other files and it's > worth to extend and enforce its use formally by software. That way we > should kill several birds with one stone: reduce the size of main database > section and separate different kinds of work on different sections. This > will make git easier to use concurrently and will formally meet your > concerns at the same time. >
I fully agree, splitting set.mm in smaler files would be very helpful, and, in my opinion, possible since the split command is available. But this should be discussed in a separate thread. My proposal, however, could be a first step in this direction, splitting set.mm in 4 files according to my "Volumes"... -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/74ba54ae-f8cd-4970-af10-a790968052e2%40googlegroups.com.
