carlinmack / afp

Archive of Formal Proofs Redesign

Masters Project at the University of Edinburgh

---

This project is a reimplementation of the Archive of Formal Proofs using Hugo. The resulting website has many advantages over the previous version.

👉 View website - afp.theoremproving.com

👉 View project report - Developing a New Web Application for the Archive of Formal Proofs: Part One

If there is a feature you'd like, or a roadblock to you using this, please create an issue!

Contents

• Current Status
• Requirements and installation
• Locally hosting the site
  • Updating the site
• Contributions

Current Status

This project is a redesign which feature complete with the AFP, plus the following features:

• Client-side search:
  • Responsive to user input plus autocomplete suggestions. The search was then
  • Integration with FindFacts which provides additional results from the code of the AFP.
• Improved navigation:
  • Addition of author, topic and dependency pages which allow navigation to all entries by an author, in a topic, or depend on the same entry.
  • Related entries are generated and added to entries where appropriate.
• Script browsing:
  • All scripts from an entry are visible on one page.
  • Links to lemmas similar to SideKick
• Machine Readable Format:
  • A JSON release of the metadata.

Performance

Version	Time (sec)	# Pages	Pages/sec	Size (MB)	MB/sec
Current AFP	48–79	602	8–13	4	0.05–0.09
Redesigned AFP	44–53	2,506	47–57	951	17.9–26.1
without theories	20–22	1,913	80–96	26	1.2–1.3

Requirements and installation

For development, you will need the ability to run bash scripts. So if you are on Windows you will need to install WSL.

You will also need Python >= v3.3 and pip. Once these are installed, please change directory to src/afp-devel/admin and run python -m pip install -r requirements.txt.

Additionally, you need to download hugo_extended >= v0.81. Personally I download hugo_extended_0.81.0_Linux-64bit.deb from the releases and install it with sudo dpkg -i hugo_extended_0.81.0_Linux-64bit.deb.

If the site is only to be locally hosted, only installation of Hugo is needed.

Locally hosting the site

1. Clone the repository (note the depth flag to save space)

git clone --depth 1 https://github.com/carlinmack/afp.git

2. Change directory

cd afp/src/afp-devel/admin/hugo/

3. Start the Hugo server

hugo server

The site should now be available at localhost:1313/

Updating the site

1. Ensure you are in the afp/src/afp-devel/admin/ directory.

2. Update the site

python exportMetadata.py

3. Regenerate the site by changing to the afp/src/afp-devel/admin/hugo/ directory

hugo --minify

👉 Documentation of all available modules

Contributions

I gladly accept contributions via GitHub pull requests! Please create an issue first so I can advise you on the best approach :)

---

afp's Issues

bad encoding in newer entries' theory files

So I just stumbled over this redesign, and I have to say, I like it a lot!

Unfortunately, newer entries appear to have broken encoding/templating in their theory files (e.g. this one):

There's a lone ead> under the header, and non-ascii characters in the theory seem to get "chunked" apart:

Some cursory poking around in the history of entries seems to show that this first happened for Regular Tree Relations & for every entry since, but not for any before. That entry got added in 0ca12c2, and there's a bunch of non-automatic commits just before it (aafb704 through 1774166) so I guess the bug got introduced somewhere in there, probably in this diff?

… anyways, since I didn't get a python environment working to try and test this out further I'm just leaving this here as a bug report

Add LICENSE

to clarify reusability