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: elaborate theorem bodies in parallel #5864

Draft
wants to merge 136 commits into
base: async-proofs-base
Choose a base branch
from
Draft

feat: elaborate theorem bodies in parallel #5864

wants to merge 136 commits into from

Commits on Jul 5, 2024

  1. feat: parallel linting

    @Kha
    Kha committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    35bbf70 View commit details
    Browse the repository at this point in the history

  2. fix

    @Kha
    Kha committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    2873696 View commit details
    Browse the repository at this point in the history

  3. hacky async kernel

    @Kha
    Kha committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    61f44b8 View commit details
    Browse the repository at this point in the history

Commits on Aug 1, 2024

  1. feat: disable old cmdline driver

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

  2. opt

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

  3. linearize

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

  4. single promise

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

  5. porgess

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

  6. add back

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

  7. restore server code

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

  8. more

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

  9. final

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

  10. more

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

  11. fix tests

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

Commits on Aug 2, 2024

  1. Merge branch 'het-snaps-cmdline' into async-kernel

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

  2. minimalSnapshots for async linting

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

  3. minimalSnapshots for async TC

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

  4. Merge branch 'master' of https://github.com/leanprover/lean4 into asy… 

    …nc-kernel
    @Kha
    Kha committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    2b7e048 View commit details
    Browse the repository at this point in the history

  5. fix

    @Kha
    Kha committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    3bd32d7 View commit details
    Browse the repository at this point in the history

  6. go back to theorems only for now

    @Kha
    Kha committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    17452b6 View commit details
    Browse the repository at this point in the history

  7. chore: update stage0

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

Commits on Aug 3, 2024

  1. oops

    @Kha
    Kha committed Aug 3, 2024
    Configuration menu
    Copy the full SHA
    3f3a03e View commit details
    Browse the repository at this point in the history

  2. disable async linting again

    @Kha
    Kha committed Aug 3, 2024
    Configuration menu
    Copy the full SHA
    23f61d1 View commit details
    Browse the repository at this point in the history

Commits on Aug 5, 2024

  1. Revert "chore: update stage0" 

    This reverts commit cc66581.
    @Kha
    Kha committed Aug 5, 2024
    Configuration menu
    Copy the full SHA
    64673a1 View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2024

  1. cleanup

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

Commits on Aug 7, 2024

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

    …nc-kernel
    @Kha
    Kha committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    bd3003d View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2024

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

    …nc-kernel
    @Kha
    Kha committed Aug 9, 2024
    Configuration menu
    Copy the full SHA
    0f5390d View commit details
    Browse the repository at this point in the history

  2. fix trace.Elab.snapshotTree

    @Kha
    Kha committed Aug 9, 2024
    Configuration menu
    Copy the full SHA
    5a20929 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' of https://github.com/leanprover/lean4 into asy… 

    …nc-kernel
    @Kha
    Kha committed Aug 9, 2024
    Configuration menu
    Copy the full SHA
    41a2b52 View commit details
    Browse the repository at this point in the history

  4. fix

    @Kha
    Kha committed Aug 9, 2024
    Configuration menu
    Copy the full SHA
    763cd89 View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2024

  1. chore: clean up cmdline snapshots logic

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

Commits on Aug 16, 2024

  1. Merge branch 'clean-cmdline-snaps' into async-kernel

    @Kha
    Kha committed Aug 16, 2024
    Configuration menu
    Copy the full SHA
    c1044f0 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/nightly-with-mathlib' into asy… 

    …nc-kernel
    @Kha
    Kha committed Aug 16, 2024
    Configuration menu
    Copy the full SHA
    c57f9dd View commit details
    Browse the repository at this point in the history

  3. clean up async promise use

    @Kha
    Kha committed Aug 16, 2024
    Configuration menu
    Copy the full SHA
    d07aad4 View commit details
    Browse the repository at this point in the history

  4. async kernel test

    @Kha
    Kha committed Aug 16, 2024
    Configuration menu
    Copy the full SHA
    5a2ee0f View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2024

  1. Kernel.Environment

    @Kha
    Kha committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    0477624 View commit details
    Browse the repository at this point in the history

