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: support Lake for building Lean core oleans #3886

Merged
merged 16 commits into from
Jun 13, 2024
Merged

feat: support Lake for building Lean core oleans #3886

merged 16 commits into from
Jun 13, 2024

Commits on Apr 11, 2024

  1. feat: lake builds for Lean parts 

    Add lakefile.toml in the right places so that working interactively on
the Lean repository will have the same features WRT the language
server as ordinary Lean projects.

This also requires adding Lake to stage0.
    @david-christiansen
    david-christiansen committed Apr 11, 2024
    Configuration menu
    Copy the full SHA
    7738e5d View commit details
    Browse the repository at this point in the history

Commits on Apr 12, 2024

  1. wip: chore: get stage0 update to also include Lake 

    (doesn't work yet, but we ran out of time pair programming)
    @david-christiansen
    david-christiansen committed Apr 12, 2024
    Configuration menu
    Copy the full SHA
    4022a35 View commit details
    Browse the repository at this point in the history

  2. Add missing file to commit

    @david-christiansen
    david-christiansen committed Apr 12, 2024
    Configuration menu
    Copy the full SHA
    67bc59f View commit details
    Browse the repository at this point in the history

Commits on May 2, 2024

  1. chore: revert stage0 change

    @tydeu
    tydeu committed May 2, 2024
    Configuration menu
    Copy the full SHA
    96a9473 View commit details
    Browse the repository at this point in the history

  2. feat: proper update-stage0 Lake

    @tydeu
    tydeu committed May 2, 2024
    Configuration menu
    Copy the full SHA
    584f02f View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into lake-build-core

    @tydeu
    tydeu committed May 2, 2024
    Configuration menu
    Copy the full SHA
    1796aa3 View commit details
    Browse the repository at this point in the history

  4. fix: update-stage0 commit stage/src/lake

    @tydeu
    tydeu committed May 2, 2024
    Configuration menu
    Copy the full SHA
    b0d2d53 View commit details
    Browse the repository at this point in the history

Commits on May 3, 2024

  1. chore: exclude stage0 Lake/Build from .gitignore

    @tydeu
    tydeu committed May 3, 2024
    Configuration menu
    Copy the full SHA
    f23ecda View commit details
    Browse the repository at this point in the history

  2. chore: update stage0

    @tydeu
    tydeu committed May 3, 2024
    Configuration menu
    Copy the full SHA
    0f6d797 View commit details
    Browse the repository at this point in the history

  3. chore: better build ignore

    @tydeu
    tydeu committed May 3, 2024
    Configuration menu
    Copy the full SHA
    e2fb637 View commit details
    Browse the repository at this point in the history

Commits on Jun 2, 2024

  1. chore: -DUSE_LAKE=ON CMake opt-in

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

Commits on Jun 11, 2024

  1. chore: revertt "update stage0" 

    This reverts commit 0f6d797.
    @tydeu
    tydeu committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    abfc66a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'nightly-with-mathlib' into lake-build-core

    @tydeu
    tydeu committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    76f7036 View commit details
    Browse the repository at this point in the history

  3. feat: configured lakefile.toml for tests & root + config touchups

    @tydeu
    tydeu committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    ce2e175 View commit details
    Browse the repository at this point in the history

  4. chore: rm stage0 leftover & ignore generated TOML in update-stage0

    @tydeu
    tydeu committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    a25f4b4 View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2024

  1. chore: add default value for USE_LAKE

    @tydeu
    tydeu authored Jun 13, 2024
    Configuration menu
    Copy the full SHA
    96ed62a View commit details
    Browse the repository at this point in the history