Web editor bug?

Stream: general

[Heather Macbeth]

The following snippet in the web editor

import measure_theory.lebesgue_measure

open measure_theory

variables {α β : Type*} [measurable_space α] [measurable_space β] (μ : measure α) (ν : measure β)

#check μ.prod ν

gives the error

invalid field notation, 'prod' is not a valid "field" because environment does not contain 'measure_theory.measure.prod'
  μ
which has type
  measure α

This goes away if one adds the extra import import measure_theory.prod. But it's strange, because

• measure_theory.prod is imported by something imported by measure_theory.lebesgue_measure, so I'd have thought the extra import wouldn't do anything
• the same snippet in VSCode gives me no errors.

[Bryan Gin-ge Chen]

Ah, it turns out the web editor hasn't been rebuilt in almost 3 weeks because GitHub turns off scheduled actions if the repo hasn't been modified in over 60 days. I've re-enabled the action and pushed a change so it should update shortly.

[Bryan Gin-ge Chen]

You can check the commit of mathlib it's using by clicking the purple ? button and scrolling to the bottom.

[Bryan Gin-ge Chen]

It looks like #5635 is the PR that changed the imports and that was only merged 15 days ago.

[Heather Macbeth]

Funny, I did check the last 24 hours of PRs for updates to measure theory, but it didn't occur to me that the bug might be an extension of the time window from 24 hours to 3 weeks :)

[Bryan Gin-ge Chen]

Looks like the build finished; if you refresh, the snippet should work now (after waiting for everything to re-download).

[Heather Macbeth]

Bryan Gin-ge Chen said:

Ah, it turns out the web editor hasn't been rebuilt in almost 3 weeks because GitHub turns off scheduled actions if the repo hasn't been modified in over 60 days. I've re-enabled the action and pushed a change so it should update shortly.

@Bryan Gin-ge Chen I believe the web editor scheduled action may have fallen into abeyance again. I don't know how to fix it, but probably you do? Last update was 20 days ago according to
https://github.com/leanprover-community/lean-web-editor/actions
and according to the mathlib version (apparently dc5d0c10).

[Bryan Gin-ge Chen]

Thanks for letting me know! For future reference, anyone with sufficient permissions (I think all mathlib maintainers should have this power) should be able to click on the "enable workflows" button (circled in red) to re-enable the workflow. I also just re-ran the last action for good measure to trigger an update. Screen-Shot-2021-07-06-at-10.07.07-PM.png

[Heather Macbeth]

Thanks for explaining! I'll try it myself next time :)

[Bryan Gin-ge Chen]

I get email notifications from GitHub before workflows like this are disabled in repos under my personal account, but I don't know to set up notifications for any of the repos in the leanprover-community organization.