Commits on Aug 23, 2024

  1. feat: split Lean.Kernel.Environment from Lean.Environment

    @Kha
    Kha committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    c06a09c View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2024

  1. fix deprecation

    @Kha
    Kha authored Aug 24, 2024
    Configuration menu
    Copy the full SHA
    2d84289 View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2024

  1. even more deprecations

    @Kha
    Kha committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    dd71ff9 View commit details
    Browse the repository at this point in the history

  2. fixes

    @Kha
    Kha committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    90d71bd View commit details
    Browse the repository at this point in the history

  3. make sure Kernel.isDefEq/whnf use native reduction

    @Kha
    Kha committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    4c5088e View commit details
    Browse the repository at this point in the history

  4. replace scope_native_reduce_fn with parameter passing

    @Kha
    Kha committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    89cfafe View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2024

  1. update documentation

    @Kha
    Kha committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    348b652 View commit details
    Browse the repository at this point in the history

  2. make setBase private again

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

  3. Merge branch 'kernel-env' into async-proofs

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

  4. correct prefix restriction, Prelude passes

    @Kha
    Kha committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    45ff446 View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2024

  1. progess

    @Kha
    Kha committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    efc0772 View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2024

  1. traces

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

Commits on Sep 3, 2024

  1. more

    @Kha
    Kha committed Sep 3, 2024
    Configuration menu
    Copy the full SHA
    da63230 View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2024

  1. feat: IO.getTID

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

  2. feat: thread support for trace.profiler.output

    @Kha
    Kha committed Sep 10, 2024
    Configuration menu
    Copy the full SHA
    651f043 View commit details
    Browse the repository at this point in the history

  3. feat: trace.profiler: unconditionally show times of trace classes ena… 

    …bled manually
    @Kha
    Kha committed Sep 10, 2024
    Configuration menu
    Copy the full SHA
    a4f5866 View commit details
    Browse the repository at this point in the history

  4. profile async proofs

    @Kha
    Kha committed Sep 10, 2024
    Configuration menu
    Copy the full SHA
    cdd3265 View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2024

  1. Elab.block

    @Kha
    Kha committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    556af07 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master' into async-proofs

    @Kha
    Kha committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    5ad9bb1 View commit details
    Browse the repository at this point in the history

Commits on Sep 12, 2024

  1. disable Lake

    @Kha
    Kha committed Sep 12, 2024
    Configuration menu
    Copy the full SHA
    e90f4de View commit details
    Browse the repository at this point in the history

  2. Elab.block cont

    @Kha
    Kha committed Sep 12, 2024
    Configuration menu
    Copy the full SHA
    a5bcd27 View commit details
    Browse the repository at this point in the history

  3. Avoid some getConstInfos

    @Kha
    Kha committed Sep 12, 2024
    Configuration menu
    Copy the full SHA
    ec67cdd View commit details
    Browse the repository at this point in the history

  4. AsyncConstantInfo

    @Kha
    Kha committed Sep 12, 2024
    Configuration menu
    Copy the full SHA
    c658d6b View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2024

  1. fix variable inclusion in async theorems

    @Kha
    Kha committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    367540a View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2024

  1. Merge branch 'upstream/master' into async-proofs

    @Kha
    Kha committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    5a52c3a View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2024

  1. fix

    @Kha
    Kha committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    47dd9d3 View commit details
    Browse the repository at this point in the history

Commits on Sep 18, 2024

  1. No async processing with late-triggering attrs

    @Kha
    Kha committed Sep 18, 2024
    Configuration menu
    Copy the full SHA
    459d0f7 View commit details
    Browse the repository at this point in the history

  2. Disable broken linter for now

    @Kha
    Kha committed Sep 18, 2024
    Configuration menu
    Copy the full SHA
    af65397 View commit details
    Browse the repository at this point in the history

  3. Global theorems

    @Kha
    Kha committed Sep 18, 2024
    Configuration menu
    Copy the full SHA
    5825496 View commit details
    Browse the repository at this point in the history

  4. fixes

    @Kha
    Kha committed Sep 18, 2024
    Configuration menu
    Copy the full SHA
    d8bc2cb View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2024

  1. more fixes

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

  2. more global theorems

    @Kha
    Kha committed Sep 19, 2024
    Configuration menu
    Copy the full SHA
    ac12529 View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2024

  1. even more global theorems

    @Kha
    Kha committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    22d939c View commit details
    Browse the repository at this point in the history

  2. this way around is faster

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

Commits on Sep 23, 2024

  1. perf: optimize unfolding constant lookup

    @Kha
    Kha committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    fc9b8a8 View commit details
    Browse the repository at this point in the history

  2. that's not unfoldable

    @Kha
    Kha committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    17dce45 View commit details
    Browse the repository at this point in the history

  3. optimize Environment.findX

    @Kha
    Kha committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    a1b2182 View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2024

  1. dbg_trace Environment.setState

    @Kha
    Kha committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    fee8e84 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2024

  1. chore: remove matcherExt cache

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

