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.

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

chore: modernize build instructions #4032

Merged
merged 10 commits into from
May 23, 2024
Merged

chore: modernize build instructions #4032

merged 10 commits into from
May 23, 2024

Conversation

Kha
Copy link
Member

@Kha Kha commented Apr 30, 2024

Use cmake --preset, adjust and document parallelism settings

@Kha Kha requested a review from semorrison as a code owner April 30, 2024 11:27
doc/make/index.md Outdated Show resolved Hide resolved
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 2, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented May 2, 2024

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6e731b4370000a8e7a5cfb675a7f3d7635d21f58 --onto 806e41151b6eb645e4ed5a40915b94b99f933564. (2024-05-02 12:42:50)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6e731b4370000a8e7a5cfb675a7f3d7635d21f58 --onto b470eb522bfd68ca96938c23f6a1bce79da8a99f. (2024-05-03 07:57:21)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6e731b4370000a8e7a5cfb675a7f3d7635d21f58 --onto ff37e5d512efcd3981290270a2fc3ecb100bbd0c. (2024-05-23 10:58:47)

@kmill
Copy link
Collaborator

kmill commented May 2, 2024

While we're editing doc/main/index.md, could we add an explanation to the top for who these instructions are for? At a Lean school I taught at, one of the participants' first inclinations as a hardcore Linux user was to get started with Mathematics in Lean by building Lean from source, which immediately caused issues, so it would be good to at least include a pointer to the quickstart. Here's a draft:

These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the Development Guide.

We strongly suggest that new users instead follow the Quickstart to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.

@Kha Kha enabled auto-merge May 3, 2024 07:40
@Kha Kha added this pull request to the merge queue May 3, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks May 3, 2024
@Kha Kha enabled auto-merge May 3, 2024 11:52
@Kha Kha added this pull request to the merge queue May 3, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks May 3, 2024
@Kha Kha added the full-ci label May 3, 2024
@Kha Kha enabled auto-merge May 3, 2024 13:15
@Kha Kha added this pull request to the merge queue May 23, 2024
Merged via the queue into leanprover:master with commit 73a0c73 May 23, 2024
21 checks passed
nomeata added a commit that referenced this pull request Jul 23, 2024
to include the check that the stage2 and stage3 are identical. This was
lost in #4032 it seems.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants