Code

feat: MiM PR report#15355

Code

Open

adomani wants to merge 166 commits intomasterleanprover-community/mathlib4:masterfrom adomani/yd_find_labelleanprover-community/mathlib4:adomani/yd_find_labelCopy head branch name to clipboard

+153

Commits

Commits on Jul 31, 2024

• add find_labels

  adomani

  committed
  73a6ac9

• excl

  adomani

  committed
  713a1b7

• token?

  adomani

  committed
  9d491b6

• format message

  adomani

  committed
  557f339

• move env

  adomani

  committed
  12eedba

• move env

  adomani

  committed
  f1c4c5a

• checkout master

  adomani

  committed
  c9af61b

• origin

  adomani

  committed
  3d7de17

• closed, rather than merged

  adomani

  committed
  f5dd7fe

• switch

  adomani

  committed
  a8e65ae

• print date

  adomani

  committed
  39e0a44

• fetch all

  adomani

  committed
  8139287

• checkout later

  adomani

  committed
  d6d231c

• no origin

  adomani

  committed
  ad54316

• do not filter much

  adomani

  committed
  23795f9

• print more

  adomani

  committed
  70b9390

• no pages

  adomani

  committed
  65d04a3

• closed

  adomani

  committed
  c6b67fa

• used commit numbers as limit

  adomani

  committed
  70857d0

• print title

  adomani

  committed
  fb27aa9

• print title really

  adomani

  committed
  ff57b09

• add number of commits

  adomani

  committed
  09aa949

• rename CI step

  adomani

  committed
  2310592

• starts with Merged by Bors

  adomani

  committed
  6f191db

• double the number of commits searched

  adomani

  committed
  d59268a

• one fewer day

  adomani

  committed
  7fde707

• two different dates

  adomani

  committed
  3bffc81

• print all prs

  adomani

  committed
  97a76bd

• do not print prs

  adomani

  committed
  2006ef2

• 15 days

  adomani

  committed
  5d29134

• number of commits

  adomani

  committed
  75f13fc

• commits in range

  adomani

  committed
  8bb1097

• prune

  adomani

  committed
  5c6aee8

• print closed

  adomani

  committed
  3cc12d2

• closedAt

  adomani

  committed
  da61d9e

• restore closed

  adomani

  committed
  3dc7d93

• range dates

  adomani

  committed
  3a5dc18

• closedAt

  adomani

  committed
  f33dcdd

• use search

  adomani

  committed
  5dd222c

• search closed

  adomani

  committed
  09c6474

• embed time in date

  adomani

  committed
  d7abc43

• remove printing of closed

  adomani

  committed
  d3eb548

• print repository name

  adomani

  committed
  bd13254

• use github API name for repo

  adomani

  committed
  1c6f6d4

• Capitalize Repository

  adomani

  committed
  88882ae

• base on master

  adomani

  committed
  0bbb60b

• report missed PRs

  adomani

  committed
  f010c98

• fix

  adomani

  committed
  5b022b3

• dates in git

  adomani

  committed
  941964b

• engulph

  adomani

  committed
  2d09ba4

• both

  adomani

  committed
  eaa5398

• better reporting

  adomani

  committed
  b3358bc

• formatting

  adomani

  committed
  53da2c4

• separation

  adomani

  committed
  f6fca31

• switch back to original branch

  adomani

  committed
  bf8180e

• switch back to original branch

  adomani

  committed
  e9e4bf5

• checkout

  adomani

  committed
  8bd675a

• print branch name

  adomani

  committed
  5424675

• use BRANCH_NAME as env variable

  adomani

  committed
  bee9d55

• create and remove temp files

  adomani

  committed
  9cfdaf1

• print PRs

  adomani

  committed
  d4c6b83

• refactor

  adomani

  committed
  2cb4eda

• start extracting dates and docs

  adomani

  committed
  53557ea

• extract reports

  adomani

  committed
  60d2eab

• checkout outside of the function

  adomani

  committed
  1b5ccb9

• run twice to cover a whole month

  adomani

  committed
  42cc216

• sort

  adomani

  committed
  360d2f8

• commit in range once

  adomani

  committed
  3c18faa

• print commits in range

  adomani

  committed
  93f0a06

• remove ticks

  adomani

  committed
  923b3ec

• abstract year month

  adomani

  committed
  3a56678

• recycle variable

  adomani

  committed
  a2e68b4

• local vars

  adomani

  committed
  5031911

• use current year and month

  adomani

  committed
  33af814

• Merge remote-tracking branch 'origin/master' into adomani/yd_find_label

  adomani

  committed
  9491ab2

• split differently

  adomani

  committed
  3126e27

Commits on Aug 1, 2024

• Merge remote-tracking branch 'origin/master' into adomani/yd_find_label

  adomani

  committed
  84da4d9

• print prs

  adomani

  committed
  48384c5

• filter better

  adomani

  committed
  ea56e86

• line breaks around reports

  adomani

  committed
  136093f

