feature(coq): coq_version variable #5913
Closed
Conversation
This file contains 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
Signed-off-by: Rudi Grinberg <me@rgrinberg.com> ps-id: 1D3DEAE1-5C8A-4736-B72F-84E30AB1E036
ejgallego
reviewed
Jun 23, 2022
| @@ -46,6 +46,7 @@ module Var = struct | |||
| | Corrected_suffix | |||
| | Inline_tests | |||
| | Toolchain | |||
| | Coq_version | |||
There was a problem hiding this comment.
I guess we could add a parameter to this to have a %{coq:var} form, WDYT?
There was a problem hiding this comment.
@ejgallego I am currently working on a coq-config macro that will subsume all of this
ejgallego
reviewed
Jun 23, 2022
| let impl bin = | ||
| let* _ = Build_system.build_file bin in | ||
| let+ line = | ||
| Memo.of_non_reproducible_fiber |
There was a problem hiding this comment.
Does this mean that even within a single run we will re-exec?
All Coq config is deterministic, just set a Coq configure time.
There was a problem hiding this comment.
And guarantee to change only if the hash changes.
There was a problem hiding this comment.
It should only run once since it is memoed?
There was a problem hiding this comment.
Is memoed as non reproducible tho.
|
FTR I am still working on the coq-config thing, but I will be unable to work on it much this week. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
coq_versioncoq_configmacro