[coq_rules] Refactor boot flag handling.#5866
Merged
ejgallego merged 3 commits intoocaml:mainfrom Jun 21, 2022
Merged
Conversation
5411b54 to
19adc78
Compare
Collaborator
Author
|
Actually let me enforce that last invariant. |
Alizter
reviewed
Jun 11, 2022
19adc78 to
e1c2d47
Compare
f1165e9 to
8015d8e
Compare
Alizter
reviewed
Jun 11, 2022
rgrinberg
reviewed
Jun 11, 2022
9c54c71 to
d9a9564
Compare
Collaborator
Author
|
I think this is ready, let me know folks if you have any further comment. |
Collaborator
|
@ejgallego Shouldn't you rebase rather than merge? |
Collaborator
Author
|
@Alizter that was github's auto-stuff , let me see. |
8eb207f to
dcf7510
Compare
Instead of doing an special case in Coq_lib, we handle the boot library directly in the flags. This allows us to handle coqdoc-specific flags related to `-boot`, and is more in line with what we expect the future theory model will be. Downside is that `-boot` is now not included in the closure dep, but that seems fine, actually we should forbid `(boot)` libraries from declaring `(theories ...)` deps, but as we are getting rid of it eventually maybe it is not worth the effort. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
dcf7510 to
71a5da8
Compare
Collaborator
Author
|
Ping @Alizter @rgrinberg , or can I just merge? |
Collaborator
|
@ejgallego I'll take another look. |
Alizter
approved these changes
Jun 21, 2022
Collaborator
|
@ejgallego Looks good to me |
40 tasks
Collaborator
Author
|
This PR has a bug 🤦 , we forgot to include the ML flags of the boot theory. Will fix |
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 27, 2022
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 27, 2022
Should fix a bug introduced in ocaml#5866 , the handling of boot Coq lib really needs to be done at the top level as coqdep's `source_rule` etc... need to be aware of it.
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 27, 2022
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 27, 2022
Should fix a bug introduced in ocaml#5866 , the handling of boot Coq lib really needs to be done at the top level as coqdep's `source_rule` etc... need to be aware of it.
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 27, 2022
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 27, 2022
Should fix a bug introduced in ocaml#5866 , the handling of boot Coq lib really needs to be done at the top level as coqdep's `source_rule` etc... need to be aware of it.
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 27, 2022
…oduced in ocaml#5866) Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 27, 2022
Should fix a bug introduced in ocaml#5866 , the handling of boot Coq lib really needs to be done at the top level as coqdep's `source_rule` etc... need to be aware of it. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Sep 28, 2022
Should fix a bug introduced in ocaml#5866 , the handling of boot Coq lib really needs to be done at the top level as coqdep's `source_rule` etc... need to be aware of it. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego
added a commit
that referenced
this pull request
Sep 28, 2022
…oduced in #5866) Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego
added a commit
that referenced
this pull request
Sep 28, 2022
Should fix a bug introduced in #5866 , the handling of boot Coq lib really needs to be done at the top level as coqdep's `source_rule` etc... need to be aware of it. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
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
3 participants
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.
Instead of doing an special case in Coq_lib, we handle the boot
library directly in the flags.
This allows us to handle coqdoc-specific flags related to
-boot, andis more in line with what we expect the future theory model will be.
Downside is that
-bootis now not included in the closure dep, butthat seems fine, actually we should forbid
(boot)libraries fromdeclaring
(theories ...)deps, but as we are getting rid of iteventually maybe it is not worth the effort.