Zulip Chat Archive

Stream: general

Topic: Web editor bug?


Heather Macbeth (Jan 29 2021 at 02:32):

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 (Jan 29 2021 at 02:40):

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 (Jan 29 2021 at 02:41):

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

Bryan Gin-ge Chen (Jan 29 2021 at 02:44):

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

Heather Macbeth (Jan 29 2021 at 02:49):

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 (Jan 29 2021 at 03:16):

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

Heather Macbeth (Jul 07 2021 at 01:21):

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 (Jul 07 2021 at 02:09):

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 (Jul 07 2021 at 02:14):

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

Bryan Gin-ge Chen (Jul 07 2021 at 02:21):

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.


Last updated: Dec 20 2023 at 11:08 UTC