Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] PDF documents missing on the AFP website

view this post on Zulip Email Gateway (Dec 18 2025 at 12:10):

From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>

Dear all,

I am writing to report that the "Proof outline" and "Proof document" PDF
documents are currently missing on the Archive of Formal Proofs website,
seemingly for every entry. When I click either link on any entry's webpage, a
404 Not Found error occurs.

Best regards,
Pasquale Noce

view this post on Zulip Email Gateway (Dec 18 2025 at 14:38):

From: Lawrence Paulson <lp15@cam.ac.uk>

I don't know what might've caused that, but in fixing a different issue I seem to have fixed this one as well.

Larry

On 18 Dec 2025, at 12:09, Pasquale Noce <pasquale.noce.lavoro@gmail.com> wrote:

I am writing to report that the "Proof outline" and "Proof document" PDF
documents are currently missing on the Archive of Formal Proofs website,
seemingly for every entry. When I click either link on any entry's webpage, a
404 Not Found error occurs.

view this post on Zulip Email Gateway (Dec 18 2025 at 22:28):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>

This was caused by the release process for AFP 2025-1. It was interrupted and is currently re-running. Please do not add anything new.

Cheers,
Gerwin

On 19 Dec 2025, at 01:38, Lawrence Paulson [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

I don't know what might've caused that, but in fixing a different issue I seem to have fixed this one as well.

Larry

On 18 Dec 2025, at 12:09, Pasquale Noce <pasquale.noce.lavoro@gmail.com> wrote:

I am writing to report that the "Proof outline" and "Proof document" PDF
documents are currently missing on the Archive of Formal Proofs website,
seemingly for every entry. When I click either link on any entry's webpage, a
404 Not Found error occurs.

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.

view this post on Zulip Email Gateway (Dec 19 2025 at 09:10):

From: Peter <cl-isabelle-users@lists.cam.ac.uk>

Right now, I cannot access html nor pdf documents on AFP, at least not
for some theories. Others seem to work well.

Example:

Not working:

https://www.isa-afp.org/thys/AFP/Pre_Star_CFG/Labeled_Transition_System.html

https://www.isa-afp.org/browser_info/current/AFP/Pre_Star_CFG/outline.pdf

Working fine:

https://www.isa-afp.org/thys/AFP/Chomsky_Schuetzenberger/Dyck_Language_Syms.html

https://www.isa-afp.org/browser_info/current/AFP/Chomsky_Schuetzenberger/outline.pdf

Are we in the middle of a non-atomic update, or is something broken again?

--

Peter

On 18/12/2025 23:09, Gerwin Klein (via cl-isabelle-users Mailing List)
wrote:

This was caused by the release process for AFP 2025-1. It was interrupted and is currently re-running. Please do not add anything new.

Cheers,
Gerwin

On 19 Dec 2025, at 01:38, Lawrence Paulson [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

I don't know what might've caused that, but in fixing a different issue I seem to have fixed this one as well.

Larry

On 18 Dec 2025, at 12:09, Pasquale Noce <pasquale.noce.lavoro@gmail.com> wrote:

I am writing to report that the "Proof outline" and "Proof document" PDF
documents are currently missing on the Archive of Formal Proofs website,
seemingly for every entry. When I click either link on any entry's webpage, a
404 Not Found error occurs.

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.

view this post on Zulip Email Gateway (Dec 21 2025 at 04:58):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>

Summary for the list: this was indeed an intermediate state of the AFP release, which this time was not atomic (it usually is). Everything should be back to normal now.

Cheers,
Gerwin

On 19 Dec 2025, at 20:09, Peter (via cl-isabelle-users Mailing List) [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

Right now, I cannot access html nor pdf documents on AFP, at least not for some theories. Others seem to work well.

Example:

Not working:

https://www.isa-afp.org/thys/AFP/Pre_Star_CFG/Labeled_Transition_System.html

https://www.isa-afp.org/browser_info/current/AFP/Pre_Star_CFG/outline.pdf

Working fine:

https://www.isa-afp.org/thys/AFP/Chomsky_Schuetzenberger/Dyck_Language_Syms.html

https://www.isa-afp.org/browser_info/current/AFP/Chomsky_Schuetzenberger/outline.pdf

Are we in the middle of a non-atomic update, or is something broken again?

--

Peter

On 18/12/2025 23:09, Gerwin Klein (via cl-isabelle-users Mailing List) wrote:

This was caused by the release process for AFP 2025-1. It was interrupted and is currently re-running. Please do not add anything new.

Cheers,
Gerwin

On 19 Dec 2025, at 01:38, Lawrence Paulson [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

I don't know what might've caused that, but in fixing a different issue I seem to have fixed this one as well.

Larry

On 18 Dec 2025, at 12:09, Pasquale Noce <pasquale.noce.lavoro@gmail.com> wrote:

I am writing to report that the "Proof outline" and "Proof document" PDF
documents are currently missing on the Archive of Formal Proofs website,
seemingly for every entry. When I click either link on any entry's webpage, a
404 Not Found error occurs.

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.

view this post on Zulip Email Gateway (Dec 21 2025 at 17:10):

From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>

Dear Gerwin,

I have just checked again, and there seems to be some extant issue for some
AFP entries.
In more detail, both PDF documents are still missing (404 Not Found) for the
following entries of mine.

https://www.isa-afp.org/entries/Noninterference_Concurrent_Composition.html
https://www.isa-afp.org/entries/Noninterference_Sequential_Composition.html
https://www.isa-afp.org/entries/Noninterference_Inductive_Unwinding.html
https://www.isa-afp.org/entries/Noninterference_Ipurge_Unwinding.html
https://www.isa-afp.org/entries/Noninterference_Generic_Unwinding.html
https://www.isa-afp.org/entries/Noninterference_CSP.html

Thus, they might be still missing for some other entries as well.
Thank you very much, best regards,
Pasquale

Last updated: Dec 21 2025 at 20:24 UTC