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: snapshot trees and language processors #3014

Merged
merged 69 commits into from
Mar 14, 2024
Merged

feat: snapshot trees and language processors #3014

merged 69 commits into from
Mar 14, 2024

Commits on Oct 24, 2023

  1. feat: start integrating new snapshot types into cmdline driver

    @Kha
    Kha committed Oct 24, 2023
    Configuration menu
    Copy the full SHA
    ceeaff7 View commit details
    Browse the repository at this point in the history

  2. feat: switch Language to bundled, integrate into cmdline driver in … 

    …full
    @Kha
    Kha committed Oct 24, 2023
    Configuration menu
    Copy the full SHA
    d0fd3d7 View commit details
    Browse the repository at this point in the history

  3. fix: do not duplicate output

    @Kha
    Kha committed Oct 24, 2023
    Configuration menu
    Copy the full SHA
    152d594 View commit details
    Browse the repository at this point in the history

  4. fix: more output fixes

    @Kha
    Kha committed Oct 24, 2023
    Configuration menu
    Copy the full SHA
    a68d1c6 View commit details
    Browse the repository at this point in the history

Commits on Nov 3, 2023

  1. foo

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

Commits on Nov 9, 2023

  1. fix: run_task/deactivate_task race condition on m_imp->m_closure

    @Kha
    Kha committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    986d1c1 View commit details
    Browse the repository at this point in the history

Commits on Nov 10, 2023

  1. fix: re-read HTTP header when skipping notification in `Ipc.readRespo… 

    …nseAs`
    @Kha
    Kha committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    d2bf996 View commit details
    Browse the repository at this point in the history

  2. fix: debounce server status reporting

    @Kha
    Kha committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    23da22e View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2023

  1. fix: create snapshot for header in legacy adapter

    @Kha
    Kha committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    7932c0d View commit details
    Browse the repository at this point in the history

  2. fix: memoize cmdSnaps legacy adapter so getFinishedPrefix works a… 

    …s expected
    @Kha
    Kha committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    00e976c View commit details
    Browse the repository at this point in the history

  3. fix: waitForDiagnostics must wait on reporter task

    @Kha
    Kha committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    7c0ad9c View commit details
    Browse the repository at this point in the history

Commits on Nov 13, 2023

  1. doc: Language

    @Kha
    Kha committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    89383cf View commit details
    Browse the repository at this point in the history

Commits on Nov 25, 2023

  1. chore: rely on auto cancellation of reporter

    @Kha
    Kha committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    58c19d7 View commit details
    Browse the repository at this point in the history

Commits on Nov 27, 2023

  1. doc: more

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

Commits on Nov 29, 2023

  1. Merge remote-tracking branch 'upstream/master' into het-snaps

    @Kha
    Kha committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    1d547d3 View commit details
    Browse the repository at this point in the history

  2. import at most once per worker process

    @Kha
    Kha committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    0ce8fee View commit details
    Browse the repository at this point in the history

  3. fix test outputs

    @Kha
    Kha committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    4c9b70b View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2023

  1. File worker: synchronize output messages

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

Commits on Dec 1, 2023

  1. fix: incremental parsing

    @Kha
    Kha committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    8fff2e2 View commit details
    Browse the repository at this point in the history

  2. polish Lean.Language.Lean

    @Kha
    Kha committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    ca75ce2 View commit details
    Browse the repository at this point in the history

Commits on Dec 2, 2023

  1. better naming

    @Kha
    Kha committed Dec 2, 2023
    Configuration menu
    Copy the full SHA
    44cb1cc View commit details
    Browse the repository at this point in the history

  2. feat: synchronous execution of task continuations

    @Kha
    Kha committed Dec 2, 2023
    Configuration menu
    Copy the full SHA
    057184b View commit details
    Browse the repository at this point in the history

  3. synchronous fast forwarding in Lean processor

    @Kha
    Kha committed Dec 2, 2023
    Configuration menu
    Copy the full SHA
    0688e22 View commit details
    Browse the repository at this point in the history

  4. Bring back trust level

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

  5. Merge remote-tracking branch 'upstream/master' into het-snaps

    @Kha
    Kha committed Dec 2, 2023
    Configuration menu
    Copy the full SHA
    85a151b View commit details
    Browse the repository at this point in the history

  6. Try a shortcut

    @Kha
    Kha committed Dec 2, 2023
    Configuration menu
    Copy the full SHA
    3930e40 View commit details
    Browse the repository at this point in the history

  7. Remove redundant fields

    @Kha
    Kha committed Dec 2, 2023
    Configuration menu
    Copy the full SHA
    3b14598 View commit details
    Browse the repository at this point in the history

  8. doc

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

  9. code owner

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

  10. doc

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

Commits on Dec 8, 2023

  1. Merge remote-tracking branch 'upstream/master' into het-snaps

    @Kha
    Kha committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    edefad1 View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2023

  1. Fix explicit cancellation

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

