> > 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. -- 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/5fcda8d4-25e0-4949-9f08-2c5811ff4551%40googlegroups.com.
