Skip to content

Conversation

@ayushman1210
Copy link

  • Added (workflow): .github/workflows/erdos-watcher.yml — GitHub Actions workflow that runs daily (and manually) to check Erdős problem pages, produce updates, create issues labeled erdos-update, and commit the last-seen dates file.
  • Added (script): .github/scripts/check_erdos_updates.py — Python checker that:
  • finds https://www.erdosproblems.com/ URLs in *.lean files,
  • fetches pages and extracts the "last edited / updated" date,
  • compares with the persisted dates and emits an updates.json list.
  • Supports --dry-run, --sample-html (test a local HTML file), and normal mode.
  • Added (state): .github/erdos-updates/erdos_dates.json — initial empty JSON used to persist last-seen dates.
  • Added (docs): .github/erdos-updates/README.md — usage notes and local testing instructions.
  • Added (deps): .github/erdos-updates/requirements.txt — Python packages needed by the checker.
  • Added (examples): .github/erdos-updates/examples/erdos_1.html — sample HTML for quick local testing.
  • Added (local automation): scripts/run_erdos_check.ps1 — PowerShell helper that creates a venv, (optionally) installs deps, and runs the checker in dry-run (default) or full mode (-FullRun).
  • Added (editor task): .vscode/tasks.json — VS Code tasks to run the dry-run or full checker from the editor.
  • Edited (script): .github/scripts/check_erdos_updates.py — improved date-extraction to prefer the site's "last edited" phrasing and added --dry-run / --sample-html modes (if you run the file now it will show results instead of immediately writing files).

@google-cla
Copy link

google-cla bot commented Nov 22, 2025

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

@seewoo5
Copy link
Collaborator

seewoo5 commented Dec 1, 2025

I'm not sure if I'm the best person to review this, at least I don't know if I can test it since I'm not a maintainer of this repo. At least it would be nice if you could tell how to test it ourselves.

@Paul-Lez Paul-Lez requested a review from mo271 December 2, 2025 14:41
@mo271
Copy link
Collaborator

mo271 commented Dec 2, 2025

Just a few first thoughts on this:

  • I think it would be easier to add something on the side of the (non-public?) repo that generates erdosproblems.com.
  • Instead of keeping state, we could write a simple script that
    (1) gets for each problem the state of each problem (open/solved) and
    (2) compares with our attribute for the main problem, which is typically names "erdos_$num".
    For (1), we can rely on https://github.com/teorth/erdosproblems/blob/main/data/problems.yaml, which is kept up-to-date, I believe.
    Wdyt?

@YaelDillies YaelDillies added the awaiting-author The author should answer a question or perform changes. Reply when done. label Dec 9, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author The author should answer a question or perform changes. Reply when done.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants