Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: run hint tactics in parallel #8435

Open
wants to merge 58 commits into
base: master
Choose a base branch
from
Open

feat: run hint tactics in parallel #8435

wants to merge 58 commits into from
+360 −26

Commits on Nov 12, 2023

  1. feat: the 'hint' tactic

    @semorrison
    semorrison committed Nov 12, 2023
    Configuration menu
    Copy the full SHA
    32e7f90 View commit details
    Browse the repository at this point in the history

  2. imports

    @semorrison
    semorrison committed Nov 12, 2023
    Configuration menu
    Copy the full SHA
    b00f84d View commit details
    Browse the repository at this point in the history

  3. linting

    @semorrison
    semorrison committed Nov 12, 2023
    Configuration menu
    Copy the full SHA
    446f173 View commit details
    Browse the repository at this point in the history

  4. linting

    @semorrison
    semorrison committed Nov 12, 2023
    Configuration menu
    Copy the full SHA
    a4c98a4 View commit details
    Browse the repository at this point in the history

  5. linter: relax, dude

    @semorrison
    semorrison committed Nov 12, 2023
    Configuration menu
    Copy the full SHA
    f23ebb5 View commit details
    Browse the repository at this point in the history

Commits on Nov 14, 2023

  1. Merge branch 'master' into hint_tactic

    @Komyyy
    Komyyy committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    3fa0c62 View commit details
    Browse the repository at this point in the history

  2. integrate

    @Komyyy
    Komyyy committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    8f09de2 View commit details
    Browse the repository at this point in the history

  3. merge; enable aesop

    @semorrison
    semorrison committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    90c6dfe View commit details
    Browse the repository at this point in the history

  4. trickery for monadic tasks

    @semorrison
    semorrison committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    69868ae View commit details
    Browse the repository at this point in the history

  5. Merge branch 'monadic_tasks' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    a3daba0 View commit details
    Browse the repository at this point in the history

  6. kawow

    @semorrison
    semorrison committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    cbda2f7 View commit details
    Browse the repository at this point in the history

Commits on Nov 15, 2023

  1. restore module doc

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    6dfdb9d View commit details
    Browse the repository at this point in the history

  2. remove #align_import

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    ec48fd0 View commit details
    Browse the repository at this point in the history

  3. use guard_msgs

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    d6a2989 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into monadic_tasks

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    0730fb5 View commit details
    Browse the repository at this point in the history

  5. cleanup

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    7d63f4e View commit details
    Browse the repository at this point in the history

  6. .

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    1d37b33 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'hint_tactic' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    67fa640 View commit details
    Browse the repository at this point in the history

  8. working

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    d1a7db2 View commit details
    Browse the repository at this point in the history

  9. merge master

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    1ac08bd View commit details
    Browse the repository at this point in the history

  10. .

    @semorrison
    semorrison committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    cc64973 View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2023

  1. Merge remote-tracking branch 'origin/master' into monadic_tasks

    @semorrison
    semorrison committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    2105ad9 View commit details
    Browse the repository at this point in the history

  2. cleanup

    @semorrison
    semorrison committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    5f16406 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'monadic_tasks' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    c1883f3 View commit details
    Browse the repository at this point in the history

  4. cleanup

    @semorrison
    semorrison committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    8d6cd12 View commit details
    Browse the repository at this point in the history

  5. merge master

    @semorrison
    semorrison committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    3324e07 View commit details
    Browse the repository at this point in the history

  6. import all

    @semorrison
    semorrison committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    10ba3e9 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/master' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    d1aaaa2 View commit details
    Browse the repository at this point in the history

  8. non-deterministic messages

    @semorrison
    semorrison committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    50828c6 View commit details
    Browse the repository at this point in the history

Commits on Nov 19, 2023

  1. Merge remote-tracking branch 'origin/master' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    a2efb42 View commit details
    Browse the repository at this point in the history

  2. now with task cancellation

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    7ee951d View commit details
    Browse the repository at this point in the history

  3. another test of the cancellation hook

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    54c5b79 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    1689861 View commit details
    Browse the repository at this point in the history

  5. .

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    a7d6308 View commit details
    Browse the repository at this point in the history

  6. update TODO

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    d6edaf7 View commit details
    Browse the repository at this point in the history

  7. slightly refactor

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    335a414 View commit details
    Browse the repository at this point in the history

  8. missing doc-string

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    4866672 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'origin/master' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    4cbc8bb View commit details
    Browse the repository at this point in the history

  10. chore: bump Std

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    b657004 View commit details
    Browse the repository at this point in the history

  11. remove upstreamed lemmas

    @semorrison
    semorrison committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    28f88a2 View commit details
    Browse the repository at this point in the history

Commits on Nov 20, 2023

  1. .

    @semorrison
    semorrison committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    f6c8115 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'bump_std18' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    02ab251 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    f5d9e00 View commit details
    Browse the repository at this point in the history

Commits on Nov 26, 2023

  1. Apply suggestions from code review 

    Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
    @semorrison @thorimur
    semorrison and thorimur committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    01a40a6 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    6f1826b View commit details
    Browse the repository at this point in the history

Commits on Nov 27, 2023

  1. use high priority tasks for map steps

    @semorrison
    semorrison committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    831a3de View commit details
    Browse the repository at this point in the history

  2. chore: reduce imports of Data.List.Defs

    @semorrison
    semorrison committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    e0e99b4 View commit details
    Browse the repository at this point in the history

  3. import all

    @semorrison
    semorrison committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    8213334 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'data_list_defs' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    707e2fa View commit details
    Browse the repository at this point in the history

Commits on Nov 28, 2023

  1. fix test

    @semorrison
    semorrison committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    f59153b View commit details
    Browse the repository at this point in the history

  2. Merge branch 'data_list_defs' into hint_tactic_parallel

    @semorrison
    semorrison committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    aeba8d0 View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2023

  1. Update Mathlib/Data/List/BigOperators/Defs.lean 

    Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
    @semorrison @thorimur
    semorrison and thorimur committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    d9b197e View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2023

  1. fix test (congr.lean)

    @thorimur
    thorimur committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    a0e9e06 View commit details
    Browse the repository at this point in the history

  2. fix rel_prod type signature 

    * was inferring `Nat` as arguments for `R`
* note that `[Monoid M]`/`[Monoid N]` are variables
    @thorimur
    thorimur committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    b970465 View commit details
    Browse the repository at this point in the history

Commits on Dec 10, 2023

  1. remove autoImplicit

    @semorrison
    semorrison committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    2d708e0 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'data_list_defs' into hint_tactic_parallel

    @semorrison
    semorrison committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    25c3b1b View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2023

  1. Merge remote-tracking branch 'origin/master' into hint_tactic_parallel

    @semorrison
    semorrison committed Dec 12, 2023
    Configuration menu
    Copy the full SHA
    b98ab8b View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2023

  1. fix

    @semorrison
    semorrison committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    c78a96f View commit details
    Browse the repository at this point in the history