Commits on Dec 13, 2023

  1. Adjust comments

    @Kha
    Kha committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    91e7e28 View commit details
    Browse the repository at this point in the history

  2. Cache interactive diagnostics properly

    @Kha
    Kha committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    33a9647 View commit details
    Browse the repository at this point in the history

  3. fix: clear progress notifications from lake in the end

    @Kha
    Kha committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    63a853e View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2023

  1. fix: header errors should be fatal

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

  2. Header diagnostics should cover the full file

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

  3. server reporting delay

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

  4. fix: header errors should be fatal

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

  5. Merge remote-tracking branch 'upstream/master' into het-snaps

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

  6. fix nondeterministic test output from new debouncing

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

  7. trigger CI

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

Commits on Dec 15, 2023

  1. trigger CI again

    @Kha
    Kha committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    078cef0 View commit details
    Browse the repository at this point in the history

  2. remove unused Option.forM, already in std4

    @Kha
    Kha committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    561f260 View commit details
    Browse the repository at this point in the history

Commits on Dec 18, 2023

  1. perf: keep alive old single-threaded cmdline driver for a little longer

    @Kha
    Kha committed Dec 18, 2023
    Configuration menu
    Copy the full SHA
    6ec85ec View commit details
    Browse the repository at this point in the history

Commits on Dec 21, 2023

  1. fix: don't report the same info tree twice

    @Kha
    Kha committed Dec 21, 2023
    Configuration menu
    Copy the full SHA
    b50c9e2 View commit details
    Browse the repository at this point in the history

  2. refactor: previous commit

    @Kha
    Kha committed Dec 21, 2023
    Configuration menu
    Copy the full SHA
    0480045 View commit details
    Browse the repository at this point in the history

  3. fix: report all info trees at ileanInfoFinal

    @Kha
    Kha committed Dec 21, 2023
    Configuration menu
    Copy the full SHA
    29b6612 View commit details
    Browse the repository at this point in the history

Commits on Jan 25, 2024

  1. refactor: move interactive diagnostics caching from Snapshot to fil… 

    …e worker

Avoids many problematic dependencies this early in the elab pipeline
    @Kha
    Kha committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    5de7e2c View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master' into het-snaps

    @Kha
    Kha committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    8b96499 View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2024

  1. clean up Lean.Server changes

    @Kha
    Kha committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    8bd6612 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2024

  1. refactor: remove unique ID indirection for interactive diagnostics ca… 

    …ching
    @Kha
    Kha committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    a0a65b6 View commit details
    Browse the repository at this point in the history

Commits on Feb 20, 2024

  1. Merge branch 'master' of https://github.com/leanprover/lean4 into het… 

    …-snaps
    @Kha
    Kha committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    25886d2 View commit details
    Browse the repository at this point in the history

  2. Remove Language interface for now, to be refined in hash-lang

    @Kha
    Kha committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    58d5b58 View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2024

  1. Move setup-file logic back from language processor into file worker

    @Kha
    Kha committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    4665f41 View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2024

  1. Run lake setup-file at most once per worker process, like before 

    In particular, we shouldn't run two instances in parallel. Would be nice
to find a better solution in the future.
    @Kha
    Kha committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    8830667 View commit details
    Browse the repository at this point in the history

Commits on Feb 29, 2024

  1. Merge remote-tracking branch 'upstream/master' into het-snaps

    @Kha
    Kha committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    91a0fee View commit details
    Browse the repository at this point in the history

  2. Fix cancellation in reportSnapshots

    @Kha
    Kha committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    2c99cf5 View commit details
    Browse the repository at this point in the history

Commits on Mar 1, 2024

  1. refactor: lazy initialization of request caches 

    This avoids an additional worker-language ping-pong of getting the
header environment into the worker as well as the startup delay
    @Kha
    Kha committed Mar 1, 2024
    Configuration menu
    Copy the full SHA
    44e5163 View commit details
    Browse the repository at this point in the history

  2. fix: traces on partial syntax

    @Kha
    Kha committed Mar 1, 2024
    Configuration menu
    Copy the full SHA
    ad6b225 View commit details
    Browse the repository at this point in the history

Commits on Mar 6, 2024

  1. address some comments

    @Kha
    Kha committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    2745d55 View commit details
    Browse the repository at this point in the history

Commits on Mar 7, 2024

  1. remove ElabTaskError.aborted

    @Kha
    Kha committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    491b125 View commit details
    Browse the repository at this point in the history

  2. address more comments

    @Kha
    Kha committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    c64fe35 View commit details
    Browse the repository at this point in the history

  3. address more comments

    @Kha
    Kha committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    34ff994 View commit details
    Browse the repository at this point in the history

  4. address even more comments

    @Kha
    Kha committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    27c90ba View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'upstream/master' into het-snaps

    @Kha
    Kha committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    959fa55 View commit details
    Browse the repository at this point in the history

Commits on Mar 8, 2024

  1. Replace silly critical section code with modifyGet

    @Kha
    Kha committed Mar 8, 2024
    Configuration menu
    Copy the full SHA
    f7db589 View commit details
    Browse the repository at this point in the history

  2. Address review comments

    @Kha
    Kha committed Mar 8, 2024
    Configuration menu
    Copy the full SHA
    c26033c View commit details
    Browse the repository at this point in the history

Commits on Mar 14, 2024

  1. Merge remote-tracking branch 'upstream/master' into het-snaps

    @Kha
    Kha committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    723910a View commit details
    Browse the repository at this point in the history