Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] A Redesign of the Archive of Formal Proofs

view this post on Zulip Email Gateway (May 03 2021 at 13:00):

From: MACKENZIE Carlin <>
Dear all,

We (Carlin MacKenzie, James Vaughan and Jacques Fleuriot) would like to present a prototype of our redesign of the Archive of Formal Proofs. Our earlier survey ( was a part of this project and informed our strategy.

As well as a redesign, the are many new features, including:

* A dynamic search with autocomplete and integration with FindFacts (a web interface to search the code of the AFP).
* Author pages which list all entries by an author.
* Similar pages for topics (which can be found on an entry page).
* Related entries have been added to entry pages where appropriate.
* A new browse theories interface. All scripts appear on one page and can be directly navigated to from the entry page.
* Additionally, there are links to jump directly to specific lemmas from the sidebar. We will continue to improve this feature.
* New Help and Contribution pages in the menu.
* The metadata of the AFP can now be downloaded from the Download page.

The prototype can be accessed at:

Please note that this project is unaffiliated with the AFP and that this website is not a replacement for the official archive.

As this is still a work in progress, we would be grateful to hear your thoughts and feedback. We intend to open-source the code at the end of the project and are open to collaborations.

Carlin MacKenzie, James Vaughan and Jacques Fleuriot
The University of Edinburgh
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th' ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

Last updated: Jan 25 2022 at 02:35 UTC