Email Gateway (May 03 2021 at 13:00): Email Gateway (May 03 2021 at 13:00):From: MACKENZIE Carlin <s1724780@sms.ed.ac.uk>
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 (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:
https://afp.theoremproving.org/
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.
Regards,
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: Jul 15 2022 at 23:21 UTC