Commits on Oct 2, 2024

  1. revamp async env API

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

  2. Merge branch 'upstream/nightly-with-mathlib' into async-proofs

    @Kha
    Kha committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    4aa1d1f View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2024

  1. remove dbgStackTrace with panic

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    8615c7a View commit details
    Browse the repository at this point in the history

  2. merge push-xwrmupowysmt

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

  3. async matcherinfo

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

  4. async exportEntriesFn

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

  5. postponed compilation

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    4ea6136 View commit details
    Browse the repository at this point in the history

  6. fix async environment access

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    94d0973 View commit details
    Browse the repository at this point in the history

  7. support asyncly added axioms

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    4e17aa1 View commit details
    Browse the repository at this point in the history

  8. make all SimplePersistentEnvExts async-aware

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    9f79c9f View commit details
    Browse the repository at this point in the history

  9. fixes

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    5fd0b75 View commit details
    Browse the repository at this point in the history

  10. fix duplicate exports

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    29d5c91 View commit details
    Browse the repository at this point in the history

  11. enable realizations

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

  12. chore: remove dead code

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    995555d View commit details
    Browse the repository at this point in the history

  13. fix section var filtering with async theorems

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

  14. fix findNoAsyncTheorem

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    2fa3615 View commit details
    Browse the repository at this point in the history

  15. reserved name action for preprocessed simp theorems

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

  16. fix: add realized consts to env once

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

  17. allow realizations in aux decls ad-hoc

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    59bd509 View commit details
    Browse the repository at this point in the history

  18. consider private names in realization

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    45a06e3 View commit details
    Browse the repository at this point in the history

  19. further fix realizations

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

  20. use nicer Inhabited Expr value

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

  21. fix: realizing in async

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    28542b1 View commit details
    Browse the repository at this point in the history

  22. fix: exporting async

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

  23. allow async eqn cache accesses

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    053a863 View commit details
    Browse the repository at this point in the history

  24. fix: async thms turned into axioms

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

  25. force compile in evalExpr

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

  26. async reducible

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

  27. async header elab, avoids deadlock

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    409d54c View commit details
    Browse the repository at this point in the history

  28. enable realizations for inductive ctors

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

  29. fix async profile

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

  30. improve async profile

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    117ec10 View commit details
    Browse the repository at this point in the history

  31. unblock getEqnsFor on theorems

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    4111e49 View commit details
    Browse the repository at this point in the history

  32. Back out "chore: remove matcherExt cache" 

    This backs out commit b0c61fe.
    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    48e2778 View commit details
    Browse the repository at this point in the history

  33. allow matcherExt to work locally in async branches

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

  34. skip duplicate realized consts, will need to revisit

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

  35. merge master

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

  36. fix compiler setState

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    2bcacaa View commit details
    Browse the repository at this point in the history

  37. fix trace.Elab.snapshotTree

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

  38. fix auto params in async theorems

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

  39. fix async env lookup of hygiened names

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

  40. fix auto implicits in async thms

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    6351b67 View commit details
    Browse the repository at this point in the history

  41. fix open tactic in async theorems

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

  42. Environment.dbgFormatAsyncState

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

  43. isRflTheorem must realize missing constants

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

  44. comment findAsync? a bit

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    26fdd06 View commit details
    Browse the repository at this point in the history

  45. the crucial comment

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

  46. chore: allow specifying LEAN_OPTS in make invocation

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    518b9fb View commit details
    Browse the repository at this point in the history

  47. fix nested realization

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    371fe0c View commit details
    Browse the repository at this point in the history

  48. fix unresolved promise

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    6ae4c68 View commit details
    Browse the repository at this point in the history

  49. fix native_decide

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    4d634bf View commit details
    Browse the repository at this point in the history

  50. fix const realization deadlock

    @Kha
    Kha committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    5882aaa View commit details
    Browse the repository at this point in the history

  51. remove obsolete test

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

Commits on Oct 28, 2024

  1. restrict benchmarks for now due to missing -lLake

    @Kha
    Kha committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    91d036e View commit details
    Browse the repository at this point in the history

  2. realized constants should not report extensions

    @Kha
    Kha committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    0828604 View commit details
    Browse the repository at this point in the history

  3. fix addDecl (skipExisting := true)

    @Kha
    Kha committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    3319266 View commit details
    Browse the repository at this point in the history

  4. optimize setImportedEntries

    @Kha
    Kha committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    600b587 View commit details
    Browse the repository at this point in the history

  5. debugAsSorry doesn't seem necessary anymore

    @Kha
    Kha committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    e298702 View commit details
    Browse the repository at this point in the history

  6. work around gettid not being available on glibc 2.27 and macOS

    @Kha
    Kha committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    c11567b View commit details
    Browse the repository at this point in the history

  7. chore: update stage0

    @Kha
    Kha committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    4c90dee View commit details
    Browse the repository at this point in the history

  8. reactivate building Lake

    @Kha
    Kha committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    9727358 View commit details
    Browse the repository at this point in the history