I don't think the book needs to stay rigidly in sync at all. It's only had two editions in how many years? In any case, while it is undoubtedly more work to have to manage parallel PRs, it is definitely more scalable than assuming that everything lives in the same repo. If set.mm is to be a monorepo it should probably be renamed to reflect that.
On Tue, Nov 22, 2022 at 5:45 PM David A. Wheeler <[email protected]> wrote: > > > > On Nov 22, 2022, at 3:59 PM, Mario Carneiro <[email protected]> wrote: > > > > I think we should not put everything in set.mm repo, or if we do, we > clearly separate set.mm from the rest of it. I think there is already too > much stuff in the repo that isn't about set.mm itself. What you have > described clearly sounds like a separate project, like a blog post series > or something, and as such it wouldn't need to stay rigidly in sync and > could just pin a version of set.mm to work with. > > I agree with your general point of "don't put everything in the set.mm > repo". > > However, I have in mind a book that syncs with set.mm, that is, the book > is updated as set.mm changes, that is, it *DOES* stay rigidly in sync. > The easiest way to simultaneously edit them is to put them in the same repo > :-). > > ---- 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/067489BC-395A-4AC3-AB27-5D632D09B4DE%40dwheeler.com > . > -- 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/CAFXXJSu2%2BjzQqDVUwwreox%2BezTUf9fmZ_uJfop4pPriye5tNKQ%40mail.gmail.com.
