Todo

Feature complete

• Entries would be need to be converted from toml in metadata/metadata to json files in content/entries.
  • Time estimate: 2 hours
• Dependency generation would need to be examined and a plan created.
  • Time estimate: 2-6 hours. It's hard to say as I'm not sure what the scala outputs, but hopefully it can be modified to add/append to an array in the json
• Previous release in entries would also need to be looked into
  • Time estimate: 2-6 hours. Also difficult to say here, but hopefully a similar approach can be used
• Statistics will need to be converted from jinja2 to hugo.
  • Time estimate: 1-3 hours.
• The topics index will need to be generated.
  • Time estimate: 1-3 hours. I think I'll need to write a script to add the topic to each entries json file, and then creating the page will be fairly easy
• Create the submission form here https://ci.isabelle.systems/afp-submission/
  • Time estimate: 30 mins. Didn't realise this was a page as it's not on the same domain.
• Update the logic in the entry page
  • Time estimate: 1 hour. I did a basic implementation to suit the two pages chosen, but there is good logic that can be taken from the jinja2 template
• The entries/release and entries/browser_info directories (which stores the pdfs, html directories and tar/zips of the proofs) would need to be added as static files
  • Time estimate: 1 hour. They would need to be exported/copied to the static directory

Fundamental steps

• Make sure all the pages are valid by W3C standards.
  • We use a few invalid tags and attributes such as <font> and the name attribute on <a> tags. There are modern alternatives to these
• Move away from a table based layout
  • Depending on the users of the project, I would like to move to a div based layout that is styled with CSS grid where necessary.

Search

• Add pagination to search results
• Have the query pick up the URL attribute
• investigate how to tackle diacritics, would be nice to have a hugo solution
• maybe have a thing to be like "Do you want to go to this author/topic?" if it matches
• maybe have a direct download entry/copy entry name button
• add indices for topics and authors
• somehow have integration (link) to the FindFacts
• autocomplete?
• Have topics hyperlink to the rest of the topic
• improve design, take cues from other search interfaces (also remove gap between input and button)
• have link near pagination to do a google search with the query
• think about how this search would work on the header bar -> show just titles? only 5 then see more?
• fix rendering of math

Design

• [x Conduct a user survey to understand needs
  • Structured survey with space for comments
  • Follow on interview with select participants
• Change the entry pages to not be a key: value table
  • This format is very redundant and harder to parse than a standard layout.

Software Engineering

• Add a search widget that isn't google
  • add it to the side bar
  • This is not something I'm too familiar with, but as there are only 560 articles it could probably be done on the client side.
• Wikidata integration
  • A lot of information about journals and academics is being collating in Wikidata see https://scholia.toolforge.org. As the AFP functions as a journal, we could have a bidirectional linkage with Wikidata. There are many motivations for doing this:
    • People come to Wikipedia for information, and this could help surface the AFP to more people.
    • Additionally, many insights can be surfaced with this integration that couldn't be possible before. For example, we could discover which theorems have many implementations in theorem provers and which
    • We could have links to the same proofs in different archives, wikipedia articles, etc.
  • Figure out the process
  • Figure out if the AFP wants to do this
  • Figure out if submissions should be automatically contributed to wikidata or something else
• Have maintenance of articles performed through the website instead of manually
  • I think this will be eased by moving towards JSON as the source-of-truth
  • Investigate log in mechanism with a corresponding backend
  • Create profiles for all authors, allow them to only edit their own entries
  • Entries can be editing by sending a JSON response with the entry
  • Editing the entry with a GUI? or raw text with json validation

Other

• Accessibility
• Dark mode
• RSS feed
  • Atom feed
  • for taxonomies
• Social media cards for when links are shared
• Improve the icon to an SVG version
  • The fidelity of the icon is poor and would be greatly improved with a flawless vector version.

Bugs

• The taxonomy pages are not rendered for children of that taxonomy