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

fix: lake: save config trace before elab #3069

Merged
merged 1 commit into from
Dec 19, 2023

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Dec 13, 2023

Lake will now delete any old .olean and save the new trace before elaborating a configuration file. This will enable the automatic reconfiguration of the file if elaboration fails.

Fixes an issue that was discussed on Zulip.

@tydeu tydeu added the will-merge-soon …unless someone speaks up label Dec 15, 2023
@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 Dec 15, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Dec 15, 2023

  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-15 21:08:39)
  • ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-19' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-19 10:20:32)

@tydeu tydeu added the full-ci label Dec 15, 2023
@tydeu tydeu force-pushed the lake/pretrace-config branch 2 times, most recently from e857c11 to 0d613ab Compare December 19, 2023 09:35
@tydeu tydeu force-pushed the lake/pretrace-config branch from 0d613ab to a69b64b Compare December 19, 2023 17:16
@tydeu tydeu added this pull request to the merge queue Dec 19, 2023
Merged via the queue into leanprover:master with commit eb432cd Dec 19, 2023
17 checks passed
@tydeu tydeu deleted the lake/pretrace-config branch December 20, 2023 03:49
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 will-merge-soon …unless someone speaks up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants