diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 988dfe0eea..ac8ff2251c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -58,6 +58,7 @@ jobs: github_repo: ${{ github.repository }} github_ref: ${{ github.ref }} ZULIP_KEY: ${{ secrets.ZULIP_KEY }} + QUEUEBOARD_REVIEWER_INTERESTS_API_URL: ${{ vars.QUEUEBOARD_REVIEWER_INTERESTS_API_URL }} - name: Upload artifact id: upload-artifact diff --git a/css/lean.css b/css/lean.css index 4dc17feb0e..21d9a0802b 100644 --- a/css/lean.css +++ b/css/lean.css @@ -8237,6 +8237,9 @@ pre { .card-body > *:first-child { margin-top: unset; } +.reviewer-freeform > p:last-child { + margin-bottom: 0; } + /* Theorem statements in the 100 theorem list: */ .doc-stmt { font-family: 'Source Code Pro', monospace; diff --git a/data/people.yaml b/data/people.yaml index 5a1614212e..a50d0cc7df 100644 --- a/data/people.yaml +++ b/data/people.yaml @@ -1,5 +1,6 @@ - name: Jeremy Avigad + github: avigad descr: | Jeremy is a Professor of Philosophy at Carnegie Mellon University (USA). He did a PhD in mathematical logic at Berkeley, and has @@ -8,6 +9,7 @@ img: jeremy.png - name: Anne Baanen + github: Vierkantor descr: | Anne is a mathematical research engineer at the Mathlib Initiative. They did a PhD on formalizing algebraic number theory at Vrije @@ -16,6 +18,7 @@ img: anne.jpg - name: Matthew Robert Ballard + github: mattrobball descr: | Matt is a Professor of Mathematics at the University of South Carolina (Columbia, USA). He did a PhD on derived categories in algebraic @@ -24,6 +27,7 @@ img: mrb.png - name: Reid Barton + github: rwbarton descr: | Reid is a post-doc at the University of Pittsburgh (USA). He did a PhD in algebraic topology in Harvard. He worked on the Glasgow @@ -32,6 +36,7 @@ img: reid.jpg - name: Riccardo Brasca + github: riccardobrasca descr: | Riccardo is an Associate Professor of Mathematics at Université Paris Cité (France). He did a PhD in number theory in Milan. He has @@ -39,6 +44,7 @@ img: riccardo.jpg - name: Kevin Buzzard + github: kbuzzard descr: | Kevin is a professor of pure mathematics at Imperial College London. He did a PhD under Richard Taylor in Cambridge UK. @@ -46,6 +52,7 @@ img: kbuzzard.jpg - name: Mario Carneiro + github: digama0 descr: | Mario is a post-doc at Carnegie Mellon University (USA). He did a PhD in pure & applied logic at CMU under Jeremy Avigad. He @@ -54,6 +61,7 @@ img: mario.jpg - name: Bryan Gin-ge Chen + github: bryangingechen descr: | Bryan is a senior engineer at the Mathlib Initiative. He did a PhD in theoretical condensed matter physics at University of @@ -62,6 +70,7 @@ img: bryan.jpg - name: Johan Commelin + github: jcommelin descr: | Johan is universitair docent (assistant professor) at Utrecht University (Netherlands) and the director of the Mathlib Initiative. @@ -70,6 +79,7 @@ img: Johan.jpg - name: Anatole Dedecker + github: ADedecker descr: | Anatole is a PhD student in Mathematics, specifically operator algebras, at Université Paris Cité (France). He has been formalizing @@ -77,6 +87,7 @@ img: anatole.jpg - name: Rémy Degenne + github: RemyDegenne descr: | Rémy is a researcher at the Inria centre at the University of Lille (France). He did a PhD in applied mathematics at Université Paris Cité. He has been @@ -84,6 +95,7 @@ img: remy.jpg - name: Floris van Doorn + github: fpvandoorn descr: | Floris is a professor in the mathematics department of the University of Bonn (Germany) on formal mathematics. @@ -93,6 +105,7 @@ img: floris.jpg - name: Frédéric Dupuis + github: dupuisf descr: | Frédéric is an Associate Professor of Computer Science at the Université de Montréal. His main area of research is quantum @@ -101,6 +114,7 @@ img: frederic.jpg - name: Gabriel Ebner + github: gebner descr: | Gabriel is an engineer at Microsoft Research (USA). He did a PhD in computational proof theory at TU Wien (Austria). @@ -110,6 +124,7 @@ img: gabriel.jpeg - name: Sébastien Gouëzel + github: sgouezel descr: | Sébastien is a Professor of Mathematics at Université de Rennes 1 (France). He did a PhD in dynamical systems in Orsay. He has @@ -117,14 +132,16 @@ now in Lean. img: sebastien.jpg - - name: Markus Himmel + name: Julia Markus Himmel + github: TwoFX descr: | - Markus is a tech lead at the Lean FRO. - He did a master's in pure mathematics in Cambridge (UK). - He has been formalizing mathematics since 2020. + Julia is a tech lead at the Lean FRO. + She did a master's in pure mathematics in Cambridge (UK). + She has been formalizing mathematics since 2020. img: markus.jpg - name: Simon Hudon + github: cipher1024 descr: | Simon is a research engineer and proof engineer at Bedrock Systems where he works on the formal verification of a novel hypervisor. He did a Master's @@ -136,12 +153,14 @@ img: Simon.jpg - name: Chris Hughes + github: ChrisHughes24 descr: | Chris is a PhD student at INRIA with the Gallinette team in Nantes (France). He has been formalizing mathematics since 2017. img: chris.png - name: Yury G. Kudryashov + github: urkud descr: | Yury is a Formalization Lead at Harmonic. He did a PhD in dynamical systems in Lyon and Moscow. @@ -149,6 +168,7 @@ img: yury.jpeg - name: Robert Y. Lewis + github: robertylewis descr: | Rob is a lecturer in the Department of Computer Science at Brown University (USA). @@ -158,6 +178,7 @@ img: rob.jpg - name: Jireh Loreaux + github: j-loreaux descr: | Jireh is an Associate Professor of Mathematics in the Department of Mathematics and Statistics at Southern Illinois University Edwardsville (USA). @@ -167,6 +188,7 @@ img: jireh.jpg - name: Marcelo Lynch + github: marcelolynch descr: | Marcelo is a senior engineer at the Mathlib Initiative, working on improving and maintaining ecosystem infrastructure. At previous positions, he has worked on @@ -174,6 +196,7 @@ img: marcelo.png - name: Heather Macbeth + github: hrmacbeth descr: | Heather is an Assistant Professor of Mathematics at Fordham University (USA). She did a PhD in differential geometry in Princeton. @@ -181,6 +204,7 @@ img: heather.jpeg - name: Patrick Massot + github: PatrickMassot descr: | Patrick is a Professor of Mathematics at Université Paris-Saclay at Orsay (France). He did a PhD in differential topology in @@ -188,12 +212,14 @@ img: patrick.png - name: Bhavik Mehta + github: b-mehta descr: | Bhavik is a PhD student in Mathematics at the University of Cambridge (UK). He has been formalizing mathematics since 2019. img: bhavik.jpg - name: Kyle Miller + github: kmill descr: | Kyle is a post-doc in mathematics at UC Santa Cruz and a research software engineer at the Lean FRO. @@ -202,6 +228,7 @@ img: kyle.jpg - name: Kim Morrison + github: kim-em descr: | Kim is a senior research engineer at the Lean Focused Research Organization. Their background is in mathematics, particularly topology and category theory. @@ -211,6 +238,7 @@ img: Kim.jpg - name: Oliver Nash + github: ocfnash descr: | Oliver is a mathematician who originally trained as a geometer. He is a senior manager at the Mathlib Initiative. He has @@ -222,15 +250,17 @@ img: ocfnash.png - name: Filippo A. E. Nuccio + github: faenuccio descr: | Filippo is an Associate Professor of Mathematics at Université Jean Monnet - in Saint-Étienne (France). He did a PhD in Algebraic Number Theory in Rome and + in Saint-Étienne (France). He did a PhD in Algebraic Number Theory in Rome and has been specialising in Iwasawa theory, alongside some archimedean and non-archimedean functional analysis. As an advocate for Open Science, he is a member of MathOA and of the French Committee for Open Science. He has been formalising mathematics since 2020. img: filippo.jpg - name: Joël Riou + github: joelriou descr: | Joël is an Associate Professor of Mathematics at Université Paris-Saclay at Orsay (France). He did a PhD in homotopy theory of schemes at @@ -238,12 +268,14 @@ img: joel.jpg - name: Michael Rothgang + github: grunweg descr: | Michael is a postdoc in the formalised mathematics group at the university of Bonn (Germany). He did a PhD in symplectic geometry at Humboldt-Universität zu Berlin. He has been formalising mathematics since 2023. - name: Damiano Testa + github: adomani descr: | Damiano is a reader in the Department of Mathematics at the University of Warwick (UK). He did a PhD in Algebraic Geometry at MIT (USA). @@ -251,6 +283,7 @@ img: damiano.jpeg - name: Adam Topaz + github: adamtopaz descr: | Adam is an Assistant Professor of Mathematics at the University of Alberta (Canada) and senior manager at the Mathlib Initiative. @@ -260,6 +293,7 @@ img: adam.jpg - name: Eric Wieser + github: eric-wieser descr: | Eric is a Senior Software Engineer on the AlphaProof team at Google DeepMind. He did a PhD formalizing Clifford algebras at the University of Cambridge (UK). @@ -268,6 +302,7 @@ img: eric.jpg - name: Leonardo de Moura + github: leodemoura descr: | Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS as well as Chief Architect and co-founder of the Lean FRO. @@ -277,14 +312,91 @@ img: leo.jpg - name: Wojciech Nawrocki + github: Vtec234 descr: | Wojciech is a PhD student at Carnegie Mellon University (USA). He has been contributing to open source software since 2016. img: wojciech.jpg - name: Sebastian Ullrich + github: Kha descr: | Sebastian is Head of Engineering and co-founder of the Lean FRO. He did a PhD on the Lean 4 frontend at Karlsruhe Institute of Technology (Germany). He has been working on Lean since 2015. img: sebastian.jpg +- + name: Aaron Anderson + github: awainverse +- + name: Alex J. Best + github: alexjbest +- + name: Andrew Yang + github: erdOne +- + name: Christian Merten + github: chrisflav +- + name: Dagur Asgeirsson + github: dagurtomas +- + name: David Loeffler + github: loefflerd +- + name: David Renshaw + github: dwrensha +- + name: Eric Rodriguez Boidi + github: ericrbg +- + name: Etienne Marion + github: EtienneC30 +- + name: Jon Eugster + github: joneugster +- + name: Joseph Myers + github: jsm28 +- + name: Jovan Gerbscheid + github: JovanGerb +- + name: Junyan Xu + github: alreadydone +- + name: Kexing Ying + github: kex-y +- + name: María Inés de Frutos-Fernández + github: mariainesdff +- + name: Michael Stoll + github: MichaelStollBayreuth +- + name: Miyahara Kō + github: Komyyy +- + name: Monica Omar + github: themathqueen +- + name: Moritz Doll + github: mcdoll +- + name: Robin Carlier + github: robin-carlier +- + name: Ruben Van de Velde + github: Ruben-VandeVelde +- + name: Thomas Browning + github: tb65536 +- + name: Thomas R. Murrills + github: thorimur +- + name: Yakov Pechersky + github: pechersky +- + name: Yaël Dillies + github: YaelDillies diff --git a/data/teams.yaml b/data/teams.yaml index d617688bca..90171c8b17 100644 --- a/data/teams.yaml +++ b/data/teams.yaml @@ -84,7 +84,7 @@ - Jon Eugster - Jovan Gerbscheid - Sébastien Gouëzel - - Markus Himmel + - Julia Markus Himmel - Simon Hudon - Yury G. Kudryashov - Robert Y. Lewis diff --git a/make_site.py b/make_site.py index e186ee50bc..e543278069 100755 --- a/make_site.py +++ b/make_site.py @@ -157,10 +157,20 @@ class People: name: str descr: str = '' img: str = '' + github: str = '' with (DATA/'people.yaml').open('r', encoding='utf-8') as m_file: peoples = {mtr['name']: People(**mtr) for mtr in yaml.safe_load(m_file)} +reviewer_data: dict = {} +_queueboard_url = os.environ.get('QUEUEBOARD_REVIEWER_INTERESTS_API_URL') +if _queueboard_url: + try: + with urllib.request.urlopen(_queueboard_url) as _resp: + reviewer_data = {r['github_login']: r for r in json.loads(_resp.read())['reviewers']} + except Exception as e: + print(f'Warning: could not fetch reviewer data: {e}', file=sys.stderr) + @dataclass class Team: name: str @@ -938,8 +948,9 @@ def read_md(src: str) -> str: env.filters={ 'url': url, 'md': render_markdown, 'tex': clean_tex } team_tpl = env.get_template('_team.html') for team in teams: + extra = {'reviewer_data': reviewer_data} if team.url == 'reviewers' else {} with (target/'teams'/(team.url + '.html')).open('w') as tgt_file: - team_tpl.stream(team=team, menus=menus, base_url=base_url).dump(tgt_file) + team_tpl.stream(team=team, menus=menus, base_url=base_url, **extra).dump(tgt_file) for folder in ['css', 'js', 'img', 'papers', str(target/'teams')]: diff --git a/scss/lean.scss b/scss/lean.scss index 924786a398..a299670cd3 100644 --- a/scss/lean.scss +++ b/scss/lean.scss @@ -120,6 +120,10 @@ pre { margin-top: unset; } +.reviewer-freeform > p:last-child { + margin-bottom: 0; +} + /* Theorem statements in the 100 theorem list: */ .doc-stmt { diff --git a/templates/_team.html b/templates/_team.html index 7721ef450b..ca3b33ffba 100644 --- a/templates/_team.html +++ b/templates/_team.html @@ -24,9 +24,19 @@
{{ member.name }}
{% else %} {% endif %} {% endblock %} -