From: MACKENZIE Carlin <firstname.lastname@example.org>
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 (https://arxiv.org/abs/2104.01052) 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: Dec 05 2021 at 23:19 UTC