Zulip Chat Archive

Stream: PhysLean

Topic: The PhysLean café

Joseph Tooby-Smith (Apr 30 2025 at 14:20):

I'm not sure where this sits on the spectrum of bad to good ideas, but in the off-chance that it happens to be a good idea and useful:

Tomorrow (1st of May) between 2pm and 3pm UTC+0 I'm going to be working on PhysLean.

I'm going to post a zoom link here if anyone wants to join virtually, has any questions, or just wants to chat more generally about the project or just say hi. Nothing formal, and super unstructured - so if you want to join feel free to come and leave as you please (you don't need to let me know in advance). If no one turns up - that's fine by me - I'll just work anyway.

Jeremy Lindsay (May 01 2025 at 07:34):

can’t join tonight but would love to in future!!

Joseph Tooby-Smith (May 01 2025 at 13:52):

I'll be here for the next hour or so: https://eu01web.zoom.us/j/63343408776, if anyone feels inclined to join.

I'll make sure it happens earlier next time @Jeremy Lindsay :).

Joseph Tooby-Smith (May 19 2025 at 06:43):

I will do another one of these from 9-10am UTC+0 this Thursday (May 22nd). Will post zoom link here just before, anyone welcome to come and say hi.

Jeremy Lindsay (May 19 2025 at 06:48):

added to my calendar!

Joseph Tooby-Smith (May 22 2025 at 08:53):

Here is a zoom link: https://eu01web.zoom.us/j/61918225558. I'll be there for the next hour - anyone welcome to join.

Jeremy Lindsay (May 22 2025 at 08:54):

out bouldering with friends atm sorry :(

Joseph Tooby-Smith (May 22 2025 at 08:55):

No worries :)

Joseph Tooby-Smith (Jul 09 2025 at 13:38):

Haven't done one of these in a while so thought it may be worthwhile. So I'll be on zoom (will post a link here beforehand) for 1 hour starting . Anyone welcome to join if they want to chat about anything related to the project.

Joseph Tooby-Smith (Jul 10 2025 at 08:39):

Here is a link for this: https://eu01web.zoom.us/j/61929650908

Joseph Tooby-Smith (Aug 24 2025 at 07:06):

I'm going to do another one of these , I'll post a zoom link closer to the time.

Here is how it works: It lasts for 1 hour and is just a time for people to come and chat about PhysLean - there is no structure and any questions/topics/concerns are welcome. People can turn up anytime throughout the hour.

Shlok Vaibhav (Aug 25 2025 at 07:15):

I have a request regarding backend, can you demonstrate the steps listed for bump? Even as the steps are all literally listed in the GitHub issue yet I often get stuck in updating mathlib or physlean versions on my vscode and end up doing bruteforce reinstallation. I wanted to see how people do it properly in single shot, I'm doing something wrong

Shlok Vaibhav (Aug 25 2025 at 07:16):

I'm not sure how long the process takes and if it's feasible to show it in the session but decided to request

Joseph Tooby-Smith (Aug 25 2025 at 07:26):

So there are two different things here, there is:

  1. Updating PhysLean to a new version, as described by this issue. This is something only one person has to do.
  2. Once (1) has been done by someone, then everyone has to run 
lake exe cache get; lake build

on merging with master and redownloading PhysLean etc.

I usually end up doing (1) but haven't had chance yet this month as am currently hot-spotting of my phone, and dare not risk downloading Mathlib over 4G. (Recently moved into a new apartment and am not getting internet installed until early September :sad: ). But any help with this is much appreciated

Happy to go over either of these on Wednesday.

Joseph Tooby-Smith (Aug 25 2025 at 07:31):

(But everyone should only ever have to do (2) at most once a month).

Matteo Cipollina (Aug 25 2025 at 08:03):

If no one dares, I can give a try at bumping PhysLean, but I'd need you to pls guide me from the chat or DM in case I have any doubt:) I'll ping you when I get on it

Joseph Tooby-Smith (Aug 25 2025 at 08:09):

@Matteo Cipollina I would be happy to help guide! Maybe we could even just start by making a branch and draft pull-request for this, and use that PR to discuss.

Joseph Tooby-Smith (Aug 25 2025 at 09:07):

Actually, @Matteo Cipollina , I think I managed to safely download the new Mathlib - I forgot I could make two local copies of PhysLean so my old one would remain safe. So I can make the branch and PR. I'll see how far I get in fixing the errors that arise from updating mathlib

