diff --git a/data/events.yaml b/data/events.yaml index f677fda43..39e0f8f79 100644 --- a/data/events.yaml +++ b/data/events.yaml @@ -2,7 +2,8 @@ url: https://pitmonticone.github.io/ItaLean2025/ start_date: December 9 2025 end_date: December 12 2025 - location: Bologna, Italy + city: Bologna + country: IT type: conference - title: "Lean Together 2026" @@ -16,151 +17,184 @@ url: https://leaning.in/2026/ start_date: March 12 2026 end_date: March 12 2026 - location: Spielfeld, Berlin, Germany + venue: Spielfeld + city: Berlin + country: DE type: conference - title: "Formalization and Proof Assistants (Swiss Math Soc Spring Meeting)" url: https://unidistance.ch/evenement/sms-spring-meeting-formalization-and-proof-assistants start_date: March 25 2026 end_date: March 27 2026 - location: UniDistance Suisse, Brig, Switzerland + venue: UniDistance Suisse + city: Brig + country: CH type: workshop - title: Techniques and Tools for the Formalization of Analysis url: https://icerm.brown.edu/program/topical_workshop/tw-26-ttfa start_date: May 11 2026 end_date: May 15 2026 - location: ICERM, Providence, RI, USA + venue: ICERM + city: Providence + state: Rhode Island + country: US type: workshop - title: Proof assistant users meetup in Ghent url: https://www.meetup.com/nl-NL/sysghent/events/311198787 start_date: October 27 2025 end_date: October 27 2025 - location: Ghent, Belgium + city: Ghent + country: BE type: workshop - title: Lean for the Curious Mathematician 2026 (Italy) url: https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Lean.20for.20the.20Curious.20Mathematician.202026/with/523718160 start_date: September 7 2026 end_date: September 11 2026 - location: SNS, Cortona, Italy + venue: SNS + city: Cortona + country: IT type: tutorial - title: Formalising Algebraic Geometry in Lean url: https://judithludwig.github.io/LeanWorkshop2025 start_date: November 19 2025 end_date: November 21 2025 - location: Heidelberg, Germany + city: Heidelberg + country: DE type: workshop - title: Lean for PDEs url: https://www.slmath.org/workshops/1180 start_date: October 6 2025 end_date: October 9 2025 - location: Berkeley, CA, USA + city: Berkeley + state: California + country: US type: workshop - title: "VSTTE 2025: Conference on Verified Software: Theories, Tools, and Experiments" url: https://systemf.epfl.ch/etc/vstte2025/ start_date: October 6 2025 end_date: October 7 2025 - location: Menlo Park, USA + city: Menlo Park + state: California + country: US type: conference - title: EuroProofNet final symposium url: https://europroofnet.github.io/Symposium/ start_date: September 8 2025 end_date: September 19 2025 - location: Orsay, France + city: Orsay + country: FR type: conference - title: Mechanization and Mathematical Research url: https://www.lorentzcenter.nl/mechanization-and-mathematical-research.html start_date: September 15 2025 end_date: September 19 2025 - location: Leiden, the Netherlands + city: Leiden + country: NL type: workshop - title: Summer School on Formalizing Mathematics in Lean url: https://utrechtsummerschool.nl/courses/science/formalizing-mathematics-in-lean start_date: July 21 2025 end_date: July 25 2025 - location: Utrecht, the Netherlands + city: Utrecht + country: NL type: tutorial - title: Lean for Mathematicians url: https://sites.google.com/view/simonsleanworkshop2025 start_date: June 16 2025 end_date: June 27 2025 - location: New York, NY, USA + city: New York + state: New York + country: US type: tutorial - title: Formalizing Class Field Theory url: https://www.claymath.org/events/formalizing-class-field-theory/ start_date: July 21 2025 end_date: July 25 2025 - location: Oxford, England + city: Oxford + country: GB type: workshop - title: Solving riddles with Lean url: https://sysghent.be/events/lean start_date: July 17 2025 end_date: July 17 2025 - location: Ghent, Belgium + city: Ghent + country: BE type: workshop - title: Lean for the Curious Mathematician (India) url: https://www.icts.res.in/discussion-meeting/LCMaths start_date: April 24 2025 end_date: April 27 2025 - location: ICTS, Bengaluru, India + venue: ICTS + city: Bengaluru + country: IN type: workshop - title: Autoformalization for the Working Mathematician url: https://icerm.brown.edu/program/hot_topics_workshop/htw-25-aftwm start_date: April 24 2025 end_date: April 27 2025 - location: Providence, RI, USA + city: Providence + state: Rhode Island + country: US type: workshop - title: Interactive Theorem Proving 2025 url: https://icetcs.github.io/frocos-itp-tableaux25/itp/ start_date: September 27 2025 end_date: October 3 2025 - location: Reykjavik, Iceland + city: Reykjavik + country: IS type: conference - title: AI for Mathematics and Theoretical Computer Science url: https://simons.berkeley.edu/workshops/simons-institute-theory-computing-slmath-joint-workshop-ai-mathematics-theoretical start_date: April 7 2025 end_date: April 11 2025 - location: Berkeley, CA, USA + city: Berkeley + state: California + country: US type: workshop - title: Computational Algebraic Geometry Workshop url: https://sites.google.com/view/durhamcompalggeom/home start_date: November 18 2024 end_date: November 22 2024 - location: Durham, UK + city: Durham + country: GB type: workshop - title: Lean Tutorial url: https://www.dmg.tuwien.ac.at/lean2024/ start_date: September 18 2024 end_date: September 20 2024 - location: Vienna, Austria + city: Vienna + country: AT type: tutorial - title: Interactive Theorem Proving 2024 url: https://www.viam.science.tsu.ge/itp2024/ start_date: September 9 2024 end_date: September 14 2024 - location: Tblisi, Georgia + city: Tbilisi + country: GE type: conference - title: "Interactions Between Proof Assistants and Mathematical Software, ICMS 2024" - location: Durham, UK + city: Durham + country: GB type: conference url: https://proof-assistants-and-software-icms2024.github.io/ start_date: July 22 2024 @@ -174,7 +208,8 @@ end_date: January 12 2024 - title: "Computer-verified proofs: 48 hours in Rome" - location: Rome, Italy + city: Rome + country: IT url: https://www.mat.uniroma2.it/butterley/formalisation/ start_date: January 24 2024 end_date: January 26 2024 @@ -184,70 +219,83 @@ url: https://mizar.uwb.edu.pl/ITP2023/ start_date: July 31 2023 end_date: August 4 2023 - location: Bialystok, Poland + city: Bialystok + country: PL type: conference - title: Conference on Intelligent Computer Mathematics 2023 url: https://cicm-conference.org/2023/cicm.php start_date: September 4 2023 end_date: September 8 2023 - location: Cambridge, UK + city: Cambridge + country: GB type: conference - title: Conference on Intelligent Computer Mathematics 2024 url: https://cicm-conference.org/2024/cicm.php start_date: August 5 2024 end_date: August 9 2024 - location: Montréal, Québec, Canada + city: Montréal + state: Québec + country: CA type: conference - title: Conference on Intelligent Computer Mathematics 2025 url: https://cicm-conference.org/2025/cicm.php start_date: October 6 2025 end_date: October 11 2025 - location: Brasilia, Brazil + city: Brasilia + country: BR type: conference - title: Certified Programs and Proofs 2023 url: https://popl23.sigplan.org/home/CPP-2023 start_date: January 16 2023 end_date: January 17 2023 - location: Boston, MA, USA + city: Boston + state: Massachusetts + country: US type: conference - title: Certified Programs and Proofs 2024 url: https://popl24.sigplan.org/home/CPP-2024 start_date: January 15 2024 end_date: January 16 2024 - location: London, UK + city: London + country: GB type: conference - title: Certified Programs and Proofs 2025 url: https://popl25.sigplan.org/home/CPP-2025 start_date: January 20 2025 end_date: January 21 2025 - location: Denver, CO, USA + city: Denver + state: Colorado + country: US type: conference - title: Certified Programs and Proofs 2026 url: https://popl26.sigplan.org/home/CPP-2026 start_date: January 12 2026 end_date: January 13 2026 - location: Rennes, France + city: Rennes + country: FR type: conference - title: Interactions of Proof Assistants and Mathematics url: https://itp-school-2023.github.io/ start_date: September 18 2023 end_date: September 29 2023 - location: Regensburg, Germany + city: Regensburg + country: DE type: tutorial - title: Formal Mathematics and Computer-Assisted Proving url: https://www.hsm.uni-bonn.de/events/hsm-schools/formal2023/description/ start_date: September 18 2023 end_date: September 22 2023 - location: Bonn, Germany + city: Bonn + country: DE type: tutorial - title: Learning Mathematics with Lean - 2 @@ -261,14 +309,16 @@ url: https://events.ilds.ro/autumnschool2023/ start_date: September 18 2023 end_date: September 20 2023 - location: Bucharest, Romania + city: Bucharest + country: RO type: tutorial - title: Machine-Checked Mathematics url: https://www.lorentzcenter.nl/machine-checked-mathematics.html start_date: July 10 2023 end_date: July 14 2023 - location: Leiden, the Netherlands + city: Leiden + country: NL type: workshop - title: Formalising algebraic geometry @@ -280,20 +330,23 @@ - title: Summer School about proof assistants for teaching proof and proving (PAT 2023) url: https://pat2023.icube.unistra.fr/ - location: Val d'Ajol, France + city: Val d'Ajol + country: FR start_date: June 18 2023 end_date: June 23 2023 type: tutorial - title: Lean for the Curious Mathematician 2023 url: https://lftcm2023.github.io/tutorial - location: Düsseldorf, Germany + city: Düsseldorf + country: DE start_date: September 4 2023 end_date: September 7 2023 type: tutorial - title: Lean for the Curious Mathematician 2023 – Colloquium - location: Düsseldorf, Germany + city: Düsseldorf + country: DE url: https://lftcm2023.github.io/colloquium start_date: September 7 2023 end_date: September 8 2023 @@ -301,49 +354,64 @@ - title: Atelier Lean of the seventh mini symposium of the Roman Number Theory Association url: http://www.rnta.eu/7MSRNTA/registrationLEAN.html - location: Università Roma Tre, Rome, Italy + venue: Università Roma Tre + city: Rome + country: IT start_date: May 2 2023 end_date: May 3 2023 type: tutorial - title: Lean for the Curious Mathematician 2024 url: https://conferences.cirm-math.fr/2970.html - location: Centre international de rencontres mathématiques (CIRM), Luminy, France + venue: CIRM + city: Luminy + country: FR start_date: March 25 2024 end_date: March 29 2024 type: tutorial - title: "Formalisation of Mathematics: Workshop for Women and Mathematicians of Minority Gender" url: https://www.icms.org.uk/ - location: International Centre for Mathematical Sciences (ICMS), Edinburgh, United Kingdom + venue: ICMS + city: Edinburgh + country: GB start_date: May 27 2024 end_date: May 31 2024 type: tutorial - title: Formalisation of mathematics url: https://www.math.ku.dk/english/calendar/events/formalisation-of-mathematics/ - location: University of Copenhagen, Denmark + venue: University of Copenhagen + city: Copenhagen + country: DK start_date: June 26 2023 end_date: June 30 2023 type: tutorial - title: Formalization of mathematics url: https://www.msri.org/summer_schools/1021 - location: MSRI, Berkeley, USA + venue: MSRI + city: Berkeley + state: California + country: US start_date: June 5 2023 end_date: June 16 2023 type: tutorial - title: Formal Languages, AI and Mathematics url: https://www.ihp.fr/fr/agenda/conference-flaim-formal-languages-ai-and-mathematics - location: IHP, Paris, France + venue: IHP + city: Paris + country: FR start_date: November 3 2022 end_date: November 5 2022 type: conference - title: Prospects of formal mathematics url: https://www.him.uni-bonn.de/programs/future-programs/future-trimester-programs/prospects-of-formal-mathematics/description/ - location: HIM, Bonn, Germany + venue: HIM + city: Bonn + country: DE start_date: May 6 2024 end_date: August 16 2024 type: conference @@ -352,26 +420,34 @@ url: https://www.birs.ca/events/2023/5-day-workshops/23w5124 start_date: May 21 2023 end_date: May 26 2023 - location: BIRS, Banff, Alberta, Canada + venue: BIRS + city: Banff + state: Alberta + country: CA type: workshop - title: Machine Assisted Proofs url: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/ - location: IPAM. Los Angeles + venue: IPAM + city: Los Angeles + state: California + country: US start_date: February 13 2023 end_date: February 17 2023 type: workshop - title: Conference on Intelligent Computer Mathematics 2022 url: https://cicm-conference.org/2022/cicm.php - location: Tbilisi, Georgia + city: Tbilisi + country: GE start_date: September 19 2022 end_date: September 23 2022 type: conference - title: Interactive Theorem Proving 2022 url: https://itpconference.github.io/ITP22/ - location: Haifa, Israel + city: Haifa + country: IL start_date: August 7 2022 end_date: August 10 2022 type: conference @@ -380,21 +456,27 @@ url: https://icerm.brown.edu/topical_workshops/tw-22-lean/ start_date: July 11 2022 end_date: July 15 2022 - location: ICERM, Providence, RI, USA + venue: ICERM + city: Providence + state: Rhode Island + country: US type: tutorial - title: LeaN in LyoN url: https://www.univ-st-etienne.fr/lean-in-lyon.html start_date: May 10 2022 end_date: May 10 2022 - location: Lyon, France + city: Lyon + country: FR type: workshop - title: Learning Mathematics with Lean url: https://www.lboro.ac.uk/departments/mec/events/2022/learningmathematicswithlean/ start_date: April 6 2022 end_date: April 6 2022 - location: Loughborough, UK and virtual + city: Loughborough + country: GB + hybrid: true type: workshop - title: Fields Institute MathEd Forum @@ -413,7 +495,9 @@ - title: Certified Programs and Proofs 2022 url: https://popl22.sigplan.org/home/CPP-2022 - location: Philadelphia, PA, USA + city: Philadelphia + state: Pennsylvania + country: US start_date: January 17 2022 end_date: January 18 2022 type: conference @@ -455,28 +539,33 @@ - title: Formal Methods in Mathematics / Lean Together 2020 url: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/ - location: Pittsburgh, PA, USA + city: Pittsburgh + state: Pennsylvania + country: US start_date: January 6 2020 end_date: January 10 2020 type: workshop - title: Lean Together 2019 url: https://lean-forward.github.io/lean-together/2019/ - location: Amsterdam, NL + city: Amsterdam + country: NL start_date: January 7 2019 end_date: January 11 2019 type: workshop - title: Big Proof url: https://www.newton.ac.uk/event/bpr/ - location: Cambridge, UK + city: Cambridge + country: GB start_date: June 26 2017 end_date: August 4 2017 type: workshop - title: Big Proof url: https://www.newton.ac.uk/event/bprw03/ - location: Cambridge, UK + city: Cambridge + country: GB start_date: June 9 2025 end_date: June 13 2025 type: workshop @@ -489,7 +578,8 @@ end_date: January 17 2025 - title: "Leaning In! 2025" - location: Berlin, DE + city: Berlin + country: DE type: workshop url: https://leaning.in start_date: March 13 2025 diff --git a/make_site.py b/make_site.py index c9c1b878c..ba79cd315 100755 --- a/make_site.py +++ b/make_site.py @@ -31,6 +31,11 @@ import zulip +from pydantic2_schemaorg.Event import Event as SchemaOrgEvent +from pydantic2_schemaorg.Place import Place +from pydantic2_schemaorg.PostalAddress import PostalAddress +from pydantic2_schemaorg.VirtualLocation import VirtualLocation + FilePath = Union[str, Path] DOWNLOAD = not 'NODOWNLOAD' in os.environ @@ -143,10 +148,14 @@ class Formalization: @cached_property def github_repo(self): - return github.get_repo(self.organization + '/' + self.repo) + if DOWNLOAD: + return github.get_repo(self.organization + '/' + self.repo) + return None @property def stars(self): + if not DOWNLOAD or self.github_repo is None: + return 0 return self.github_repo.stargazers_count with (DATA/'formalizations.yaml').open('r', encoding='utf-8') as f_file: @@ -290,12 +299,145 @@ class TheoremForWebpage: @dataclass class Event: title: str - location: str type: str url: str = 'TBA' start_date: str = '' end_date: str = '' date_range: str = 'TBA' + schema_org_json: str = '' + location: str = '' # Computed from structured fields or explicitly provided + city: Optional[str] = None + country: Optional[str] = None + state: Optional[str] = None + venue: Optional[str] = None + hybrid: bool = False + + def is_fully_remote(self) -> bool: + """Check if this is a fully remote/virtual event.""" + return self.location.lower() in ['virtual', 'online'] + + def compute_location(self) -> str: + """Compute location string from structured fields.""" + # For virtual events + if self.is_fully_remote(): + return self.location + + # Build location from structured fields + parts = [] + if self.venue: + parts.append(self.venue) + if self.city: + parts.append(self.city) + if self.state: + parts.append(self.state) + if self.country: + parts.append(self.country) + + if parts: + return ', '.join(parts) + elif self.location: + # Fall back to explicit location if provided + return self.location + else: + return 'TBA' + + def validate(self) -> None: + """Validate event data consistency.""" + if self.hybrid: + if not self.city or not self.country: + raise ValueError( + f"Hybrid event '{self.title}' must have both city and country fields" + ) + + if self.is_fully_remote(): + if self.city or self.state or self.country: + raise ValueError( + f"Fully remote event '{self.title}' should not have city, state, or country fields" + ) + +def generate_schema_org_json(event: Event) -> str: + """Generate schema.org JSON-LD for an event using pydantic2-schemaorg models.""" + # Parse dates to ISO 8601 format + try: + start_date_iso = datetime.strptime(event.start_date, '%B %d %Y').strftime('%Y-%m-%d') + except (ValueError, TypeError, AttributeError): + raise ValueError(f"Invalid start date for event '{event.title}': {event.start_date}") + + try: + end_date_iso = datetime.strptime(event.end_date, '%B %d %Y').strftime('%Y-%m-%d') + except (ValueError, TypeError, AttributeError): + raise ValueError(f"Invalid end date for event '{event.title}': {event.end_date}") + + # Build location - determine if virtual, hybrid, or physical + location = None + event_attendance_mode = None + + if event.hybrid: + # Hybrid event: both physical and virtual attendance + event_attendance_mode = "https://schema.org/MixedEventAttendanceMode" + + # Build physical location + address_kwargs = { + "addressLocality": event.city, + "addressCountry": event.country + } + if event.state: + address_kwargs["addressRegion"] = event.state + + place_name = event.venue if event.venue else event.city + + # Location is an array with both Place and VirtualLocation + location = [ + Place( + name=place_name, + address=PostalAddress(**address_kwargs) + ), + VirtualLocation(url=event.url) + ] + elif event.is_fully_remote(): + # Purely virtual event + event_attendance_mode = "https://schema.org/OnlineEventAttendanceMode" + location = VirtualLocation(url=event.url) + else: + # Physical event only + event_attendance_mode = "https://schema.org/OfflineEventAttendanceMode" + + # Use structured address data if available, otherwise fall back to location string + if event.city and event.country: + address_kwargs = { + "addressLocality": event.city, + "addressCountry": event.country + } + # Add state/region for US addresses if available + if event.state: + address_kwargs["addressRegion"] = event.state + + # Use venue as Place name if available, otherwise use city + place_name = event.venue if event.venue else event.city + + location = Place( + name=place_name, + address=PostalAddress(**address_kwargs) + ) + else: + # Fall back to simple Place with just name + location = Place(name=event.location) + + # Create the schema.org Event model - Pydantic will validate it + schema_event = SchemaOrgEvent( + name=event.title, + url=event.url, + startDate=start_date_iso, + endDate=end_date_iso, + location=location, + eventAttendanceMode=event_attendance_mode, + eventStatus="https://schema.org/EventScheduled" + ) + + # Convert to JSON-LD format with pretty printing and add @context + event_dict = json.loads(schema_event.json(exclude_none=True)) + event_dict["@context"] = "https://schema.org" + return json.dumps(event_dict, indent=2) @dataclass class Course: @@ -592,7 +734,13 @@ def format_date_range(event): new_events = sorted((e for e in events if (not e.end_date) or datetime.strptime(e.end_date, '%B %d %Y').date() >= present), key=lambda e: datetime.strptime(e.end_date, '%B %d %Y').date()) for e in old_events + new_events: + # Compute location from structured fields if not explicitly provided + if not e.location or e.location == '': + e.location = e.compute_location() + # Validate event data consistency + e.validate() e.date_range = format_date_range(e) + e.schema_org_json = generate_schema_org_json(e) @dataclass @@ -612,7 +760,7 @@ class Project: oprojects_3 = yaml.safe_load(h_file) pkl_dump('oprojects_3', oprojects_3) else: - oprojects_3 = pkl_load('oprojects_3', []) + oprojects_3 = pkl_load('oprojects_3', {}) projects_3 = [] diff --git a/requirements.txt b/requirements.txt index 7a93ae221..396a19e38 100644 --- a/requirements.txt +++ b/requirements.txt @@ -20,3 +20,4 @@ ruamel.yaml>=0.17.10 html5lib>=1.1 python-slugify>=4.0.1 zulip>=0.9.0 +pydantic2-schemaorg>=0.3.0 diff --git a/templates/events.html b/templates/events.html index a8bfee443..e94c20c98 100644 --- a/templates/events.html +++ b/templates/events.html @@ -25,7 +25,13 @@

Upcoming events

  • {{ e.title }} ({{ e.location }}. {{ e.date_range }}) {{ e.type }} -
  • + + {% if e.schema_org_json %} + + {% endif %} + {% endfor %} @@ -35,7 +41,13 @@

    Past events

  • {{ e.title }} ({{ e.location }}. {{ e.date_range }}) {{ e.type }} -
  • + + {% if e.schema_org_json %} + + {% endif %} + {% endfor %} {% endblock %}