Add setOptions#130
Open
augustepoiroux wants to merge 37 commits into
Open
Conversation
augustepoiroux
force-pushed
the
add-set-option
branch
from
October 14, 2025 20:23
aee691d to
14a7c0f
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
2 times, most recently
from
October 22, 2025 10:44
743d01d to
4899df4
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
3 times, most recently
from
November 19, 2025 11:00
1783393 to
527a29f
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
November 24, 2025 09:04
527a29f to
a8f7b0a
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
December 15, 2025 13:14
a8f7b0a to
ad2b221
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
January 29, 2026 12:34
ad2b221 to
3d8bbf7
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
February 22, 2026 17:16
3d8bbf7 to
94d4bfb
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
April 12, 2026 08:34
94d4bfb to
d3e7872
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
May 14, 2026 20:21
d3e7872 to
934dfdd
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
June 6, 2026 11:12
934dfdd to
9672433
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
July 16, 2026 20:52
9672433 to
20e0462
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add a
setOptionsparameter toCommandOption. This enables setting options for a specific Lean command.It has various use-cases. My favorite one is activating parallel elaboration to speed up processing:
{"cmd": "...", "setOptions":[[["Elab","async"],true]]}Note: this PR is built on top of #119