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

fix: use dsimp to remove abstraction overhead of our parsing stage #225

Merged
merged 75 commits into from
May 13, 2024
Merged

fix: use dsimp to remove abstraction overhead of our parsing stage #225

merged 75 commits into from
May 13, 2024

Commits on Apr 15, 2024

  1. feat: make our generalize trick work for arbitrary number of variables

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    5b9412e View commit details
    Browse the repository at this point in the history

  2. reduce test case for broken alive autogenerated

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    9504a09 View commit details
    Browse the repository at this point in the history

  3. Further reduction

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    dfd232d View commit details
    Browse the repository at this point in the history

  4. Further reduction

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    ca96cec View commit details
    Browse the repository at this point in the history

  5. WIP

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    733f053 View commit details
    Browse the repository at this point in the history

  6. test

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    190e38b View commit details
    Browse the repository at this point in the history

  7. Add back bug

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    f354eaf View commit details
    Browse the repository at this point in the history

  8. Further reduce bug

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    1ac1adf View commit details
    Browse the repository at this point in the history

  9. Proof equivalence

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    ad67b68 View commit details
    Browse the repository at this point in the history

  10. WIP

    @tobiasgrosser
    tobiasgrosser committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    890125e View commit details
    Browse the repository at this point in the history

Commits on Apr 16, 2024

  1. WIP

    @tobiasgrosser
    tobiasgrosser committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    261c197 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    b4077e4 View commit details
    Browse the repository at this point in the history

  3. WIP

    @tobiasgrosser
    tobiasgrosser committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    0c80d09 View commit details
    Browse the repository at this point in the history

  4. Test

    @tobiasgrosser
    tobiasgrosser committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    97d266e View commit details
    Browse the repository at this point in the history

Commits on Apr 17, 2024

  1. use rw only

    @tobiasgrosser
    tobiasgrosser committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    4f56135 View commit details
    Browse the repository at this point in the history

  2. We need more simps than I thought

    @tobiasgrosser
    tobiasgrosser committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    5e7e64d View commit details
    Browse the repository at this point in the history

Commits on Apr 18, 2024

  1. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @bollu
    bollu committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    38574a1 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    228de9c View commit details
    Browse the repository at this point in the history

  3. Fix CI

    @tobiasgrosser
    tobiasgrosser committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    6df32d4 View commit details
    Browse the repository at this point in the history

Commits on Apr 19, 2024

  1. feat: add RegionSignature.map

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    a41cf48 View commit details
    Browse the repository at this point in the history

  2. feat: add Signature.map

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    d34700b View commit details
    Browse the repository at this point in the history

  3. chore: change from <$> to map function

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    04ea281 View commit details
    Browse the repository at this point in the history

  4. chore: change to Ctxt.map

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    7b99d80 View commit details
    Browse the repository at this point in the history

  5. chore: spell out Signature.map

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    5117e61 View commit details
    Browse the repository at this point in the history

  6. chore: spell out Signature.map

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    de1d636 View commit details
    Browse the repository at this point in the history

  7. feat, wip: get tactic sequence to simplify instantiation

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    1ce53bb View commit details
    Browse the repository at this point in the history

  8. feat: remove deliberate simp-punning between ctxt and list

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    dfbd397 View commit details
    Browse the repository at this point in the history

  9. write slightly higher level lemmas about simplifying instantiates

    @bollu
    bollu committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    bfdf58b View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2024

  1. feat: add simp set and notation for simplifying proof state of theore… 

    …m ok
    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    d21431d View commit details
    Browse the repository at this point in the history

  2. feat: Valuation.snoc_zero to defeq

    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    a30bde4 View commit details
    Browse the repository at this point in the history

  3. feat: make theorems in ErasedContext have rfl proof

    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    c86954f View commit details
    Browse the repository at this point in the history

  4. feat: add comment about Fin and simp normal form

    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    080f69c View commit details
    Browse the repository at this point in the history

  5. feat: add pairing session simp-set 

    We now have a simp set that successfully simplifies
programs
    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    bfa8ec5 View commit details
    Browse the repository at this point in the history

  6. feat: disable Com.Refinement since we invoke it previously in Bug

    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    302b0ac View commit details
    Browse the repository at this point in the history

  7. chore: move code from Bug.lean into a simp_alive_meta tactic. 

    Note that `theorem ok` is now proven via `simp_alive_peephole`,
while `theorem broken` is still not.
    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    af495c1 View commit details
    Browse the repository at this point in the history

  8. feat: add ConcreteOrMVar.instantiate_concrete_eq into simp set. 

    For unclear reasons, this needs a (config := {autoUnfold := true})
to be enabled.

We don't know how to log what changed, so we asked on Zulip.
    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    f5188f8 View commit details
    Browse the repository at this point in the history

  9. feat: change tactic to 'failIfUnchanged := false'

    @bollu
    bollu committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    8f7935b View commit details
    Browse the repository at this point in the history

  10. Make AliveAutoGenerated.lean compile

    @tobiasgrosser
    tobiasgrosser committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    4f7ae21 View commit details
    Browse the repository at this point in the history

  11. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    c3f0ea3 View commit details
    Browse the repository at this point in the history

  12. chore: drop unnecessary delta in Core/Tactic

    @tobiasgrosser
    tobiasgrosser committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    8b4a35a View commit details
    Browse the repository at this point in the history