Tyler Josephson ⚛️ (Aug 26 2025 at 14:56):

Joseph Tooby-Smith said:

I'm going to do another one of these , I'll post a zoom link closer to the time.

I'll try to join! I won't be able to stop in until close to the end of the hour, though.

Joseph Tooby-Smith (Aug 27 2025 at 05:19):

Here is the zoom invite for this for later on today:

Zoom invite

Joseph Tooby-Smith (Aug 27 2025 at 11:53):

Starts in <10< 10 min

Joseph Tooby-Smith (Aug 27 2025 at 12:08):

Sorry I accidentally kicked everyone out :) - should be able to join again.

Joseph Tooby-Smith (Aug 27 2025 at 13:39):

@Tyler Josephson ⚛️ , here is a file containing examples of informal definitions and lemmas:

https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Cosmology/FLRW/Basic.lean

Joseph Tooby-Smith (Aug 27 2025 at 19:53):

In the discussion @Krishna Padmasola mentioned: https://www.youtube.com/@LeanFirstSteps
Just wanted to make sure this link doesn't get lost - and I think it would be awesome to have something like this dedicated to PhysLean.

Joseph Tooby-Smith (Aug 28 2025 at 13:39):

Also @Tyler Josephson ⚛️ Here is a tutorial on how to upload add informal results to PhysLean https://www.youtube.com/watch?v=f9kJyQs92TM

Joseph Tooby-Smith (Aug 29 2025 at 07:46):

One thing that came up in the last café was actionable points. I think a way that a computer scientist would keep track of these is via GitHub issues, but I think it is probably true that a lot of people, especially those not familiar with GitHub never check the issues. Thus, maybe it is best to make a thread here on this channel dedicated to actionable points with TODO lists like the following, and links to the GitHub issues. Thoughts?

Joseph Tooby-Smith (Aug 29 2025 at 07:46):

/todo Task list
Actionable point 1: Description of actionable point1
Actionable point 2: Description of actionable point2

Joseph Tooby-Smith (Aug 29 2025 at 07:47):

(don't know if everyone can edit this?)

Joseph Tooby-Smith (Sep 02 2025 at 13:02):

Ok, let's do another Cafe on ... I promise my internet will be better this time :slight_smile: .

I in particular want to carry on the conversation here, but also feel free to come along with anything else aswell.

Joseph Tooby-Smith (Sep 05 2025 at 15:17):

Zoom invitation for this, starting in ≤\le 1 hour - anyone welcome to join.

Zoom invitation

Tyler Josephson ⚛️ (Sep 05 2025 at 15:24):

Have a good chat! I have a dentist appointment but @Max Bobbin will be able to join.

Alfredo Moreira-Rosa (Sep 05 2025 at 17:02):

thank you for hosting this session. was really nice.

Joseph Tooby-Smith (Sep 05 2025 at 17:06):

Thanks for taking the time to join @ecyrbe !

Joseph Tooby-Smith (Oct 07 2025 at 07:51):

Hey, let's do another café at some point. You can use the link below to state your availability
https://www.when2meet.com/?32827566-1iAXG
which I will take into account when choosing a time :).

Alfredo Moreira-Rosa (Oct 07 2025 at 09:09):

Thanks, i'll check later this afternoon

Joseph Tooby-Smith (Oct 09 2025 at 15:34):

Ok, given the form, it seems the best time is: , so let us do then.

Tyler Josephson ⚛️ (Oct 13 2025 at 16:18):

Inspired by today's XKCD comic, I made a meme:

xkcdLean.png

Kevin Buzzard (Oct 13 2025 at 17:44):

Just to let you know, memes are not really acceptable on this forum (although I suspect that many of the people who would object to them are not subscribed to this channel).

Joseph Tooby-Smith (Oct 15 2025 at 12:18):

Zoom invitation for later today (anyone is welcome to attend):

Zoom Invitation

Joseph Tooby-Smith (Oct 15 2025 at 15:15):

(Starting now)

Joseph Tooby-Smith (Dec 03 2025 at 11:59):

It has been a while since we did one of these, so I'm going to host one on . Will post a Zoom link here closer to the time. Format is given in the first message of this thread.

Joseph Tooby-Smith (Dec 12 2025 at 08:41):

Zoom invitation for the PhysLean café happening later today:

Zoom Invitation

Joseph Tooby-Smith (Dec 12 2025 at 16:00):

Starting now

Last updated: Dec 20 2025 at 21:32 UTC