hmijail (Jun 10 2025 at 14:16): hmijail (Jun 10 2025 at 14:16):I am using Isabelle2024 (and 2021 and others) because I'm exploring old projects. I need to install the AFP. Which version can / should I use? I can't find any guidance.
The AFP download page only shows the current version as a downloadable - which seems to change frequently, which suggests to there being a range of acceptable afp versions for the current Isabelle. But I suppose that today's version isn't expected to work with older Isabelle versions?
That download page has a link to older versions in Sourceforge, but those are for 2020 and earlier.
There is also a link to the Hg repo afp-devel, which has year tags. But e.g. there's no tag for 2025. So, what is the latest repo that I can use with Isabelle2024? Should I play it safe and just use the 2024 tag?
I also found that the Heptapod isa-afp group has projects named after each year, like afp-2024. This looks like the latest afp version that should work with Isabelle2024 - but having something official would be great. And, why is it a separate repo?
Relatedly, looking at the afp-devel repo, looks like it uses branches with the name of each version, like afp-2025 (see e.g. this commit merging it). This makes perfect sense, but could we please have those branches visible? If they were I could go and check out the branch I need for my Isabelle version (e.g. afp-2021), see where it stopped being updated, and generally make sense of everything by myself.
Am I missing some documentation? If not, it'd be great to have all of this explained somewhere. As an Isabelle beginner, it's already difficult enough to make sense of things without wondering if things are breaking because I'm using a "bad" AFP.
Mathias Fleury (Jun 10 2025 at 14:20):https://foss.heptapod.net/isa-afp/afp-2021
https://foss.heptapod.net/isa-afp/afp-2022
https://foss.heptapod.net/isa-afp/afp-2023
....
Mathias Fleury (Jun 10 2025 at 14:20):The afp-devel is following the development version of Isabelle
Mathias Fleury (Jun 10 2025 at 14:21):the other afp-20XX are the latest version the AFP
Mathias Fleury (Jun 10 2025 at 14:22):Isabelle does not use branches, only tags
Mathias Fleury (Jun 10 2025 at 14:23):And you are misunderstanding how the AFP works: you submit a theory to the current year. Then the editors merge it to afp-devel and adapt it to the latest Isabelle repo version
Mathias Fleury (Jun 10 2025 at 14:25):Am I missing some documentation?
Just use the last version and consider everything else abandonned
irvin (Jun 10 2025 at 14:26):What projects are you exploring that don't work with Isabelle2025
Mathias Fleury (Jun 10 2025 at 14:27):Isabelle is more stable than before, but as a beginner you don't want to port anything.
hmijail (Jun 11 2025 at 03:34):Mathias Fleury said:
And you are misunderstanding how the AFP works: you submit a theory to the current year. Then the editors merge it to afp-devel and adapt it to the latest Isabelle repo version
Aha, thank you for that. I was assuming the typical workflow where development happens mostly in a main branch, and from which release branches grow for each new release and gather relatively few changes just to somehow pack the release. I see now that it's more complicated than that in the AFP's case.
I added those afp-20XX repos as origins to my afp-devel clone and now the picture makes much more sense.
Mathias Fleury said:
Just use the last version and consider everything else abandonned
To make it explicit: there is no backporting happening across Isabelle releases, right? One is supposed to keep moving to new versions?
Mathias Fleury said:
Isabelle is more stable than before, but as a beginner you don't want to port anything.
But eventually I will need to port some of that old Isabelle code/projects to current versions. Is there any documentation about how to do that? What to expect, pitfalls, ...?
Or should I just get enough "ambient knowledge" that I can stumble my way through it? Like, just open the old project in a new Isabelle and just fix any errors as they appear?
hmijail (Jun 11 2025 at 03:37):Mathias Fleury said:
And you are misunderstanding how the AFP works: you submit a theory to the current year. Then the editors merge it to afp-devel and adapt it to the latest Isabelle repo version
Also, I see that there's work happening separately both in afp-2025 and in afp-devel. Why, what is the difference between them?
Mathias Fleury (Jun 11 2025 at 04:34):To make it explicit: there is no backporting happening across Isabelle releases, right? One is supposed to keep moving to new versions?
No
Mathias Fleury (Jun 11 2025 at 04:35):Also, I see that there's work happening separately both in afp-2025 and in afp-devel. Why, what is the difference between them?
There should not be: new entries come in afp-2025, but some people also work on their entries in afp-devel to improve it or add new lemmas
Mathias Fleury (Jun 11 2025 at 04:38):But eventually I will need to port some of that old Isabelle code/projects to current versions. Is there any documentation about how to do that? What to expect, pitfalls, ...?
Depending on the proof style:
- <5 years (not a math development), sledgehammer your way through
- <5 years (math development like relying on HOL-Analysis), then you probably need to know what changed since that. There is a global NEWS file
- <5 years (apply style) or >= 5 years: cheaper to redo and generalize than to port
irvin (Jun 12 2025 at 01:22):Note there's a fairly recent breaking changed caused by catch_all exceptions being banned.
declare[[ML_catch_all=true]]
Serves as a temporary fix.
Last updated: Jun 21 2025 at 01:46 UTC