[build] Consolidation of build system infrastructure#15560
Merged
coqbot-app[bot] merged 2 commits intorocq-prover:masterfrom Jun 28, 2022
Merged
[build] Consolidation of build system infrastructure#15560coqbot-app[bot] merged 2 commits intorocq-prover:masterfrom
coqbot-app[bot] merged 2 commits intorocq-prover:masterfrom
Conversation
ejgallego
added
kind: cleanup
This comment was marked as outdated.
This comment was marked as outdated.
ejgallego
force-pushed
the
build+coq_dune
branch
5 times, most recently
from
9ca3bd0 to
9b90a48
Compare
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
ejgallego
force-pushed
the
build+coq_dune
branch
from
9b90a48 to
a6770c5
Compare
This comment was marked as outdated.
This comment was marked as outdated.
SkySkimmer
force-pushed
the
build+coq_dune
branch
from
9e506d5 to
6a6cdee
Compare
This comment was marked as resolved.
This comment was marked as resolved.
github-actions
Bot
added
the
needs: rebase
Contributor
|
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed. |
This comment was marked as outdated.
This comment was marked as outdated.
coqbot-app
Bot
removed
needs: rebase
ejgallego
force-pushed
the
build+coq_dune
branch
from
6a6cdee to
23ca618
Compare
ejgallego
force-pushed
the
build+coq_dune
branch
from
23ca618 to
e7eaae5
Compare
This comment was marked as resolved.
This comment was marked as resolved.
ejgallego
force-pushed
the
build+coq_dune
branch
from
4dbab18 to
85e39d6
Compare
Alizter
reviewed
Jun 24, 2022
Contributor
Author
|
@erikmd yes, I forgot depopts obviously!!! I always get confused. |
Contributor
|
Good catch @erikmd! |
Contributor
|
🏁 Bench results: 🐢 Top 25 slow downs🐇 Top 25 speed ups |
Contributor
@ejgallego could you please push another commit that adds in Then, I'll re-trigger the build of |
Contributor
Author
|
Done thanks @erikmd , I added it to
I've also updated the |
Contributor
|
@ejgallego thanks!
I wouldn't say that exactly, because
So even if But regarding |
Contributor
Author
Yes I think you are right, in the sense that it would be possible for coq-core to actually not depend on coq-native (for example if we would use coqnative is too slow tho so I didn't enable it by default. |
Contributor
@ejgallego can you be more specific? do you still confirm that when |
Contributor
|
@Alizter you removed the label
|
Contributor
|
@erikmd I removed the "needs: fixing" label since I added it about the native compilation and that issue specifically has been fixed. I did say I would possibly merge today, however I have decided not to just yet until all these details are fully resolved. |
Contributor
@erikmd : yes, c.f., the |
We replace both the dune-based `(coq.theory ...)` and the "legacy" make-based build systems for .vo into a single setup, based on our own Dune rule generation using a coq_dune tool. This requires a bootstrap process to generate the rule files, until Dune gets support for `(include stdlib_rules.sexp)` (hopefully soon) By disabling the `(coq.theory ...)` stanza on `theories/dune` we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), this is not really used as of today so we are fine. This should supersede rocq-prover#15545 , avoid many troubles that rocq-prover#15220 had to endure, and close rocq-prover#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. At some point some of this code should be moved to a common loadpath library to compute native target names, and maybe some other stuff. Some other changes in `Nativelib`: - We fix incorrect early initialization of `Boot.Env.t` - We extend the path passed to the ocamlc compiler as to search for files in the dir where the .vo is. That can be reverted if we pass all the explicit `-nI` paths. We could just get rid of `.coq-native`, additionally.
coqdep was using a mixed separator scheme on Windows, to avoid makefile quoting bugs. As we want to support non-cygwin envs, we disable this hack for the Dune build, thus using paths fully native to windows.
Contributor
|
Merging after rocq-community/docker-coq#50 |
Contributor
|
Merging when green |
Contributor
|
@coqbot merge now |
Contributor
|
@Alizter: Please take care of the following overlays:
|
1 task
This was referenced Jul 11, 2022
1 task
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
12 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.
We replace both the dune-based
(coq.theory ...)and the "legacy"make-based build systems for .vo into a single setup, based on our own
Dune rule generation using a coq_dune tool.
This requires a bootstrap process to generate the rule files, until
Dune gets support for
(include stdlib_rules.sexp)(hopefully soon)By disabling the
(coq.theory ...)stanza ontheories/dunewe losecompositional building of .vo libs (for OCaml we are still fine, which
our main use case), this is not really used as of today so we are
fine.
This should supersede #15545 , avoid many troubles that #15220 had
to endure.
PRs for Docker and OPAM that need to be merged after this:
List of relevant bugs that should be closed by this PR:
-jwhen invoking dune #15730make test-suitefails #14342native_compute#8860make helpis very incomplete #7208Legacy makefiles will be removed in the next commit, closing a few
more bugs hopefully.
Todos are:
can set that up? Likely for a later PR.
At some point some of this code should be moved to a common loadpath
library to compute native target names, and maybe some other stuff.
Some other changes in
Nativelib:We fix incorrect early initialization of
Boot.Env.tWe extend the path passed to the ocamlc compiler as to search for
files in the dir where the .vo is.
That can be reverted if we pass all the explicit
-nIpaths.We could just get rid of
.coq-native, additionally.