Add setOptions#130
Open
augustepoiroux wants to merge 36 commits into
Open
Conversation
augustepoiroux
force-pushed
the
add-set-option
branch
from
aee691d to
14a7c0f
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
2 times, most recently
from
743d01d to
4899df4
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
3 times, most recently
from
1783393 to
527a29f
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
527a29f to
a8f7b0a
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
a8f7b0a to
ad2b221
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
ad2b221 to
3d8bbf7
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
3d8bbf7 to
94d4bfb
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
94d4bfb to
d3e7872
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
d3e7872 to
934dfdd
Compare
augustepoiroux
force-pushed
the
add-set-option
branch
from
934dfdd to
9672433
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