diff --git a/make_site.py b/make_site.py index 2b5953aee..75b577833 100755 --- a/make_site.py +++ b/make_site.py @@ -193,7 +193,7 @@ class HundredTheorem: # like |decl|, but a list of declarations (if one theorem is split into multiple declarations) (optional) decls: Optional[List[str]] = None # name(s) of the author(s) of this formalization (optional) - author: Optional[str] = None + authors: Optional[str] = None # Date of the formalization, in the form `YYYY`, `YYYY-MM` or `YYYY-MM-DD` (optional) date: Optional[str] = None links: Optional[Mapping[str, str]] = None @@ -226,7 +226,7 @@ class ThousandPlusTheorem: # like |decl|, but a list of declarations (if one theorem is split into multiple declarations) (optional) decls: Optional[List[str]] = None # name(s) of the author(s) of this formalization (optional) - author: Optional[str] = None + authors: Optional[str] = None # Date of the formalization, in the form `YYYY`, `YYYY-MM` or `YYYY-MM-DD` (optional) date: Optional[str] = None # for external projects, an URL referring to the result @@ -260,8 +260,8 @@ class TheoremForWebpage: # for the declaration associated to this theorem. doc_decls: Optional[List[DocDecl]] links: Optional[Mapping[str, str]] = None - # See above for the meaning of |author|, |date| and |note|. - author: Optional[str] = None + # See above for the meaning of |authors|, |date| and |note|. + authors: Optional[str] = None date: Optional[str] = None note: Optional[str] = None @@ -358,8 +358,8 @@ def download_N_theorems(kind: NTheorems) -> dict: (id, links, thms, note) = (h.wikidata, {'url': h.url} if h.url else {}, '1000+ theorems', h.comment) if h.statement: statement_formalized = True - # A theorem's proof counts as formalized if the author or `decl`(s) field is non-empty. - proof_formalized = bool(h.author) or h.decls or h.decl + # A theorem's proof counts as formalized if the authors or `decl`(s) field is non-empty. + proof_formalized = bool(h.authors) or h.decls or h.decl decls = h.decls or ([h.decl] if h.decl else []) or ([h.statement] if h.statement else []) doc_decls = [] if decls: @@ -378,7 +378,7 @@ def download_N_theorems(kind: NTheorems) -> dict: docs_link='/mathlib4_docs/' + decl_info.info.docLink, src_link=decl_info.info.sourceLink)) - theorems.append(TheoremForWebpage(id, h.title, statement_formalized, proof_formalized, doc_decls, links, h.author, h.date, note)) + theorems.append(TheoremForWebpage(id, h.title, statement_formalized, proof_formalized, doc_decls, links, h.authors, h.date, note)) pkl_dump(name, theorems) else: theorems = pkl_load(name, dict()) diff --git a/templates/100-missing.html b/templates/100-missing.html index b6e4d67e9..3bba53a0c 100644 --- a/templates/100-missing.html +++ b/templates/100-missing.html @@ -14,7 +14,7 @@ The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome. {% for theorem in thousand_theorems|selectattr('statement_formalized') %}
{{ theorem.id }}: {{ theorem.title }} #
- {% if theorem.author %}

Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}

{% endif %} + {% if theorem.authors %}

Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}

{% endif %} {% if theorem.statement %}

{{ theorem.statement }}

{% endif %} {% for doc in theorem.doc_decls|default([], true) %}
{{ doc.decl_header_html }}
diff --git a/templates/100.html b/templates/100.html index 6b6cd212a..7ffa87de4 100644 --- a/templates/100.html +++ b/templates/100.html @@ -20,7 +20,7 @@

100 theorems

{% for theorem in hundred_theorems|selectattr('proof_formalized') %}
{{ theorem.id }}. {{ theorem.title }} #
- {% if theorem.author %}

Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}

{% endif %} + {% if theorem.authors %}

Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}

{% endif %} {% if theorem.statement %}

{{ theorem.statement }}

{% endif %} {% for doc in theorem.doc_decls|default([], true) %}
{{ doc.decl_header_html }}
diff --git a/templates/1000-missing.html b/templates/1000-missing.html index 414d7aa4e..56df36493 100644 --- a/templates/1000-missing.html +++ b/templates/1000-missing.html @@ -14,7 +14,7 @@ The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome. {% for theorem in thousand_theorems|selectattr('statement_formalized') %}
{{ theorem.id }}: {{ theorem.title }} #
- {% if theorem.author %}

Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}

{% endif %} + {% if theorem.authors %}

Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}

{% endif %} {% if theorem.statement %}

{{ theorem.statement }}

{% endif %} {% for doc in theorem.doc_decls|default([], true) %}
{{ doc.decl_header_html }}
diff --git a/templates/1000.html b/templates/1000.html index c446ee166..6e76ea80c 100644 --- a/templates/1000.html +++ b/templates/1000.html @@ -19,7 +19,7 @@

1000+ theorems

{% for theorem in thousand_theorems|selectattr('proof_formalized') %}
{{ theorem.id }}: {{ theorem.title }} #
- {% if theorem.author %}

Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}

{% endif %} + {% if theorem.authors %}

Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}

{% endif %} {% if theorem.statement %}

{{ theorem.statement }}

{% endif %} {% for doc in theorem.doc_decls|default([], true) %}
{{ doc.decl_header_html }}
@@ -32,7 +32,7 @@
{{ theorem.id }}: {{ the The following theorems have just their statement formalized. Contributions to their proofs are welcome. {% for theorem in thousand_theorems|selectattr('statement_formalized') %}
{{ theorem.id }}: {{ theorem.title }} #
- {% if theorem.author %}

Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}

{% endif %} + {% if theorem.authors %}

Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}

{% endif %} {% if theorem.statement %}

{{ theorem.statement }}

{% endif %} {% for doc in theorem.doc_decls|default([], true) %}
{{ doc.decl_header_html }}