Commits on Apr 23, 2024

  1. chore: drop HVector stuff that is unneeded

    @tobiasgrosser
    tobiasgrosser committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    a0036fd View commit details
    Browse the repository at this point in the history

  2. chore: drop unnecessary changes

    @tobiasgrosser
    tobiasgrosser committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    ab3cc7e View commit details
    Browse the repository at this point in the history

  3. chore: drop change_mlir_context

    @tobiasgrosser
    tobiasgrosser committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    a83ef85 View commit details
    Browse the repository at this point in the history

  4. chore: drop redundant implementation of instantiate_mvar_zero

    @tobiasgrosser
    tobiasgrosser committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    50eb835 View commit details
    Browse the repository at this point in the history

  5. chore: drop by for rfl

    @tobiasgrosser
    tobiasgrosser committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    c1c03b9 View commit details
    Browse the repository at this point in the history

  6. Revert "chore: drop redundant implementation of instantiate_mvar_zero" 

    This reverts commit 50eb835.
    @tobiasgrosser
    tobiasgrosser committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    df0387e View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    48e5c72 View commit details
    Browse the repository at this point in the history

Commits on May 7, 2024

  1. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed May 7, 2024
    Configuration menu
    Copy the full SHA
    8e61a0b View commit details
    Browse the repository at this point in the history

Commits on May 9, 2024

  1. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed May 9, 2024
    Configuration menu
    Copy the full SHA
    d163848 View commit details
    Browse the repository at this point in the history

  2. Update to master

    @tobiasgrosser
    tobiasgrosser committed May 9, 2024
    Configuration menu
    Copy the full SHA
    f32d4eb View commit details
    Browse the repository at this point in the history

  3. Add back change_mlir_context

    @tobiasgrosser
    tobiasgrosser committed May 9, 2024
    Configuration menu
    Copy the full SHA
    0a3ead9 View commit details
    Browse the repository at this point in the history

  4. chore: split CI in fast and slow

    @tobiasgrosser
    tobiasgrosser committed May 9, 2024
    Configuration menu
    Copy the full SHA
    734ffc6 View commit details
    Browse the repository at this point in the history

  5. Make it work?

    @tobiasgrosser
    tobiasgrosser committed May 9, 2024
    Configuration menu
    Copy the full SHA
    061ab7f View commit details
    Browse the repository at this point in the history

  6. WIP

    @tobiasgrosser
    tobiasgrosser committed May 9, 2024
    Configuration menu
    Copy the full SHA
    4c0f17e View commit details
    Browse the repository at this point in the history

  7. green?

    @tobiasgrosser
    tobiasgrosser committed May 9, 2024
    Configuration menu
    Copy the full SHA
    3355c77 View commit details
    Browse the repository at this point in the history

Commits on May 10, 2024

  1. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    04fa040 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    f6fec7e View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    84af681 View commit details
    Browse the repository at this point in the history

  4. fix tactic

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    f1c128e View commit details
    Browse the repository at this point in the history

  5. remove old code that is not necessarily needed

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    95e5b14 View commit details
    Browse the repository at this point in the history

  6. reduce diff

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    9591bea View commit details
    Browse the repository at this point in the history

  7. reduce diff

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    f8b8bf5 View commit details
    Browse the repository at this point in the history

  8. reduce diff

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    dcd26b7 View commit details
    Browse the repository at this point in the history

  9. simplify the proof

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    188732c View commit details
    Browse the repository at this point in the history

  10. simplify the proof

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    7c5e568 View commit details
    Browse the repository at this point in the history

  11. simplify the proof

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    3340279 View commit details
    Browse the repository at this point in the history

  12. simplify the proof

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    ba4ded3 View commit details
    Browse the repository at this point in the history

  13. simplify the proof

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    92199de View commit details
    Browse the repository at this point in the history

  14. Drop the bug

    @tobiasgrosser
    tobiasgrosser committed May 10, 2024
    Configuration menu
    Copy the full SHA
    5e745c8 View commit details
    Browse the repository at this point in the history

Commits on May 11, 2024

  1. fix: simplify double-sorry

    @tobiasgrosser
    tobiasgrosser committed May 11, 2024
    Configuration menu
    Copy the full SHA
    81d1d47 View commit details
    Browse the repository at this point in the history

  2. fix: comma

    @tobiasgrosser
    tobiasgrosser committed May 11, 2024
    Configuration menu
    Copy the full SHA
    04aa94e View commit details
    Browse the repository at this point in the history

  3. remove wip comments

    @tobiasgrosser
    tobiasgrosser committed May 11, 2024
    Configuration menu
    Copy the full SHA
    9f13bf7 View commit details
    Browse the repository at this point in the history

  4. fix formatting

    @tobiasgrosser
    tobiasgrosser committed May 11, 2024
    Configuration menu
    Copy the full SHA
    1305378 View commit details
    Browse the repository at this point in the history

  5. Update SSA/Projects/InstCombine/Tactic.lean

    @tobiasgrosser
    tobiasgrosser authored May 11, 2024
    Configuration menu
    Copy the full SHA
    1ad642b View commit details
    Browse the repository at this point in the history

Commits on May 13, 2024

  1. Merge remote-tracking branch 'origin/main' into broken_alive_autogene… 

    …rated
    @tobiasgrosser
    tobiasgrosser committed May 13, 2024
    Configuration menu
    Copy the full SHA
    aba4e83 View commit details
    Browse the repository at this point in the history