I realized that we have two kinds of libraries: ones that are essentially only archives (do we have a better name?; currently TPS, TPTP, GenCS, ...) and libraries that are made active in MathHub.info (SMgloM, MMT, Mizar), I am not quite sure how to conceptualize this. -> discussion.
We should discuss this @m-iancu @jucovschi and then update the user interface, and the help documentation.
I realized that we have two kinds of libraries: ones that are essentially only archives (do we have a better name?; currently TPS, TPTP, GenCS, ...) and libraries that are made active in MathHub.info (SMgloM, MMT, Mizar), I am not quite sure how to conceptualize this. -> discussion. We should discuss this @m-iancu @jucovschi and then update the user interface, and the help documentation.