Stream: General

Topic: AFP Fork Date


view this post on Zulip Katherine Kosaian (Feb 26 2025 at 18:13):

As subject, is there a date planned for the Isabelle 2025 AFP fork?

view this post on Zulip Mathias Fleury (Feb 26 2025 at 18:32):

https://foss.heptapod.net/isa-afp/afp-2025

view this post on Zulip Mathias Fleury (Feb 26 2025 at 18:32):

already done, as announced on the mailing list

view this post on Zulip Katherine Kosaian (Feb 26 2025 at 20:00):

Just to make sure that I'm understanding correctly, does that mean updates are no longer allowed for the 2025 AFP?

view this post on Zulip Mathias Fleury (Feb 26 2025 at 20:11):

hmmmmm no?

view this post on Zulip Mathias Fleury (Feb 26 2025 at 20:12):

New submissions got the 2025 AFP fork

view this post on Zulip Mathias Fleury (Feb 26 2025 at 20:12):

But kind of, if you are working on your entries, this should be done on afp-devel

view this post on Zulip Katherine Kosaian (Feb 26 2025 at 20:31):

ah yeah I meant whether the deadline has been passed for making updates to existing entries to be migrated into the 2025 AFP.

view this post on Zulip Mathias Fleury (Feb 26 2025 at 20:36):

As far as I know, the AFP version is mostly frozen and work should happen on the devel version, but an AFP editor like @Manuel Eberl should confirm

view this post on Zulip Manuel Eberl (Feb 27 2025 at 13:43):

Yes. Metadata can be changed in the release version as well, but that's it. Any changes to Isabelle theories can only happen in afp-devel, and they only appear in the release version when a new release happens. For AFP-2025, the fork point has already passed, so changes made to devel now will probably not make it to AFP-2025.

But if it's really important you ought to be able to convince Gerwin to still add a patch so that your changes will appear in AFP-2025 as well. Just contact him if that is the case.

view this post on Zulip Katherine Kosaian (Mar 07 2025 at 15:52):

Actually, while I have you on this thread... I have been trying to change my email on the development branch of the AFP for a couple of months (I sent a couple of emails about this, but think they may have gotten lost). Anyways I receive the message "an error occurred editing the blob".  Maybe I don't have the right permissions? Is there a way to receive these permissions, or something else I should do?

view this post on Zulip Manuel Eberl (Mar 07 2025 at 16:00):

We did get those emails. There was some confusion with afp-devel vs the release and now the fork and that delayed things. But someone will do it eventually.

When exactly do you get that error message? Normally, you should only have to edit the file metadata/authors.toml.

view this post on Zulip Manuel Eberl (Mar 07 2025 at 16:00):

(and then ideally run ./admin/sitegen to make sure it still works)

view this post on Zulip Katherine Kosaian (Mar 07 2025 at 16:03):

I get the error message when trying to commit the changes. I only attempted to edit the metadata/authors.toml file.

view this post on Zulip Fabian Huch (Mar 07 2025 at 16:05):

How is your hg configured?

view this post on Zulip Fabian Huch (Mar 07 2025 at 16:05):

I've never seen that problem, but had a few other weird issues with heptapod in the past

view this post on Zulip Katherine Kosaian (Mar 07 2025 at 16:08):

I don't know what that means, so I think the answer is that it's not configured. I was trying to edit in the heptapod UI. Is there something I need to do to set up my computer to be able to do that?

view this post on Zulip Manuel Eberl (Mar 07 2025 at 16:12):

Okay, that sounds like a Heptapod issue then. Perhaps that's something you'd have to report to them. The normal workflow is to clone the afp-devel repository, do the changes there, commit + push.

And, as I said, ideally run the sitegen. But that would require installing the development version of Isabelle as well and registering afp-devel as a component and then installing a bunch of more components by running isabelle-dev components -a. So not sure if this effort is worth it just for changing an email address.

view this post on Zulip Katherine Kosaian (Mar 07 2025 at 17:18):

Thank you!!


Last updated: Apr 03 2025 at 20:22 UTC