Eric Ren (Sep 02 2024 at 05:20): Eric Ren (Sep 02 2024 at 05:20):Hi,
I'm preparing a result for AFP submission which needs one lemma (with four other lemmas as dependencies) from another fairly hefty AFP session. Including the entire other session in ROOT significantly increases initial load time. Would it be acceptable to avoid that by copy-pasting the required lemmas (with acknowledgement, of course) into my session? More generally, does having an excessively heavy session build slow the AFP review process?
Yong Kiam (Sep 02 2024 at 07:58):if the lemma is not deeply into the "hefty" session, you may consider not putting it as ROOT and just loading the relevant theory as necessary
Fabian Huch (Sep 02 2024 at 08:01):If it's a small lemma that you need to re-use in an otherwise unrelated session, chances are the lemma belongs somewhere else.
Fabian Huch (Sep 02 2024 at 08:02):In that case I would copy the lemma, make note in the submission form saying that you'll move the lemmas afterwards (or request that being done should they go in the Isabelle distribution), and after your entry is accepted change things in the devel verison.
Eric Ren (Sep 06 2024 at 02:49):I tried loading the theory by itself like Yong suggested, but that took over an hour. I also don't think the lemma quite fits anywhere else. Would it be especially bad practice to copy the lemma purely to reduce load time?
Yong Kiam (Sep 06 2024 at 02:51):maybe you can say which lemma this is...? if it is taking 1 hour to load, then perhaps it does make sense to have it as a dependency?
Eric Ren (Sep 06 2024 at 03:02):It's "corollary lattice_of_as_mat_mult" from Modular_arithmetic_and_HNF_algorithms.HNF_Mod_Det_Soundness
Yong Kiam (Sep 06 2024 at 03:07):oh yeah... those lemmas should be in vec_module --- in fact... I think I needed to do something similar for one of my recent entries
I think going for @Fabian Huch 's approach sounds fair enough to me
edit: https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Generalizing.20some.20lemmas.20about.20vector.20spaces.20to.20modules/near/399890532 <-- I didn't get an answer, so I ended up just copy-pasting two lemmas ...
Last updated: Dec 21 2024 at 16:20 UTC