First user experience involves "Imports are out of date"
Maintainers usually reply within 1 day
@robsimmons is already working on this.
Since Oct 12, 2026.
Assessment
This issue has not been assessed yet.
Description
Steps to reproduce:
Go to https://lean.voidma.in/ for the first time, register with Github, choose the Mathematics in Lean project, navigate to some .lean file (e.g. S02_Induction_and_Recursion)
Observe:
"Imports are out of date and must be rebuilt; use the "Restart File" command in your editor."
This is relatively benign since the user can Restart File, but why should they have to?
Seems like this shouldn't happen if the template is set up properly and has all .oleans. Not sure about cause. Hypothesis: something misconfigured in this particular template.
- Dominant language
- TypeScript
- Stars
- 11
- Forks
- 1
- Avg merge
- 1d 11h
- Merged PRs (30d)
- 18
Getting set up
- Ships a Dockerfile or Docker Compose file
- No pull request template
- No contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean-workbench
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
leanprover/lean-workbench#54 ·
Maintainers usually reply within 1 day
-
Difficulty 4/5 3-5 days Newbie friendliness 45/100
leanprover/lean-workbench#188 ·
Maintainers usually reply within 1 day
-
Difficulty 3/5 1-2 days Newbie friendliness 55/100
leanprover/lean-workbench#184 ·
Maintainers usually reply within 1 day
-
Difficulty 5/5 Over a week Newbie friendliness 35/100
leanprover/lean-workbench#183 ·
Maintainers usually reply within 1 day
-
enhancement
Difficulty 4/5 3-5 days Newbie friendliness 48/100
leanprover/lean-workbench#182 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean-workbench
Similar issues
-
Sequências em espanhol: «Atualizado em», a aba «Fila» e o valor 'pause' ainda saem em portuguêsOpen
Difficulty 2/5 1-3 hours Newbie friendliness 77/100
melgarafael/DeskcommCRM#3104 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
Maintainers usually reply within 1 day
-
bug service: webapp
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
Ocelot-Social-Community/Ocelot-Social#10684 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
nicobailon/pi-subagents#2978 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
getsentry/sentry-conventions#732 · 1 comment ·
Maintainers usually reply within 1 day