Legacy build warns cannot-open-dir #15482
Labels
Projects
Milestone
Comments
Alizter
added
kind: user messages
|
I can reproduce. Apparently, |
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - improve prefix / path adjustment in `coq_dune` - improve option handling - changelog / doc update - use the loadpath common library to compute native target names
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - improve prefix / path adjustment in `coq_dune` - improve option handling - changelog / doc update - use the loadpath common library to compute native target names
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - improve prefix / path adjustment in `coq_dune` - improve option handling - changelog / doc update - use the loadpath common library to compute native target names
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - improve prefix / path adjustment in `coq_dune` - improve option handling - changelog / doc update - use the loadpath common library to compute native target names
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - improve prefix / path adjustment in `coq_dune` - improve option handling - changelog / doc update - use the loadpath common library to compute native target names
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - improve option handling, add native, etc... - improve prefix / path adjustment in `coq_dune` - changelog / doc update - use the loadpath common library to compute native target names
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - improve option handling, add native, etc... - improve prefix / path adjustment in `coq_dune` - changelog / doc update - use the loadpath common library to compute native target names
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
6 tasks
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jan 31, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 6, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 27, 2022
We replace both the dune-based `(coq.theory ...` and the "legacy" make-based build systems into a single setup, based on our own rule generation and using Dune. Thus, we go back to the first implementation of dune setup, where compilation of .vo files do require a bootstrap process to generate the rules, which is done by the `coq_dune` tool. But now, the process is much more cleaner, as we got rid of the OCaml make rules. We thus disable the `(coq.theory ...)` stanza on `theories/dune` for now; the only downside to this is that we lose compositional building of .vo libs (for OCaml we are still fine, which our main use case), which anyways it is not used yet as inter-scope composition is missing from dune for now. At some point tho, once `(coq.theory ...)` is stable, we could go back to it, and remove `coq_dune`. Hopefully, `coq_dune` will be used in coq#13364 to implement the rules for the test suite too. Dune 3.0 may bring two important improvements for this PR: - `(deps (:read file))` so we could let dune handle the call to coqdep - `(include rules.sexp)` so no more bootstrapping is necessary. This should supersede coq#15545 , avoid many troubles that coq#15220 had to endure, and lose coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] aux files, vos, etc... - [ ] don't call coqdep once per file (but that's maybe conveneint for the test-suite, so we may want to keep both modes) - [ ] improve / add option handling, add native, etc... - [ ] improve prefix / path adjustment in `coq_dune` - [ ] changelog / doc update - [ ] use the loadpath common library to compute native target names, and maybe more
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 27, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] vos files? - [ ] quick and async CI jobs - [ ] rest of CI - [ ] big cleanup of coq_dune, in particular w.r.t how ltac2 is handled - [ ] changelog / documentation update - [ ] remove the native hackery for loadpaths now that the build system can set that up? - [ ] should we use coqnative? [not for now maybe?] At some point this code should use the loadpath common library to compute native target names, and maybe more stuff. Some other changes: - We also fixup incorrecty early initialization of coqlib. - We extend the path passed to the ocamlc compiler as to search for files in the dir where the .vo is [to be reverted if we remove the hackery], also we could just get rid of `.coq-native`. - We remove an obsolete / uselss message on configure
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 27, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] vos files? - [ ] quick and async CI jobs - [ ] rest of CI - [ ] big cleanup of coq_dune, in particular w.r.t how ltac2 is handled - [ ] changelog / documentation update - [ ] remove the native hackery for loadpaths now that the build system can set that up? - [ ] should we use coqnative? [not for now maybe?] At some point this code should use the loadpath common library to compute native target names, and maybe more stuff. Some other changes: - We also fixup incorrecty early initialization of coqlib. - We extend the path passed to the ocamlc compiler as to search for files in the dir where the .vo is [to be reverted if we remove the hackery], also we could just get rid of `.coq-native`. - We remove an obsolete / uselss message on configure
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 28, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] vos files? - [ ] quick and async CI jobs - [ ] rest of CI - [ ] big cleanup of coq_dune, in particular w.r.t how ltac2 is handled - [ ] changelog / documentation update - [ ] remove the native hackery for loadpaths now that the build system can set that up? - [ ] should we use coqnative? [not for now maybe?] At some point this code should use the loadpath common library to compute native target names, and maybe more stuff. Some other changes: - We also fixup incorrecty early initialization of coqlib. - We extend the path passed to the ocamlc compiler as to search for files in the dir where the .vo is [to be reverted if we remove the hackery], also we could just get rid of `.coq-native`. - We remove an obsolete / uselss message on configure
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 28, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] vos files? - [ ] quick and async CI jobs - [ ] rest of CI - [ ] big cleanup of coq_dune, in particular w.r.t how ltac2 is handled - [ ] changelog / documentation update - [ ] remove the native hackery for loadpaths now that the build system can set that up? - [ ] should we use coqnative? [not for now maybe?] At some point this code should use the loadpath common library to compute native target names, and maybe more stuff. Some other changes: - We also fixup incorrecty early initialization of coqlib. - We extend the path passed to the ocamlc compiler as to search for files in the dir where the .vo is [to be reverted if we remove the hackery], also we could just get rid of `.coq-native`. - We remove an obsolete / uselss message on configure
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 28, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] vos files? - [ ] quick and async CI jobs - [ ] rest of CI - [ ] big cleanup of coq_dune, in particular w.r.t how ltac2 is handled - [ ] changelog / documentation update - [ ] remove the native hackery for loadpaths now that the build system can set that up? - [ ] should we use coqnative? [not for now maybe?] At some point this code should use the loadpath common library to compute native target names, and maybe more stuff. Some other changes: - We also fixup incorrecty early initialization of coqlib. - We extend the path passed to the ocamlc compiler as to search for files in the dir where the .vo is [to be reverted if we remove the hackery], also we could just get rid of `.coq-native`. - We remove an obsolete / uselss message on configure
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 28, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] vos files? - [ ] quick and async CI jobs - [ ] rest of CI - [ ] big cleanup of coq_dune, in particular w.r.t how ltac2 is handled - [ ] changelog / documentation update - [ ] remove the native hackery for loadpaths now that the build system can set that up? - [ ] should we use coqnative? [not for now maybe?] At some point this code should use the loadpath common library to compute native target names, and maybe more stuff. Some other changes: - We also fixup incorrecty early initialization of coqlib. - We extend the path passed to the ocamlc compiler as to search for files in the dir where the .vo is [to be reverted if we remove the hackery], also we could just get rid of `.coq-native`. - We remove an obsolete / uselss message on configure
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 28, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] quick and async CI jobs - [ ] rest of of CI / determine obsolete targets - [ ] install for documentation [check Dune 3.0] - [ ] changelog / documentation update - [ ] should we use coqnative? [not for now maybe?] - [ ] remove the native hackery for loadpaths now that the build system 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.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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Apr 28, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#15482 . Legacy makefiles will be removed in the next commit, closing a few more bugs hopefully. Todos are: - [ ] quick and async CI jobs - [ ] rest of of CI / determine obsolete targets - [ ] install for documentation [check Dune 3.0] - [ ] changelog / documentation update - [ ] should we use coqnative? [not for now maybe?] - [ ] remove the native hackery for loadpaths now that the build system 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.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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 7, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 16, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 21, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 21, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 21, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 22, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 22, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 23, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 23, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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. [ci] [coqbot] Install compat dirs for coqbot and documentation This should be reverted once coqbot is updated, or we do install the documentation of a package.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 23, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 24, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 24, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 24, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 27, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 27, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Jun 28, 2022
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 coq#15545 , avoid many troubles that coq#15220 had to endure, and close coq#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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
On my machine
./configure -prefix /usr && makesays
on every coqc execution
No idea why this doesn't happen in CI.
The text was updated successfully, but these errors were encountered: