Sage Binder (Jun 05 2025 at 19:52): Sage Binder (Jun 05 2025 at 19:52):I have a development X that I would like to submit to the AFP. Development X depends on a modification of an existing AFP entry Y (I am one of the authors on Y). Eventually, we would like entry Y on the AFP to reflect the updated version. However, my understanding is that we cannot update existing entries until the new Isabelle release. In the meantime, we would like to submit entry X now. What is the preferred way of handling this situation?
If it helps, the existing entry Y is small and is not currently used by any other AFP entry.
Yosuke Ito (Jun 07 2025 at 02:31):Maybe you should require the write access to AFP-devel.
https://devel.isa-afp.org/submission/
If you would like to get write access to your entry in the mercurial repository or if you need assistance, please contact the editors.
Chelsea Edmonds (Jun 09 2025 at 10:44):Contacting the editors as Yosuke mentioned will definitely get you the most accurate answer on this question. In the meantime... my experience has been that once you have development access on the AFP (so can change submission Y), that change becomes available in the development version (also online here: https://devel.isa-afp.org/). Then from memory, I think your new submission relying on the change in Y can target the development version, so it'll only be available there until the next Isabelle release when both will become available on the main archive.
Sage Binder (Jun 10 2025 at 21:21):Thank you for the responses. I've contacted the editors.
I am hoping to have the entry X available on the standard AFP soon (not the development version), so I am hoping it is ok to submit entry X containing the updated Y, then refactor things during the next Isabelle release cycle.
Last updated: Jun 30 2025 at 01:55 UTC