開発機と運用機が別れていないためおれがMathlib4の適当なファイルを開いてもし証明が非常に複雑だった場合はCPU使用率が100%になってOtoMADB側のAPIが重くなるというメチャクチャな事態でずっと生きている