Email Gateway (Dec 20 2025 at 07:51): Email Gateway (Dec 20 2025 at 07:51):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
I can see that (at least one of) my theories for Isabelle2025-1 at
https://isa-afp.org do not contain recent updates. More specifically,
they differ from https://foss.heptapod.net/isa-afp/afp-2025-1.
Am I wrong assuming that this should not be the case?
Stepan
On 20-Dec-25 1:55 AM, Gerwin Klein (via cl-isabelle-users Mailing List)
wrote:
Following the Isabelle release, the AFP is now available for Isabelle2025-1 fromhttps://isa-afp.org
There are now more than 5 million lines of Isabelle proof in 944 entries by 576 authors.
Five new entries have become available from the home page that were previously only available in the development version:
Dedekind Sums
by Manuel Eberl, Anthony Bordg, Lawrence C. Paulson and Wenda Li
https://www.isa-afp.org/entries/Dedekind_Sums.htmlComplex Lattices, Elliptic Functions, and the Modular Group
by Manuel Eberl, Anthony Bordg, Wenda Li and Lawrence C. Paulson
https://www.isa-afp.org/entries/Elliptic_Functions.htmlThe Partition Function and the Pentagonal Number Theorem
by Manuel Eberl
https://www.isa-afp.org/entries/Pentagonal_Number_Theorem.htmlTyped Ordered Resolution
by Adnan Mohammed Ahmed and Balazs Toth
https://www.isa-afp.org/entries/Typed_Ordered_Resolution.html
Ordered Resolution is a proof calculus for reasoning about first-order
logic that is implemented in many automatic theorem provers. It works
by saturating the given set of clauses and is refutationally complete,
meaning that if the set is inconsistent, the saturation will contain a
contradiction. In this formalization, we restructured the completeness
proof to cleanly separate the ground (i.e., variable-free) and
nonground aspects. We also added a type system to the calculus. We
relied on the library for first-order clauses and on the saturation
framework.Zippy - Generic White-Box Proof Search with Zippers
by Kevin Kappelmann
https://www.isa-afp.org/entries/Zippy.htmlThis entry contains Zippy, a framework for tree-based searches. Zippy
is largely independent of concrete search tree representations, search
algorithms, states and effects. It is designed to create analysable
and navigable searches that are open to customisation and extensions
by users. An accompanying arXiv preprint is available here.This entry also provides a concrete instantiation of the framework in
the form of a general purpose white-box prover, called zip. The prover
performs a proof tree search with customisable expansion actions and
search strategies, including A, breadth-first, depth-first, and
best-first search. By default, it integrates the classical reasoner,
simplifier, the blast and metis prover, and supports resolution with
higher-order and proof-producing unification, conditional substitutions,
case splitting, and induction, among other things. Users are free to
extend the prover with additional expansion actions and search
strategies. We demonstrate the capabilities of zip in an examples theory.In most cases, zip can be used as a drop-in replacement for
Isabelle's classical methods, including auto, fastforce, force, fast, etc.
We demonstrate this with a benchmark containing 2267 method calls from
Isabelle's standard library, where zip achieves a success rate of
99.82% (2263/2267).The Zippy framework is founded on concepts from functional programming
theory, particularly zippers, arrows, monads, lenses, and coroutines.
This entry contains a library of mentioned concepts for Isabelle/ML.Enjoy!
GerwinThis email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error.
Email Gateway (Dec 20 2025 at 22:00):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
The should indeed be equal to afp-2025-1.
It would be helpful to point out which URL. It might be a caching issue, or something has gone wrong for that entry.
Cheers,
Gerwin
On 20 Dec 2025, at 18:50, Stepan Holub (via cl-isabelle-users Mailing List) [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:
I can see that (at least one of) my theories for Isabelle2025-1 at https://isa-afp.org<https://isa-afp.org/> do not contain recent updates. More specifically, they differ from https://foss.heptapod.net/isa-afp/afp-2025-1.
Am I wrong assuming that this should not be the case?
Stepan
On 20-Dec-25 1:55 AM, Gerwin Klein (via cl-isabelle-users Mailing List) wrote:
Following the Isabelle release, the AFP is now available for Isabelle2025-1 from https://isa-afp.org<https://isa-afp.org/>
There are now more than 5 million lines of Isabelle proof in 944 entries by 576 authors.
Five new entries have become available from the home page that were previously only available in the development version:
Dedekind Sums
by Manuel Eberl, Anthony Bordg, Lawrence C. Paulson and Wenda Li
https://www.isa-afp.org/entries/Dedekind_Sums.html
Complex Lattices, Elliptic Functions, and the Modular Group
by Manuel Eberl, Anthony Bordg, Wenda Li and Lawrence C. Paulson
https://www.isa-afp.org/entries/Elliptic_Functions.html
The Partition Function and the Pentagonal Number Theorem
by Manuel Eberl
https://www.isa-afp.org/entries/Pentagonal_Number_Theorem.html
Typed Ordered Resolution
by Adnan Mohammed Ahmed and Balazs Toth
https://www.isa-afp.org/entries/Typed_Ordered_Resolution.html
Ordered Resolution is a proof calculus for reasoning about first-order
logic that is implemented in many automatic theorem provers. It works
by saturating the given set of clauses and is refutationally complete,
meaning that if the set is inconsistent, the saturation will contain a
contradiction. In this formalization, we restructured the completeness
proof to cleanly separate the ground (i.e., variable-free) and
nonground aspects. We also added a type system to the calculus. We
relied on the library for first-order clauses and on the saturation
framework.
Zippy - Generic White-Box Proof Search with Zippers
by Kevin Kappelmann
https://www.isa-afp.org/entries/Zippy.html
This entry contains Zippy, a framework for tree-based searches. Zippy
is largely independent of concrete search tree representations, search
algorithms, states and effects. It is designed to create analysable
and navigable searches that are open to customisation and extensions
by users. An accompanying arXiv preprint is available here.
This entry also provides a concrete instantiation of the framework in
the form of a general purpose white-box prover, called zip. The prover
performs a proof tree search with customisable expansion actions and
search strategies, including A, breadth-first, depth-first, and
best-first search. By default, it integrates the classical reasoner,
simplifier, the blast and metis prover, and supports resolution with
higher-order and proof-producing unification, conditional substitutions,
case splitting, and induction, among other things. Users are free to
extend the prover with additional expansion actions and search
strategies. We demonstrate the capabilities of zip in an examples theory.
In most cases, zip can be used as a drop-in replacement for
Isabelle's classical methods, including auto, fastforce, force, fast, etc.
We demonstrate this with a benchmark containing 2267 method calls from
Isabelle's standard library, where zip achieves a success rate of
99.82% (2263/2267).
The Zippy framework is founded on concepts from functional programming
theory, particularly zippers, arrows, monads, lenses, and coroutines.
This entry contains a library of mentioned concepts for Isabelle/ML.
Enjoy!
Gerwin
This email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error.
Email Gateway (Dec 20 2025 at 22:06):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
It was caching, indeed. I was also confused by the fact that the
development version https://devel.isa-afp.org/ seems to be not actual
for real.
Thank you and sorry for a false alarm.
Stepan
On 20-Dec-25 11:00 PM, Gerwin Klein wrote:
The should indeed be equal to afp-2025-1.
It would be helpful to point out which URL. It might be a caching
issue, or something has gone wrong for that entry.Cheers,
GerwinOn 20 Dec 2025, at 18:50, Stepan Holub (via cl-isabelle-users Mailing
List) [cl-isabelle-users-bounces@lists.cam.ac.uk]
<forwarded_for@cse.unsw.edu.au> wrote:I can see that (at least one of) my theories for Isabelle2025-1 at
https://isa-afp.org do not contain recent updates. More specifically,
they differ from https://foss.heptapod.net/isa-afp/afp-2025-1.Am I wrong assuming that this should not be the case?
Stepan
On 20-Dec-25 1:55 AM, Gerwin Klein (via cl-isabelle-users Mailing
List) wrote:Following the Isabelle release, the AFP is now available for Isabelle2025-1 fromhttps://isa-afp.org
There are now more than 5 million lines of Isabelle proof in 944 entries by 576 authors.
Five new entries have become available from the home page that were previously only available in the development version:
Dedekind Sums
by Manuel Eberl, Anthony Bordg, Lawrence C. Paulson and Wenda Li
https://www.isa-afp.org/entries/Dedekind_Sums.htmlComplex Lattices, Elliptic Functions, and the Modular Group
by Manuel Eberl, Anthony Bordg, Wenda Li and Lawrence C. Paulson
https://www.isa-afp.org/entries/Elliptic_Functions.htmlThe Partition Function and the Pentagonal Number Theorem
by Manuel Eberl
https://www.isa-afp.org/entries/Pentagonal_Number_Theorem.htmlTyped Ordered Resolution
by Adnan Mohammed Ahmed and Balazs Toth
https://www.isa-afp.org/entries/Typed_Ordered_Resolution.html
Ordered Resolution is a proof calculus for reasoning about first-order
logic that is implemented in many automatic theorem provers. It works
by saturating the given set of clauses and is refutationally complete,
meaning that if the set is inconsistent, the saturation will contain a
contradiction. In this formalization, we restructured the completeness
proof to cleanly separate the ground (i.e., variable-free) and
nonground aspects. We also added a type system to the calculus. We
relied on the library for first-order clauses and on the saturation
framework.Zippy - Generic White-Box Proof Search with Zippers
by Kevin Kappelmann
https://www.isa-afp.org/entries/Zippy.htmlThis entry contains Zippy, a framework for tree-based searches. Zippy
is largely independent of concrete search tree representations, search
algorithms, states and effects. It is designed to create analysable
and navigable searches that are open to customisation and extensions
by users. An accompanying arXiv preprint is available here.This entry also provides a concrete instantiation of the framework in
the form of a general purpose white-box prover, called zip. The prover
performs a proof tree search with customisable expansion actions and
search strategies, including A, breadth-first, depth-first, and
best-first search. By default, it integrates the classical reasoner,
simplifier, the blast and metis prover, and supports resolution with
higher-order and proof-producing unification, conditional substitutions,
case splitting, and induction, among other things. Users are free to
extend the prover with additional expansion actions and search
strategies. We demonstrate the capabilities of zip in an examples theory.In most cases, zip can be used as a drop-in replacement for
Isabelle's classical methods, including auto, fastforce, force, fast, etc.
We demonstrate this with a benchmark containing 2267 method calls from
Isabelle's standard library, where zip achieves a success rate of
99.82% (2263/2267).The Zippy framework is founded on concepts from functional programming
theory, particularly zippers, arrows, monads, lenses, and coroutines.
This entry contains a library of mentioned concepts for Isabelle/ML.Enjoy!
GerwinThis email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error.
Last updated: Dec 21 2025 at 20:24 UTC