Metadata Release of the Archive of Formal Proofs for Isabelle2021 (04-16)

Release corresponds to https://foss.heptapod.net/isa-afp/afp-2021 @ 679cb16760ca490e5bd161495ad9cb5b629d16a6 Archive of Formal Proofs Metadata This is a release of the entries metadata from the Archive of Formal Proofs which corresponds to https://foss.heptapod.net/isa-afp/afp-2021 @ 679cb16760ca490e5bd161495ad9cb5b629d16a6 (2021-04-16). Format The data is in the form of a list of JSON objects, one per entry. The objects are ordered by session name but there is no strict ordering of the attributes in each object. session Required: Yes Type: String Description: The name of the Isabelle session. This is the name used when importing the theory. title Required: Yes Type: String Description: The title of the entry in the Archive of Formal Proofs authors Required: Yes Type: [String] Description: A list of the authors in the order they were submitted in contributors Required: Type: [String] Description: Optional list of contributors, often with a description under the extra attribute date Required: Yes Type: String Description: Date of submission in the YYYY-MM-DD ISO 8601 format topics Required: Yes Type: [String] Description: List of topics abstract Required: Yes Type: String Description: The abstract of the entry which may contain HTML, MathJax and newlines ("\n") extra Required: Type: {String: String} Description: Extra information about the entry which is "Change history" most of the time. Other keys found here are "Origin" and "Note". license Required: Yes Type: String Description: Either "BSD" or "LGPL". "BSD" is the default license in the AFP. olderReleases Required: Type: [{String: String}] Description: Date of each release and the corresponding Isabelle release it featured in, in descending order. dependencies Required: Type: [String] Description: Session names that the entry is dependent on. theories Required: Type: [String] Description: List of theory files in order that they are executed in. Changes from the upstream data The license is always specified. Dependencies, older releases and theories are new attributes. The upstream data uses strings for all attributes. The author names are consolidated so that authors can be collated properly. Author email addresses are removed. The example submission is omitted.