• omit unnecessary escaped double quote

  adomani

  committed
  0716baa

• clean up, add closed PR numbers

  adomani

  committed
  088dda3

• formatting

  adomani

  committed
  20ca0da

• fix line break

  adomani

  committed
  453aa58

• print date ranges once

  adomani

  committed
  59711cf

• formatting

  adomani

  committed
  50a23e7

• stars

  adomani

  committed
  da0203e

• months

  adomani

  committed
  9ed2e09

• next month

  adomani

  committed
  be8a01f

• pad exceptions, remove parens

  adomani

  committed
  6f0e59b

• Add question marks

  adomani

  committed
  7e51b99

• dates go up

  adomani

  committed
  a2f1a2f

• 14 15 16

  adomani

  committed
  93cf6c6

• recycle

  adomani

  committed
  f2143bd

• add authors

  adomani

  committed
  63f9835

• new workflow

  adomani

  committed
  6ec7878

• add author

  adomani

  committed
  a8a3b72

• ls

  adomani

  committed
  3c49769

• checkout the right file

  adomani

  committed
  edf76eb

• checkout origin

  adomani

  committed
  e122bc7

• clean up after new action

  adomani

  committed
  9702a0d

• print with authors

  adomani

  committed
  7f7c1ac

• really print

  adomani

  committed
  eb5ea7f

• single line

  adomani

  committed
  e96c649

• start/end _date

  adomani

  committed
  30d5331

• add author name

  adomani

  committed
  f6a6e0c

• do not print the json

  adomani

  committed
  de359dc

• remove "or null"

  adomani

  committed
  74bdcad

• PR number before author

  adomani

  committed
  5b37820

• rename job

  adomani

  committed
  d931fef

• reformat

  adomani

  committed
  4da1164

• print seen

  adomani

  committed
  9cf2cb1

• initialize seen, use seen[order[i]]

  adomani

  committed
  0888ad4

• header

  adomani

  committed
  23744bd

• maintain a comment

  adomani

  committed
  923dc2d

• embed title in message

  adomani

  committed
  4ded3a4

• printf

  adomani

  committed
  7e39374

• use secrets

  adomani

  committed
  c097f4d

• some formatting

  adomani

  committed
  8cc618d

• quotes

  adomani

  committed
  0ae1677

• end

  adomani

  committed
  8fedb6e

• remove filename

  adomani

  committed
  da8605f

• ticks

  adomani

  committed
  ed4c190

• line break

  adomani

  committed
  2eb5998

• close details

  adomani

  committed
  0a9b684

• remove initial PR

  adomani

  committed
  f3d0a09

• plural to singular

  adomani

  committed
  d4974a6

• spaces

  adomani

  committed
  96d44cb

• Update .github/workflows/monthly_pr_report.yaml

  adomani

  authored
  00bfe68

• Update .github/workflows/monthly_pr_report.yaml

  adomani

  authored
  12f5456

• Remove PR title

  adomani

  authored
  44864ff

Commits on Aug 2, 2024

• remove unneeded line breaks

  adomani

  authored
  2561ea3

• plural in all reports, format, remove initial </details>

  adomani

  committed
  96d685b

• shorten name

  adomani

  committed
  c66244f

• reports collapse

  adomani

  committed
  79be0eb

• details at end

  adomani

  committed
  6fdfb6e

• close details

  adomani

  committed
  d8ef988

• space out final details

  adomani

  committed
  a12987a

• one more line break

  adomani

  committed
  ed02c7c

• extract date

  adomani

  committed
  a62b5b4

• <Month> in mathlib

  adomani

  committed
  903b0b5

• show date

  adomani

  committed
  dd75942

• Do not continue on error

  adomani

  committed
  f6e8a4c

• pass the date

  adomani

  committed
  fcd366e

• do not print the date

  adomani

  committed
  6999c07

• start with comment

  adomani

  committed
  f2e8804

• environment variable

  adomani

  committed
  ac291ce

• quotes

  adomani

  committed
  f6847e5

• print more

  adomani

  committed
  26bea5d

• one line

  adomani

  committed
  353bec4

• another one line

  adomani

  committed
  eeb1318

• add permissions

  adomani

  committed
  a7d5a0f

• also pull request

  adomani

  committed
  a8825b5

• colon

  adomani

  committed
  e9a69c5

• comment better

  adomani

  committed
  ca6cf86

• hide pull request

  adomani

  committed
  a6eca90

• only if

  adomani

  committed
  09db8a7

• no name

  adomani

  committed
  b35c31e

• remove permissions

  adomani

  committed
  4176673

• run on any comment

  adomani

  committed
  47b6d65

• also deleted comments

  adomani

  committed
  90dc246

• cleanup comment

  adomani

  committed
  a761751

• two workflows: PR and comment

  adomani

  committed
  31112d7

• add explicit repository

  adomani

  committed
  c7967a9

• remove comment action

  adomani

  committed
  4261540

• use leanprover

  adomani

  committed
  acaf9f3